spn_siphons.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_SIPHONS_H
#define LINE_API_SPN_SPN_SIPHONS_H
 
/**
 * @file
 * @ingroup api_spn
 * All minimal siphons of a stochastic Petri net and Commoner's condition
 * (Murata 1989, sec. VI-A; Silva, Teruel and Colom 1998). A siphon S is a
 * level set with *S contained in S*: once S is empty it stays empty. The
 * enumeration is the branch and bound of Cordone, Ferrarini and Piroddi
 * (2005): a node (I, O) asks for a minimal siphon containing I and avoiding
 * O, prunes with the largest siphon inside the complement of O (a fixpoint
 * that drops every level fed by an event taking nothing from the set), and
 * branches on the first level of that siphon outside I. A net can hold
 * exponentially many minimal siphons, so time and output are exponential in
 * the number of levels in the worst case; each node costs O(n^2 E).
 *
 * S lists the siphons as 0/1 rows over the levels, sorted by size and then
 * by their level indices. trapped(i) is true when the largest trap inside
 * siphon i is marked at m0; commoner = all(trapped). The check is
 * structural: inhibitor arcs, priorities and the timed/immediate split are
 * ignored. MATLAB twin: matlab/src/api/spn/spn_siphons.m.
 */
 
#include <cstddef>
#include <vector>
 
#include "line/api/spn/spn_net.h"
 
namespace line {
namespace spn {
 
struct SpnSiphons {
    std::vector<std::size_t> places;    ///< 1-based node indices, in level order
    std::vector<std::vector<int>> S;    ///< one minimal siphon per row (0/1 over levels)
    std::vector<bool> trapped;          ///< largest trap inside S(i) is marked at m0
    bool commoner = true;               ///< every minimal siphon holds a marked trap
    std::vector<long long> m0;
};
 
template <class T>
SpnSiphons spn_siphons(const qn::NetworkStruct<T>& sn,
                       const std::vector<double>& init = std::vector<double>()) {
    const detail::SpnNet net = detail::spn_build_net(sn, "spn_siphons");
    SpnSiphons out;
    out.places = net.places;
    out.m0 = detail::spn_initmarking(sn, net, init, "spn_siphons");
    const std::vector<std::vector<bool>> L = detail::spn_minsiphons(net.pre, net.post);
    out.S = detail::spn_sets_to_int(L);
    out.trapped.assign(L.size(), false);
    for (std::size_t i = 0; i < L.size(); ++i) {
        const std::vector<bool> Q = detail::spn_maxsiphon(net.post, net.pre, L[i]);
        for (std::size_t l = 0; l < net.n; ++l)
            if (Q[l] && out.m0[l] > 0) out.trapped[i] = true;
        out.commoner = out.commoner && out.trapped[i];
    }
    return out;
}
 
}  // namespace spn
}  // namespace line
 
#endif  // LINE_API_SPN_SPN_SIPHONS_H