spn_structprops.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_STRUCTPROPS_H
#define LINE_API_SPN_SPN_STRUCTPROPS_H
 
/**
 * @file
 * @ingroup api_spn
 * Structural properties of a stochastic Petri net, from its incidence matrix
 * C alone (Murata 1989, sec. VI-B; Silva, Teruel and Colom 1998; Haverkort
 * 1998, sec. 14.2). Each LP property is decided by one covering linear
 * program over [z; t] with 0 <= t <= 1, t <= z, maximising sum(t): t_j = 1
 * exactly when some solution has z_j > 0, so the program both decides the
 * property and names the levels or events that satisfy it.
 *   bounded:      exists y > 0 with y' C <= 0 (structurally bounded)
 *   conservative: exists y > 0 with y' C  = 0
 *   consistent:   exists x > 0 with C x   = 0
 *   repetitive:   exists x > 0 with C x  >= 0
 * The net classes (ordinary, state machine, marked graph, free choice,
 * extended free choice, asymmetric choice) follow Murata's definitions on
 * the arc supports. All of these ignore inhibitor arcs, priorities and the
 * timed/immediate split; `ignored` lists those of the three the net uses.
 * MATLAB twin: matlab/src/api/spn/spn_structprops.m.
 */
 
#include <cmath>
#include <cstddef>
#include <string>
#include <vector>
 
#include "line/api/spn/spn_net.h"
#include "line/util/lp_highs.h"
#include "line/util/simplex.h"
 
namespace line {
namespace spn {
 
struct SpnStructProps {
    std::vector<std::size_t> places;       ///< 1-based node indices, in level order
    std::vector<std::size_t> transitions;  ///< 1-based node index of each event
    std::vector<std::size_t> modes;        ///< 0-based mode index of each event
    bool bounded = false, conservative = false, consistent = false, repetitive = false;
    std::vector<bool> boundedlevels, conservedlevels, consistentevents, repetitiveevents;
    bool ordinary = false, statemachine = false, markedgraph = false;
    bool freechoice = false, efc = false, asymmetric = false;
    std::vector<std::string> ignored;      ///< inhibitor, immediate, priority (when used)
};
 
namespace detail {
 
/** Covering LP: which columns of z admit z_j > 0 with A z <= 0 (le) or A z = 0 (eq), z >= 0. */
inline std::vector<bool> spn_cover(const std::vector<std::vector<long long>>& A, std::size_t N,
                                   bool eq) {
    lp::LpModel<double> lpm(2 * N);
    for (std::size_t j = 0; j < N; ++j) {
        lpm.set_cost(j, 0.0);
        lpm.set_cost(N + j, 1.0);
        lpm.set_bounds(N + j, 0.0, 1.0);
    }
    lpm.set_maximize(true);
    for (std::size_t i = 0; i < A.size(); ++i) {
        for (std::size_t j = 0; j < N; ++j)
            if (A[i][j] != 0) lpm.row_add(j, static_cast<double>(A[i][j]));
        lpm.emit(eq ? lp::LpSense::EQ : lp::LpSense::LE, 0.0);
    }
    for (std::size_t j = 0; j < N; ++j) {
        lpm.row_add(N + j, 1.0);
        lpm.row_add(j, -1.0);
        lpm.emit(lp::LpSense::LE, 0.0);
    }
    const lp::LpSolution<double> sol = lp::lp_solve(lpm);
    bool fin = sol.ok() && sol.x.size() == 2 * N;
    for (std::size_t j = 0; fin && j < 2 * N; ++j) fin = std::isfinite(sol.x[j]);
    if (!fin)
        throw NumericError(ErrorKind{"Infeasible"},
                           "spn_structprops: the covering linear program returned no solution, "
                           "although z = 0 is feasible");
    std::vector<bool> cov(N);
    for (std::size_t j = 0; j < N; ++j) cov[j] = sol.x[N + j] > 0.5;
    return cov;
}
 
inline bool spn_all(const std::vector<bool>& v) {
    for (std::size_t i = 0; i < v.size(); ++i)
        if (!v[i]) return false;
    return true;
}
 
}  // namespace detail
 
template <class T>
SpnStructProps spn_structprops(const qn::NetworkStruct<T>& sn) {
    const detail::SpnNet net = detail::spn_build_net(sn, "spn_structprops");
    const std::size_t n = net.n, E = net.E;
    const std::vector<std::vector<long long>> Ct = detail::spn_transpose(net.C, E);
    std::vector<std::vector<long long>> negC(n, std::vector<long long>(E));
    for (std::size_t l = 0; l < n; ++l)
        for (std::size_t e = 0; e < E; ++e) negC[l][e] = -net.C[l][e];
    SpnStructProps sp;
    sp.places = net.places;
    sp.transitions = net.transitions;
    sp.modes = net.modes;
    sp.boundedlevels = detail::spn_cover(Ct, n, false);
    sp.conservedlevels = detail::spn_cover(Ct, n, true);
    sp.consistentevents = detail::spn_cover(net.C, E, true);
    sp.repetitiveevents = detail::spn_cover(negC, E, false);
    sp.bounded = detail::spn_all(sp.boundedlevels);
    sp.conservative = detail::spn_all(sp.conservedlevels);
    sp.consistent = detail::spn_all(sp.consistentevents);
    sp.repetitive = detail::spn_all(sp.repetitiveevents);
 
    bool ordinary = true;
    std::vector<std::size_t> intake(E, 0), outfeed(E, 0), lout(n, 0), lin(n, 0);
    for (std::size_t l = 0; l < n; ++l)
        for (std::size_t e = 0; e < E; ++e) {
            if (net.pre[l][e] > 0) {
                ordinary = ordinary && net.pre[l][e] == 1;
                ++intake[e];
                ++lout[l];
            }
            if (net.post[l][e] > 0) {
                ordinary = ordinary && net.post[l][e] == 1;
                ++outfeed[e];
                ++lin[l];
            }
        }
    bool smach = ordinary, mgraph = ordinary;
    for (std::size_t e = 0; e < E; ++e) smach = smach && intake[e] == 1 && outfeed[e] == 1;
    for (std::size_t l = 0; l < n; ++l) mgraph = mgraph && lout[l] == 1 && lin[l] == 1;
    bool fc = ordinary, efc = ordinary, ac = ordinary;
    for (std::size_t p = 0; p < n; ++p) {
        if (lout[p] > 1)
            for (std::size_t e = 0; e < E; ++e)
                if (net.pre[p][e] > 0 && intake[e] != 1) fc = false;
        for (std::size_t q = 0; q < n; ++q) {
            bool share = false, aonly = false, bonly = false;
            for (std::size_t e = 0; e < E; ++e) {
                const bool a = net.pre[p][e] > 0, b = net.pre[q][e] > 0;
                share = share || (a && b);
                aonly = aonly || (a && !b);
                bonly = bonly || (b && !a);
            }
            if (share) {
                if (aonly || bonly) efc = false;
                if (aonly && bonly) ac = false;
            }
        }
    }
    sp.ordinary = ordinary;
    sp.statemachine = smach;
    sp.markedgraph = mgraph;
    sp.freechoice = fc;
    sp.efc = efc;
    sp.asymmetric = ac;
    sp.ignored = net.ignored;
    return sp;
}
 
}  // namespace spn
}  // namespace line
 
#endif  // LINE_API_SPN_SPN_STRUCTPROPS_H