spn_reachgraph.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_REACHGRAPH_H
#define LINE_API_SPN_SPN_REACHGRAPH_H
 
/**
 * @file
 * @ingroup api_spn
 * Reachability graph of a stochastic Petri net under the GSPN firing rule
 * (Haverkort 1998, sec. 14.2; Ajmone Marsan et al.). An event is enabled in
 * m when m covers its enabling arcs and no inhibitor threshold is reached;
 * when any immediate event is enabled only the enabled immediate events of
 * the highest priority may fire, otherwise every enabled event may. The
 * markings are found breadth first from m0 and numbered in discovery order;
 * E lists the edges (from, to, event), 0-based.
 *
 * status is "complete" when the graph is finite and fully explored, "cap"
 * when maxstates markings were found and another one appeared, and
 * "unbounded" when a new marking strictly covers one of its ancestors
 * (Karp-Miller), which proves unboundedness only for a monotone net: the
 * covering test runs only without inhibitor arcs, priorities and mixed
 * timed/immediate events. unboundedlevels marks the strictly larger levels.
 * tangible(i) is false when an immediate event may fire in marking i.
 * QUEUEING places carry state the marking does not hold and are refused.
 * MATLAB twin: matlab/src/api/spn/spn_reachgraph.m.
 */
 
#include <cstddef>
#include <map>
#include <string>
#include <vector>
 
#include "line/api/spn/spn_net.h"
 
namespace line {
namespace spn {
 
/** Default cap on the number of explored markings. */
constexpr std::size_t SPN_REACH_MAXSTATES = 100000;
 
struct SpnReachGraph {
    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
    std::vector<std::vector<long long>> M; ///< markings, discovery order
    std::vector<std::vector<std::size_t>> E; ///< edges (from, to, event), 0-based
    std::vector<bool> tangible;
    std::string status;                    ///< complete, cap or unbounded
    std::vector<bool> unboundedlevels;
    std::vector<long long> m0;
};
 
namespace detail {
 
template <class T>
void spn_check_places(const qn::NetworkStruct<T>& sn, const SpnNet& net, const std::string& caller) {
    for (std::size_t pp = 0; pp < net.places.size(); ++pp) {
        const std::size_t nd = net.places[pp];
        const std::size_t ist = sn.nodes[nd - 1].station;
        if (ist >= 1 && ist <= sn.stations.size() &&
            sn.stations[ist - 1].sched != lang::SchedStrategy::INF)
            throw UnsupportedError(ErrorKind{"QueueingPlace"},
                                   caller + ": place " + sn.nodes[nd - 1].name +
                                       " is a QUEUEING place: its embedded service is state "
                                       "that the marking does not carry");
    }
}
 
inline SpnReachGraph spn_explore(const SpnNet& net, const std::vector<long long>& m0,
                                 std::size_t maxstates) {
    const std::size_t n = net.n;
    SpnReachGraph g;
    g.places = net.places;
    g.transitions = net.transitions;
    g.modes = net.modes;
    g.m0 = m0;
    g.status = "complete";
    g.unboundedlevels.assign(n, false);
    std::vector<std::size_t> parent;
    std::map<std::vector<long long>, std::size_t> key;
    g.M.push_back(m0);
    parent.push_back(0);  // the root has no parent; guarded by a == 0 below
    key[m0] = 0;
    const bool monotone = net.monotone();
    for (std::size_t head = 0; head < g.M.size() && g.status == "complete"; ++head) {
        const std::vector<long long> m = g.M[head];
        const std::vector<bool> f = net.fireable(m);
        for (std::size_t e = 0; e < net.E; ++e) {
            if (!f[e]) continue;
            std::vector<long long> mp(n);
            for (std::size_t l = 0; l < n; ++l) mp[l] = m[l] - net.pre[l][e] + net.post[l][e];
            const std::map<std::vector<long long>, std::size_t>::const_iterator it = key.find(mp);
            if (it != key.end()) {
                g.E.push_back(std::vector<std::size_t>{head, it->second, e});
                continue;
            }
            if (g.M.size() >= maxstates) {
                g.status = "cap";
                break;
            }
            const std::size_t id = g.M.size();
            g.M.push_back(mp);
            parent.push_back(head);
            key[mp] = id;
            g.E.push_back(std::vector<std::size_t>{head, id, e});
            if (monotone) {
                std::size_t a = head;
                for (;;) {
                    bool le = true, lt = false;
                    for (std::size_t l = 0; l < n; ++l) {
                        le = le && g.M[a][l] <= mp[l];
                        lt = lt || g.M[a][l] < mp[l];
                    }
                    if (le && lt) {
                        for (std::size_t l = 0; l < n; ++l) g.unboundedlevels[l] = mp[l] > g.M[a][l];
                        g.status = "unbounded";
                        break;
                    }
                    if (a == 0) break;
                    a = parent[a];
                }
                if (g.status != "complete") break;
            }
        }
    }
    g.tangible.assign(g.M.size(), true);
    for (std::size_t i = 0; i < g.M.size(); ++i) {
        const std::vector<bool> f = net.fireable(g.M[i]);
        for (std::size_t e = 0; e < net.E; ++e)
            if (f[e] && net.immediate[e]) g.tangible[i] = false;
    }
    return g;
}
 
}  // namespace detail
 
/**
 * @param init      initial marking per level; empty: the declared Place
 *                  state, else the reference station populations
 * @param maxstates cap on the number of markings (0: SPN_REACH_MAXSTATES)
 */
template <class T>
SpnReachGraph spn_reachgraph(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_reachgraph");
    detail::spn_check_places(sn, net, "spn_reachgraph");
    const std::vector<long long> m0 = detail::spn_initmarking(sn, net, init, "spn_reachgraph");
    return detail::spn_explore(net, m0, maxstates == 0 ? SPN_REACH_MAXSTATES : maxstates);
}
 
}  // namespace spn
}  // namespace line
 
#endif  // LINE_API_SPN_SPN_REACHGRAPH_H