Add Token Elimination abstraction

.github/workflows/build-linux.yml

@@ -21,7 +21,7 @@ jobs:
       - name: Install Packages
         run: |
           sudo apt-get update
-          sudo apt-get install flex libboost-all-dev
+          sudo apt-get install flex libboost-all-dev g++-10 gcc-10
 
           wget https://ftp.gnu.org/gnu/bison/bison-3.7.6.tar.gz
           tar xvfz bison-3.7.6.tar.gz

include/CTL/CTLEngine.h

@@ -21,6 +21,7 @@ ReturnValue CTLMain(PetriEngine::PetriNet* net,
                     Strategy strategytype,
                     StatisticsLevel printstatistics,
                     bool partial_order,
+                    TokenEliminationMethod token_elim_method,
                     const std::vector<std::string>& querynames,
                     const std::vector<std::shared_ptr<PetriEngine::PQL::Condition>>& reducedQueries,
                     const std::vector<size_t>& ids,

include/CTL/CTLResult.h

@@ -26,6 +26,7 @@ struct CTLResult {
     size_t processedNegationEdges = 0;
     size_t exploredConfigurations = 0;
     size_t numberOfEdges = 0;
+    size_t tokensEliminated = 0;
     size_t maxTokens = 0;
 #ifdef VERIFYPNDIST
     size_t numberOfRoundsComputingDistance = 0;

include/CTL/PetriNets/OnTheFlyDG.h

@@ -14,6 +14,7 @@
 #include "PetriEngine/Structures/AlignedEncoder.h"
 #include "PetriEngine/Structures/linked_bucket.h"
 #include "PetriEngine/ReducingSuccessorGenerator.h"
+#include "PetriEngine/TokenEliminator.h"
 
 namespace PetriNets {
 class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
@@ -22,7 +23,8 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
     using Condition = PetriEngine::PQL::Condition;
     using Condition_ptr = PetriEngine::PQL::Condition_ptr;
     using Marking = PetriEngine::Structures::State;
-    OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
+    using TokenEliminator = PetriEngine::TokenEliminator;
+    OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order, TokenEliminator& token_elim);
 
     virtual ~OnTheFlyDG();
 
@@ -45,6 +47,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
     size_t configurationCount() const;
     size_t markingCount() const;
     size_t maxTokens() const;
+    size_t tokensEliminated() const;
     Condition::Result initialEval();
 
 protected:
@@ -55,6 +58,8 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
     PetriConfig* initial_config;
     Marking working_marking;
     Marking query_marking;
+    Marking abstracted_marking;
+    TokenEliminator& token_elim;
     uint32_t n_transitions = 0;
     uint32_t n_places = 0;
     size_t _markingCount = 0;
@@ -89,8 +94,8 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
             }
         }
     }
-    PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
-    PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
+    PetriConfig *createConfiguration(const Marking& marking, size_t own, Condition* query);
+    PetriConfig *createConfiguration(const Marking& marking, size_t own, const Condition_ptr& query)
     {
         return createConfiguration(marking, own, query.get());
     }

include/PetriEngine/PetriNet.h

@@ -69,8 +69,22 @@ namespace PetriEngine {
         /** Fire transition if possible and store result in result */
         bool deadlocked(const MarkVal* marking) const;
         bool fireable(const MarkVal* marking, int transitionIndex);
-        std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const;
-        std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const;
+
+        [[nodiscard]] std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const
+        {
+            const TransPtr& transition = _transitions[id];
+            uint32_t first = transition.inputs;
+            uint32_t last = transition.outputs;
+            return std::make_pair(&_invariants[first], &_invariants[last]);
+        }
+
+        [[nodiscard]] std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const
+        {
+            uint32_t first = _transitions[id].outputs;
+            uint32_t last = _transitions[id+1].inputs;
+            return std::make_pair(&_invariants[first], &_invariants[last]);
+        }
+
         uint32_t numberOfTransitions() const {
             return _ntransitions;
         }
@@ -150,6 +164,7 @@ namespace PetriEngine {
         friend class ReducingSuccessorGenerator;
         friend class STSolver;
         friend class StubbornSet;
+        friend class TokenEliminator;
     };
 
 } // PetriEngine

include/PetriEngine/Reachability/ReachabilitySearch.h

@@ -32,6 +32,7 @@
 #include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
 
 #include "PetriEngine/options.h"
+#include "PetriEngine/TokenEliminator.h"
 
 #include <memory>
 #include <vector>
@@ -65,7 +66,8 @@ namespace PetriEngine {
                     size_t seed,
                     int64_t depthRandomWalk = 50000,
                     const int64_t incRandomWalk = 5000,
-                    const std::vector<MarkVal>& initPotencies = std::vector<MarkVal>());
+                    const std::vector<MarkVal>& initPotencies = std::vector<MarkVal>(),
+                    TokenEliminationMethod tokenElim = TokenEliminationMethod::Disabled);
             size_t maxTokens() const;
         private:
             struct searchstate_t {
@@ -94,7 +96,8 @@ namespace PetriEngine {
                 bool usequeries,
                 StatisticsLevel statisticsLevel,
                 size_t seed,
-                const std::vector<MarkVal>& initPotencies);
+                const std::vector<MarkVal>& initPotencies,
+                TokenEliminationMethod tokenElim);
 
             void printStats(searchstate_t& s, Structures::StateSetInterface*, StatisticsLevel);
 
@@ -114,6 +117,7 @@ namespace PetriEngine {
             Structures::State _initial;
             AbstractHandler& _callback;
             size_t _max_tokens = 0;
+            TokenEliminator token_elim{};
         };
 
         template <typename G>
@@ -131,7 +135,7 @@ namespace PetriEngine {
         bool ReachabilitySearch::tryReach(std::vector<std::shared_ptr<PQL::Condition> >& queries,
                                         std::vector<ResultPrinter::Result>& results, bool usequeries,
                                         StatisticsLevel statisticsLevel, size_t seed,
-                                        const std::vector<MarkVal>& initPotencies)
+                                        const std::vector<MarkVal>& initPotencies, TokenEliminationMethod tokenElim)
         {
 
             // set up state
@@ -180,13 +184,18 @@ namespace PetriEngine {
                     queue.push(r.second, &dc, queries[ss.heurquery].get());
                 }
 
+                token_elim.init(&_net);
+                token_elim.setEnabled(tokenElim != TokenEliminationMethod::Disabled);
+                token_elim.setDynamic(tokenElim == TokenEliminationMethod::Dynamic);
+
                 // Search!
                 for(auto nid = queue.pop(); nid != Structures::Queue::EMPTY; nid = queue.pop()) {
                     states.decode(state, nid);
                     generator.prepare(&state);
 
                     while(generator.next(working)){
                         ss.enabledTransitionsCount[generator.fired()]++;
+                        token_elim.eliminate(&working, queries[ss.heurquery].get());
                         auto res = states.add(working);
                         // If we have not seen this state before
                         if (res.first) {

include/PetriEngine/TokenEliminator.h

@@ -0,0 +1,127 @@
+/**
+ * Original author(s):
+ *      Nicolaj Ø. Jensen <noje@cs.aau.dk>
+ */
+
+#ifndef VERIFYPN_TOKENELIMINATOR_H
+#define VERIFYPN_TOKENELIMINATOR_H
+
+
+#include <utility>
+
+#include "PetriEngine/Structures/State.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "CTL/PetriNets/PetriConfig.h"
+
+namespace PetriEngine {
+    using Condition = PQL::Condition;
+    using Condition_ptr = PQL::Condition_ptr;
+    using Marking = Structures::State;
+
+    const static uint8_t IN_Q_INC = 1 << 0;
+    const static uint8_t IN_Q_DEC = 1 << 1;
+    const static uint8_t VIS_INC = 1 << 2;
+    const static uint8_t VIS_DEC = 1 << 3;
+    const static uint8_t MUST_KEEP = 1 << 4;
+    const static uint8_t CAN_INC = 1 << 5;
+    const static uint8_t CAN_DEC = 1 << 6;
+
+    /**
+     * The TokenEliminator removes tokens from a marking based on impossible, visible, and directional effects
+     * while preserving reachability properties. It will do nothing when given a query of a different kind.
+     * The static setting does not take the current marking into account and will often be much faster
+     * (but less effective) on repeated invocations involving the same reachability queries due to caching.
+     *
+     * The abstraction provided through token elimination is similar to that of structural reduction rule I+M
+     * as well as stubborn reductions, but can additionally be used on-the-fly in state space searches to
+     * simplify states and thus reduce the size of the state space.
+     *
+     * The TokenEliminator is based on the work in 'Token Elimination in Model Checking of Petri Nets' (TACAS'25)
+     * by Nicolaj Ø. Jensen, Kim G. Larsen, and Jiri Srba.
+     */
+    class TokenEliminator {
+    public:
+        virtual ~TokenEliminator() = default;
+
+        void init(const PetriNet *net);
+
+        void eliminate(Marking *marking, Condition *query);
+
+        [[nodiscard]] virtual size_t tokensEliminated() const {
+            return _tokensEliminated;
+        }
+
+        TokenEliminator * setEnabled(bool enabled) {
+            _enabled = enabled;
+            return this;
+        }
+
+        TokenEliminator * setDynamic(bool dynamic) {
+            _doDynamic = dynamic;
+            return this;
+        }
+    private:
+        struct place_t {
+            uint32_t producers, consumers;
+        };
+
+        struct trans_t {
+            uint32_t index;
+            int8_t direction;
+
+            trans_t() = default;
+
+            trans_t(uint32_t id, int8_t dir) : index(id), direction(dir) {};
+
+            bool operator<(const trans_t &t) const {
+                return index < t.index;
+            }
+        };
+
+    private:
+        /** Built data structure that makes it faster to go from places to transitions */
+        void setupProducersAndConsumers();
+
+        void setupExtBounds();
+
+        [[nodiscard]] std::pair<const trans_t*, const trans_t*> producers(uint32_t p) const;
+        [[nodiscard]] std::pair<const trans_t*, const trans_t*> consumers(uint32_t p) const;
+
+        /** Compute which places cannot increase and/or decrease as well as which transitions cannot be enabled.
+         * This is an over-approximation. */
+        void findDeadPlacesAndTransitions(const PetriEngine::Marking *marking);
+
+        void eliminateDynamic(PetriEngine::Marking * marking, PetriEngine::Condition * query);
+
+        /** Compute fixed point of visibility respecting dead places and transitions in the current marking. */
+        void findDynamicVisiblePlaces(PetriEngine::Condition *query);
+
+        void eliminateStatic(PetriEngine::Marking * marking, PetriEngine::Condition * query);
+
+        /** Compute fixed point of visibility by net structure alone. Subsequent calls with same query is faster. */
+        const std::vector<bool> &findStaticVisiblePlaces(PetriEngine::Condition *query);
+
+    private:
+        // === Settings
+        bool _enabled = true;
+        bool _doDynamic = false;
+        bool _env_TOKEN_ELIM_DEBUG = false; //std::getenv("TAPAAL_TOKEN_ELIM_DEBUG") != nullptr;
+
+        // === Net
+        PetriNet const *_net;
+        std::vector<uint32_t> _extBounds;
+        std::unique_ptr<place_t[]> _prodcons;
+        std::unique_ptr<trans_t[]> _parcs;
+        std::vector<std::vector<uint32_t>> _inhibpost;
+
+        // === Cache and working flags
+        std::unordered_map<const Condition *, const std::vector<bool>> _cache;
+        std::vector<uint8_t> _pflags;
+        std::vector<bool> _fireable;
+
+        // === Statistics
+        size_t _tokensEliminated = 0;
+    };
+}
+
+#endif //VERIFYPN_TOKENELIMINATOR_H

include/PetriEngine/options.h

@@ -41,6 +41,12 @@ enum class StatisticsLevel {
     Full
 };
 
+enum TokenEliminationMethod {
+    Disabled,
+    Dynamic,
+    Static,
+};
+
 struct options_t {
 //    bool outputtrace = false;
     int kbound = 0;
@@ -67,6 +73,8 @@ struct options_t {
     bool doUnfolding = true;
     int64_t depthRandomWalk = 50000;
     int64_t incRandomWalk = 5000;
+    TokenEliminationMethod tokenElimMethodCTL = TokenEliminationMethod::Disabled;
+    TokenEliminationMethod tokenElimMethodReach = TokenEliminationMethod::Disabled;
 
     TemporalLogic logic = TemporalLogic::CTL;
     bool noreach = false;

src/CTL/Algorithm/CertainZeroFPA.cpp

@@ -32,7 +32,10 @@ bool Algorithm::CertainZeroFPA::search(DependencyGraph::BasicDependencyGraph &t_
             if(vertex->isDone()) return vertex->assignment == ONE;
         }
 
-        if(vertex->isDone()) return vertex->assignment == ONE;
+        if(vertex->isDone()) {
+            graph->cleanUp();
+            return vertex->assignment == ONE;
+        }
 
         if(!strategy->trivialNegation())
         {

src/CTL/CTLEngine.cpp

@@ -54,7 +54,8 @@ bool CTLSingleSolve(Condition* query, PetriNet* net,
                  CTLAlgorithmType algorithmtype,
                  Strategy strategytype, bool partial_order, CTLResult& result)
 {
-    OnTheFlyDG graph(net, partial_order);
+    TokenEliminator token_elim;
+    OnTheFlyDG graph(net, partial_order, *token_elim.setEnabled(false));
     graph.setQuery(query);
     std::shared_ptr<Algorithm::FixedPointAlgorithm> alg = nullptr;
     getAlgorithm(alg, algorithmtype,  strategytype);
@@ -71,6 +72,7 @@ bool CTLSingleSolve(Condition* query, PetriNet* net,
     result.processedNegationEdges += alg->processedNegationEdges();
     result.exploredConfigurations += alg->exploredConfigurations();
     result.numberOfEdges += alg->numberOfEdges();
+    result.tokensEliminated = graph.tokensEliminated();
     result.maxTokens = std::max(graph.maxTokens(), result.maxTokens);
     return res;
 }
@@ -315,6 +317,7 @@ ReturnValue CTLMain(PetriNet* net,
                     Strategy strategytype,
                     StatisticsLevel printstatistics,
                     bool partial_order,
+                    const TokenEliminationMethod token_elim_method,
                     const std::vector<std::string>& querynames,
                     const std::vector<std::shared_ptr<Condition>>& queries,
                     const std::vector<size_t>& querynumbers,
@@ -326,7 +329,11 @@ ReturnValue CTLMain(PetriNet* net,
         bool solved = false;
 
         {
-            OnTheFlyDG graph(net, partial_order);
+            TokenEliminator token_elim;
+            token_elim.setDynamic(token_elim_method == TokenEliminationMethod::Dynamic);
+            token_elim.setEnabled(token_elim_method == TokenEliminationMethod::Disabled);
+
+            OnTheFlyDG graph(net, partial_order, token_elim);
             graph.setQuery(result.query);
             switch (graph.initialEval()) {
                 case Condition::Result::RFALSE:

src/CTL/CTLResult.cpp

@@ -21,14 +21,15 @@ void CTLResult::print(const std::string& qname, StatisticsLevel statisticslevel,
     if(statisticslevel != StatisticsLevel::None){
         out << "\n";
         out << "STATS:" << "\n";
-        out << "	Time (seconds)    : " << std::setprecision(4) << duration / 1000 << "\n";
-        out << "	Configurations    : " << numberOfConfigurations << "\n";
-        out << "	Markings          : " << numberOfMarkings << "\n";
-        out << "	Edges             : " << numberOfEdges << "\n";
-        out << "	Processed Edges   : " << processedEdges << "\n";
-        out << "	Processed N. Edges: " << processedNegationEdges << "\n";
-        out << "	Explored Configs  : " << exploredConfigurations << "\n";
-        out << "	max tokens:       : " << maxTokens << "\n"; // kept lower case to be compatible with reachability format 
+        out << "	Time (seconds)      : " << std::setprecision(4) << duration / 1000 << "\n";
+        out << "	Configurations      : " << numberOfConfigurations << "\n";
+        out << "	Markings            : " << numberOfMarkings << "\n";
+        out << "	Edges               : " << numberOfEdges << "\n";
+        out << "	Processed Edges     : " << processedEdges << "\n";
+        out << "	Processed N. Edges  : " << processedNegationEdges << "\n";
+        out << "	Explored Configs    : " << exploredConfigurations << "\n";
+        out << "	Tokens Eliminated   : " << tokensEliminated << "\n";
+        out << "	max tokens:         : " << maxTokens << "\n"; // kept lower case to be compatible with reachability format
     }
     out << std::endl;
 }