diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml index c666e5966..8b6fb4503 100644 --- a/.github/workflows/build-linux.yml +++ b/.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 diff --git a/include/CTL/CTLEngine.h b/include/CTL/CTLEngine.h index 9a52ce69d..ce53c5efe 100644 --- a/include/CTL/CTLEngine.h +++ b/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& querynames, const std::vector>& reducedQueries, const std::vector& ids, diff --git a/include/CTL/CTLResult.h b/include/CTL/CTLResult.h index c12ce100f..8d4b783bd 100644 --- a/include/CTL/CTLResult.h +++ b/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; diff --git a/include/CTL/PetriNets/OnTheFlyDG.h b/include/CTL/PetriNets/OnTheFlyDG.h index 7efc21731..e410314c2 100644 --- a/include/CTL/PetriNets/OnTheFlyDG.h +++ b/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()); } diff --git a/include/PetriEngine/PetriNet.h b/include/PetriEngine/PetriNet.h index 76897648f..0c54a4659 100644 --- a/include/PetriEngine/PetriNet.h +++ b/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 preset(uint32_t id) const; - std::pair postset(uint32_t id) const; + + [[nodiscard]] std::pair 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 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 diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index 46cc2acea..a2a3a0651 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -32,6 +32,7 @@ #include "PetriEngine/Stubborn/ReachabilityStubbornSet.h" #include "PetriEngine/options.h" +#include "PetriEngine/TokenEliminator.h" #include #include @@ -65,7 +66,8 @@ namespace PetriEngine { size_t seed, int64_t depthRandomWalk = 50000, const int64_t incRandomWalk = 5000, - const std::vector& initPotencies = std::vector()); + const std::vector& initPotencies = std::vector(), + 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& initPotencies); + const std::vector& 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 @@ -131,7 +135,7 @@ namespace PetriEngine { bool ReachabilitySearch::tryReach(std::vector >& queries, std::vector& results, bool usequeries, StatisticsLevel statisticsLevel, size_t seed, - const std::vector& initPotencies) + const std::vector& initPotencies, TokenEliminationMethod tokenElim) { // set up state @@ -180,6 +184,10 @@ 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); @@ -187,6 +195,7 @@ namespace PetriEngine { 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) { diff --git a/include/PetriEngine/TokenEliminator.h b/include/PetriEngine/TokenEliminator.h new file mode 100644 index 000000000..fbd82958b --- /dev/null +++ b/include/PetriEngine/TokenEliminator.h @@ -0,0 +1,127 @@ +/** + * Original author(s): + * Nicolaj Ø. Jensen + */ + +#ifndef VERIFYPN_TOKENELIMINATOR_H +#define VERIFYPN_TOKENELIMINATOR_H + + +#include + +#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 producers(uint32_t p) const; + [[nodiscard]] std::pair 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 &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 _extBounds; + std::unique_ptr _prodcons; + std::unique_ptr _parcs; + std::vector> _inhibpost; + + // === Cache and working flags + std::unordered_map> _cache; + std::vector _pflags; + std::vector _fireable; + + // === Statistics + size_t _tokensEliminated = 0; + }; +} + +#endif //VERIFYPN_TOKENELIMINATOR_H diff --git a/include/PetriEngine/options.h b/include/PetriEngine/options.h index 5dd2b1c51..58284e28e 100644 --- a/include/PetriEngine/options.h +++ b/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; diff --git a/src/CTL/Algorithm/CertainZeroFPA.cpp b/src/CTL/Algorithm/CertainZeroFPA.cpp index 7c3c0220a..9a1263373 100644 --- a/src/CTL/Algorithm/CertainZeroFPA.cpp +++ b/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()) { diff --git a/src/CTL/CTLEngine.cpp b/src/CTL/CTLEngine.cpp index b8511db38..eaa053626 100644 --- a/src/CTL/CTLEngine.cpp +++ b/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 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& querynames, const std::vector>& queries, const std::vector& 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: diff --git a/src/CTL/CTLResult.cpp b/src/CTL/CTLResult.cpp index 227ab132d..356fa6418 100644 --- a/src/CTL/CTLResult.cpp +++ b/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; } \ No newline at end of file diff --git a/src/CTL/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index 6cb625a50..1f9d3a7d3 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -19,7 +19,8 @@ using namespace DependencyGraph; namespace PetriNets { -OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encoder(t_net->numberOfPlaces(), 0), +OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order, TokenEliminator& token_elim) : encoder(t_net->numberOfPlaces(), 0), + token_elim(token_elim), edge_alloc(new linked_bucket_t(1)), conf_alloc(new linked_bucket_t(1)), _redgen(*t_net, std::make_shared(*t_net)), _partial_order(partial_order) { @@ -69,14 +70,14 @@ std::vector OnTheFlyDG::successors(Configuration *c) assert(false); //assert(false && "Someone told me, this was a bad place to be."); if (fastEval(query, &query_marking) == Condition::RTRUE){ - succs.push_back(newEdge(*v, 0));///*v->query->distance(context))*/0); + succs.push_back(newEdge(*v, 0));///*v->query->distance(context))*/0);F } } else if (query_type == LOPERATOR){ if(v->query->getQuantifier() == NEG){ // no need to try to evaluate here -- this is already transient in other evaluations. auto cond = static_cast(v->query); - Configuration* c = createConfiguration(v->marking, v->getOwner(), (*cond)[0]); + Configuration* c = createConfiguration(query_marking, v->getOwner(), (*cond)[0]); Edge* e = newEdge(*v, /*v->query->distance(context)*/0); e->is_negated = true; if (!e->addTarget(c)) { @@ -112,7 +113,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) for(auto c : conds) { assert(PetriEngine::PQL::isTemporal(c)); - if (e->addTarget(createConfiguration(v->marking, v->getOwner(), c))) + if (e->addTarget(createConfiguration(query_marking, v->getOwner(), c))) break; } if (e->handled) { @@ -147,7 +148,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) { assert(PetriEngine::PQL::isTemporal(c)); Edge *e = newEdge(*v, /*cond->distance(context)*/0); - if (e->addTarget(createConfiguration(v->marking, v->getOwner(), c))) { + if (e->addTarget(createConfiguration(query_marking, v->getOwner(), c))) { --e->refcnt; release(e); } @@ -174,7 +175,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) } else { //right side is temporal, we need to evaluate it as normal - Configuration* c = createConfiguration(v->marking, v->getOwner(), (*cond)[1]); + Configuration* c = createConfiguration(query_marking, v->getOwner(), (*cond)[1]); right = newEdge(*v, /*(*cond)[1]->distance(context)*/0); right->addTarget(c); } @@ -186,7 +187,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) valid = r0 == Condition::RTRUE; } else { //left side is temporal, include it in the edge - left = createConfiguration(v->marking, v->getOwner(), (*cond)[0]); + left = createConfiguration(query_marking, v->getOwner(), (*cond)[0]); } if (valid || left != nullptr) { //if left side is guaranteed to be not satisfied, skip successor generation @@ -205,7 +206,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) return false; } context.setMarking(mark.marking()); - Configuration* c = createConfiguration(createMarking(mark), owner(mark, cond), cond); + Configuration* c = createConfiguration(mark, owner(mark, cond), cond); return !leftEdge->addTarget(c); }, [&]() @@ -248,7 +249,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) } } else { subquery = newEdge(*v, /*cond->distance(context)*/0); - Configuration* c = createConfiguration(v->marking, v->getOwner(), (*cond)[0]); + Configuration* c = createConfiguration(query_marking, v->getOwner(), (*cond)[0]); subquery->addTarget(c); // cannot be self-loop since the formula is smaller } Edge* e1 = nullptr; @@ -270,7 +271,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) return false; } context.setMarking(mark.marking()); - Configuration* c = createConfiguration(createMarking(mark), owner(mark, cond), cond); + Configuration* c = createConfiguration(mark, owner(mark, cond), cond); return !e1->addTarget(c); }, [&]() @@ -308,7 +309,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) { allValid = Condition::RUNKNOWN; context.setMarking(mark.marking()); - Configuration* c = createConfiguration(createMarking(mark), v->getOwner(), (*cond)[0]); + Configuration* c = createConfiguration(mark, v->getOwner(), (*cond)[0]); e->addTarget(c); } return true; @@ -340,7 +341,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) Edge *right = nullptr; auto r1 = fastEval((*cond)[1], &query_marking); if (r1 == Condition::RUNKNOWN) { - Configuration* c = createConfiguration(v->marking, v->getOwner(), (*cond)[1]); + Configuration* c = createConfiguration(query_marking, v->getOwner(), (*cond)[1]); right = newEdge(*v, /*(*cond)[1]->distance(context)*/0); right->addTarget(c); } else { @@ -358,7 +359,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) [&](){ auto r0 = fastEval((*cond)[0], &query_marking); if (r0 == Condition::RUNKNOWN) { - left = createConfiguration(v->marking, v->getOwner(), (*cond)[0]); + left = createConfiguration(query_marking, v->getOwner(), (*cond)[0]); } else { valid = r0 == Condition::RTRUE; } @@ -389,7 +390,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) } context.setMarking(marking.marking()); Edge* e = newEdge(*v, /*cond->distance(context)*/0); - Configuration* c1 = createConfiguration(createMarking(marking), owner(marking, cond), cond); + Configuration* c1 = createConfiguration(marking, owner(marking, cond), cond); e->addTarget(c1); if (left != nullptr) { e->addTarget(left); @@ -424,7 +425,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) return succs; } } else { - Configuration* c = createConfiguration(v->marking, v->getOwner(), (*cond)[0]); + Configuration* c = createConfiguration(query_marking, v->getOwner(), (*cond)[0]); subquery = newEdge(*v, /*cond->distance(context)*/0); subquery->addTarget(c); } @@ -449,7 +450,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) } context.setMarking(mark.marking()); Edge* e = newEdge(*v, /*cond->distance(context)*/0); - Configuration* c = createConfiguration(createMarking(mark), owner(mark, cond), cond); + Configuration* c = createConfiguration(mark, owner(mark, cond), cond); e->addTarget(c); if (!e->handled) succs.push_back(e); @@ -484,7 +485,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) { context.setMarking(marking.marking()); Edge* e = newEdge(*v, /*(*cond)[0]->distance(context)*/0); - Configuration* c = createConfiguration(createMarking(marking), v->getOwner(), query); + Configuration* c = createConfiguration(marking, v->getOwner(), query); e->addTarget(c); succs.push_back(e); } @@ -517,10 +518,11 @@ Configuration* OnTheFlyDG::initialConfiguration() { if(working_marking.marking() == nullptr) { - working_marking.setMarking (net->makeInitialMarking()); - query_marking.setMarking (net->makeInitialMarking()); + working_marking.setMarking(net->makeInitialMarking()); + query_marking.setMarking(net->makeInitialMarking()); + abstracted_marking.setMarking(net->makeInitialMarking()); auto o = owner(working_marking, this->query); - initial_config = createConfiguration(createMarking(working_marking), o, this->query); + initial_config = createConfiguration(working_marking, o, this->query); } return initial_config; } @@ -550,6 +552,28 @@ void OnTheFlyDG::nextStates(Marking& t_marking, Condition* ptr, void OnTheFlyDG::cleanUp() { + if (std::getenv("CZERO_CONF_DEBUG") != nullptr) + { + for (auto& c : trie) + { + for(auto& conf : c) + { + trie.unpack(conf->marking, encoder.scratchpad().raw()); + encoder.decode(query_marking.marking(), encoder.scratchpad().raw()); + + std::cout << "CONF M:"; + for (uint32_t i = 0; i < n_places; i++) + { + std::cout << query_marking[i]; + } + std::cout << " Q:"; + conf->query->toString(std::cout); + char ass = "0?%1"[conf->assignment + 2]; + std::cout << " A:" << ass << std::endl; + } + } + } + while(!recycle.empty()) { assert(recycle.top()->refcnt == -1); @@ -564,8 +588,11 @@ void OnTheFlyDG::setQuery(Condition* query) this->query = query; delete[] working_marking.marking(); delete[] query_marking.marking(); + delete[] abstracted_marking.marking(); working_marking.setMarking(nullptr); query_marking.setMarking(nullptr); + abstracted_marking.setMarking(nullptr); + token_elim.init(net); initialConfiguration(); assert(this->query); } @@ -584,9 +611,17 @@ size_t OnTheFlyDG::maxTokens() const { return _maxTokens; } -PetriConfig *OnTheFlyDG::createConfiguration(size_t marking, size_t own, Condition* t_query) +size_t OnTheFlyDG::tokensEliminated() const { + return token_elim.tokensEliminated(); +} + +PetriConfig *OnTheFlyDG::createConfiguration(const Marking& marking, size_t own, Condition* t_query) { - auto& configs = trie.get_data(marking); + abstracted_marking.copy(marking.marking(), n_places); + token_elim.eliminate(&abstracted_marking, t_query); + + size_t encoded = createMarking(abstracted_marking); + auto& configs = trie.get_data(encoded); for(PetriConfig* c : configs){ if(c->query == t_query) return c; @@ -596,7 +631,7 @@ PetriConfig *OnTheFlyDG::createConfiguration(size_t marking, size_t own, Conditi size_t id = conf_alloc->next(0); char* mem = (*conf_alloc)[id]; PetriConfig* newConfig = new (mem) PetriConfig(); - newConfig->marking = marking; + newConfig->marking = encoded; newConfig->query = t_query; newConfig->setOwner(own); configs.push_back(newConfig); diff --git a/src/PetriEngine/CMakeLists.txt b/src/PetriEngine/CMakeLists.txt index 81ede0ed0..064883120 100644 --- a/src/PetriEngine/CMakeLists.txt +++ b/src/PetriEngine/CMakeLists.txt @@ -17,6 +17,7 @@ add_library(PetriEngine ${HEADER_FILES} STSolver.cpp SuccessorGenerator.cpp TraceReplay.cpp + TokenEliminator.cpp options.cpp) target_link_libraries(PetriEngine PRIVATE Colored ColoredReduction Structures Simplification Stubborn Reachability PQL TAR Synthesis) diff --git a/src/PetriEngine/PetriNet.cpp b/src/PetriEngine/PetriNet.cpp index 7d5c5edfb..80fde3de7 100644 --- a/src/PetriEngine/PetriNet.cpp +++ b/src/PetriEngine/PetriNet.cpp @@ -126,21 +126,6 @@ namespace PetriEngine { return true; } - std::pair PetriNet::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]); - } - - std::pair PetriNet::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]); - } - bool PetriNet::fireable(const MarkVal *marking, int transitionIndex) { const TransPtr& transition = _transitions[transitionIndex]; diff --git a/src/PetriEngine/Reachability/ReachabilitySearch.cpp b/src/PetriEngine/Reachability/ReachabilitySearch.cpp index 796e5e831..4b5852be4 100644 --- a/src/PetriEngine/Reachability/ReachabilitySearch.cpp +++ b/src/PetriEngine/Reachability/ReachabilitySearch.cpp @@ -91,10 +91,11 @@ namespace PetriEngine { if (statisticsLevel == StatisticsLevel::None) return; - std::cout << "STATS:\n" - << "\tdiscovered states: " << states->discovered() << std::endl - << "\texplored states: " << ss.exploredStates << std::endl - << "\texpanded states: " << ss.expandedStates << std::endl + std::cout << "STATS:\n" + << "\tdiscovered states: " << states->discovered() << std::endl + << "\texplored states: " << ss.exploredStates << std::endl + << "\texpanded states: " << ss.expandedStates << std::endl + << "\tTokens Eliminated: " << token_elim.tokensEliminated() << std::endl << "\tmax tokens: " << states->maxTokens() << std::endl; if (statisticsLevel != StatisticsLevel::Full) @@ -127,7 +128,7 @@ namespace PetriEngine { std::cout << std::endl << std::endl; } -#define TRYREACHPAR (queries, results, usequeries, printstats, seed, initPotencies) +#define TRYREACHPAR (queries, results, usequeries, printstats, seed, initPotencies, tokenElim) #define TEMPPAR(X, Y) if(keep_trace) return tryReach TRYREACHPAR ; \ else return tryReach TRYREACHPAR ; #define TRYREACH(X) if(stubbornreduction) TEMPPAR(X, ReducingSuccessorGenerator) \ @@ -154,7 +155,8 @@ namespace PetriEngine { size_t seed, int64_t depthRandomWalk, const int64_t incRandomWalk, - const std::vector& initPotencies) + const std::vector& initPotencies, + const TokenEliminationMethod tokenElim) { bool usequeries = !statespacesearch; diff --git a/src/PetriEngine/TokenEliminator.cpp b/src/PetriEngine/TokenEliminator.cpp new file mode 100644 index 000000000..db9a75fec --- /dev/null +++ b/src/PetriEngine/TokenEliminator.cpp @@ -0,0 +1,616 @@ +/** + * Original author(s): + * Nicolaj Ø. Jensen + */ + +#include +#include "PetriEngine/TokenEliminator.h" +#include "PetriEngine/PQL/PlaceUseVisitor.h" +#include "PetriEngine/PQL/PredicateCheckers.h" + +namespace PetriEngine { + /*** + * The PlaceReachabilityDirectionVisitor analyzes which places are part of a a reachability query + * and whether increases or decreases will bring us closer to satisfying the query. + * The result is a vector of bytes where the IN_Q_DEC bit and/or the IN_Q_INC indicates if + * and what direction is relevant. + */ + class PlaceReachabilityDirectionVisitor : public PQL::Visitor { + public: + explicit PlaceReachabilityDirectionVisitor(size_t n_places) : _in_use(n_places) {} + + uint32_t operator[](size_t id) const { + return _in_use[id]; + } + + [[nodiscard]] const std::vector& get_result() const { + return _in_use; + } + + protected: + void _accept(const PQL::NotCondition* element) override { + Visitor::visit(this, (*element)[0]); + } + void _accept(const PQL::AndCondition* element) override { + for (auto& e : *element) Visitor::visit(this, e); + } + void _accept(const PQL::OrCondition* element) override { + for (auto& e : *element) Visitor::visit(this, e); + } + void _accept(const PQL::LessThanCondition* element) override { + direction = IN_Q_DEC; + Visitor::visit(this, (*element)[0]); + direction = IN_Q_INC; + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::LessThanOrEqualCondition* element) override { + direction = IN_Q_DEC; + Visitor::visit(this, (*element)[0]); + direction = IN_Q_INC; + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::EqualCondition* element) override { + throw std::runtime_error("EqualCondition should not exist in compiled reachability expression"); + direction = IN_Q_INC | IN_Q_DEC; + Visitor::visit(this, (*element)[0]); + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::NotEqualCondition* element) override { + throw std::runtime_error("NotEqualCondition should not exist in compiled reachability expression"); + direction = IN_Q_INC | IN_Q_DEC; + Visitor::visit(this, (*element)[0]); + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::UnfoldedIdentifierExpr* element) override { + _in_use[element->offset()] |= direction; + } + void _accept(const PQL::PlusExpr* element) override { + // TODO: Test this + for(auto& p : element->places()) _in_use[p.first] |= direction; + } + void _accept(const PQL::MultiplyExpr* element) override { + // TODO: Test this. Especially negative values + for(auto& p : element->places()) _in_use[p.first] |= direction; + } + void _accept(const PQL::MinusExpr* element) override { + // TODO: Do we need to negate here? + Visitor::visit(this, (*element)[0]); + } + void _accept(const PQL::SubtractExpr* element) override { + // TODO: Do we need to negate here? + for(auto& e : element->expressions()) Visitor::visit(this, e); + } + void _accept(const PQL::CompareConjunction* element) override { + // Compiled fireability proposition + if (element->isNegated() == negated) { + for (auto& e : *element) { + if (e._lower != 0) _in_use[e._place] |= IN_Q_INC; + if (e._upper != std::numeric_limits::max()) _in_use[e._place] |= IN_Q_DEC; + } + } else { + for (auto& e : *element) { + if (e._lower != 0) _in_use[e._place] |= IN_Q_DEC; + if (e._upper != std::numeric_limits::max()) _in_use[e._place] |= IN_Q_INC; + } + } + } + void _accept(const PQL::UnfoldedUpperBoundsCondition* element) override { + for(auto& p : element->places()) + _in_use[p._place] |= IN_Q_INC; + } + + void _accept(const PQL::EFCondition* el) override { + Visitor::visit(this, (*el)[0]); + } + void _accept(const PQL::EGCondition* el) override { + throw std::runtime_error("EGCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::AGCondition* el) override { + throw std::runtime_error("AGCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::AFCondition* el) override { + throw std::runtime_error("AFCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::EXCondition* el) override { + throw std::runtime_error("EXCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::AXCondition* el) override { + throw std::runtime_error("AXCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::EUCondition* el) override { + throw std::runtime_error("EUCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::AUCondition* el) override { + throw std::runtime_error("AUCondition should not exist in compiled reachability expression"); + } + void _accept(const PQL::LiteralExpr* element) override { + // no-op + } + void _accept(const PQL::DeadlockCondition* element) override { + // no-op, disallowed due to loop sensitivity + } + + private: + std::vector _in_use; + bool negated = false; + uint8_t direction = 0; + }; + + void TokenEliminator::init(const PetriNet *net) { + _cache.clear(); + _net = net; + setupProducersAndConsumers(); + setupExtBounds(); + } + + void TokenEliminator::setupProducersAndConsumers() { + _inhibpost.resize(0); + _inhibpost.resize(_net->_nplaces); + std::vector, std::vector>> tmp_places(_net->_nplaces); + + for (uint32_t t = 0; t < _net->_ntransitions; t++) { + const TransPtr &ptr = _net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; + for (; finv < linv; finv++) { // Post set of places + if (_net->_invariants[finv].inhibitor) { + _inhibpost[_net->_invariants[finv].place].push_back(t); + } else { + tmp_places[_net->_invariants[finv].place].second.emplace_back(t, _net->_invariants[finv].direction); + } + } + + finv = linv; + linv = _net->_transitions[t + 1].inputs; + for (; finv < linv; finv++) { // Pre set of places + if (_net->_invariants[finv].direction > 0) + tmp_places[_net->_invariants[finv].place].first.emplace_back(t, _net->_invariants[finv].direction); + } + } + + // flatten + size_t ntrans = 0; + for (const auto& p : tmp_places) { + ntrans += p.first.size() + p.second.size(); + } + _parcs = std::make_unique(ntrans); + + _prodcons = std::make_unique(_net->_nplaces + 1); + uint32_t offset = 0; + uint32_t p = 0; + for (; p < _net->_nplaces; ++p) { + auto &pre = tmp_places[p].first; + auto &post = tmp_places[p].second; + + // keep things nice for caches + std::sort(pre.begin(), pre.end()); + std::sort(post.begin(), post.end()); + + _prodcons[p].producers = offset; + offset += pre.size(); + _prodcons[p].consumers = offset; + offset += post.size(); + for (size_t tn = 0; tn < pre.size(); ++tn) { + _parcs[tn + _prodcons[p].producers] = pre[tn]; + } + + for (size_t tn = 0; tn < post.size(); ++tn) { + _parcs[tn + _prodcons[p].consumers] = post[tn]; + } + + } + assert(offset == ntrans); + _prodcons[p].producers = offset; + _prodcons[p].consumers = offset; + } + + void TokenEliminator::setupExtBounds() { + _extBounds.assign(_net->_nplaces, 0); + for (uint32_t i = 0; i < _net->_ntransitions; ++i) { + uint32_t finv = _net->_transitions[i].inputs; + uint32_t linv = _net->_transitions[i].outputs; + + for ( ; finv < linv; ++finv) { + const Invariant& inv = _net->_invariants[finv]; + if (inv.inhibitor) { + _extBounds[inv.place] = std::max(_extBounds[inv.place], inv.tokens); + } + } + } + } + + std::pair TokenEliminator::producers(uint32_t p) const { + const place_t pmeta = _prodcons[p]; + return std::make_pair(&_parcs[pmeta.producers], &_parcs[pmeta.consumers]); + } + + std::pair TokenEliminator::consumers(uint32_t p) const { + return std::make_pair(&_parcs[_prodcons[p].consumers], &_parcs[_prodcons[p + 1].producers]); + } + + void TokenEliminator::eliminate(Marking *marking, Condition *query) { + if (!_enabled) return; + if (_doDynamic) { + eliminateDynamic(marking, query); + } else { + eliminateStatic(marking, query); + } + } + + void TokenEliminator::findDeadPlacesAndTransitions(const Marking *marking) { + + _pflags.resize(_net->_nplaces); + std::fill(_pflags.begin(), _pflags.end(), 0); + _fireable.resize(_net->_ntransitions); + std::fill(_fireable.begin(), _fireable.end(), false); + + std::queue queue; + + // Helper functions + + auto processIncPlace = [&](uint32_t p) { + if ((_pflags[p] & CAN_INC) == 0) { + _pflags[p] |= CAN_INC; + for (auto [t, last] = consumers(p); t < last; ++t) { + if (!_fireable[t->index]) + queue.push(t->index); + } + } + }; + + auto processDecPlace = [&](uint32_t p) { + if ((_pflags[p] & CAN_DEC) == 0) { + _pflags[p] |= CAN_DEC; + for (uint32_t t : _inhibpost[p]) { + if (!_fireable[t]) + queue.push(t); + } + } + }; + + auto processEnabled = [&](uint32_t t) { + _fireable[t] = true; + // Find and process negative pre-set and positive post-set + for (auto [finv, linv] = _net->preset(t); finv < linv; ++finv) { + if (finv->direction < 0) + processDecPlace(finv->place); + } + for (auto [finv, linv] = _net->postset(t); finv < linv; ++finv) { + if (finv->direction > 0) + processIncPlace(finv->place); + } + }; + + // Process initially enabled transitions + for (uint32_t t = 0; t < _net->_ntransitions; ++t) { + uint32_t i = _net->_transitions[t].inputs; + uint32_t fout = _net->_transitions[t].outputs; + bool enabled = true; + for ( ; i < fout; i++) { + const Invariant& preinv = _net->_invariants[i]; + if (preinv.inhibitor != (preinv.tokens > (*marking)[preinv.place])) { + enabled = false; + break; + } + } + if (enabled) { + processEnabled(t); + } + } + + // Compute fixed point of effectively dead places and transitions + + while (!queue.empty()) { + uint32_t t = queue.front(); + queue.pop(); + if (_fireable[t]) continue; + + // Is t enabled? + bool enabled = true; + uint32_t finv = _net->_transitions[t].inputs; + uint32_t linv = _net->_transitions[t].outputs; + for (; finv < linv; ++finv) { + const Invariant& arc = _net->_invariants[finv]; + bool notInhibited = !arc.inhibitor || arc.tokens > (*marking)[arc.place] || (_pflags[arc.place] & CAN_DEC) > 0; + bool enoughTokens = arc.inhibitor || arc.tokens <= (*marking)[arc.place] || (_pflags[arc.place] & CAN_INC) > 0; + if (!notInhibited || !enoughTokens) { + enabled = false; + break; + } + } + if (enabled) { + processEnabled(t); + } + } + } + + void TokenEliminator::eliminateDynamic(Marking * marking, Condition * query) { + + if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { + return; + } + + std::stringstream before; + if (_env_TOKEN_ELIM_DEBUG) { + for (uint32_t i = 0; i < _net->_nplaces; i++) { + before << (*marking)[i]; + } + } + + findDeadPlacesAndTransitions(marking); + findDynamicVisiblePlaces(query); + + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if ((_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP | IN_Q_INC | IN_Q_DEC)) == 0) { + // Going below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _extBounds[i]); + _tokensEliminated += cur - ex; + marking->marking()[i] = ex; + } + } + + if (_env_TOKEN_ELIM_DEBUG) { + std::stringstream after; + for (uint32_t i = 0; i < _net->_nplaces; i++) + { + after << (*marking)[i]; + } + if (before.str() == after.str()) + return; + + PQL::PlaceUseVisitor puv(_net->numberOfPlaces()); + PQL::Visitor::visit(&puv, query); + auto& inQuery = puv.in_use(); + + std::cout << before.str() << "->" << after.str() << " | Visible: "; + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if (inQuery[i] || (_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP)) > 0) { + std::cout << *_net->placeNames()[i] << "#" << inQuery[i] << ((_pflags[i] & VIS_INC) > 0) + << ((_pflags[i] & VIS_DEC) > 0) << ((_pflags[i] & MUST_KEEP) > 0) << " "; + } + } + std::cout << "| Live: "; + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if ((_pflags[i] & (CAN_INC | CAN_DEC)) > 0) { + std::cout << *_net->placeNames()[i] << "#" << ((_pflags[i] & CAN_INC) > 0) + << ((_pflags[i] & CAN_DEC) > 0) << " "; + } + } + std::stringstream ss; + query->toString(ss); + std::cout << "| " << ss.str() << "\n"; + } + } + + void TokenEliminator::findDynamicVisiblePlaces(Condition *query) { + + PlaceReachabilityDirectionVisitor pv(_net->numberOfPlaces()); + PQL::Visitor::visit(&pv, query); + auto& use = pv.get_result(); + + std::queue queue; + + // Places in query are visible + for (uint32_t p = 0; p < _net->_nplaces; ++p) { + if (use[p] > 0) { + _pflags[p] |= use[p]; + if ((_pflags[p] & IN_Q_DEC) > 0 && (_pflags[p] & CAN_DEC) > 0) { + _pflags[p] |= VIS_DEC; + } + if ((_pflags[p] & IN_Q_INC) > 0 && (_pflags[p] & CAN_INC) > 0) { + _pflags[p] |= VIS_INC; + } + queue.push(p); + } + } + + // Propagate visibility + while (!queue.empty()) { + uint32_t p = queue.front(); + queue.pop(); + + if ((_pflags[p] & VIS_DEC) > 0) { + // Put pre-set of negative consumers in vis_inc, + // and inhibiting pre-set of negative consumers in vis_dec + for (auto [t, last] = consumers(p); t < last; ++t) { + if (!_fireable[t->index] || t->direction >= 0) continue; + for (auto [finv, linv] = _net->preset(t->index) ; finv < linv; ++finv) { + const Invariant& arc = *finv; + if (arc.inhibitor) { + if ((_pflags[arc.place] & VIS_DEC) == 0 && (_pflags[arc.place] & CAN_DEC) > 0) { + queue.push(arc.place); + _pflags[arc.place] |= VIS_DEC; + } + } else { + if (arc.place != p && (_pflags[arc.place] & VIS_INC) == 0 && (_pflags[arc.place] & CAN_INC) > 0) { + queue.push(arc.place); + _pflags[arc.place] |= VIS_INC; + } + if (arc.tokens > 1 && (_pflags[arc.place] & CAN_INC) > 0) { + // This consumer may need more tokens to fire, so increases are also visible + _pflags[arc.place] |= VIS_INC; + } + } + } + } + } + + // This case is checker last since the first case may set VIS_INC for p + if ((_pflags[p] & VIS_INC) > 0) { + // Put pre-set of positive producers in vis_inc, + // and inhibiting pre-set positive producers in vis_dec + for (auto [t, last] = producers(p); t < last; ++t) { + if (!_fireable[t->index] || t->direction <= 0) continue; + for (auto [finv, linv] = _net->preset(t->index) ; finv < linv; ++finv) { + const Invariant& arc = *finv; + if (arc.inhibitor) { + if ((_pflags[arc.place] & VIS_DEC) == 0 && (_pflags[arc.place] & CAN_DEC) > 0) { + queue.push(arc.place); + _pflags[arc.place] |= VIS_DEC; + } + } else { + if ((_pflags[arc.place] & VIS_INC) == 0 && (_pflags[arc.place] & CAN_INC) > 0) { + queue.push(arc.place); + _pflags[arc.place] |= VIS_INC; + } + } + } + } + } + } + + // We cannot disable fireable transitions affecting visible places, so their pre-set must be preserved, + // even if their pre-set is effectively dead. + for (uint32_t t = 0; t < _net->_ntransitions; ++t) { + if (!_fireable[t]) continue; + uint32_t finv = _net->_transitions[t].inputs; + uint32_t linv = _net->_transitions[t+1].inputs; + bool affectsVisible = false; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _net->_invariants[finv]; + if (arc.direction > 0 && (_pflags[arc.place] & (VIS_INC | IN_Q_INC)) > 0) { + affectsVisible = true; + break; + } + if (arc.direction < 0 && (_pflags[arc.place] & (VIS_DEC | IN_Q_DEC)) > 0) { + affectsVisible = true; + break; + } + } + if (affectsVisible) { + finv = _net->_transitions[t].inputs; + linv = _net->_transitions[t].outputs; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _net->_invariants[finv]; + if (!arc.inhibitor) { + _pflags[arc.place] |= MUST_KEEP; + } + } + } + } + } + + void TokenEliminator::eliminateStatic(Marking * marking, Condition * query) { + const std::vector *visible; + auto it = _cache.find(query); + if (it != _cache.end()) { + visible = &it->second; + } else { + visible = &findStaticVisiblePlaces(query); + } + + if (!visible->empty()) { + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if (!(*visible)[i]) { + // Going below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _extBounds[i]); + _tokensEliminated += cur - ex; + marking->marking()[i] = ex; + } + } + } + } + + const std::vector &TokenEliminator::findStaticVisiblePlaces(Condition *query) { + + if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { + _cache.insert(std::make_pair(query, std::vector())); + return _cache.at(query); + } + + PlaceReachabilityDirectionVisitor puv(_net->numberOfPlaces()); + PQL::Visitor::visit(&puv, query); + auto& use = puv.get_result(); + + std::vector vis_inc(_net->_nplaces); // Places where token increment is visible to query + std::vector vis_dec(_net->_nplaces); // Places where token decrement is visible to query + std::vector queue; + + // Places in query are visible + for (uint32_t p = 0; p < _net->_nplaces; ++p) { + if (use[p] > 0) { + vis_inc[p] = (use[p] & IN_Q_INC) > 0; + vis_dec[p] = (use[p] & IN_Q_DEC) > 0; + queue.push_back(p); + } + } + + // Propagate visibility + while (!queue.empty()) { + uint32_t p = queue.back(); + queue.pop_back(); + + if (vis_dec[p]) { + // Put pre-set of negative consumers in vis_inc, + // and inhibiting pre-set of negative consumers in vis_dec + for (auto [t, last] = consumers(p); t < last; ++t) { + if (t->direction >= 0) continue; + for (auto [finv, fout] = _net->preset(t->index); finv < fout; ++finv) { + const Invariant& arc = *finv; + if (arc.inhibitor) { + if (!vis_dec[arc.place]) { + queue.push_back(arc.place); + vis_dec[arc.place] = true; + } + } else { + if (!vis_inc[arc.place] && arc.place != p) { + queue.push_back(arc.place); + vis_inc[arc.place] = true; + } + if (arc.tokens > 1) { + // This consumer may need more tokens to fire, so increases are also visible + vis_inc[p] = true; + } + } + } + } + } + + // This case is checker last since the first case may set VIS_INC for p + if (vis_inc[p]) { + // Put pre-set of positive producers in vis_inc, + // and inhibiting pre-set of positive producers in vis_dec + for (auto [t, last] = producers(p); t < last; ++t) { + if (t->direction <= 0) continue; + for (auto [finv, linv] = _net->preset(t->index) ; finv < linv; ++finv) { + const Invariant& arc = *finv; + if (arc.inhibitor) { + if (!vis_dec[arc.place]) { + queue.push_back(arc.place); + vis_dec[arc.place] = true; + } + } else { + if (!vis_inc[arc.place]) { + queue.push_back(arc.place); + vis_inc[arc.place] = true; + } + } + } + } + } + } + + std::vector visible(_net->_nplaces); + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + visible[i] = vis_inc[i] || vis_dec[i]; + } + + if (_env_TOKEN_ELIM_DEBUG) { + std::stringstream ss; + query->toString(ss); + std::cout << "Visible places : "; + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if (use[i] > 0 || vis_inc[i] || vis_dec[i]) { + std::cout << *_net->placeNames()[i] << "#" << ((use[i] & (IN_Q_INC | IN_Q_DEC)) > 0) << vis_inc[i] + << vis_dec[i] << " "; + } + } + std::cout << ": " << ss.str() << "\n"; + } + + _cache.insert(std::make_pair(query, visible)); + return _cache.at(query); + } +} \ No newline at end of file diff --git a/src/PetriEngine/options.cpp b/src/PetriEngine/options.cpp index 99ceaefa2..3beae983f 100644 --- a/src/PetriEngine/options.cpp +++ b/src/PetriEngine/options.cpp @@ -110,6 +110,21 @@ void options_t::print(std::ostream& optionsOut) { optionsOut << ",LPSolve_Timeout=" << lpsolveTimeout; + if (tokenElimMethodReach == TokenEliminationMethod::Disabled) { + optionsOut << ",TokenElim_Reach=DISABLED"; + } else if (tokenElimMethodReach == TokenEliminationMethod::Static) { + optionsOut << ",TokenElim_Reach=STATIC"; + } else if (tokenElimMethodReach == TokenEliminationMethod::Dynamic) { + optionsOut << ",TokenElim_Reach=DYNAMIC"; + } + + if (tokenElimMethodCTL == TokenEliminationMethod::Disabled) { + optionsOut << ",TokenElim_CTL=DISABLED"; + } else if (tokenElimMethodCTL == TokenEliminationMethod::Static) { + optionsOut << ",TokenElim_CTL=STATIC"; + } else if (tokenElimMethodCTL == TokenEliminationMethod::Dynamic) { + optionsOut << ",TokenElim_CTL=DYNAMIC"; + } if (usedctl) { if (ctlalgorithm == CTL::CZero) { @@ -206,6 +221,11 @@ void printHelp() { " - none Run preprocessing steps only.\n" " --noweak Disable optimizations for weak Büchi automata when doing \n" " LTL model checking. Not recommended.\n" + " --token-elim-reach Simplify markings by removing tokens in reachability engine (see --token-elim-ctl for options).\n" + " --token-elim-ctl Simplify markings by removing tokens in certain zero engine.\n" + " - none No token elimination (default)\n" + " - static Elimination based on net structure with caching\n" + " - dynamic Aggressive elimination based on net structure and current marking\n" " --noreach Force use of CTL/LTL engine, even when queries are reachability.\n" " Not recommended since the reachability engine is faster.\n" " --nounfold Stops after colored structural reductions and writing the reduced net\n" @@ -638,6 +658,34 @@ bool options_t::parse(int argc, const char** argv) { ++i; strategy_output = argv[i]; } + else if (std::strcmp(argv[i], "--token-elim-reach") == 0) { + if (argc == i + 1) { + throw base_error("Missing argument to --token-elim-reach"); + } else if (std::strcmp(argv[i + 1], "none") == 0) { + tokenElimMethodReach = TokenEliminationMethod::Disabled; + } else if (std::strcmp(argv[i + 1], "static") == 0) { + tokenElimMethodReach = TokenEliminationMethod::Static; + } else if (std::strcmp(argv[i + 1], "dynamic") == 0) { + tokenElimMethodReach = TokenEliminationMethod::Dynamic; + } else { + throw base_error("Unrecognized argument ", std::quoted(argv[i + 1]), " to --token-elim-reach\n"); + } + ++i; + } + else if (std::strcmp(argv[i], "--token-elim-ctl") == 0) { + if (argc == i + 1) { + throw base_error("Missing argument to --token-elim-ctl"); + } else if (std::strcmp(argv[i + 1], "none") == 0) { + tokenElimMethodCTL = TokenEliminationMethod::Disabled; + } else if (std::strcmp(argv[i + 1], "static") == 0) { + tokenElimMethodCTL = TokenEliminationMethod::Static; + } else if (std::strcmp(argv[i + 1], "dynamic") == 0) { + tokenElimMethodCTL = TokenEliminationMethod::Dynamic; + } else { + throw base_error("Unrecognized argument ", std::quoted(argv[i + 1]), " to --token-elim-ctl\n"); + } + ++i; + } else if (std::strcmp(argv[i], "-h") == 0 || std::strcmp(argv[i], "--help") == 0) { printHelp(); return true; diff --git a/src/main.cpp b/src/main.cpp index 871e41481..2362a31c5 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -388,6 +388,7 @@ int main(int argc, const char** argv) { options.strategy, options.printstatistics, options.stubbornreduction, + options.tokenElimMethodCTL, querynames, queries, ctl_ids, @@ -535,7 +536,8 @@ int main(int argc, const char** argv) { options.seed(), options.depthRandomWalk, options.incRandomWalk, - initialPotencies); + initialPotencies, + options.tokenElimMethodReach); } else { strategy.reachable(queries, results, options.strategy, @@ -545,7 +547,9 @@ int main(int argc, const char** argv) { options.trace != TraceLevel::None, options.seed(), options.depthRandomWalk, - options.incRandomWalk); + options.incRandomWalk, + std::vector(), + options.tokenElimMethodReach); } } }