spn_properties.h

Go to the documentation of this file.

/*
 * Copyright (c) 2012-2026, QORE Lab, Imperial College London
 * All rights reserved.
 */
#ifndef LINE_API_SPN_SPN_PROPERTIES_H
#define LINE_API_SPN_SPN_PROPERTIES_H
 
/**
 * @file
 * @ingroup api_spn
 * Aggregate Petri-net property analysis: P- and T-invariants, minimal
 * siphons and traps with Commoner's condition, the LP structural checks and
 * net classes, and the reachability-graph verdicts, all at one initial
 * marking. Two structural verdicts are derived when the net is monotone
 * (`ignored` empty; inhibitor arcs, priorities and mixed timed/immediate
 * events void the structural theorems):
 *   structdeadlockfree = 1 when the net is ordinary and Commoner holds
 *     (a deadlock empties a siphon; Murata 1989, Thm. 26-27), else -1;
 *   structlive = 1 for an asymmetric-choice net with Commoner, 0 for an
 *     extended free-choice net without it (Commoner/Hack), else -1.
 * MATLAB twin: matlab/src/api/spn/spn_properties.m.
 */
 
#include <cstddef>
#include <string>
#include <vector>
 
#include "line/api/spn/spn_reachprops.h"
#include "line/api/spn/spn_siphons.h"
#include "line/api/spn/spn_sinvariants.h"
#include "line/api/spn/spn_structprops.h"
#include "line/api/spn/spn_tinvariants.h"
#include "line/api/spn/spn_traps.h"
 
namespace line {
namespace spn {
 
struct SpnProperties {
    std::vector<long long> m0;
    std::vector<std::string> ignored;
    SpnInvariants sinv;
    SpnTInvariants tinv;
    SpnSiphons siphons;
    SpnTraps traps;
    SpnStructProps structp;   ///< MATLAB/Java/Python field "struct"
    SpnReachProps reach;
    bool commoner = true;
    int structdeadlockfree = -1;
    int structlive = -1;
};
 
template <class T>
SpnProperties spn_properties(const qn::NetworkStruct<T>& sn,
                             const std::vector<double>& init = std::vector<double>(),
                             std::size_t maxstates = 0) {
    const detail::SpnNet net = detail::spn_build_net(sn, "spn_properties");
    SpnProperties pr;
    pr.m0 = detail::spn_initmarking(sn, net, init, "spn_properties");
    const std::vector<double> m0d(pr.m0.begin(), pr.m0.end());
    pr.ignored = net.ignored;
    pr.sinv = spn_sinvariants(sn, m0d);
    pr.tinv = spn_tinvariants(sn);
    pr.siphons = spn_siphons(sn, m0d);
    pr.traps = spn_traps(sn, m0d);
    pr.structp = spn_structprops(sn);
    pr.reach = spn_reachprops(sn, m0d, maxstates);
    pr.commoner = pr.siphons.commoner;
    if (net.ignored.empty()) {
        if (pr.structp.ordinary && pr.commoner) pr.structdeadlockfree = 1;
        if (pr.structp.asymmetric && pr.commoner) pr.structlive = 1;
        else if (pr.structp.efc && !pr.commoner) pr.structlive = 0;
    }
    return pr;
}
 
}  // namespace spn
}  // namespace line
 
#endif  // LINE_API_SPN_SPN_PROPERTIES_H