soundness_report.h

Go to the documentation of this file.

/*
 * Copyright (c) 2012-2026, QORE Lab, Imperial College London
 * All rights reserved.
 */
#ifndef LINE_API_WFN_SOUNDNESS_REPORT_H
#define LINE_API_WFN_SOUNDNESS_REPORT_H
 
/**
 * @file
 * @ingroup api_wfn
 * The report of `WorkflowNet::check_soundness`.
 *
 * Markings are row vectors over the places, in the order of
 * `WorkflowNet::places()`.
 *
 * MATLAB twin: the `report` struct of matlab/src/api/wfn/WorkflowNet.m checkSoundness
 */
 
#include <cstddef>
#include <string>
#include <vector>
 
namespace line {
namespace wfn {
 
struct SoundnessReport {
    typedef std::vector<long> Marking;
 
    /** The first output of MATLAB's checkSoundness: true only when the verdict is "sound". */
    bool sound = false;
    long k = 1;
    /** "sound", "unsound" or "unknown" (state cap reached first). */
    std::string verdict = "unknown";
    std::size_t state_space_size = 0;
    std::vector<Marking> deadlocks;
    std::vector<Marking> no_option_to_complete;
    std::vector<Marking> improper_completion;
    std::vector<std::string> dead_transitions;
    bool unbounded = false;
    Marking unbounded_witness;
    bool unbounded_or_too_large = false;
    /** One readable line per defect. */
    std::vector<std::string> witnesses;
};
 
}  // namespace wfn
}  // namespace line
 
#endif  // LINE_API_WFN_SOUNDNESS_REPORT_H