ldes_spn.h

Go to the documentation of this file.

/*
 * Copyright (c) 2012-2026, QORE Lab, Imperial College London
 * All rights reserved.
 */
#ifndef LINE_SOLVERS_LDES_LDES_SPN_H
#define LINE_SOLVERS_LDES_LDES_SPN_H
 
/**
 * @file
 * @ingroup line_solvers
 * The Petri-net layer of the native LDES engine: Places and Transitions.
 *
 * A PLACE holds tokens per class and a TRANSITION moves them. A mode of a
 * transition is ENABLED when every input place holds at least its enabling
 * count and no inhibiting count is met; firing consumes the enabling tokens and
 * deposits the firing counts.
 *
 * IMMEDIATE MODES FIRE BEFORE ANY TIMED ONE, and among themselves in priority
 * order, weighted at equal priority. That is not an optimization: an immediate
 * transition takes zero time, so a marking that enables one is not a marking
 * the net ever rests in, and letting a timed mode fire from it would visit a
 * state the model does not have.
 *
 * THE FIRING RATE MAY DEPEND ON THE MARKING. `firingdep` multiplies the mode's
 * nominal rate by g(marking), and the clock has to be RESAMPLED whenever the
 * marking changes, not merely scaled: an exponential clock drawn under one
 * rate and left to run carries the old rate into the new marking.
 */
 
#include <algorithm>
#include <cstddef>
#include <functional>
#include <limits>
#include <vector>
 
#include "line/lang/lang_types.h"
 
namespace line {
namespace ldes {
namespace engine {
 
/**
 * One mode of a transition, resolved to what the event loop needs.
 *
 * THE ARC VECTORS ARE INDEXED BY (place slot, class), flattened `p * K + r`,
 * and the marking handed to `spn_enabled` and `spn_fire` uses the same layout.
 * A Petri net whose arcs carry a class is a COLOURED net and its behaviour is
 * not that of the class-summed one: a mode needing two Class1 tokens must not
 * be enabled by two Class2 tokens sitting at the same place.
 */
struct SpnMode {
    std::vector<double> enabling;   ///< per (place, class), tokens required
    std::vector<double> inhibiting; ///< per (place, class), tokens that block (inf = never)
    std::vector<double> firing;     ///< per (place, class), tokens moved on a firing
    double servers = 1.0;
    double priority = 0.0;
    double weight = 1.0;
    bool immediate = false;
    double rate = 1.0;              ///< nominal firing rate of a timed mode
    std::function<double(const std::vector<double>&)> dep;  ///< marking multiplier
};
 
/** One Transition node. */
struct SpnTransition {
    std::size_t node = 0;
    std::vector<SpnMode> modes;
    std::vector<std::size_t> places;  ///< the place NODES its modes reference, in order
    std::vector<double> fired;        ///< per mode
};
 
/**
 * True when `m` is enabled by the marking `tok`, which is indexed the same way
 * as the mode's own vectors -- (place slot, class), flattened.
 *
 * An INHIBITING arc is a bound, not a requirement: the mode is blocked once the
 * place reaches the count IN THAT CLASS, and an infinite count never blocks.
 */
inline bool spn_enabled(const SpnMode& m, const std::vector<double>& tok) {
    for (std::size_t p = 0; p < m.enabling.size() && p < tok.size(); ++p)
        if (tok[p] < m.enabling[p]) return false;
    for (std::size_t p = 0; p < m.inhibiting.size() && p < tok.size(); ++p)
        if (std::isfinite(m.inhibiting[p]) && m.inhibiting[p] > 0.0 && tok[p] >= m.inhibiting[p])
            return false;
    return true;
}
 
/** The rate of a timed mode under the current marking. */
inline double spn_rate(const SpnMode& m, const std::vector<double>& tok) {
    double r = m.rate;
    if (m.dep) {
        const double g = m.dep(tok);
        r *= (g > 0.0) ? g : 0.0;
    }
    return r;
}
 
/** Move the tokens of one firing: consume the enabling counts, deposit the firing ones. */
inline void spn_fire(const SpnMode& m, std::vector<double>& tok) {
    for (std::size_t p = 0; p < m.enabling.size() && p < tok.size(); ++p)
        tok[p] -= m.enabling[p];
    for (std::size_t p = 0; p < m.firing.size() && p < tok.size(); ++p) tok[p] += m.firing[p];
}
 
/**
 * Pick among the enabled IMMEDIATE modes: the highest priority first (lowest
 * value), then weighted at random among the ties. Returns -1 when none is
 * enabled.
 */
inline int spn_pick_immediate(const std::vector<SpnMode>& modes, const std::vector<double>& tok,
                              double u) {
    double best_prio = std::numeric_limits<double>::infinity();
    for (const SpnMode& m : modes)
        if (m.immediate && spn_enabled(m, tok)) best_prio = std::min(best_prio, m.priority);
    if (!std::isfinite(best_prio)) return -1;
    double total = 0.0;
    for (const SpnMode& m : modes)
        if (m.immediate && m.priority == best_prio && spn_enabled(m, tok)) total += m.weight;
    if (!(total > 0.0)) {
        for (std::size_t k = 0; k < modes.size(); ++k)
            if (modes[k].immediate && modes[k].priority == best_prio && spn_enabled(modes[k], tok))
                return static_cast<int>(k);
        return -1;
    }
    double acc = 0.0;
    const double x = u * total;
    for (std::size_t k = 0; k < modes.size(); ++k)
        if (modes[k].immediate && modes[k].priority == best_prio && spn_enabled(modes[k], tok)) {
            acc += modes[k].weight;
            if (x < acc) return static_cast<int>(k);
        }
    return -1;
}
 
}  // namespace engine
}  // namespace ldes
}  // namespace line
 
#endif  // LINE_SOLVERS_LDES_LDES_SPN_H