From 8e58bc3cbeeeab2f749ef376111bc5dd5661211c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 31 Oct 2023 16:59:53 +0100 Subject: [PATCH 01/29] Add simple extrapolation class --- include/PetriEngine/Extrapolator.h | 64 ++++++++++++++ src/PetriEngine/Extrapolator.cpp | 129 +++++++++++++++++++++++++++++ 2 files changed, 193 insertions(+) create mode 100644 include/PetriEngine/Extrapolator.h create mode 100644 src/PetriEngine/Extrapolator.cpp diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h new file mode 100644 index 000000000..c8b6accb5 --- /dev/null +++ b/include/PetriEngine/Extrapolator.h @@ -0,0 +1,64 @@ +#ifndef VERIFYPN_EXTRAPOLATOR_H +#define VERIFYPN_EXTRAPOLATOR_H + + +#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; + + class Extrapolator { + public: + virtual void init(const PetriEngine::PetriNet *net, const Condition *query) = 0; + + virtual void extrapolate(Marking *marking, Condition *query) = 0; + }; + + class NoExtrapolator : public Extrapolator { + public: + void init(const PetriEngine::PetriNet *net, const Condition *query) override { + // no-op + }; + + void extrapolate(Marking *marking, Condition *query) override { + // no-op + }; + }; + + /** + * The SimpleExtrapolator removes tokens in places that are not visible for the query, + * neither directly or indirectly. + */ + class SimpleExtrapolator : public Extrapolator { + public: + void init(const PetriEngine::PetriNet *net, const Condition *query) override; + + void extrapolate(Marking *marking, Condition *query) override; + + protected: + std::vector find_visible_places(const Condition *query); + + bool _initialized = false; + PetriEngine::PetriNet const *_net; + std::vector _inQuery; + std::unordered_map> _cache; + }; + + /** + * The SmartExtrapolator removes tokens in places that are *effectively* not visible for the query, + * neither directly or indirectly, by considering the current marking and + * which places can never gain or lose tokens. + */ + class SmartExtrapolator : public Extrapolator { + public: + void init(const PetriEngine::PetriNet *net, const Condition *query) override; + + void extrapolate(Marking *marking, Condition *query) override; + }; +} + +#endif //VERIFYPN_EXTRAPOLATOR_H diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp new file mode 100644 index 000000000..2acb8d639 --- /dev/null +++ b/src/PetriEngine/Extrapolator.cpp @@ -0,0 +1,129 @@ +#include "PetriEngine/Extrapolator.h" +#include "PetriEngine/PQL/PlaceUseVisitor.h" + +void PetriEngine::SimpleExtrapolator::init(const PetriEngine::PetriNet *net, const Condition *query) { + _initialized = true; + _net = net; + PetriEngine::PQL::PlaceUseVisitor puv(net->numberOfPlaces()); + PetriEngine::PQL::Visitor::visit(&puv, query); + _inQuery = puv.in_use(); + _cache.clear(); +} + +void PetriEngine::SimpleExtrapolator::extrapolate(Marking *marking, Condition *query) { + assert(_initialized); + const auto live_places = find_visible_places(query); + + for (int i = 0; i < _net->_nplaces; ++i) { + if (!live_places[i]) { + marking->marking()[i] = 0; // TODO: Minimum of current and greatest inhibitor weight + } + } +} + +std::vector PetriEngine::SimpleExtrapolator::find_visible_places(const Condition *query) { + auto it = _cache.find(query); + if (it != _cache.end()) { + return it->second; + } + + std::vector vis_inc(_net->_nplaces); + std::vector vis_dec(_net->_nplaces); + std::vector queue; + + for (int i = 0; i < _net->_nplaces; ++i) { + if (_inQuery[i]) { + vis_inc[i] = _inQuery[i]; + vis_dec[i] = _inQuery[i]; + queue.push_back(i); + } + } + + while (!queue.empty()) { + uint32_t p = queue.back(); + queue.pop_back(); + + uint32_t t = _net->_placeToPtrs[p]; + uint32_t tLast = _net->_placeToPtrs[p + 1]; + + for (; t < tLast; ++t) { + + // Is transition consumer and/or producer? + bool isConsumer = false; + uint32_t finv = _net->_transitions[t].inputs; + uint32_t linv = _net->_transitions[t].outputs; + for ( ; finv < linv; ++finv) { + if (_net->_invariants[finv].place == p && !_net->_invariants[finv].inhibitor) { + isConsumer = true; + break; + } + } + bool isProducer = false; + finv = _net->_transitions[t].outputs; + linv = _net->_transitions[t + 1].inputs; + for ( ; finv < linv; ++finv) { + if (_net->_invariants[finv].place == p && !_net->_invariants[finv].inhibitor) { + isProducer = true; + break; + } + } + + if (vis_inc[p] && isProducer) { + // Put preset of preset in vis_inc, + // and inhibiting preset of preset in vis_dec + const TransPtr &ptr = _net->_transitions[t]; + finv = ptr.inputs; + linv = ptr.outputs; + for ( ; finv < linv; ++finv) { + const Invariant& inv = _net->_invariants[finv]; + if (inv.inhibitor) { + if (!vis_dec[inv.place]) { + queue.push_back(inv.place); + vis_dec[inv.place] = true; + } + } else { + if (!vis_inc[inv.place]) { + queue.push_back(inv.place); + vis_inc[inv.place] = true; + } + } + } + } + + if (vis_dec[p] && isConsumer) { + // Put preset of postset in vis_inc, + // and inhibiting preset of postset in vis_dec + finv = _net->_transitions[t].outputs; + linv = _net->_transitions[t + 1].inputs; + for ( ; finv < linv; ++finv) { + const Invariant& inv = _net->_invariants[finv]; + if (inv.inhibitor) { + if (!vis_dec[inv.place]) { + queue.push_back(inv.place); + vis_dec[inv.place] = true; + } + } else { + if (!vis_inc[inv.place]) { + queue.push_back(inv.place); + vis_inc[inv.place] = true; + } + } + } + } + } + } + + std::vector visible(_net->_nplaces); + for (int i = 0; i < _net->_nplaces; ++i) { + visible[i] = vis_inc[i] || vis_dec[i]; + } + return visible; +} + +void PetriEngine::SmartExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { + // TODO +} + +void PetriEngine::SmartExtrapolator::extrapolate(Marking *marking, Condition *query) { + // TODO +} From 3bbf70000f6b96cdb5d504feaca0409d187dc862 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Thu, 2 Nov 2023 12:46:54 +0100 Subject: [PATCH 02/29] Improve SimpleExtrapolator using upper bounds --- include/PetriEngine/Extrapolator.h | 5 ++++- include/PetriEngine/PetriNet.h | 3 +++ src/PetriEngine/CMakeLists.txt | 1 + src/PetriEngine/Extrapolator.cpp | 34 ++++++++++++++++++++++++------ 4 files changed, 35 insertions(+), 8 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index c8b6accb5..a6113cc12 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -16,6 +16,8 @@ namespace PetriEngine { virtual void init(const PetriEngine::PetriNet *net, const Condition *query) = 0; virtual void extrapolate(Marking *marking, Condition *query) = 0; + + std::vector find_upper_bounds(const PetriEngine::PetriNet *net); }; class NoExtrapolator : public Extrapolator { @@ -40,11 +42,12 @@ namespace PetriEngine { void extrapolate(Marking *marking, Condition *query) override; protected: - std::vector find_visible_places(const Condition *query); + const std::vector & find_visible_places(const Condition *query); bool _initialized = false; PetriEngine::PetriNet const *_net; std::vector _inQuery; + std::vector _upperBounds; std::unordered_map> _cache; }; diff --git a/include/PetriEngine/PetriNet.h b/include/PetriEngine/PetriNet.h index 76897648f..91048bba6 100644 --- a/include/PetriEngine/PetriNet.h +++ b/include/PetriEngine/PetriNet.h @@ -150,6 +150,9 @@ namespace PetriEngine { friend class ReducingSuccessorGenerator; friend class STSolver; friend class StubbornSet; + friend class Extrapolator; + friend class SimpleExtrapolator; + friend class SmartExtrapolator; }; } // PetriEngine diff --git a/src/PetriEngine/CMakeLists.txt b/src/PetriEngine/CMakeLists.txt index 81ede0ed0..316cd01d5 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 + Extrapolator.cpp options.cpp) target_link_libraries(PetriEngine PRIVATE Colored ColoredReduction Structures Simplification Stubborn Reachability PQL TAR Synthesis) diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 2acb8d639..384e1b37c 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -1,34 +1,53 @@ #include "PetriEngine/Extrapolator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" +std::vector PetriEngine::Extrapolator::find_upper_bounds(const PetriEngine::PetriNet *net) { + std::vector bounds(net->_nplaces); + for (int i; 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) { + bounds[inv.place] = std::max(bounds[inv.place], inv.tokens); + } + } + } + + return bounds; +} + void PetriEngine::SimpleExtrapolator::init(const PetriEngine::PetriNet *net, const Condition *query) { _initialized = true; _net = net; PetriEngine::PQL::PlaceUseVisitor puv(net->numberOfPlaces()); PetriEngine::PQL::Visitor::visit(&puv, query); _inQuery = puv.in_use(); + _upperBounds = find_upper_bounds(net); _cache.clear(); } void PetriEngine::SimpleExtrapolator::extrapolate(Marking *marking, Condition *query) { assert(_initialized); - const auto live_places = find_visible_places(query); + const auto visible = find_visible_places(query); for (int i = 0; i < _net->_nplaces; ++i) { - if (!live_places[i]) { - marking->marking()[i] = 0; // TODO: Minimum of current and greatest inhibitor weight + if (!visible[i]) { + // Extrapolating below the upper bound may introduce behaviour + marking->marking()[i] = std::min(marking->marking()[i], _upperBounds[i]); } } } -std::vector PetriEngine::SimpleExtrapolator::find_visible_places(const Condition *query) { +const std::vector& PetriEngine::SimpleExtrapolator::find_visible_places(const Condition *query) { auto it = _cache.find(query); if (it != _cache.end()) { return it->second; } - std::vector vis_inc(_net->_nplaces); - std::vector vis_dec(_net->_nplaces); + 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; for (int i = 0; i < _net->_nplaces; ++i) { @@ -117,7 +136,8 @@ std::vector PetriEngine::SimpleExtrapolator::find_visible_places(const Con for (int i = 0; i < _net->_nplaces; ++i) { visible[i] = vis_inc[i] || vis_dec[i]; } - return visible; + _cache.insert(std::make_pair(query, visible)); + return _cache.at(query); } void PetriEngine::SmartExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { From f21079cc211b014d20d206afc969060a7b2c5ef7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Thu, 2 Nov 2023 14:25:08 +0100 Subject: [PATCH 03/29] Apply Extrapolation --- include/CTL/CTLResult.h | 1 + include/CTL/PetriNets/OnTheFlyDG.h | 8 +++-- include/PetriEngine/Extrapolator.h | 9 ++++++ src/CTL/CTLEngine.cpp | 1 + src/CTL/CTLResult.cpp | 17 ++++++----- src/CTL/PetriNets/OnTheFlyDG.cpp | 48 ++++++++++++++++++------------ src/PetriEngine/Extrapolator.cpp | 5 +++- 7 files changed, 59 insertions(+), 30 deletions(-) diff --git a/include/CTL/CTLResult.h b/include/CTL/CTLResult.h index c12ce100f..fd55d0008 100644 --- a/include/CTL/CTLResult.h +++ b/include/CTL/CTLResult.h @@ -27,6 +27,7 @@ struct CTLResult { size_t exploredConfigurations = 0; size_t numberOfEdges = 0; size_t maxTokens = 0; + size_t tokensExtrapolated = 0; #ifdef VERIFYPNDIST size_t numberOfRoundsComputingDistance = 0; size_t numberOfTokensReceived = 0; diff --git a/include/CTL/PetriNets/OnTheFlyDG.h b/include/CTL/PetriNets/OnTheFlyDG.h index 7efc21731..6474ecdd5 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/Extrapolator.h" namespace PetriNets { class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph @@ -22,6 +23,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph using Condition = PetriEngine::PQL::Condition; using Condition_ptr = PetriEngine::PQL::Condition_ptr; using Marking = PetriEngine::Structures::State; + using Extrapolator = PetriEngine::Extrapolator; OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order); 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 tokensExtrapolated() const; Condition::Result initialEval(); protected: @@ -55,6 +58,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph PetriConfig* initial_config; Marking working_marking; Marking query_marking; + Extrapolator* extrapolator = nullptr; uint32_t n_transitions = 0; uint32_t n_places = 0; size_t _markingCount = 0; @@ -89,8 +93,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(Marking& marking, size_t own, Condition* query); + PetriConfig *createConfiguration(Marking& marking, size_t own, const Condition_ptr& query) { return createConfiguration(marking, own, query.get()); } diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index a6113cc12..021cdec00 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -13,11 +13,20 @@ namespace PetriEngine { class Extrapolator { public: + virtual ~Extrapolator() = default; + virtual void init(const PetriEngine::PetriNet *net, const Condition *query) = 0; virtual void extrapolate(Marking *marking, Condition *query) = 0; std::vector find_upper_bounds(const PetriEngine::PetriNet *net); + + size_t tokensExtrapolated() const { + return _tokensExtrapolated; + } + + protected: + size_t _tokensExtrapolated = 0; }; class NoExtrapolator : public Extrapolator { diff --git a/src/CTL/CTLEngine.cpp b/src/CTL/CTLEngine.cpp index b8511db38..9c36b86fa 100644 --- a/src/CTL/CTLEngine.cpp +++ b/src/CTL/CTLEngine.cpp @@ -72,6 +72,7 @@ bool CTLSingleSolve(Condition* query, PetriNet* net, result.exploredConfigurations += alg->exploredConfigurations(); result.numberOfEdges += alg->numberOfEdges(); result.maxTokens = std::max(graph.maxTokens(), result.maxTokens); + result.tokensExtrapolated = graph.tokensExtrapolated(); return res; } diff --git a/src/CTL/CTLResult.cpp b/src/CTL/CTLResult.cpp index 227ab132d..8b16acc47 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 << " max tokens: : " << maxTokens << "\n"; // kept lower case to be compatible with reachability format + out << " Tokens Extrapolated : " << tokensExtrapolated << "\n"; } 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..8d29aafd6 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -26,6 +26,7 @@ OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encod net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); + extrapolator = new PetriEngine::SimpleExtrapolator(); } @@ -41,6 +42,7 @@ OnTheFlyDG::~OnTheFlyDG() } delete conf_alloc; delete edge_alloc; + delete extrapolator; } Condition::Result OnTheFlyDG::initialEval() @@ -76,7 +78,7 @@ std::vector OnTheFlyDG::successors(Configuration *c) 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 +114,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 +149,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 +176,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 +188,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 +207,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 +250,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 +272,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 +310,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 +342,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 +360,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 +391,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 +426,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 +451,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 +486,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); } @@ -520,7 +522,7 @@ Configuration* OnTheFlyDG::initialConfiguration() working_marking.setMarking (net->makeInitialMarking()); query_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; } @@ -566,6 +568,7 @@ void OnTheFlyDG::setQuery(Condition* query) delete[] query_marking.marking(); working_marking.setMarking(nullptr); query_marking.setMarking(nullptr); + extrapolator->init(net, query); initialConfiguration(); assert(this->query); } @@ -584,9 +587,16 @@ size_t OnTheFlyDG::maxTokens() const { return _maxTokens; } -PetriConfig *OnTheFlyDG::createConfiguration(size_t marking, size_t own, Condition* t_query) +size_t OnTheFlyDG::tokensExtrapolated() const { + return extrapolator->tokensExtrapolated(); +} + +PetriConfig *OnTheFlyDG::createConfiguration(Marking& marking, size_t own, Condition* t_query) { - auto& configs = trie.get_data(marking); + extrapolator->extrapolate(&marking, t_query); + + size_t encoded = createMarking(marking); + auto& configs = trie.get_data(encoded); for(PetriConfig* c : configs){ if(c->query == t_query) return c; @@ -596,7 +606,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/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 384e1b37c..fbca6f69d 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -35,7 +35,10 @@ void PetriEngine::SimpleExtrapolator::extrapolate(Marking *marking, Condition *q for (int i = 0; i < _net->_nplaces; ++i) { if (!visible[i]) { // Extrapolating below the upper bound may introduce behaviour - marking->marking()[i] = std::min(marking->marking()[i], _upperBounds[i]); + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _upperBounds[i]); + _tokensExtrapolated += cur - ex; + marking->marking()[i] = ex; } } } From 732d1694979315d596261cba24a6fe6f03d7f683 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 3 Nov 2023 15:08:42 +0100 Subject: [PATCH 04/29] Use extrapolation in algorithm --- include/CTL/CTLResult.h | 2 +- include/PetriEngine/Extrapolator.h | 7 +- src/CTL/CTLEngine.cpp | 2 +- src/CTL/CTLResult.cpp | 2 +- src/PetriEngine/Extrapolator.cpp | 116 +++++++++++++++++------------ 5 files changed, 74 insertions(+), 55 deletions(-) diff --git a/include/CTL/CTLResult.h b/include/CTL/CTLResult.h index fd55d0008..2aa6463d9 100644 --- a/include/CTL/CTLResult.h +++ b/include/CTL/CTLResult.h @@ -26,8 +26,8 @@ struct CTLResult { size_t processedNegationEdges = 0; size_t exploredConfigurations = 0; size_t numberOfEdges = 0; - size_t maxTokens = 0; size_t tokensExtrapolated = 0; + size_t maxTokens = 0; #ifdef VERIFYPNDIST size_t numberOfRoundsComputingDistance = 0; size_t numberOfTokensReceived = 0; diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 021cdec00..ae7a71554 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -19,7 +19,8 @@ namespace PetriEngine { virtual void extrapolate(Marking *marking, Condition *query) = 0; - std::vector find_upper_bounds(const PetriEngine::PetriNet *net); + std::vector findUpperBounds(const PetriEngine::PetriNet *net); + std::vector> findProducers(const PetriEngine::PetriNet *net); size_t tokensExtrapolated() const { return _tokensExtrapolated; @@ -51,12 +52,12 @@ namespace PetriEngine { void extrapolate(Marking *marking, Condition *query) override; protected: - const std::vector & find_visible_places(const Condition *query); + const std::vector & findVisiblePlaces(Condition *query); bool _initialized = false; PetriEngine::PetriNet const *_net; - std::vector _inQuery; std::vector _upperBounds; + std::vector> _producers; std::unordered_map> _cache; }; diff --git a/src/CTL/CTLEngine.cpp b/src/CTL/CTLEngine.cpp index 9c36b86fa..3920d83fa 100644 --- a/src/CTL/CTLEngine.cpp +++ b/src/CTL/CTLEngine.cpp @@ -71,8 +71,8 @@ bool CTLSingleSolve(Condition* query, PetriNet* net, result.processedNegationEdges += alg->processedNegationEdges(); result.exploredConfigurations += alg->exploredConfigurations(); result.numberOfEdges += alg->numberOfEdges(); - result.maxTokens = std::max(graph.maxTokens(), result.maxTokens); result.tokensExtrapolated = graph.tokensExtrapolated(); + result.maxTokens = std::max(graph.maxTokens(), result.maxTokens); return res; } diff --git a/src/CTL/CTLResult.cpp b/src/CTL/CTLResult.cpp index 8b16acc47..fff65c6c9 100644 --- a/src/CTL/CTLResult.cpp +++ b/src/CTL/CTLResult.cpp @@ -28,8 +28,8 @@ void CTLResult::print(const std::string& qname, StatisticsLevel statisticslevel, out << " Processed Edges : " << processedEdges << "\n"; out << " Processed N. Edges : " << processedNegationEdges << "\n"; out << " Explored Configs : " << exploredConfigurations << "\n"; + out << " Tokens Extrapolated : " << tokensExtrapolated << "\n"; out << " max tokens: : " << maxTokens << "\n"; // kept lower case to be compatible with reachability format - out << " Tokens Extrapolated : " << tokensExtrapolated << "\n"; } out << std::endl; } \ No newline at end of file diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index fbca6f69d..2a7bbd111 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -1,9 +1,28 @@ #include "PetriEngine/Extrapolator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" -std::vector PetriEngine::Extrapolator::find_upper_bounds(const PetriEngine::PetriNet *net) { +std::vector> PetriEngine::Extrapolator::findProducers(const PetriEngine::PetriNet *net) { + // The PetriNet data structure does not allow us to find producers efficiently. + // We (re)construct that information here since we will need it a lot for extrapolation. + + std::vector> producers(net->_nplaces); + + for (uint32_t i = 0; i < net->_ntransitions; ++i) { + uint32_t finv = net->_transitions[i].outputs; + uint32_t linv = net->_transitions[i+1].inputs; + + for ( ; finv < linv; ++finv) { + const Invariant& inv = net->_invariants[finv]; + producers[inv.place].push_back(i); + } + } + + return producers; +} + +std::vector PetriEngine::Extrapolator::findUpperBounds(const PetriEngine::PetriNet *net) { std::vector bounds(net->_nplaces); - for (int i; i < net->_ntransitions; ++i) { + for (uint32_t i = 0; i < net->_ntransitions; ++i) { uint32_t finv = net->_transitions[i].inputs; uint32_t linv = net->_transitions[i].outputs; @@ -21,18 +40,16 @@ std::vector PetriEngine::Extrapolator::find_upper_bounds(const PetriEn void PetriEngine::SimpleExtrapolator::init(const PetriEngine::PetriNet *net, const Condition *query) { _initialized = true; _net = net; - PetriEngine::PQL::PlaceUseVisitor puv(net->numberOfPlaces()); - PetriEngine::PQL::Visitor::visit(&puv, query); - _inQuery = puv.in_use(); - _upperBounds = find_upper_bounds(net); + _upperBounds = findUpperBounds(net); + _producers = findProducers(net); _cache.clear(); } void PetriEngine::SimpleExtrapolator::extrapolate(Marking *marking, Condition *query) { assert(_initialized); - const auto visible = find_visible_places(query); + const auto visible = findVisiblePlaces(query); - for (int i = 0; i < _net->_nplaces; ++i) { + for (uint32_t i = 0; i < _net->_nplaces; ++i) { if (!visible[i]) { // Extrapolating below the upper bound may introduce behaviour uint32_t cur = marking->marking()[i]; @@ -43,20 +60,24 @@ void PetriEngine::SimpleExtrapolator::extrapolate(Marking *marking, Condition *q } } -const std::vector& PetriEngine::SimpleExtrapolator::find_visible_places(const Condition *query) { +const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Condition *query) { auto it = _cache.find(query); if (it != _cache.end()) { return it->second; } + PetriEngine::PQL::PlaceUseVisitor puv(_net->numberOfPlaces()); + PetriEngine::PQL::Visitor::visit(&puv, query); + auto& inQuery = puv.in_use(); + 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; - for (int i = 0; i < _net->_nplaces; ++i) { - if (_inQuery[i]) { - vis_inc[i] = _inQuery[i]; - vis_dec[i] = _inQuery[i]; + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if (inQuery[i]) { + vis_inc[i] = inQuery[i]; + vis_dec[i] = inQuery[i]; queue.push_back(i); } } @@ -65,39 +86,20 @@ const std::vector& PetriEngine::SimpleExtrapolator::find_visible_places(co uint32_t p = queue.back(); queue.pop_back(); - uint32_t t = _net->_placeToPtrs[p]; - uint32_t tLast = _net->_placeToPtrs[p + 1]; - - for (; t < tLast; ++t) { + if (vis_dec[p]) { + uint32_t t = _net->_placeToPtrs[p]; + uint32_t lastt = _net->_placeToPtrs[p + 1]; - // Is transition consumer and/or producer? - bool isConsumer = false; - uint32_t finv = _net->_transitions[t].inputs; - uint32_t linv = _net->_transitions[t].outputs; - for ( ; finv < linv; ++finv) { - if (_net->_invariants[finv].place == p && !_net->_invariants[finv].inhibitor) { - isConsumer = true; - break; - } - } - bool isProducer = false; - finv = _net->_transitions[t].outputs; - linv = _net->_transitions[t + 1].inputs; - for ( ; finv < linv; ++finv) { - if (_net->_invariants[finv].place == p && !_net->_invariants[finv].inhibitor) { - isProducer = true; - break; - } - } - - if (vis_inc[p] && isProducer) { - // Put preset of preset in vis_inc, - // and inhibiting preset of preset in vis_dec - const TransPtr &ptr = _net->_transitions[t]; - finv = ptr.inputs; - linv = ptr.outputs; + for (; t < lastt; ++t) { + // Put preset of postset in vis_inc, + // and inhibiting preset of postset in vis_dec + uint32_t finv = _net->_transitions[t].inputs; + uint32_t linv = _net->_transitions[t].outputs; for ( ; finv < linv; ++finv) { const Invariant& inv = _net->_invariants[finv]; + if (inv.place == p) { + continue; + } if (inv.inhibitor) { if (!vis_dec[inv.place]) { queue.push_back(inv.place); @@ -108,15 +110,22 @@ const std::vector& PetriEngine::SimpleExtrapolator::find_visible_places(co queue.push_back(inv.place); vis_inc[inv.place] = true; } + if (inv.tokens > 1) { + // This consumer may need more tokens to fire, so increases are also visible + vis_inc[p] = true; + } } } } + } - if (vis_dec[p] && isConsumer) { - // Put preset of postset in vis_inc, - // and inhibiting preset of postset in vis_dec - finv = _net->_transitions[t].outputs; - linv = _net->_transitions[t + 1].inputs; + if (vis_inc[p]) { + // Put preset of preset in vis_inc, + // and inhibiting preset of preset in vis_dec + for (uint32_t t = 0; t < _producers[p].size(); ++t) { + const TransPtr &ptr = _net->_transitions[_producers[p][t]]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; for ( ; finv < linv; ++finv) { const Invariant& inv = _net->_invariants[finv]; if (inv.inhibitor) { @@ -136,9 +145,18 @@ const std::vector& PetriEngine::SimpleExtrapolator::find_visible_places(co } std::vector visible(_net->_nplaces); - for (int i = 0; i < _net->_nplaces; ++i) { + for (uint32_t i = 0; i < _net->_nplaces; ++i) { visible[i] = vis_inc[i] || vis_dec[i]; } + + std::stringstream ss; + query->toString(ss); + std::cout << "Visible places : "; + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + std::cout << *_net->placeNames()[i] << "#" << inQuery[i] << vis_inc[i] << vis_dec[i] << " "; + } + std::cout << ": " << ss.str() << "\n"; + _cache.insert(std::make_pair(query, visible)); return _cache.at(query); } From b6f1b5fe6bd0cf3b0f21f11b768ab5f4958a4eed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 8 Nov 2023 14:45:17 +0100 Subject: [PATCH 05/29] Fixed missing consumer handling --- include/PetriEngine/Extrapolator.h | 7 +++-- src/PetriEngine/Extrapolator.cpp | 42 ++++++++++++++++++------------ 2 files changed, 30 insertions(+), 19 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index ae7a71554..c14357442 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -19,8 +19,10 @@ namespace PetriEngine { virtual void extrapolate(Marking *marking, Condition *query) = 0; - std::vector findUpperBounds(const PetriEngine::PetriNet *net); - std::vector> findProducers(const PetriEngine::PetriNet *net); + static std::vector findUpperBounds(const PetriEngine::PetriNet *net); + + static std::pair>, std::vector>> + findProducersAndConsumers(const PetriEngine::PetriNet *net); size_t tokensExtrapolated() const { return _tokensExtrapolated; @@ -58,6 +60,7 @@ namespace PetriEngine { PetriEngine::PetriNet const *_net; std::vector _upperBounds; std::vector> _producers; + std::vector> _consumers; std::unordered_map> _cache; }; diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 2a7bbd111..ef7857ad4 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -1,23 +1,31 @@ #include "PetriEngine/Extrapolator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" -std::vector> PetriEngine::Extrapolator::findProducers(const PetriEngine::PetriNet *net) { +std::pair>, std::vector>> +PetriEngine::Extrapolator::findProducersAndConsumers(const PetriEngine::PetriNet *net) { // The PetriNet data structure does not allow us to find producers efficiently. // We (re)construct that information here since we will need it a lot for extrapolation. std::vector> producers(net->_nplaces); + std::vector> consumers(net->_nplaces); for (uint32_t i = 0; i < net->_ntransitions; ++i) { - uint32_t finv = net->_transitions[i].outputs; - uint32_t linv = net->_transitions[i+1].inputs; + uint32_t a = net->_transitions[i].inputs; + uint32_t outs = net->_transitions[i].outputs; + uint32_t last = net->_transitions[i + 1].inputs; - for ( ; finv < linv; ++finv) { - const Invariant& inv = net->_invariants[finv]; + for ( ; a < outs; ++a) { + const Invariant& inv = net->_invariants[a]; + consumers[inv.place].push_back(i); + } + + for ( ; a < last; ++a) { + const Invariant& inv = net->_invariants[a]; producers[inv.place].push_back(i); } } - return producers; + return { producers, consumers }; } std::vector PetriEngine::Extrapolator::findUpperBounds(const PetriEngine::PetriNet *net) { @@ -41,7 +49,9 @@ void PetriEngine::SimpleExtrapolator::init(const PetriEngine::PetriNet *net, con _initialized = true; _net = net; _upperBounds = findUpperBounds(net); - _producers = findProducers(net); + auto [prod, con] = findProducersAndConsumers(net); + _producers = prod; + _consumers = con; _cache.clear(); } @@ -87,14 +97,12 @@ const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Cond queue.pop_back(); if (vis_dec[p]) { - uint32_t t = _net->_placeToPtrs[p]; - uint32_t lastt = _net->_placeToPtrs[p + 1]; - - for (; t < lastt; ++t) { - // Put preset of postset in vis_inc, - // and inhibiting preset of postset in vis_dec - uint32_t finv = _net->_transitions[t].inputs; - uint32_t linv = _net->_transitions[t].outputs; + // Put preset of postset in vis_inc, + // and inhibiting preset of postset in vis_dec + for (auto t : _consumers[p]) { + const TransPtr &ptr = _net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; for ( ; finv < linv; ++finv) { const Invariant& inv = _net->_invariants[finv]; if (inv.place == p) { @@ -122,8 +130,8 @@ const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Cond if (vis_inc[p]) { // Put preset of preset in vis_inc, // and inhibiting preset of preset in vis_dec - for (uint32_t t = 0; t < _producers[p].size(); ++t) { - const TransPtr &ptr = _net->_transitions[_producers[p][t]]; + for (auto t : _producers[p]) { + const TransPtr &ptr = _net->_transitions[t]; uint32_t finv = ptr.inputs; uint32_t linv = ptr.outputs; for ( ; finv < linv; ++finv) { From beceeb788d0056c064c3cf90fc8f33d4d987bb21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 13 Nov 2023 15:57:54 +0100 Subject: [PATCH 06/29] Refactor Extrapolator and use in Reachability. --- include/PetriEngine/Extrapolator.h | 75 ++++++++++++------- include/PetriEngine/PetriNet.h | 6 +- .../Reachability/ReachabilitySearch.h | 10 +++ src/CTL/PetriNets/OnTheFlyDG.cpp | 2 +- src/PetriEngine/Extrapolator.cpp | 73 +++++++++--------- 5 files changed, 103 insertions(+), 63 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index c14357442..1a75d50ff 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -2,6 +2,8 @@ #define VERIFYPN_EXTRAPOLATOR_H +#include + #include "PetriEngine/Structures/State.h" #include "PetriEngine/PQL/PQL.h" #include "CTL/PetriNets/PetriConfig.h" @@ -11,69 +13,92 @@ namespace PetriEngine { using Condition_ptr = PQL::Condition_ptr; using Marking = Structures::State; + struct ExtrapolationContext { + PetriNet const *net; + std::vector upperBounds; + std::vector> producers; + std::vector> consumers; + + explicit ExtrapolationContext(const PetriNet *net); + + private: + static std::pair>, std::vector>> + findProducersAndConsumers(const PetriNet *net); + + static std::vector findUpperBounds(const PetriNet *net); + }; + + using ExtrapolationContext_cptr = std::shared_ptr; + class Extrapolator { public: virtual ~Extrapolator() = default; - virtual void init(const PetriEngine::PetriNet *net, const Condition *query) = 0; - - virtual void extrapolate(Marking *marking, Condition *query) = 0; + virtual void init(const PetriNet *net, const Condition *query) { + if (!_ctx) { + _ctx = std::make_shared(net); + } + }; - static std::vector findUpperBounds(const PetriEngine::PetriNet *net); + virtual void initWithCtx(const ExtrapolationContext_cptr &ctx, const Condition *query) { + _ctx = ctx; + init(_ctx->net, query); + } - static std::pair>, std::vector>> - findProducersAndConsumers(const PetriEngine::PetriNet *net); + virtual void extrapolate(Marking *marking, Condition *query) = 0; - size_t tokensExtrapolated() const { + [[nodiscard]] virtual size_t tokensExtrapolated() const { return _tokensExtrapolated; } protected: + ExtrapolationContext_cptr _ctx; size_t _tokensExtrapolated = 0; }; class NoExtrapolator : public Extrapolator { public: - void init(const PetriEngine::PetriNet *net, const Condition *query) override { - // no-op - }; - void extrapolate(Marking *marking, Condition *query) override { // no-op }; }; /** - * The SimpleExtrapolator removes tokens in places that are not visible for the query, - * neither directly or indirectly. + * The SimpleReachExtrapolator removes tokens in places that are not visible for the query, + * neither directly or indirectly. The SimpleReachExtrapolator preserves reachability/safety properties. */ - class SimpleExtrapolator : public Extrapolator { + class SimpleReachExtrapolator : public Extrapolator { public: - void init(const PetriEngine::PetriNet *net, const Condition *query) override; - void extrapolate(Marking *marking, Condition *query) override; protected: - const std::vector & findVisiblePlaces(Condition *query); + const std::vector &findVisiblePlaces(Condition *query); - bool _initialized = false; - PetriEngine::PetriNet const *_net; - std::vector _upperBounds; - std::vector> _producers; - std::vector> _consumers; std::unordered_map> _cache; }; /** - * The SmartExtrapolator removes tokens in places that are *effectively* not visible for the query, + * The SmartReachExtrapolator removes tokens in places that are *effectively* not visible for the query, * neither directly or indirectly, by considering the current marking and * which places can never gain or lose tokens. + * The SimpleReachExtrapolator preserves reachability/safety properties. */ - class SmartExtrapolator : public Extrapolator { + class SmartReachExtrapolator : public Extrapolator { + public: + void extrapolate(Marking *marking, Condition *query) override; + }; + + class AdaptiveExtrapolator : public Extrapolator { public: - void init(const PetriEngine::PetriNet *net, const Condition *query) override; + void init(const PetriNet *net, const Condition *query) override; void extrapolate(Marking *marking, Condition *query) override; + + size_t tokensExtrapolated() const override; + + protected: + CTLExtrapolator _ctl; + SimpleReachExtrapolator _simple; }; } diff --git a/include/PetriEngine/PetriNet.h b/include/PetriEngine/PetriNet.h index 91048bba6..41cb97a9d 100644 --- a/include/PetriEngine/PetriNet.h +++ b/include/PetriEngine/PetriNet.h @@ -150,9 +150,11 @@ namespace PetriEngine { friend class ReducingSuccessorGenerator; friend class STSolver; friend class StubbornSet; + friend struct ExtrapolationContext; friend class Extrapolator; - friend class SimpleExtrapolator; - friend class SmartExtrapolator; + friend class AdaptiveExtrapolator; + friend class SimpleReachExtrapolator; + friend class SmartReachExtrapolator; }; } // PetriEngine diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index a9102c20b..6539d3b49 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/Extrapolator.h" #include #include @@ -180,6 +181,14 @@ namespace PetriEngine { queue.push(r.second, &dc, queries[ss.heurquery].get()); } + Extrapolator* extrapolator; + if (queries.size() == 1 && usequeries) { + extrapolator = new SimpleReachExtrapolator(); + extrapolator->init(&_net, queries[0].get()); + } else { + extrapolator = new NoExtrapolator(); + } + // Search! for(auto nid = queue.pop(); nid != Structures::Queue::EMPTY; nid = queue.pop()) { states.decode(state, nid); @@ -187,6 +196,7 @@ namespace PetriEngine { while(generator.next(working)){ ss.enabledTransitionsCount[generator.fired()]++; + extrapolator->extrapolate(&working, queries[ss.heurquery].get()); auto res = states.add(working); // If we have not seen this state before if (res.first) { diff --git a/src/CTL/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index 8d29aafd6..b50eb9403 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -26,7 +26,7 @@ OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encod net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); - extrapolator = new PetriEngine::SimpleExtrapolator(); + extrapolator = new PetriEngine::NoExtrapolator(); } diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index ef7857ad4..5806a8a0a 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -1,9 +1,15 @@ #include "PetriEngine/Extrapolator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" +#include "PetriEngine/PQL/PredicateCheckers.h" + +PetriEngine::ExtrapolationContext::ExtrapolationContext(const PetriEngine::PetriNet *net) : net(net) { + std::tie(producers, consumers) = findProducersAndConsumers(net); + upperBounds = findUpperBounds(net); +} std::pair>, std::vector>> -PetriEngine::Extrapolator::findProducersAndConsumers(const PetriEngine::PetriNet *net) { - // The PetriNet data structure does not allow us to find producers efficiently. +PetriEngine::ExtrapolationContext::findProducersAndConsumers(const PetriEngine::PetriNet *net) { + // The PetriNet data structure does not allow us to go from a place to its producers and consumers. // We (re)construct that information here since we will need it a lot for extrapolation. std::vector> producers(net->_nplaces); @@ -28,7 +34,7 @@ PetriEngine::Extrapolator::findProducersAndConsumers(const PetriEngine::PetriNet return { producers, consumers }; } -std::vector PetriEngine::Extrapolator::findUpperBounds(const PetriEngine::PetriNet *net) { +std::vector PetriEngine::ExtrapolationContext::findUpperBounds(const PetriEngine::PetriNet *net) { std::vector bounds(net->_nplaces); for (uint32_t i = 0; i < net->_ntransitions; ++i) { uint32_t finv = net->_transitions[i].inputs; @@ -45,46 +51,35 @@ std::vector PetriEngine::Extrapolator::findUpperBounds(const PetriEngi return bounds; } -void PetriEngine::SimpleExtrapolator::init(const PetriEngine::PetriNet *net, const Condition *query) { - _initialized = true; - _net = net; - _upperBounds = findUpperBounds(net); - auto [prod, con] = findProducersAndConsumers(net); - _producers = prod; - _consumers = con; - _cache.clear(); -} - -void PetriEngine::SimpleExtrapolator::extrapolate(Marking *marking, Condition *query) { - assert(_initialized); +void PetriEngine::SimpleReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { const auto visible = findVisiblePlaces(query); - for (uint32_t i = 0; i < _net->_nplaces; ++i) { + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { if (!visible[i]) { // Extrapolating below the upper bound may introduce behaviour uint32_t cur = marking->marking()[i]; - uint32_t ex = std::min(cur, _upperBounds[i]); + uint32_t ex = std::min(cur, _ctx->upperBounds[i]); _tokensExtrapolated += cur - ex; marking->marking()[i] = ex; } } } -const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Condition *query) { +const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces(PetriEngine::Condition *query) { auto it = _cache.find(query); if (it != _cache.end()) { return it->second; } - PetriEngine::PQL::PlaceUseVisitor puv(_net->numberOfPlaces()); + PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); PetriEngine::PQL::Visitor::visit(&puv, query); auto& inQuery = puv.in_use(); - 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 vis_inc(_ctx->net->_nplaces); // Places where token increment is visible to query + std::vector vis_dec(_ctx->net->_nplaces); // Places where token decrement is visible to query std::vector queue; - for (uint32_t i = 0; i < _net->_nplaces; ++i) { + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { if (inQuery[i]) { vis_inc[i] = inQuery[i]; vis_dec[i] = inQuery[i]; @@ -99,12 +94,12 @@ const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Cond if (vis_dec[p]) { // Put preset of postset in vis_inc, // and inhibiting preset of postset in vis_dec - for (auto t : _consumers[p]) { - const TransPtr &ptr = _net->_transitions[t]; + for (auto t : _ctx->consumers[p]) { + const TransPtr &ptr = _ctx->net->_transitions[t]; uint32_t finv = ptr.inputs; uint32_t linv = ptr.outputs; for ( ; finv < linv; ++finv) { - const Invariant& inv = _net->_invariants[finv]; + const Invariant& inv = _ctx->net->_invariants[finv]; if (inv.place == p) { continue; } @@ -130,12 +125,12 @@ const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Cond if (vis_inc[p]) { // Put preset of preset in vis_inc, // and inhibiting preset of preset in vis_dec - for (auto t : _producers[p]) { - const TransPtr &ptr = _net->_transitions[t]; + for (auto t : _ctx->producers[p]) { + const TransPtr &ptr = _ctx->net->_transitions[t]; uint32_t finv = ptr.inputs; uint32_t linv = ptr.outputs; for ( ; finv < linv; ++finv) { - const Invariant& inv = _net->_invariants[finv]; + const Invariant& inv = _ctx->net->_invariants[finv]; if (inv.inhibitor) { if (!vis_dec[inv.place]) { queue.push_back(inv.place); @@ -152,16 +147,16 @@ const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Cond } } - std::vector visible(_net->_nplaces); - for (uint32_t i = 0; i < _net->_nplaces; ++i) { + std::vector visible(_ctx->net->_nplaces); + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { visible[i] = vis_inc[i] || vis_dec[i]; } std::stringstream ss; query->toString(ss); std::cout << "Visible places : "; - for (uint32_t i = 0; i < _net->_nplaces; ++i) { - std::cout << *_net->placeNames()[i] << "#" << inQuery[i] << vis_inc[i] << vis_dec[i] << " "; + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << vis_inc[i] << vis_dec[i] << " "; } std::cout << ": " << ss.str() << "\n"; @@ -169,10 +164,18 @@ const std::vector& PetriEngine::SimpleExtrapolator::findVisiblePlaces(Cond return _cache.at(query); } -void PetriEngine::SmartExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { - // TODO +void PetriEngine::AdaptiveExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { + if (!_ctx) { + _ctx = std::make_shared(net); + } + _simple.initWithCtx(_ctx, query); + //_ctl.initWithCtx(_ctx, query); } -void PetriEngine::SmartExtrapolator::extrapolate(Marking *marking, Condition *query) { +void PetriEngine::AdaptiveExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { // TODO } + +size_t PetriEngine::AdaptiveExtrapolator::tokensExtrapolated() const { + return _simple.tokensExtrapolated(); //+ _ctl.tokensExtrapolated(); TODO +} From eea8f7a30f58f6f8febac237b0d1364ca86271f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 29 Nov 2023 09:40:29 +0100 Subject: [PATCH 07/29] Do not use SimpleExtrapolation on loop sensitive queries --- include/PetriEngine/Extrapolator.h | 2 +- .../Reachability/ReachabilitySearch.h | 2 +- src/CTL/PetriNets/OnTheFlyDG.cpp | 4 +-- src/PetriEngine/Extrapolator.cpp | 33 ++++++++++++------- .../Reachability/ReachabilitySearch.cpp | 1 + 5 files changed, 26 insertions(+), 16 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 1a75d50ff..02b60a9bc 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -97,7 +97,7 @@ namespace PetriEngine { size_t tokensExtrapolated() const override; protected: - CTLExtrapolator _ctl; + //CTLExtrapolator _ctl; SimpleReachExtrapolator _simple; }; } diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index 6539d3b49..db7d6faec 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -114,6 +114,7 @@ namespace PetriEngine { size_t _satisfyingMarking = 0; Structures::State _initial; AbstractHandler& _callback; + Extrapolator* extrapolator = nullptr; // FIXME: Leaked size_t _max_tokens = 0; }; @@ -181,7 +182,6 @@ namespace PetriEngine { queue.push(r.second, &dc, queries[ss.heurquery].get()); } - Extrapolator* extrapolator; if (queries.size() == 1 && usequeries) { extrapolator = new SimpleReachExtrapolator(); extrapolator->init(&_net, queries[0].get()); diff --git a/src/CTL/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index b50eb9403..2b5be3256 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -26,7 +26,7 @@ OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encod net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); - extrapolator = new PetriEngine::NoExtrapolator(); + extrapolator = new PetriEngine::AdaptiveExtrapolator(); } @@ -71,7 +71,7 @@ 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){ diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 5806a8a0a..552209edd 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -52,23 +52,32 @@ std::vector PetriEngine::ExtrapolationContext::findUpperBounds(const P } void PetriEngine::SimpleReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { - const auto visible = findVisiblePlaces(query); + const std::vector *visible; + auto it = _cache.find(query); + if (it != _cache.end()) { + visible = &it->second; + } else { + visible = &findVisiblePlaces(query); + } - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (!visible[i]) { - // Extrapolating below the upper bound may introduce behaviour - uint32_t cur = marking->marking()[i]; - uint32_t ex = std::min(cur, _ctx->upperBounds[i]); - _tokensExtrapolated += cur - ex; - marking->marking()[i] = ex; + if (!visible->empty()) { + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + if (!(*visible)[i]) { + // Extrapolating below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _ctx->upperBounds[i]); + _tokensExtrapolated += cur - ex; + marking->marking()[i] = ex; + } } } } const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces(PetriEngine::Condition *query) { - auto it = _cache.find(query); - if (it != _cache.end()) { - return it->second; + + if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { + _cache.insert(std::make_pair(query, std::vector())); + return _cache.at(query); } PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); @@ -173,7 +182,7 @@ void PetriEngine::AdaptiveExtrapolator::init(const PetriEngine::PetriNet *net, c } void PetriEngine::AdaptiveExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { - // TODO + _simple.extrapolate(marking, query); } size_t PetriEngine::AdaptiveExtrapolator::tokensExtrapolated() const { diff --git a/src/PetriEngine/Reachability/ReachabilitySearch.cpp b/src/PetriEngine/Reachability/ReachabilitySearch.cpp index 796d40b50..379004b40 100644 --- a/src/PetriEngine/Reachability/ReachabilitySearch.cpp +++ b/src/PetriEngine/Reachability/ReachabilitySearch.cpp @@ -95,6 +95,7 @@ namespace PetriEngine { << "\tdiscovered states: " << states->discovered() << std::endl << "\texplored states: " << ss.exploredStates << std::endl << "\texpanded states: " << ss.expandedStates << std::endl + << "\tTokens Extrapolated: " << extrapolator->tokensExtrapolated() << std::endl << "\tmax tokens: " << states->maxTokens() << std::endl; if (statisticsLevel != StatisticsLevel::Full) From 4675a651647dbbcb3c52daefd0d36206273c50f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 1 Dec 2023 09:34:17 +0100 Subject: [PATCH 08/29] Fix bug where extrapolated marking was used in multiple queries --- include/CTL/PetriNets/OnTheFlyDG.h | 5 ++-- src/CTL/Algorithm/CertainZeroFPA.cpp | 5 +++- src/CTL/PetriNets/OnTheFlyDG.cpp | 36 ++++++++++++++++++++++++---- src/PetriEngine/Extrapolator.cpp | 4 +++- 4 files changed, 41 insertions(+), 9 deletions(-) diff --git a/include/CTL/PetriNets/OnTheFlyDG.h b/include/CTL/PetriNets/OnTheFlyDG.h index 6474ecdd5..7d5263355 100644 --- a/include/CTL/PetriNets/OnTheFlyDG.h +++ b/include/CTL/PetriNets/OnTheFlyDG.h @@ -58,6 +58,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph PetriConfig* initial_config; Marking working_marking; Marking query_marking; + Marking extrapolated_marking; Extrapolator* extrapolator = nullptr; uint32_t n_transitions = 0; uint32_t n_places = 0; @@ -93,8 +94,8 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph } } } - PetriConfig *createConfiguration(Marking& marking, size_t own, Condition* query); - PetriConfig *createConfiguration(Marking& 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/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/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index 2b5be3256..c43a33e6c 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -519,8 +519,9 @@ 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()); + extrapolated_marking.setMarking(net->makeInitialMarking()); auto o = owner(working_marking, this->query); initial_config = createConfiguration(working_marking, o, this->query); } @@ -552,6 +553,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); @@ -566,8 +589,10 @@ void OnTheFlyDG::setQuery(Condition* query) this->query = query; delete[] working_marking.marking(); delete[] query_marking.marking(); + delete[] extrapolated_marking.marking(); working_marking.setMarking(nullptr); query_marking.setMarking(nullptr); + extrapolated_marking.setMarking(nullptr); extrapolator->init(net, query); initialConfiguration(); assert(this->query); @@ -591,11 +616,12 @@ size_t OnTheFlyDG::tokensExtrapolated() const { return extrapolator->tokensExtrapolated(); } -PetriConfig *OnTheFlyDG::createConfiguration(Marking& marking, size_t own, Condition* t_query) +PetriConfig *OnTheFlyDG::createConfiguration(const Marking& marking, size_t own, Condition* t_query) { - extrapolator->extrapolate(&marking, t_query); + extrapolated_marking.copy(marking.marking(), n_places); + extrapolator->extrapolate(&extrapolated_marking, t_query); - size_t encoded = createMarking(marking); + size_t encoded = createMarking(extrapolated_marking); auto& configs = trie.get_data(encoded); for(PetriConfig* c : configs){ if(c->query == t_query) diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 552209edd..92e0db744 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -165,7 +165,9 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces query->toString(ss); std::cout << "Visible places : "; for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << vis_inc[i] << vis_dec[i] << " "; + if (inQuery[i] || vis_inc[i] || vis_dec[i]) { + std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << vis_inc[i] << vis_dec[i] << " "; + } } std::cout << ": " << ss.str() << "\n"; From a1a181804a827a034fa528f190a1df490009f5d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 6 Dec 2023 09:01:22 +0100 Subject: [PATCH 09/29] Add DynamicReachExtrapolator --- include/PetriEngine/Extrapolator.h | 20 +- include/PetriEngine/PetriNet.h | 2 +- .../Reachability/ReachabilitySearch.h | 2 +- src/PetriEngine/Extrapolator.cpp | 247 +++++++++++++++++- 4 files changed, 260 insertions(+), 11 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 02b60a9bc..a4f05095c 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -78,14 +78,26 @@ namespace PetriEngine { }; /** - * The SmartReachExtrapolator removes tokens in places that are *effectively* not visible for the query, + * The DynamicReachExtrapolator removes tokens in places that are *effectively* not visible for the query, * neither directly or indirectly, by considering the current marking and * which places can never gain or lose tokens. - * The SimpleReachExtrapolator preserves reachability/safety properties. + * The DynamicReachExtrapolator preserves reachability/safety properties. */ - class SmartReachExtrapolator : public Extrapolator { + class DynamicReachExtrapolator : public Extrapolator { public: void extrapolate(Marking *marking, Condition *query) override; + + protected: + const uint8_t VIS_INC = 0b0001; + const uint8_t VIS_DEC = 0b0010; + const uint8_t CAN_INC = 0b0100; + const uint8_t CAN_DEC = 0b1000; + + std::vector _pflags; + std::vector _fireable; + + void findDeadPlacesAndTransitions(const Marking *marking); + void findVisiblePlaces(Condition *query); }; class AdaptiveExtrapolator : public Extrapolator { @@ -98,7 +110,7 @@ namespace PetriEngine { protected: //CTLExtrapolator _ctl; - SimpleReachExtrapolator _simple; + DynamicReachExtrapolator _simple; }; } diff --git a/include/PetriEngine/PetriNet.h b/include/PetriEngine/PetriNet.h index 41cb97a9d..1ed3aee14 100644 --- a/include/PetriEngine/PetriNet.h +++ b/include/PetriEngine/PetriNet.h @@ -154,7 +154,7 @@ namespace PetriEngine { friend class Extrapolator; friend class AdaptiveExtrapolator; friend class SimpleReachExtrapolator; - friend class SmartReachExtrapolator; + friend class DynamicReachExtrapolator; }; } // PetriEngine diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index db7d6faec..863643401 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -183,7 +183,7 @@ namespace PetriEngine { } if (queries.size() == 1 && usequeries) { - extrapolator = new SimpleReachExtrapolator(); + extrapolator = new DynamicReachExtrapolator(); extrapolator->init(&_net, queries[0].get()); } else { extrapolator = new NoExtrapolator(); diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 92e0db744..ad9c5b07c 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -1,3 +1,4 @@ +#include #include "PetriEngine/Extrapolator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" #include "PetriEngine/PQL/PredicateCheckers.h" @@ -88,11 +89,11 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces std::vector vis_dec(_ctx->net->_nplaces); // Places where token decrement is visible to query std::vector queue; - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (inQuery[i]) { - vis_inc[i] = inQuery[i]; - vis_dec[i] = inQuery[i]; - queue.push_back(i); + for (uint32_t p = 0; p < _ctx->net->_nplaces; ++p) { + if (inQuery[p]) { + vis_inc[p] = inQuery[p]; + vis_dec[p] = inQuery[p]; + queue.push_back(p); } } @@ -175,6 +176,242 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces return _cache.at(query); } +void PetriEngine::DynamicReachExtrapolator::findDeadPlacesAndTransitions(const PetriEngine::Marking *marking) { + + _pflags.resize(_ctx->net->_nplaces); + std::fill(_pflags.begin(), _pflags.end(), 0); + _fireable.resize(_ctx->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 (uint32_t t : _ctx->consumers[p]) { + if (!_fireable[t]) + queue.push(t); + } + } + }; + + auto processDecPlace = [&](uint32_t p) { + if ((_pflags[p] & CAN_DEC) == 0) { + _pflags[p] |= CAN_DEC; + for (uint32_t t : _ctx->consumers[p]) { + if (!_fireable[t]) + queue.push(t); + } + } + }; + + auto processEnabled = [&](uint32_t t) { + _fireable[t] = true; + // Find and process negative preset and positive postset + uint32_t i = _ctx->net->_transitions[t].inputs; + uint32_t fout = _ctx->net->_transitions[t].outputs; + uint32_t j = fout; + uint32_t end = _ctx->net->_transitions[t+1].inputs; + while (i < fout && j < end) + { + const Invariant& preinv = _ctx->net->_invariants[i]; + const Invariant& postinv = _ctx->net->_invariants[j]; + + if (preinv.place < postinv.place) { + if (!preinv.inhibitor) + processDecPlace(preinv.place); + i++; + } else if (preinv.place > postinv.place) { + processIncPlace(postinv.place); + j++; + } else { + if (preinv.inhibitor) { + processIncPlace(postinv.place); + } else { + // There are both an in and an out arc to this place. Is the effect non-zero? + if (preinv.tokens > postinv.tokens) { + processDecPlace(preinv.place); + } else if (preinv.tokens < postinv.tokens) { + processIncPlace(postinv.place); + } + } + + i++; j++; + } + } + for ( ; i < fout; i++) { + const Invariant& preinv = _ctx->net->_invariants[i]; + if (!preinv.inhibitor) + processDecPlace(preinv.place); + } + for ( ; j < end; j++) { + processIncPlace(_ctx->net->_invariants[j].place); + } + }; + + // Process initially enabled transitions + for (uint32_t t = 0; t < _ctx->net->_ntransitions; ++t) { + uint32_t i = _ctx->net->_transitions[t].inputs; + uint32_t fout = _ctx->net->_transitions[t].outputs; + bool enabled = true; + for ( ; i < fout; i++) { + const Invariant& preinv = _ctx->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 = _ctx->net->_transitions[t].inputs; + uint32_t linv = _ctx->net->_transitions[t].outputs; + for (; finv < linv; ++finv) { + const Invariant& arc = _ctx->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 PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condition *query) { + + PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); + PetriEngine::PQL::Visitor::visit(&puv, query); + auto& inQuery = puv.in_use(); + + std::queue queue; + + for (uint32_t p = 0; p < _ctx->net->_nplaces; ++p) { + if (inQuery[p]) { + _pflags[p] |= VIS_INC; + _pflags[p] |= VIS_DEC; + queue.push(p); + } + } + + while (!queue.empty()) { + uint32_t p = queue.front(); + queue.pop(); + + if ((_pflags[p] & VIS_DEC) > 0) { + // Put preset of postset in vis_inc, + // and inhibiting preset of postset in vis_dec + for (auto t : _ctx->consumers[p]) { + if (!_fireable[t]) continue; + const TransPtr &ptr = _ctx->net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _ctx->net->_invariants[finv]; + if (arc.place == p) { + continue; + } + 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; + } + 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; + } + } + } + } + } + + if ((_pflags[p] & VIS_INC) > 0) { + // Put preset of preset in vis_inc, + // and inhibiting preset of preset in vis_dec + for (auto t : _ctx->producers[p]) { + if (!_fireable[t]) continue; + const TransPtr &ptr = _ctx->net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _ctx->net->_invariants[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; + } + } + } + } + } + } + + if (std::getenv("DYN_EXTRAP_DEBUG") != nullptr) { +// for (uint32_t i = 0; i < n_places; i++) +// { +// std::cout << marking[i]; +// } + std::cout << " | Visible: "; + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + if (inQuery[i] || (_pflags[i] & (VIS_INC | VIS_DEC)) > 0) { + std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << ((_pflags[i] & VIS_INC) > 0) + << ((_pflags[i] & VIS_DEC) > 0) << " "; + } + } + std::cout << "| Live: "; + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + if ((_pflags[i] & (CAN_INC | CAN_DEC)) > 0) { + std::cout << *_ctx->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 PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { + findDeadPlacesAndTransitions(marking); + findVisiblePlaces(query); + + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + if ((_pflags[i] & (VIS_INC | VIS_DEC)) == 0) { + // Extrapolating below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _ctx->upperBounds[i]); + _tokensExtrapolated += cur - ex; + marking->marking()[i] = ex; + } + } +} + void PetriEngine::AdaptiveExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { if (!_ctx) { _ctx = std::make_shared(net); From 7e293cc870025bb41724244532c53577691cc5b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 6 Dec 2023 09:23:42 +0100 Subject: [PATCH 10/29] Make DynamicReachExtrapolator restricted to reachability queries --- src/PetriEngine/Extrapolator.cpp | 35 ++++++++++++++++++-------------- 1 file changed, 20 insertions(+), 15 deletions(-) diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index ad9c5b07c..b865df2b3 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -176,6 +176,26 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces return _cache.at(query); } +void PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { + + if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { + return; + } + + findDeadPlacesAndTransitions(marking); + findVisiblePlaces(query); + + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + if ((_pflags[i] & (VIS_INC | VIS_DEC)) == 0) { + // Extrapolating below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _ctx->upperBounds[i]); + _tokensExtrapolated += cur - ex; + marking->marking()[i] = ex; + } + } +} + void PetriEngine::DynamicReachExtrapolator::findDeadPlacesAndTransitions(const PetriEngine::Marking *marking) { _pflags.resize(_ctx->net->_nplaces); @@ -397,21 +417,6 @@ void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condi } } -void PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { - findDeadPlacesAndTransitions(marking); - findVisiblePlaces(query); - - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if ((_pflags[i] & (VIS_INC | VIS_DEC)) == 0) { - // Extrapolating below the upper bound may introduce behaviour - uint32_t cur = marking->marking()[i]; - uint32_t ex = std::min(cur, _ctx->upperBounds[i]); - _tokensExtrapolated += cur - ex; - marking->marking()[i] = ex; - } - } -} - void PetriEngine::AdaptiveExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { if (!_ctx) { _ctx = std::make_shared(net); From 6ee2a54d2039a6b327c5b6600bec273e5c0cea58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 8 Dec 2023 09:30:57 +0100 Subject: [PATCH 11/29] Make DynamicReachExtrapolation preserve weakly visible places --- include/PetriEngine/Extrapolator.h | 9 ++-- src/PetriEngine/Extrapolator.cpp | 78 ++++++++++++++++++++++-------- 2 files changed, 64 insertions(+), 23 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index a4f05095c..c188b2b69 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -88,10 +88,11 @@ namespace PetriEngine { void extrapolate(Marking *marking, Condition *query) override; protected: - const uint8_t VIS_INC = 0b0001; - const uint8_t VIS_DEC = 0b0010; - const uint8_t CAN_INC = 0b0100; - const uint8_t CAN_DEC = 0b1000; + const uint8_t VIS_INC = 0b00001; + const uint8_t VIS_DEC = 0b00010; + const uint8_t MUST_KEEP = 0b00100; + const uint8_t CAN_INC = 0b01000; + const uint8_t CAN_DEC = 0b10000; std::vector _pflags; std::vector _fireable; diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index b865df2b3..cd2b8e39c 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -182,11 +182,17 @@ void PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *ma return; } + std::stringstream before; + for (uint32_t i = 0; i < _ctx->net->_nplaces; i++) + { + before << (*marking)[i]; + } + findDeadPlacesAndTransitions(marking); findVisiblePlaces(query); for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if ((_pflags[i] & (VIS_INC | VIS_DEC)) == 0) { + if ((_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP)) == 0) { // Extrapolating below the upper bound may introduce behaviour uint32_t cur = marking->marking()[i]; uint32_t ex = std::min(cur, _ctx->upperBounds[i]); @@ -194,6 +200,38 @@ void PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *ma marking->marking()[i] = ex; } } + + if (std::getenv("DYN_EXTRAP_DEBUG") != nullptr) { + std::stringstream after; + for (uint32_t i = 0; i < _ctx->net->_nplaces; i++) + { + after << (*marking)[i]; + } + if (before.str() == after.str()) + return; + + PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); + PetriEngine::PQL::Visitor::visit(&puv, query); + auto& inQuery = puv.in_use(); + + std::cout << before.str() << "->" << after.str() << " | Visible: "; + for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { + if (inQuery[i] || (_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP)) > 0) { + std::cout << *_ctx->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 < _ctx->net->_nplaces; ++i) { + if ((_pflags[i] & (CAN_INC | CAN_DEC)) > 0) { + std::cout << *_ctx->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 PetriEngine::DynamicReachExtrapolator::findDeadPlacesAndTransitions(const PetriEngine::Marking *marking) { @@ -392,28 +430,30 @@ void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condi } } - if (std::getenv("DYN_EXTRAP_DEBUG") != nullptr) { -// for (uint32_t i = 0; i < n_places; i++) -// { -// std::cout << marking[i]; -// } - std::cout << " | Visible: "; - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (inQuery[i] || (_pflags[i] & (VIS_INC | VIS_DEC)) > 0) { - std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << ((_pflags[i] & VIS_INC) > 0) - << ((_pflags[i] & VIS_DEC) > 0) << " "; + // We cannot disable fireable transitions affecting visible places, so their preset must be preserved, + // even if their preset is effectively dead. + for (int t = 0; t < _ctx->net->_ntransitions; ++t) { + if (!_fireable[t]) continue; + uint32_t finv = _ctx->net->_transitions[t].inputs; + uint32_t linv = _ctx->net->_transitions[t+1].inputs; + bool affectsVisible = false; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _ctx->net->_invariants[finv]; + if ((_pflags[arc.place] & (VIS_INC | VIS_DEC)) > 0) { + affectsVisible = true; + break; } } - std::cout << "| Live: "; - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if ((_pflags[i] & (CAN_INC | CAN_DEC)) > 0) { - std::cout << *_ctx->net->placeNames()[i] << "#" << ((_pflags[i] & CAN_INC) > 0) - << ((_pflags[i] & CAN_DEC) > 0) << " "; + if (affectsVisible) { + finv = _ctx->net->_transitions[t].inputs; + linv = _ctx->net->_transitions[t].outputs; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _ctx->net->_invariants[finv]; + if (!arc.inhibitor) { + _pflags[arc.place] |= MUST_KEEP; + } } } - std::stringstream ss; - query->toString(ss); - std::cout << "| " << ss.str() << "\n"; } } From 5b1cd47656e938e0a5c5847b04583ea4affe25bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 20 Dec 2023 12:08:20 +0100 Subject: [PATCH 12/29] Consider direction of query in extrapolation --- include/PetriEngine/Extrapolator.h | 20 +-- src/PetriEngine/Extrapolator.cpp | 230 ++++++++++++++++++++++------- 2 files changed, 188 insertions(+), 62 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index c188b2b69..90bd598fe 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -13,6 +13,13 @@ namespace PetriEngine { using Condition_ptr = PQL::Condition_ptr; using Marking = Structures::State; + const static uint8_t IN_Q = 0b000001; + const static uint8_t VIS_INC = 0b000010; + const static uint8_t VIS_DEC = 0b000100; + const static uint8_t MUST_KEEP = 0b001000; + const static uint8_t CAN_INC = 0b010000; + const static uint8_t CAN_DEC = 0b100000; + struct ExtrapolationContext { PetriNet const *net; std::vector upperBounds; @@ -21,11 +28,11 @@ namespace PetriEngine { explicit ExtrapolationContext(const PetriNet *net); - private: - static std::pair>, std::vector>> - findProducersAndConsumers(const PetriNet *net); + [[nodiscard]] int effect(uint32_t t, uint32_t p) const; - static std::vector findUpperBounds(const PetriNet *net); + private: + void setupProducersAndConsumers(); + void setupUpperBounds(); }; using ExtrapolationContext_cptr = std::shared_ptr; @@ -88,11 +95,6 @@ namespace PetriEngine { void extrapolate(Marking *marking, Condition *query) override; protected: - const uint8_t VIS_INC = 0b00001; - const uint8_t VIS_DEC = 0b00010; - const uint8_t MUST_KEEP = 0b00100; - const uint8_t CAN_INC = 0b01000; - const uint8_t CAN_DEC = 0b10000; std::vector _pflags; std::vector _fireable; diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index cd2b8e39c..3469dc686 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -2,19 +2,126 @@ #include "PetriEngine/Extrapolator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" #include "PetriEngine/PQL/PredicateCheckers.h" +namespace PetriEngine { + 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 = VIS_DEC; + Visitor::visit(this, (*element)[0]); + direction = VIS_INC; + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::LessThanOrEqualCondition* element) override { + direction = VIS_DEC; + Visitor::visit(this, (*element)[0]); + direction = VIS_INC; + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::EqualCondition* element) override { + direction = VIS_INC | VIS_DEC; + Visitor::visit(this, (*element)[0]); + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::NotEqualCondition* element) override { + direction = VIS_INC | VIS_DEC; + Visitor::visit(this, (*element)[0]); + Visitor::visit(this, (*element)[1]); + } + void _accept(const PQL::UnfoldedIdentifierExpr* element) override { + _in_use[element->offset()] |= direction | IN_Q; + } + void _accept(const PQL::PlusExpr* element) override { + // TODO: Test this + for(auto& p : element->places()) _in_use[p.first] |= direction | IN_Q; + } + void _accept(const PQL::MultiplyExpr* element) override { + // TODO: Test this. Especially negative values + for(auto& p : element->places()) _in_use[p.first] |= direction | IN_Q; + } + 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 { + // TODO: What even is this? + for(auto& e : *element) _in_use[e._place] |= direction | IN_Q; + } + void _accept(const PQL::UnfoldedUpperBoundsCondition* element) override { + for(auto& p : element->places()) + _in_use[p._place] |= VIS_INC | IN_Q; + } + + 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"); + } + + // Shallow elements, neither of these should exist in a compiled expression + void _accept(const PQL::LiteralExpr* element) override {} + void _accept(const PQL::DeadlockCondition* element) override {} + + private: + std::vector _in_use; + bool negated = false; + uint8_t direction = 0; + }; +} PetriEngine::ExtrapolationContext::ExtrapolationContext(const PetriEngine::PetriNet *net) : net(net) { - std::tie(producers, consumers) = findProducersAndConsumers(net); - upperBounds = findUpperBounds(net); + setupProducersAndConsumers(); + setupUpperBounds(); } -std::pair>, std::vector>> -PetriEngine::ExtrapolationContext::findProducersAndConsumers(const PetriEngine::PetriNet *net) { +void PetriEngine::ExtrapolationContext::setupProducersAndConsumers() { // The PetriNet data structure does not allow us to go from a place to its producers and consumers. // We (re)construct that information here since we will need it a lot for extrapolation. - std::vector> producers(net->_nplaces); - std::vector> consumers(net->_nplaces); + producers.resize(net->_nplaces); + consumers.resize(net->_nplaces); for (uint32_t i = 0; i < net->_ntransitions; ++i) { uint32_t a = net->_transitions[i].inputs; @@ -31,12 +138,10 @@ PetriEngine::ExtrapolationContext::findProducersAndConsumers(const PetriEngine:: producers[inv.place].push_back(i); } } - - return { producers, consumers }; } -std::vector PetriEngine::ExtrapolationContext::findUpperBounds(const PetriEngine::PetriNet *net) { - std::vector bounds(net->_nplaces); +void PetriEngine::ExtrapolationContext::setupUpperBounds() { + upperBounds.resize(net->_nplaces); for (uint32_t i = 0; i < net->_ntransitions; ++i) { uint32_t finv = net->_transitions[i].inputs; uint32_t linv = net->_transitions[i].outputs; @@ -44,12 +149,30 @@ std::vector PetriEngine::ExtrapolationContext::findUpperBounds(const P for ( ; finv < linv; ++finv) { const Invariant& inv = net->_invariants[finv]; if (inv.inhibitor) { - bounds[inv.place] = std::max(bounds[inv.place], inv.tokens); + upperBounds[inv.place] = std::max(upperBounds[inv.place], inv.tokens); } } } +} - return bounds; +int PetriEngine::ExtrapolationContext::effect(uint32_t t, uint32_t p) const { + uint32_t i = net->_transitions[t].inputs; + uint32_t fout = net->_transitions[t].outputs; + int64_t w_rem = 0; + for ( ; i < fout; ++i) { + if (net->_invariants[i].place == p) { + w_rem = net->_invariants[i].tokens; + break; + } + } + uint32_t j = fout; + uint32_t end = net->_transitions[t+1].inputs; + for ( ; j < end; ++j) { + if (net->_invariants[j].place == p) { + return net->_invariants[j].tokens - w_rem; + } + } + return -w_rem; } void PetriEngine::SimpleReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { @@ -81,18 +204,18 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces return _cache.at(query); } - PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); - PetriEngine::PQL::Visitor::visit(&puv, query); - auto& inQuery = puv.in_use(); + PlaceReachabilityDirectionVisitor puv(_ctx->net->numberOfPlaces()); + PQL::Visitor::visit(&puv, query); + auto& use = puv.get_result(); std::vector vis_inc(_ctx->net->_nplaces); // Places where token increment is visible to query std::vector vis_dec(_ctx->net->_nplaces); // Places where token decrement is visible to query std::vector queue; for (uint32_t p = 0; p < _ctx->net->_nplaces; ++p) { - if (inQuery[p]) { - vis_inc[p] = inQuery[p]; - vis_dec[p] = inQuery[p]; + if (use[p] > 0) { + vis_inc[p] = (use[p] & VIS_INC) > 0; + vis_dec[p] = (use[p] & VIS_DEC) > 0; queue.push_back(p); } } @@ -102,28 +225,29 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces queue.pop_back(); if (vis_dec[p]) { - // Put preset of postset in vis_inc, - // and inhibiting preset of postset in vis_dec + // Put pre-set of negative post-set in vis_inc, + // and inhibiting pre-set of post-set in vis_dec for (auto t : _ctx->consumers[p]) { + if (_ctx->effect(t, p) >= 0) continue; const TransPtr &ptr = _ctx->net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& inv = _ctx->net->_invariants[finv]; - if (inv.place == p) { + uint32_t i = ptr.inputs; + uint32_t fout = ptr.outputs; + for ( ; i < fout; ++i) { + const Invariant& arc = _ctx->net->_invariants[i]; + if (arc.place == p) { continue; } - if (inv.inhibitor) { - if (!vis_dec[inv.place]) { - queue.push_back(inv.place); - vis_dec[inv.place] = true; + if (arc.inhibitor) { + if (!vis_dec[arc.place]) { + queue.push_back(arc.place); + vis_dec[arc.place] = true; } } else { - if (!vis_inc[inv.place]) { - queue.push_back(inv.place); - vis_inc[inv.place] = true; + if (!vis_inc[arc.place]) { + queue.push_back(arc.place); + vis_inc[arc.place] = true; } - if (inv.tokens > 1) { + if (arc.tokens > 1) { // This consumer may need more tokens to fire, so increases are also visible vis_inc[p] = true; } @@ -133,9 +257,10 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces } if (vis_inc[p]) { - // Put preset of preset in vis_inc, - // and inhibiting preset of preset in vis_dec + // Put pre-set of positive pre-set in vis_inc, + // and inhibiting pre-set of pre-set in vis_dec for (auto t : _ctx->producers[p]) { + if (_ctx->effect(t, p) <= 0) continue; const TransPtr &ptr = _ctx->net->_transitions[t]; uint32_t finv = ptr.inputs; uint32_t linv = ptr.outputs; @@ -166,8 +291,8 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces query->toString(ss); std::cout << "Visible places : "; for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (inQuery[i] || vis_inc[i] || vis_dec[i]) { - std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << vis_inc[i] << vis_dec[i] << " "; + if (use[i] > 0 || vis_inc[i] || vis_dec[i]) { + std::cout << *_ctx->net->placeNames()[i] << "#" << ((use[i] & IN_Q) > 0) << vis_inc[i] << vis_dec[i] << " "; } } std::cout << ": " << ss.str() << "\n"; @@ -267,7 +392,7 @@ void PetriEngine::DynamicReachExtrapolator::findDeadPlacesAndTransitions(const P auto processEnabled = [&](uint32_t t) { _fireable[t] = true; - // Find and process negative preset and positive postset + // Find and process negative pre-set and positive post-set uint32_t i = _ctx->net->_transitions[t].inputs; uint32_t fout = _ctx->net->_transitions[t].outputs; uint32_t j = fout; @@ -354,16 +479,15 @@ void PetriEngine::DynamicReachExtrapolator::findDeadPlacesAndTransitions(const P void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condition *query) { - PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); - PetriEngine::PQL::Visitor::visit(&puv, query); - auto& inQuery = puv.in_use(); + PlaceReachabilityDirectionVisitor puv(_ctx->net->numberOfPlaces()); + PQL::Visitor::visit(&puv, query); + auto& use = puv.get_result(); std::queue queue; for (uint32_t p = 0; p < _ctx->net->_nplaces; ++p) { - if (inQuery[p]) { - _pflags[p] |= VIS_INC; - _pflags[p] |= VIS_DEC; + if (use[p] > 0) { + _pflags[p] |= use[p]; queue.push(p); } } @@ -373,10 +497,10 @@ void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condi queue.pop(); if ((_pflags[p] & VIS_DEC) > 0) { - // Put preset of postset in vis_inc, - // and inhibiting preset of postset in vis_dec + // Put pre-set of negative post-set in vis_inc, + // and inhibiting pre-set of post-set in vis_dec for (auto t : _ctx->consumers[p]) { - if (!_fireable[t]) continue; + if (!_fireable[t] || _ctx->effect(t, p) >= 0) continue; const TransPtr &ptr = _ctx->net->_transitions[t]; uint32_t finv = ptr.inputs; uint32_t linv = ptr.outputs; @@ -405,10 +529,10 @@ void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condi } if ((_pflags[p] & VIS_INC) > 0) { - // Put preset of preset in vis_inc, - // and inhibiting preset of preset in vis_dec + // Put pre-set of positive pre-set in vis_inc, + // and inhibiting pre-set of pre-set in vis_dec for (auto t : _ctx->producers[p]) { - if (!_fireable[t]) continue; + if (!_fireable[t] || _ctx->effect(t, p) <= 0) continue; const TransPtr &ptr = _ctx->net->_transitions[t]; uint32_t finv = ptr.inputs; uint32_t linv = ptr.outputs; @@ -430,9 +554,9 @@ void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condi } } - // We cannot disable fireable transitions affecting visible places, so their preset must be preserved, - // even if their preset is effectively dead. - for (int t = 0; t < _ctx->net->_ntransitions; ++t) { + // 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 < _ctx->net->_ntransitions; ++t) { if (!_fireable[t]) continue; uint32_t finv = _ctx->net->_transitions[t].inputs; uint32_t linv = _ctx->net->_transitions[t+1].inputs; From 7f11231ff37c0471d455c9a1c77aa15da7199ed5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 17 Jan 2024 16:40:07 +0100 Subject: [PATCH 13/29] Fix out-arc with weight bug --- src/PetriEngine/Extrapolator.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 3469dc686..758041ad4 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -234,16 +234,13 @@ const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces uint32_t fout = ptr.outputs; for ( ; i < fout; ++i) { const Invariant& arc = _ctx->net->_invariants[i]; - if (arc.place == p) { - continue; - } if (arc.inhibitor) { if (!vis_dec[arc.place]) { queue.push_back(arc.place); vis_dec[arc.place] = true; } } else { - if (!vis_inc[arc.place]) { + if (!vis_inc[arc.place] && arc.place != p) { queue.push_back(arc.place); vis_inc[arc.place] = true; } @@ -506,16 +503,13 @@ void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condi uint32_t linv = ptr.outputs; for ( ; finv < linv; ++finv) { const Invariant& arc = _ctx->net->_invariants[finv]; - if (arc.place == p) { - continue; - } 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) { + 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; } From 9a1a49736b16dd6aafbbb783a8e50458527ca42e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 6 Mar 2024 11:28:39 +0100 Subject: [PATCH 14/29] Add total time printing and stop calling std::getenv --- include/PetriEngine/Extrapolator.h | 1 + src/PetriEngine/Extrapolator.cpp | 2 +- src/main.cpp | 8 ++++++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 90bd598fe..71e26ce9c 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -98,6 +98,7 @@ namespace PetriEngine { std::vector _pflags; std::vector _fireable; + bool _env_DYN_EXTRAP_DEBUG = std::getenv("DYN_EXTRAP_DEBUG") != nullptr; void findDeadPlacesAndTransitions(const Marking *marking); void findVisiblePlaces(Condition *query); diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 758041ad4..f5de8982f 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -323,7 +323,7 @@ void PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *ma } } - if (std::getenv("DYN_EXTRAP_DEBUG") != nullptr) { + if (_env_DYN_EXTRAP_DEBUG) { std::stringstream after; for (uint32_t i = 0; i < _ctx->net->_nplaces; i++) { diff --git a/src/main.cpp b/src/main.cpp index 1703310e6..3c082f9ba 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -93,6 +93,14 @@ int main(int argc, const char** argv) { std::cout << "Finished parsing model" << std::endl; } + auto workStart = std::chrono::high_resolution_clock::now(); + // When this ptr goes out of scope it will print the time spent + std::shared_ptr defer (nullptr, [&workStart](...){ + auto workEnd = std::chrono::high_resolution_clock::now(); + auto diff = std::chrono::duration_cast(workEnd - workStart).count() / 1000000.0; + std::cout << std::setprecision(6) << "Spent " << diff << " in total" << std::endl; + }); + //----------------------- Parse Query -----------------------// std::vector querynames; auto ctlStarQueries = readQueries(string_set, options, querynames); From 6c7099ff11678b9535c8d725188efa4630369974 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 8 Mar 2024 09:15:00 +0100 Subject: [PATCH 15/29] Refactor to one Extrapolator --- include/PetriEngine/Extrapolator.h | 121 +-- .../Reachability/ReachabilitySearch.h | 4 +- src/CTL/PetriNets/OnTheFlyDG.cpp | 2 +- src/PetriEngine/Extrapolator.cpp | 776 +++++++++--------- 4 files changed, 430 insertions(+), 473 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 71e26ce9c..7b08cc5e3 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -13,108 +13,71 @@ namespace PetriEngine { using Condition_ptr = PQL::Condition_ptr; using Marking = Structures::State; - const static uint8_t IN_Q = 0b000001; - const static uint8_t VIS_INC = 0b000010; - const static uint8_t VIS_DEC = 0b000100; - const static uint8_t MUST_KEEP = 0b001000; - const static uint8_t CAN_INC = 0b010000; - const static uint8_t CAN_DEC = 0b100000; - - struct ExtrapolationContext { - PetriNet const *net; - std::vector upperBounds; - std::vector> producers; - std::vector> consumers; - - explicit ExtrapolationContext(const PetriNet *net); - - [[nodiscard]] int effect(uint32_t t, uint32_t p) const; - - private: - void setupProducersAndConsumers(); - void setupUpperBounds(); - }; - - using ExtrapolationContext_cptr = std::shared_ptr; + const static uint8_t IN_Q = 1 << 0; + const static uint8_t VIS_INC = 1 << 1; + const static uint8_t VIS_DEC = 1 << 2; + const static uint8_t MUST_KEEP = 1 << 3; + const static uint8_t CAN_INC = 1 << 4; + const static uint8_t CAN_DEC = 1 << 5; class Extrapolator { public: virtual ~Extrapolator() = default; - virtual void init(const PetriNet *net, const Condition *query) { - if (!_ctx) { - _ctx = std::make_shared(net); - } - }; + void init(const PetriNet *net, const Condition *query); - virtual void initWithCtx(const ExtrapolationContext_cptr &ctx, const Condition *query) { - _ctx = ctx; - init(_ctx->net, query); - } - - virtual void extrapolate(Marking *marking, Condition *query) = 0; + void extrapolate(Marking *marking, Condition *query); [[nodiscard]] virtual size_t tokensExtrapolated() const { return _tokensExtrapolated; } - protected: - ExtrapolationContext_cptr _ctx; - size_t _tokensExtrapolated = 0; - }; + Extrapolator * disable() { + _enabled = false; + return this; + } - class NoExtrapolator : public Extrapolator { - public: - void extrapolate(Marking *marking, Condition *query) override { - // no-op - }; - }; + Extrapolator * setDynamic(bool dynamic) { + _doDynamic = dynamic; + return this; + } - /** - * The SimpleReachExtrapolator removes tokens in places that are not visible for the query, - * neither directly or indirectly. The SimpleReachExtrapolator preserves reachability/safety properties. - */ - class SimpleReachExtrapolator : public Extrapolator { - public: - void extrapolate(Marking *marking, Condition *query) override; + private: + void setupProducersAndConsumers(); - protected: - const std::vector &findVisiblePlaces(Condition *query); + void setupExtBounds(); - std::unordered_map> _cache; - }; + [[nodiscard]] int effect(uint32_t t, uint32_t p) const; - /** - * The DynamicReachExtrapolator removes tokens in places that are *effectively* not visible for the query, - * neither directly or indirectly, by considering the current marking and - * which places can never gain or lose tokens. - * The DynamicReachExtrapolator preserves reachability/safety properties. - */ - class DynamicReachExtrapolator : public Extrapolator { - public: - void extrapolate(Marking *marking, Condition *query) override; + void findDeadPlacesAndTransitions(const PetriEngine::Marking *marking); - protected: + void extrapolateDynamicReachRelevance(PetriEngine::Marking *marking, PetriEngine::Condition *query); - std::vector _pflags; - std::vector _fireable; - bool _env_DYN_EXTRAP_DEBUG = std::getenv("DYN_EXTRAP_DEBUG") != nullptr; + void findDynamicVisiblePlaces(PetriEngine::Condition *query); - void findDeadPlacesAndTransitions(const Marking *marking); - void findVisiblePlaces(Condition *query); - }; + void extrapolateStaticReachRelevance(PetriEngine::Marking *marking, PetriEngine::Condition *query); - class AdaptiveExtrapolator : public Extrapolator { - public: - void init(const PetriNet *net, const Condition *query) override; + const std::vector &findStaticVisiblePlaces(PetriEngine::Condition *query); - void extrapolate(Marking *marking, Condition *query) override; + private: + // === Settings + bool _enabled = true; + bool _doDynamic = true; + bool _env_DYN_EXTRAP_DEBUG = std::getenv("DYN_EXTRAP_DEBUG") != nullptr; - size_t tokensExtrapolated() const override; + // === Net + PetriNet const *_net; + std::vector _extBounds; + std::vector> _producers; + std::vector> _consumers; - protected: - //CTLExtrapolator _ctl; - DynamicReachExtrapolator _simple; + // === Cache and working flags + std::unordered_map> _cache; + std::vector _pflags; + std::vector _fireable; + + // === Statistics + size_t _tokensExtrapolated = 0; }; } diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index 863643401..81f4d78f7 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -183,10 +183,10 @@ namespace PetriEngine { } if (queries.size() == 1 && usequeries) { - extrapolator = new DynamicReachExtrapolator(); + extrapolator = new Extrapolator(); extrapolator->init(&_net, queries[0].get()); } else { - extrapolator = new NoExtrapolator(); + extrapolator = (new Extrapolator())->disable(); } // Search! diff --git a/src/CTL/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index c43a33e6c..edf687534 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -26,7 +26,7 @@ OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encod net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); - extrapolator = new PetriEngine::AdaptiveExtrapolator(); + extrapolator = new Extrapolator(); } diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index f5de8982f..ff1811a64 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -109,484 +109,478 @@ namespace PetriEngine { bool negated = false; uint8_t direction = 0; }; -} -PetriEngine::ExtrapolationContext::ExtrapolationContext(const PetriEngine::PetriNet *net) : net(net) { - setupProducersAndConsumers(); - setupUpperBounds(); -} + void Extrapolator::init(const PetriNet *net, const Condition *query) { + _net = net; + setupProducersAndConsumers(); + setupExtBounds(); + } -void PetriEngine::ExtrapolationContext::setupProducersAndConsumers() { - // The PetriNet data structure does not allow us to go from a place to its producers and consumers. - // We (re)construct that information here since we will need it a lot for extrapolation. + void Extrapolator::setupProducersAndConsumers() { + // The PetriNet data structure does not allow us to go from a place to its producers and consumers. + // We (re)construct that information here since we will need it a lot for extrapolation. - producers.resize(net->_nplaces); - consumers.resize(net->_nplaces); + _producers.resize(_net->_nplaces); + _consumers.resize(_net->_nplaces); - for (uint32_t i = 0; i < net->_ntransitions; ++i) { - uint32_t a = net->_transitions[i].inputs; - uint32_t outs = net->_transitions[i].outputs; - uint32_t last = net->_transitions[i + 1].inputs; + for (uint32_t i = 0; i < _net->_ntransitions; ++i) { + uint32_t a = _net->_transitions[i].inputs; + uint32_t outs = _net->_transitions[i].outputs; + uint32_t last = _net->_transitions[i + 1].inputs; - for ( ; a < outs; ++a) { - const Invariant& inv = net->_invariants[a]; - consumers[inv.place].push_back(i); - } + for ( ; a < outs; ++a) { + const Invariant& inv = _net->_invariants[a]; + _consumers[inv.place].push_back(i); + } - for ( ; a < last; ++a) { - const Invariant& inv = net->_invariants[a]; - producers[inv.place].push_back(i); + for ( ; a < last; ++a) { + const Invariant& inv = _net->_invariants[a]; + _producers[inv.place].push_back(i); + } } } -} - -void PetriEngine::ExtrapolationContext::setupUpperBounds() { - upperBounds.resize(net->_nplaces); - 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) { - upperBounds[inv.place] = std::max(upperBounds[inv.place], inv.tokens); + + void Extrapolator::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); + } } } } -} -int PetriEngine::ExtrapolationContext::effect(uint32_t t, uint32_t p) const { - uint32_t i = net->_transitions[t].inputs; - uint32_t fout = net->_transitions[t].outputs; - int64_t w_rem = 0; - for ( ; i < fout; ++i) { - if (net->_invariants[i].place == p) { - w_rem = net->_invariants[i].tokens; - break; + int Extrapolator::effect(uint32_t t, uint32_t p) const { + uint32_t i = _net->_transitions[t].inputs; + uint32_t fout = _net->_transitions[t].outputs; + int64_t w_rem = 0; + for ( ; i < fout; ++i) { + if (_net->_invariants[i].place == p) { + w_rem = _net->_invariants[i].tokens; + break; + } } - } - uint32_t j = fout; - uint32_t end = net->_transitions[t+1].inputs; - for ( ; j < end; ++j) { - if (net->_invariants[j].place == p) { - return net->_invariants[j].tokens - w_rem; + uint32_t j = fout; + uint32_t end = _net->_transitions[t+1].inputs; + for ( ; j < end; ++j) { + if (_net->_invariants[j].place == p) { + return _net->_invariants[j].tokens - w_rem; + } } - } - return -w_rem; -} - -void PetriEngine::SimpleReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { - const std::vector *visible; - auto it = _cache.find(query); - if (it != _cache.end()) { - visible = &it->second; - } else { - visible = &findVisiblePlaces(query); + return -w_rem; } - if (!visible->empty()) { - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (!(*visible)[i]) { - // Extrapolating below the upper bound may introduce behaviour - uint32_t cur = marking->marking()[i]; - uint32_t ex = std::min(cur, _ctx->upperBounds[i]); - _tokensExtrapolated += cur - ex; - marking->marking()[i] = ex; - } + void Extrapolator::extrapolate(Marking *marking, Condition *query) { + if (!_enabled) return; + if (_doDynamic) { + extrapolateDynamicReachRelevance(marking, query); + } else { + extrapolateStaticReachRelevance(marking, query); } } -} -const std::vector &PetriEngine::SimpleReachExtrapolator::findVisiblePlaces(PetriEngine::Condition *query) { - - if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { - _cache.insert(std::make_pair(query, std::vector())); - return _cache.at(query); - } + void Extrapolator::findDeadPlacesAndTransitions(const Marking *marking) { - PlaceReachabilityDirectionVisitor puv(_ctx->net->numberOfPlaces()); - PQL::Visitor::visit(&puv, query); - auto& use = puv.get_result(); + _pflags.resize(_net->_nplaces); + std::fill(_pflags.begin(), _pflags.end(), 0); + _fireable.resize(_net->_ntransitions); + std::fill(_fireable.begin(), _fireable.end(), false); - std::vector vis_inc(_ctx->net->_nplaces); // Places where token increment is visible to query - std::vector vis_dec(_ctx->net->_nplaces); // Places where token decrement is visible to query - std::vector queue; + std::queue queue; - for (uint32_t p = 0; p < _ctx->net->_nplaces; ++p) { - if (use[p] > 0) { - vis_inc[p] = (use[p] & VIS_INC) > 0; - vis_dec[p] = (use[p] & VIS_DEC) > 0; - queue.push_back(p); - } - } + // Helper functions - while (!queue.empty()) { - uint32_t p = queue.back(); - queue.pop_back(); - - if (vis_dec[p]) { - // Put pre-set of negative post-set in vis_inc, - // and inhibiting pre-set of post-set in vis_dec - for (auto t : _ctx->consumers[p]) { - if (_ctx->effect(t, p) >= 0) continue; - const TransPtr &ptr = _ctx->net->_transitions[t]; - uint32_t i = ptr.inputs; - uint32_t fout = ptr.outputs; - for ( ; i < fout; ++i) { - const Invariant& arc = _ctx->net->_invariants[i]; - 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; - } - } + auto processIncPlace = [&](uint32_t p) { + if ((_pflags[p] & CAN_INC) == 0) { + _pflags[p] |= CAN_INC; + for (uint32_t t : _consumers[p]) { + if (!_fireable[t]) + queue.push(t); } } - } - - if (vis_inc[p]) { - // Put pre-set of positive pre-set in vis_inc, - // and inhibiting pre-set of pre-set in vis_dec - for (auto t : _ctx->producers[p]) { - if (_ctx->effect(t, p) <= 0) continue; - const TransPtr &ptr = _ctx->net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& inv = _ctx->net->_invariants[finv]; - if (inv.inhibitor) { - if (!vis_dec[inv.place]) { - queue.push_back(inv.place); - vis_dec[inv.place] = true; - } + }; + + auto processDecPlace = [&](uint32_t p) { + if ((_pflags[p] & CAN_DEC) == 0) { + _pflags[p] |= CAN_DEC; + for (uint32_t t : _consumers[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 + uint32_t i = _net->_transitions[t].inputs; + uint32_t fout = _net->_transitions[t].outputs; + uint32_t j = fout; + uint32_t end = _net->_transitions[t+1].inputs; + while (i < fout && j < end) + { + const Invariant& preinv = _net->_invariants[i]; + const Invariant& postinv = _net->_invariants[j]; + + if (preinv.place < postinv.place) { + if (!preinv.inhibitor) + processDecPlace(preinv.place); + i++; + } else if (preinv.place > postinv.place) { + processIncPlace(postinv.place); + j++; + } else { + if (preinv.inhibitor) { + processIncPlace(postinv.place); } else { - if (!vis_inc[inv.place]) { - queue.push_back(inv.place); - vis_inc[inv.place] = true; + // There are both an in and an out arc to this place. Is the effect non-zero? + if (preinv.tokens > postinv.tokens) { + processDecPlace(preinv.place); + } else if (preinv.tokens < postinv.tokens) { + processIncPlace(postinv.place); } } + + i++; j++; + } + } + for ( ; i < fout; i++) { + const Invariant& preinv = _net->_invariants[i]; + if (!preinv.inhibitor) + processDecPlace(preinv.place); + } + for ( ; j < end; j++) { + processIncPlace(_net->_invariants[j].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); + } } - } - - std::vector visible(_ctx->net->_nplaces); - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - visible[i] = vis_inc[i] || vis_dec[i]; - } - std::stringstream ss; - query->toString(ss); - std::cout << "Visible places : "; - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (use[i] > 0 || vis_inc[i] || vis_dec[i]) { - std::cout << *_ctx->net->placeNames()[i] << "#" << ((use[i] & IN_Q) > 0) << vis_inc[i] << vis_dec[i] << " "; + // 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); + } } } - std::cout << ": " << ss.str() << "\n"; - - _cache.insert(std::make_pair(query, visible)); - return _cache.at(query); -} - -void PetriEngine::DynamicReachExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { - - if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { - return; - } - std::stringstream before; - for (uint32_t i = 0; i < _ctx->net->_nplaces; i++) - { - before << (*marking)[i]; - } - - findDeadPlacesAndTransitions(marking); - findVisiblePlaces(query); + void Extrapolator::extrapolateDynamicReachRelevance(Marking *marking, Condition *query) { - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if ((_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP)) == 0) { - // Extrapolating below the upper bound may introduce behaviour - uint32_t cur = marking->marking()[i]; - uint32_t ex = std::min(cur, _ctx->upperBounds[i]); - _tokensExtrapolated += cur - ex; - marking->marking()[i] = ex; + if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { + return; } - } - if (_env_DYN_EXTRAP_DEBUG) { - std::stringstream after; - for (uint32_t i = 0; i < _ctx->net->_nplaces; i++) + std::stringstream before; + for (uint32_t i = 0; i < _net->_nplaces; i++) { - after << (*marking)[i]; + before << (*marking)[i]; } - if (before.str() == after.str()) - return; - PetriEngine::PQL::PlaceUseVisitor puv(_ctx->net->numberOfPlaces()); - PetriEngine::PQL::Visitor::visit(&puv, query); - auto& inQuery = puv.in_use(); + findDeadPlacesAndTransitions(marking); + findDynamicVisiblePlaces(query); - std::cout << before.str() << "->" << after.str() << " | Visible: "; - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if (inQuery[i] || (_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP)) > 0) { - std::cout << *_ctx->net->placeNames()[i] << "#" << inQuery[i] << ((_pflags[i] & VIS_INC) > 0) - << ((_pflags[i] & VIS_DEC) > 0) << ((_pflags[i] & MUST_KEEP) > 0) << " "; + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + if ((_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP)) == 0) { + // Extrapolating below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _extBounds[i]); + _tokensExtrapolated += cur - ex; + marking->marking()[i] = ex; } } - std::cout << "| Live: "; - for (uint32_t i = 0; i < _ctx->net->_nplaces; ++i) { - if ((_pflags[i] & (CAN_INC | CAN_DEC)) > 0) { - std::cout << *_ctx->net->placeNames()[i] << "#" << ((_pflags[i] & CAN_INC) > 0) - << ((_pflags[i] & CAN_DEC) > 0) << " "; + + if (_env_DYN_EXTRAP_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"; } - std::stringstream ss; - query->toString(ss); - std::cout << "| " << ss.str() << "\n"; } -} -void PetriEngine::DynamicReachExtrapolator::findDeadPlacesAndTransitions(const PetriEngine::Marking *marking) { + void Extrapolator::findDynamicVisiblePlaces(Condition *query) { - _pflags.resize(_ctx->net->_nplaces); - std::fill(_pflags.begin(), _pflags.end(), 0); - _fireable.resize(_ctx->net->_ntransitions); - std::fill(_fireable.begin(), _fireable.end(), false); + PlaceReachabilityDirectionVisitor pv(_net->numberOfPlaces()); + PQL::Visitor::visit(&pv, query); + auto& use = pv.get_result(); - std::queue queue; + std::queue queue; - // Helper functions - - auto processIncPlace = [&](uint32_t p) { - if ((_pflags[p] & CAN_INC) == 0) { - _pflags[p] |= CAN_INC; - for (uint32_t t : _ctx->consumers[p]) { - if (!_fireable[t]) - queue.push(t); + for (uint32_t p = 0; p < _net->_nplaces; ++p) { + if (use[p] > 0) { + _pflags[p] |= use[p]; + queue.push(p); } } - }; - auto processDecPlace = [&](uint32_t p) { - if ((_pflags[p] & CAN_DEC) == 0) { - _pflags[p] |= CAN_DEC; - for (uint32_t t : _ctx->consumers[p]) { - if (!_fireable[t]) - queue.push(t); + while (!queue.empty()) { + uint32_t p = queue.front(); + queue.pop(); + + if ((_pflags[p] & VIS_DEC) > 0) { + // Put pre-set of negative post-set in vis_inc, + // and inhibiting pre-set of post-set in vis_dec + for (auto t : _consumers[p]) { + if (!_fireable[t] || effect(t, p) >= 0) continue; + const TransPtr &ptr = _net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _net->_invariants[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; + } + } + } + } } - } - }; - - auto processEnabled = [&](uint32_t t) { - _fireable[t] = true; - // Find and process negative pre-set and positive post-set - uint32_t i = _ctx->net->_transitions[t].inputs; - uint32_t fout = _ctx->net->_transitions[t].outputs; - uint32_t j = fout; - uint32_t end = _ctx->net->_transitions[t+1].inputs; - while (i < fout && j < end) - { - const Invariant& preinv = _ctx->net->_invariants[i]; - const Invariant& postinv = _ctx->net->_invariants[j]; - if (preinv.place < postinv.place) { - if (!preinv.inhibitor) - processDecPlace(preinv.place); - i++; - } else if (preinv.place > postinv.place) { - processIncPlace(postinv.place); - j++; - } else { - if (preinv.inhibitor) { - processIncPlace(postinv.place); - } else { - // There are both an in and an out arc to this place. Is the effect non-zero? - if (preinv.tokens > postinv.tokens) { - processDecPlace(preinv.place); - } else if (preinv.tokens < postinv.tokens) { - processIncPlace(postinv.place); + if ((_pflags[p] & VIS_INC) > 0) { + // Put pre-set of positive pre-set in vis_inc, + // and inhibiting pre-set of pre-set in vis_dec + for (auto t : _producers[p]) { + if (!_fireable[t] || effect(t, p) <= 0) continue; + const TransPtr &ptr = _net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; + for ( ; finv < linv; ++finv) { + const Invariant& arc = _net->_invariants[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; + } + } } } - - i++; j++; } } - for ( ; i < fout; i++) { - const Invariant& preinv = _ctx->net->_invariants[i]; - if (!preinv.inhibitor) - processDecPlace(preinv.place); - } - for ( ; j < end; j++) { - processIncPlace(_ctx->net->_invariants[j].place); - } - }; - // Process initially enabled transitions - for (uint32_t t = 0; t < _ctx->net->_ntransitions; ++t) { - uint32_t i = _ctx->net->_transitions[t].inputs; - uint32_t fout = _ctx->net->_transitions[t].outputs; - bool enabled = true; - for ( ; i < fout; i++) { - const Invariant& preinv = _ctx->net->_invariants[i]; - if (preinv.inhibitor != (preinv.tokens > (*marking)[preinv.place])) { - enabled = false; - break; + // 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 ((_pflags[arc.place] & (VIS_INC | VIS_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; + } + } } - } - 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 = _ctx->net->_transitions[t].inputs; - uint32_t linv = _ctx->net->_transitions[t].outputs; - for (; finv < linv; ++finv) { - const Invariant& arc = _ctx->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; + void Extrapolator::extrapolateStaticReachRelevance(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]) { + // Extrapolating below the upper bound may introduce behaviour + uint32_t cur = marking->marking()[i]; + uint32_t ex = std::min(cur, _extBounds[i]); + _tokensExtrapolated += cur - ex; + marking->marking()[i] = ex; + } } } - if (enabled) { - processEnabled(t); - } } -} -void PetriEngine::DynamicReachExtrapolator::findVisiblePlaces(PetriEngine::Condition *query) { + const std::vector &Extrapolator::findStaticVisiblePlaces(Condition *query) { - PlaceReachabilityDirectionVisitor puv(_ctx->net->numberOfPlaces()); - PQL::Visitor::visit(&puv, query); - auto& use = puv.get_result(); + 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::queue queue; + 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; - for (uint32_t p = 0; p < _ctx->net->_nplaces; ++p) { - if (use[p] > 0) { - _pflags[p] |= use[p]; - queue.push(p); + for (uint32_t p = 0; p < _net->_nplaces; ++p) { + if (use[p] > 0) { + vis_inc[p] = (use[p] & VIS_INC) > 0; + vis_dec[p] = (use[p] & VIS_DEC) > 0; + queue.push_back(p); + } } - } - while (!queue.empty()) { - uint32_t p = queue.front(); - queue.pop(); - - if ((_pflags[p] & VIS_DEC) > 0) { - // Put pre-set of negative post-set in vis_inc, - // and inhibiting pre-set of post-set in vis_dec - for (auto t : _ctx->consumers[p]) { - if (!_fireable[t] || _ctx->effect(t, p) >= 0) continue; - const TransPtr &ptr = _ctx->net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& arc = _ctx->net->_invariants[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; + while (!queue.empty()) { + uint32_t p = queue.back(); + queue.pop_back(); + + if (vis_dec[p]) { + // Put pre-set of negative post-set in vis_inc, + // and inhibiting pre-set of post-set in vis_dec + for (auto t : _consumers[p]) { + if (effect(t, p) >= 0) continue; + const TransPtr &ptr = _net->_transitions[t]; + uint32_t i = ptr.inputs; + uint32_t fout = ptr.outputs; + for ( ; i < fout; ++i) { + const Invariant& arc = _net->_invariants[i]; + 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; + } } } } } - } - if ((_pflags[p] & VIS_INC) > 0) { - // Put pre-set of positive pre-set in vis_inc, - // and inhibiting pre-set of pre-set in vis_dec - for (auto t : _ctx->producers[p]) { - if (!_fireable[t] || _ctx->effect(t, p) <= 0) continue; - const TransPtr &ptr = _ctx->net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& arc = _ctx->net->_invariants[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; + if (vis_inc[p]) { + // Put pre-set of positive pre-set in vis_inc, + // and inhibiting pre-set of pre-set in vis_dec + for (auto t : _producers[p]) { + if (effect(t, p) <= 0) continue; + const TransPtr &ptr = _net->_transitions[t]; + uint32_t finv = ptr.inputs; + uint32_t linv = ptr.outputs; + for ( ; finv < linv; ++finv) { + const Invariant& inv = _net->_invariants[finv]; + if (inv.inhibitor) { + if (!vis_dec[inv.place]) { + queue.push_back(inv.place); + vis_dec[inv.place] = true; + } + } else { + if (!vis_inc[inv.place]) { + queue.push_back(inv.place); + vis_inc[inv.place] = true; + } } } } } } - } - // 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 < _ctx->net->_ntransitions; ++t) { - if (!_fireable[t]) continue; - uint32_t finv = _ctx->net->_transitions[t].inputs; - uint32_t linv = _ctx->net->_transitions[t+1].inputs; - bool affectsVisible = false; - for ( ; finv < linv; ++finv) { - const Invariant& arc = _ctx->net->_invariants[finv]; - if ((_pflags[arc.place] & (VIS_INC | VIS_DEC)) > 0) { - affectsVisible = true; - break; - } + std::vector visible(_net->_nplaces); + for (uint32_t i = 0; i < _net->_nplaces; ++i) { + visible[i] = vis_inc[i] || vis_dec[i]; } - if (affectsVisible) { - finv = _ctx->net->_transitions[t].inputs; - linv = _ctx->net->_transitions[t].outputs; - for ( ; finv < linv; ++finv) { - const Invariant& arc = _ctx->net->_invariants[finv]; - if (!arc.inhibitor) { - _pflags[arc.place] |= MUST_KEEP; - } + + 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) > 0) << vis_inc[i] << vis_dec[i] << " "; } } - } -} + std::cout << ": " << ss.str() << "\n"; -void PetriEngine::AdaptiveExtrapolator::init(const PetriEngine::PetriNet *net, const PetriEngine::Condition *query) { - if (!_ctx) { - _ctx = std::make_shared(net); + _cache.insert(std::make_pair(query, visible)); + return _cache.at(query); } - _simple.initWithCtx(_ctx, query); - //_ctl.initWithCtx(_ctx, query); -} - -void PetriEngine::AdaptiveExtrapolator::extrapolate(PetriEngine::Marking *marking, PetriEngine::Condition *query) { - _simple.extrapolate(marking, query); -} - -size_t PetriEngine::AdaptiveExtrapolator::tokensExtrapolated() const { - return _simple.tokensExtrapolated(); //+ _ctl.tokensExtrapolated(); TODO -} +} \ No newline at end of file From 230fb5f2705f0be0423116f96f09ba2675eac700 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 8 Mar 2024 13:07:26 +0100 Subject: [PATCH 16/29] Only dynamic propagation from support that can change --- include/PetriEngine/Extrapolator.h | 15 +++++----- src/PetriEngine/Extrapolator.cpp | 46 +++++++++++++++++------------- 2 files changed, 34 insertions(+), 27 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 7b08cc5e3..ca86a4c8c 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -13,12 +13,13 @@ namespace PetriEngine { using Condition_ptr = PQL::Condition_ptr; using Marking = Structures::State; - const static uint8_t IN_Q = 1 << 0; - const static uint8_t VIS_INC = 1 << 1; - const static uint8_t VIS_DEC = 1 << 2; - const static uint8_t MUST_KEEP = 1 << 3; - const static uint8_t CAN_INC = 1 << 4; - const static uint8_t CAN_DEC = 1 << 5; + 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; class Extrapolator { public: @@ -62,7 +63,7 @@ namespace PetriEngine { private: // === Settings bool _enabled = true; - bool _doDynamic = true; + bool _doDynamic = false; bool _env_DYN_EXTRAP_DEBUG = std::getenv("DYN_EXTRAP_DEBUG") != nullptr; // === Net diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index ff1811a64..54ed626eb 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -26,37 +26,37 @@ namespace PetriEngine { for (auto& e : *element) Visitor::visit(this, e); } void _accept(const PQL::LessThanCondition* element) override { - direction = VIS_DEC; + direction = IN_Q_DEC; Visitor::visit(this, (*element)[0]); - direction = VIS_INC; + direction = IN_Q_INC; Visitor::visit(this, (*element)[1]); } void _accept(const PQL::LessThanOrEqualCondition* element) override { - direction = VIS_DEC; + direction = IN_Q_DEC; Visitor::visit(this, (*element)[0]); - direction = VIS_INC; + direction = IN_Q_INC; Visitor::visit(this, (*element)[1]); } void _accept(const PQL::EqualCondition* element) override { - direction = VIS_INC | VIS_DEC; + direction = IN_Q_INC | IN_Q_DEC; Visitor::visit(this, (*element)[0]); Visitor::visit(this, (*element)[1]); } void _accept(const PQL::NotEqualCondition* element) override { - direction = VIS_INC | VIS_DEC; + 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 | IN_Q; + _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 | IN_Q; + 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 | IN_Q; + for(auto& p : element->places()) _in_use[p.first] |= direction; } void _accept(const PQL::MinusExpr* element) override { // TODO: Do we need to negate here? @@ -68,11 +68,11 @@ namespace PetriEngine { } void _accept(const PQL::CompareConjunction* element) override { // TODO: What even is this? - for(auto& e : *element) _in_use[e._place] |= direction | IN_Q; + for(auto& e : *element) _in_use[e._place] |= direction; } void _accept(const PQL::UnfoldedUpperBoundsCondition* element) override { for(auto& p : element->places()) - _in_use[p._place] |= VIS_INC | IN_Q; + _in_use[p._place] |= IN_Q_INC; } void _accept(const PQL::EFCondition* el) override { @@ -309,16 +309,17 @@ namespace PetriEngine { } std::stringstream before; - for (uint32_t i = 0; i < _net->_nplaces; i++) - { - before << (*marking)[i]; + if (_env_DYN_EXTRAP_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)) == 0) { + if ((_pflags[i] & (VIS_INC | VIS_DEC | MUST_KEEP | IN_Q_INC | IN_Q_DEC)) == 0) { // Extrapolating below the upper bound may introduce behaviour uint32_t cur = marking->marking()[i]; uint32_t ex = std::min(cur, _extBounds[i]); @@ -370,7 +371,12 @@ namespace PetriEngine { 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); } } @@ -443,7 +449,7 @@ namespace PetriEngine { bool affectsVisible = false; for ( ; finv < linv; ++finv) { const Invariant& arc = _net->_invariants[finv]; - if ((_pflags[arc.place] & (VIS_INC | VIS_DEC)) > 0) { + if ((_pflags[arc.place] & (VIS_INC | VIS_DEC | IN_Q_INC | IN_Q_DEC)) > 0) { affectsVisible = true; break; } @@ -500,8 +506,8 @@ namespace PetriEngine { for (uint32_t p = 0; p < _net->_nplaces; ++p) { if (use[p] > 0) { - vis_inc[p] = (use[p] & VIS_INC) > 0; - vis_dec[p] = (use[p] & VIS_DEC) > 0; + vis_inc[p] = (use[p] & IN_Q_INC) > 0; + vis_dec[p] = (use[p] & IN_Q_DEC) > 0; queue.push_back(p); } } @@ -575,7 +581,7 @@ namespace PetriEngine { 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) > 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"; From 12c8d87e94f240b399c14c748520a8c213588e11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 11 Mar 2024 09:00:34 +0100 Subject: [PATCH 17/29] Fix issue in dynamic extrapolation propagation from prev commit --- include/PetriEngine/Extrapolator.h | 2 +- src/PetriEngine/Extrapolator.cpp | 13 +++++++++---- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index ca86a4c8c..45e6ad543 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -63,7 +63,7 @@ namespace PetriEngine { private: // === Settings bool _enabled = true; - bool _doDynamic = false; + bool _doDynamic = true; bool _env_DYN_EXTRAP_DEBUG = std::getenv("DYN_EXTRAP_DEBUG") != nullptr; // === Net diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 54ed626eb..b16fe027b 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -38,11 +38,13 @@ namespace PetriEngine { 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]); @@ -99,10 +101,12 @@ namespace PetriEngine { void _accept(const PQL::AUCondition* el) override { throw std::runtime_error("AUCondition should not exist in compiled reachability expression"); } - - // Shallow elements, neither of these should exist in a compiled expression - void _accept(const PQL::LiteralExpr* element) override {} - void _accept(const PQL::DeadlockCondition* element) override {} + 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; @@ -371,6 +375,7 @@ namespace PetriEngine { 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; } From 9fb66c9b49bbb260f78d4204c20d29ba6ed5ca11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 25 Mar 2024 11:22:44 +0100 Subject: [PATCH 18/29] Fix Extrapolator for queries with CompareConjunction --- src/PetriEngine/Extrapolator.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index b16fe027b..5e4b91bd4 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -69,8 +69,18 @@ namespace PetriEngine { for(auto& e : element->expressions()) Visitor::visit(this, e); } void _accept(const PQL::CompareConjunction* element) override { - // TODO: What even is this? - for(auto& e : *element) _in_use[e._place] |= direction; + // 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()) From 19783c138a1674eb48e0dbd733d38ed4abccf65e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 3 May 2024 13:54:56 +0200 Subject: [PATCH 19/29] Use cache friendly data layout and invariant metadata --- include/PetriEngine/Extrapolator.h | 27 +++- src/PetriEngine/Extrapolator.cpp | 246 ++++++++++++++--------------- 2 files changed, 144 insertions(+), 129 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 45e6ad543..41eab049f 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -42,6 +42,23 @@ namespace PetriEngine { _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: void setupProducersAndConsumers(); @@ -50,6 +67,9 @@ namespace PetriEngine { [[nodiscard]] int effect(uint32_t t, uint32_t p) const; + [[nodiscard]] std::pair producers(uint32_t p) const; + [[nodiscard]] std::pair consumers(uint32_t p) const; + void findDeadPlacesAndTransitions(const PetriEngine::Marking *marking); void extrapolateDynamicReachRelevance(PetriEngine::Marking *marking, PetriEngine::Condition *query); @@ -64,13 +84,14 @@ namespace PetriEngine { // === Settings bool _enabled = true; bool _doDynamic = true; - bool _env_DYN_EXTRAP_DEBUG = std::getenv("DYN_EXTRAP_DEBUG") != nullptr; + bool _env_TOKEN_ELIM_DEBUG = std::getenv("TOKEN_ELIM_DEBUG") != nullptr; // === Net PetriNet const *_net; std::vector _extBounds; - std::vector> _producers; - std::vector> _consumers; + std::unique_ptr _prodcons; + std::unique_ptr _parcs; + std::vector> _inhibpost; // === Cache and working flags std::unordered_map> _cache; diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/Extrapolator.cpp index 5e4b91bd4..fd9685d98 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/Extrapolator.cpp @@ -131,27 +131,64 @@ namespace PetriEngine { } void Extrapolator::setupProducersAndConsumers() { - // The PetriNet data structure does not allow us to go from a place to its producers and consumers. - // We (re)construct that information here since we will need it a lot for extrapolation. + _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); + } + } - _producers.resize(_net->_nplaces); - _consumers.resize(_net->_nplaces); + 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); + } + } - for (uint32_t i = 0; i < _net->_ntransitions; ++i) { - uint32_t a = _net->_transitions[i].inputs; - uint32_t outs = _net->_transitions[i].outputs; - uint32_t last = _net->_transitions[i + 1].inputs; + // 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()); - for ( ; a < outs; ++a) { - const Invariant& inv = _net->_invariants[a]; - _consumers[inv.place].push_back(i); + _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 ( ; a < last; ++a) { - const Invariant& inv = _net->_invariants[a]; - _producers[inv.place].push_back(i); + 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 Extrapolator::setupExtBounds() { @@ -169,24 +206,13 @@ namespace PetriEngine { } } - int Extrapolator::effect(uint32_t t, uint32_t p) const { - uint32_t i = _net->_transitions[t].inputs; - uint32_t fout = _net->_transitions[t].outputs; - int64_t w_rem = 0; - for ( ; i < fout; ++i) { - if (_net->_invariants[i].place == p) { - w_rem = _net->_invariants[i].tokens; - break; - } - } - uint32_t j = fout; - uint32_t end = _net->_transitions[t+1].inputs; - for ( ; j < end; ++j) { - if (_net->_invariants[j].place == p) { - return _net->_invariants[j].tokens - w_rem; - } - } - return -w_rem; + std::pair Extrapolator::producers(uint32_t p) const { + const place_t pmeta = _prodcons[p]; + return std::make_pair(&_parcs[pmeta.producers], &_parcs[pmeta.consumers]); + } + + std::pair Extrapolator::consumers(uint32_t p) const { + return std::make_pair(&_parcs[_prodcons[p].consumers], &_parcs[_prodcons[p + 1].producers]); } void Extrapolator::extrapolate(Marking *marking, Condition *query) { @@ -212,9 +238,9 @@ namespace PetriEngine { auto processIncPlace = [&](uint32_t p) { if ((_pflags[p] & CAN_INC) == 0) { _pflags[p] |= CAN_INC; - for (uint32_t t : _consumers[p]) { - if (!_fireable[t]) - queue.push(t); + for (auto [t, last] = consumers(p); t < last; ++t) { + if (!_fireable[t->index]) + queue.push(t->index); } } }; @@ -222,7 +248,7 @@ namespace PetriEngine { auto processDecPlace = [&](uint32_t p) { if ((_pflags[p] & CAN_DEC) == 0) { _pflags[p] |= CAN_DEC; - for (uint32_t t : _consumers[p]) { + for (uint32_t t : _inhibpost[p]) { if (!_fireable[t]) queue.push(t); } @@ -232,44 +258,13 @@ namespace PetriEngine { auto processEnabled = [&](uint32_t t) { _fireable[t] = true; // Find and process negative pre-set and positive post-set - uint32_t i = _net->_transitions[t].inputs; - uint32_t fout = _net->_transitions[t].outputs; - uint32_t j = fout; - uint32_t end = _net->_transitions[t+1].inputs; - while (i < fout && j < end) - { - const Invariant& preinv = _net->_invariants[i]; - const Invariant& postinv = _net->_invariants[j]; - - if (preinv.place < postinv.place) { - if (!preinv.inhibitor) - processDecPlace(preinv.place); - i++; - } else if (preinv.place > postinv.place) { - processIncPlace(postinv.place); - j++; - } else { - if (preinv.inhibitor) { - processIncPlace(postinv.place); - } else { - // There are both an in and an out arc to this place. Is the effect non-zero? - if (preinv.tokens > postinv.tokens) { - processDecPlace(preinv.place); - } else if (preinv.tokens < postinv.tokens) { - processIncPlace(postinv.place); - } - } - - i++; j++; - } - } - for ( ; i < fout; i++) { - const Invariant& preinv = _net->_invariants[i]; - if (!preinv.inhibitor) - processDecPlace(preinv.place); + for (auto [finv, linv] = _net->preset(t); finv < linv; ++finv) { + if (finv->direction < 0) + processDecPlace(finv->place); } - for ( ; j < end; j++) { - processIncPlace(_net->_invariants[j].place); + for (auto [finv, linv] = _net->postset(t); finv < linv; ++finv) { + if (finv->direction > 0) + processIncPlace(finv->place); } }; @@ -323,12 +318,16 @@ namespace PetriEngine { } std::stringstream before; - if (_env_DYN_EXTRAP_DEBUG) { + if (_env_TOKEN_ELIM_DEBUG) { for (uint32_t i = 0; i < _net->_nplaces; i++) { before << (*marking)[i]; } } + if (before.str() == "00110000000010000000000000001100000000000000000000000101000000001") { + std::cout << "Debugging\n"; + } + findDeadPlacesAndTransitions(marking); findDynamicVisiblePlaces(query); @@ -342,7 +341,7 @@ namespace PetriEngine { } } - if (_env_DYN_EXTRAP_DEBUG) { + if (_env_TOKEN_ELIM_DEBUG) { std::stringstream after; for (uint32_t i = 0; i < _net->_nplaces; i++) { @@ -401,15 +400,12 @@ namespace PetriEngine { queue.pop(); if ((_pflags[p] & VIS_DEC) > 0) { - // Put pre-set of negative post-set in vis_inc, - // and inhibiting pre-set of post-set in vis_dec - for (auto t : _consumers[p]) { - if (!_fireable[t] || effect(t, p) >= 0) continue; - const TransPtr &ptr = _net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& arc = _net->_invariants[finv]; + // 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); @@ -430,15 +426,12 @@ namespace PetriEngine { } if ((_pflags[p] & VIS_INC) > 0) { - // Put pre-set of positive pre-set in vis_inc, - // and inhibiting pre-set of pre-set in vis_dec - for (auto t : _producers[p]) { - if (!_fireable[t] || effect(t, p) <= 0) continue; - const TransPtr &ptr = _net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& arc = _net->_invariants[finv]; + // 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); @@ -464,7 +457,11 @@ namespace PetriEngine { bool affectsVisible = false; for ( ; finv < linv; ++finv) { const Invariant& arc = _net->_invariants[finv]; - if ((_pflags[arc.place] & (VIS_INC | VIS_DEC | IN_Q_INC | IN_Q_DEC)) > 0) { + 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; } @@ -532,15 +529,12 @@ namespace PetriEngine { queue.pop_back(); if (vis_dec[p]) { - // Put pre-set of negative post-set in vis_inc, - // and inhibiting pre-set of post-set in vis_dec - for (auto t : _consumers[p]) { - if (effect(t, p) >= 0) continue; - const TransPtr &ptr = _net->_transitions[t]; - uint32_t i = ptr.inputs; - uint32_t fout = ptr.outputs; - for ( ; i < fout; ++i) { - const Invariant& arc = _net->_invariants[i]; + // 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); @@ -561,24 +555,21 @@ namespace PetriEngine { } if (vis_inc[p]) { - // Put pre-set of positive pre-set in vis_inc, - // and inhibiting pre-set of pre-set in vis_dec - for (auto t : _producers[p]) { - if (effect(t, p) <= 0) continue; - const TransPtr &ptr = _net->_transitions[t]; - uint32_t finv = ptr.inputs; - uint32_t linv = ptr.outputs; - for ( ; finv < linv; ++finv) { - const Invariant& inv = _net->_invariants[finv]; - if (inv.inhibitor) { - if (!vis_dec[inv.place]) { - queue.push_back(inv.place); - vis_dec[inv.place] = true; + // 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[inv.place]) { - queue.push_back(inv.place); - vis_inc[inv.place] = true; + if (!vis_inc[arc.place]) { + queue.push_back(arc.place); + vis_inc[arc.place] = true; } } } @@ -591,15 +582,18 @@ namespace PetriEngine { visible[i] = vis_inc[i] || vis_dec[i]; } - 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] << " "; + 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"; } - std::cout << ": " << ss.str() << "\n"; _cache.insert(std::make_pair(query, visible)); return _cache.at(query); From c7120bcd31fee07db12d61da10d187bcf7d8566d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 3 May 2024 14:18:33 +0200 Subject: [PATCH 20/29] Removed unused effect method --- include/PetriEngine/Extrapolator.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 41eab049f..79ea2e0fd 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -65,8 +65,6 @@ namespace PetriEngine { void setupExtBounds(); - [[nodiscard]] int effect(uint32_t t, uint32_t p) const; - [[nodiscard]] std::pair producers(uint32_t p) const; [[nodiscard]] std::pair consumers(uint32_t p) const; From b7c32e2f4b64f07e41f16177d2a1f44fd5b14a42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 6 May 2024 12:55:42 +0200 Subject: [PATCH 21/29] Allow for inlining of preset and postset iteration --- include/PetriEngine/PetriNet.h | 18 ++++++++++++++++-- src/PetriEngine/PetriNet.cpp | 15 --------------- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/include/PetriEngine/PetriNet.h b/include/PetriEngine/PetriNet.h index 1ed3aee14..08a285f58 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; } 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]; From f4734f0d8cc48aecf22326e957e14d36ed1c0400 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 10 Sep 2024 16:41:20 +0200 Subject: [PATCH 22/29] Add env vars to control token elim --- include/PetriEngine/Extrapolator.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/include/PetriEngine/Extrapolator.h b/include/PetriEngine/Extrapolator.h index 79ea2e0fd..01bf2b37c 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/Extrapolator.h @@ -80,9 +80,9 @@ namespace PetriEngine { private: // === Settings - bool _enabled = true; - bool _doDynamic = true; - bool _env_TOKEN_ELIM_DEBUG = std::getenv("TOKEN_ELIM_DEBUG") != nullptr; + bool _enabled = std::getenv("TAPAAL_TOKEN_ELIM") != nullptr; + bool _doDynamic = std::getenv("TAPAAL_TOKEN_ELIM_STATIC") == nullptr; + bool _env_TOKEN_ELIM_DEBUG = std::getenv("TAPAAL_TOKEN_ELIM_DEBUG") != nullptr; // === Net PetriNet const *_net; From 80b032589f83661c08b4218d67b8a421529e8c6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 20 Jan 2025 17:07:01 +0100 Subject: [PATCH 23/29] Rename to TokenEliminator --- include/CTL/CTLResult.h | 2 +- include/CTL/PetriNets/OnTheFlyDG.h | 10 ++--- include/PetriEngine/PetriNet.h | 6 +-- .../Reachability/ReachabilitySearch.h | 12 +++--- .../{Extrapolator.h => TokenEliminator.h} | 39 ++++++++++++------- src/CTL/CTLEngine.cpp | 2 +- src/CTL/CTLResult.cpp | 2 +- src/CTL/PetriNets/OnTheFlyDG.cpp | 22 +++++------ src/PetriEngine/CMakeLists.txt | 2 +- .../Reachability/ReachabilitySearch.cpp | 10 ++--- .../{Extrapolator.cpp => TokenEliminator.cpp} | 36 ++++++++--------- 11 files changed, 76 insertions(+), 67 deletions(-) rename include/PetriEngine/{Extrapolator.h => TokenEliminator.h} (61%) rename src/PetriEngine/{Extrapolator.cpp => TokenEliminator.cpp} (94%) diff --git a/include/CTL/CTLResult.h b/include/CTL/CTLResult.h index 2aa6463d9..8d4b783bd 100644 --- a/include/CTL/CTLResult.h +++ b/include/CTL/CTLResult.h @@ -26,7 +26,7 @@ struct CTLResult { size_t processedNegationEdges = 0; size_t exploredConfigurations = 0; size_t numberOfEdges = 0; - size_t tokensExtrapolated = 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 7d5263355..9684c8e82 100644 --- a/include/CTL/PetriNets/OnTheFlyDG.h +++ b/include/CTL/PetriNets/OnTheFlyDG.h @@ -14,7 +14,7 @@ #include "PetriEngine/Structures/AlignedEncoder.h" #include "PetriEngine/Structures/linked_bucket.h" #include "PetriEngine/ReducingSuccessorGenerator.h" -#include "PetriEngine/Extrapolator.h" +#include "PetriEngine/TokenEliminator.h" namespace PetriNets { class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph @@ -23,7 +23,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph using Condition = PetriEngine::PQL::Condition; using Condition_ptr = PetriEngine::PQL::Condition_ptr; using Marking = PetriEngine::Structures::State; - using Extrapolator = PetriEngine::Extrapolator; + using TokenEliminator = PetriEngine::TokenEliminator; OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order); virtual ~OnTheFlyDG(); @@ -47,7 +47,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph size_t configurationCount() const; size_t markingCount() const; size_t maxTokens() const; - size_t tokensExtrapolated() const; + size_t tokensEliminated() const; Condition::Result initialEval(); protected: @@ -58,8 +58,8 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph PetriConfig* initial_config; Marking working_marking; Marking query_marking; - Marking extrapolated_marking; - Extrapolator* extrapolator = nullptr; + Marking abstracted_marking; + TokenEliminator* token_elim = nullptr; uint32_t n_transitions = 0; uint32_t n_places = 0; size_t _markingCount = 0; diff --git a/include/PetriEngine/PetriNet.h b/include/PetriEngine/PetriNet.h index 08a285f58..0c54a4659 100644 --- a/include/PetriEngine/PetriNet.h +++ b/include/PetriEngine/PetriNet.h @@ -164,11 +164,7 @@ namespace PetriEngine { friend class ReducingSuccessorGenerator; friend class STSolver; friend class StubbornSet; - friend struct ExtrapolationContext; - friend class Extrapolator; - friend class AdaptiveExtrapolator; - friend class SimpleReachExtrapolator; - friend class DynamicReachExtrapolator; + friend class TokenEliminator; }; } // PetriEngine diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index ebabf232a..456afb88b 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -32,7 +32,7 @@ #include "PetriEngine/Stubborn/ReachabilityStubbornSet.h" #include "PetriEngine/options.h" -#include "PetriEngine/Extrapolator.h" +#include "PetriEngine/TokenEliminator.h" #include #include @@ -114,7 +114,7 @@ namespace PetriEngine { size_t _satisfyingMarking = 0; Structures::State _initial; AbstractHandler& _callback; - Extrapolator* extrapolator = nullptr; // FIXME: Leaked + TokenEliminator* token_elim = nullptr; // FIXME: Leaked size_t _max_tokens = 0; }; @@ -183,10 +183,10 @@ namespace PetriEngine { } if (queries.size() == 1 && usequeries) { - extrapolator = new Extrapolator(); - extrapolator->init(&_net, queries[0].get()); + token_elim = new TokenEliminator(); + token_elim->init(&_net, queries[0].get()); } else { - extrapolator = (new Extrapolator())->disable(); + token_elim = (new TokenEliminator())->disable(); } // Search! @@ -196,7 +196,7 @@ namespace PetriEngine { while(generator.next(working)){ ss.enabledTransitionsCount[generator.fired()]++; - extrapolator->extrapolate(&working, queries[ss.heurquery].get()); + 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/Extrapolator.h b/include/PetriEngine/TokenEliminator.h similarity index 61% rename from include/PetriEngine/Extrapolator.h rename to include/PetriEngine/TokenEliminator.h index 01bf2b37c..9a82af587 100644 --- a/include/PetriEngine/Extrapolator.h +++ b/include/PetriEngine/TokenEliminator.h @@ -1,5 +1,5 @@ -#ifndef VERIFYPN_EXTRAPOLATOR_H -#define VERIFYPN_EXTRAPOLATOR_H +#ifndef VERIFYPN_TOKENELIMINATOR_H +#define VERIFYPN_TOKENELIMINATOR_H #include @@ -21,24 +21,37 @@ namespace PetriEngine { const static uint8_t CAN_INC = 1 << 5; const static uint8_t CAN_DEC = 1 << 6; - class Extrapolator { + /** + * 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 ~Extrapolator() = default; + virtual ~TokenEliminator() = default; void init(const PetriNet *net, const Condition *query); - void extrapolate(Marking *marking, Condition *query); + void eliminate(Marking *marking, Condition *query); - [[nodiscard]] virtual size_t tokensExtrapolated() const { - return _tokensExtrapolated; + [[nodiscard]] virtual size_t tokensEliminated() const { + return _tokensEliminated; } - Extrapolator * disable() { + TokenEliminator * disable() { _enabled = false; return this; } - Extrapolator * setDynamic(bool dynamic) { + TokenEliminator * setDynamic(bool dynamic) { _doDynamic = dynamic; return this; } @@ -70,11 +83,11 @@ namespace PetriEngine { void findDeadPlacesAndTransitions(const PetriEngine::Marking *marking); - void extrapolateDynamicReachRelevance(PetriEngine::Marking *marking, PetriEngine::Condition *query); + void eliminateDynamic(PetriEngine::Marking * marking, PetriEngine::Condition * query); void findDynamicVisiblePlaces(PetriEngine::Condition *query); - void extrapolateStaticReachRelevance(PetriEngine::Marking *marking, PetriEngine::Condition *query); + void eliminateStatic(PetriEngine::Marking * marking, PetriEngine::Condition * query); const std::vector &findStaticVisiblePlaces(PetriEngine::Condition *query); @@ -97,8 +110,8 @@ namespace PetriEngine { std::vector _fireable; // === Statistics - size_t _tokensExtrapolated = 0; + size_t _tokensEliminated = 0; }; } -#endif //VERIFYPN_EXTRAPOLATOR_H +#endif //VERIFYPN_TOKENELIMINATOR_H diff --git a/src/CTL/CTLEngine.cpp b/src/CTL/CTLEngine.cpp index 3920d83fa..0002e1cf7 100644 --- a/src/CTL/CTLEngine.cpp +++ b/src/CTL/CTLEngine.cpp @@ -71,7 +71,7 @@ bool CTLSingleSolve(Condition* query, PetriNet* net, result.processedNegationEdges += alg->processedNegationEdges(); result.exploredConfigurations += alg->exploredConfigurations(); result.numberOfEdges += alg->numberOfEdges(); - result.tokensExtrapolated = graph.tokensExtrapolated(); + result.tokensEliminated = graph.tokensEliminated(); result.maxTokens = std::max(graph.maxTokens(), result.maxTokens); return res; } diff --git a/src/CTL/CTLResult.cpp b/src/CTL/CTLResult.cpp index fff65c6c9..356fa6418 100644 --- a/src/CTL/CTLResult.cpp +++ b/src/CTL/CTLResult.cpp @@ -28,7 +28,7 @@ void CTLResult::print(const std::string& qname, StatisticsLevel statisticslevel, out << " Processed Edges : " << processedEdges << "\n"; out << " Processed N. Edges : " << processedNegationEdges << "\n"; out << " Explored Configs : " << exploredConfigurations << "\n"; - out << " Tokens Extrapolated : " << tokensExtrapolated << "\n"; + out << " Tokens Eliminated : " << tokensEliminated << "\n"; out << " max tokens: : " << maxTokens << "\n"; // kept lower case to be compatible with reachability format } out << std::endl; diff --git a/src/CTL/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index edf687534..980297bbf 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -26,7 +26,7 @@ OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encod net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); - extrapolator = new Extrapolator(); + token_elim = new TokenEliminator(); } @@ -42,7 +42,7 @@ OnTheFlyDG::~OnTheFlyDG() } delete conf_alloc; delete edge_alloc; - delete extrapolator; + delete token_elim; } Condition::Result OnTheFlyDG::initialEval() @@ -521,7 +521,7 @@ Configuration* OnTheFlyDG::initialConfiguration() { working_marking.setMarking(net->makeInitialMarking()); query_marking.setMarking(net->makeInitialMarking()); - extrapolated_marking.setMarking(net->makeInitialMarking()); + abstracted_marking.setMarking(net->makeInitialMarking()); auto o = owner(working_marking, this->query); initial_config = createConfiguration(working_marking, o, this->query); } @@ -589,11 +589,11 @@ void OnTheFlyDG::setQuery(Condition* query) this->query = query; delete[] working_marking.marking(); delete[] query_marking.marking(); - delete[] extrapolated_marking.marking(); + delete[] abstracted_marking.marking(); working_marking.setMarking(nullptr); query_marking.setMarking(nullptr); - extrapolated_marking.setMarking(nullptr); - extrapolator->init(net, query); + abstracted_marking.setMarking(nullptr); + token_elim->init(net, query); initialConfiguration(); assert(this->query); } @@ -612,16 +612,16 @@ size_t OnTheFlyDG::maxTokens() const { return _maxTokens; } -size_t OnTheFlyDG::tokensExtrapolated() const { - return extrapolator->tokensExtrapolated(); +size_t OnTheFlyDG::tokensEliminated() const { + return token_elim->tokensEliminated(); } PetriConfig *OnTheFlyDG::createConfiguration(const Marking& marking, size_t own, Condition* t_query) { - extrapolated_marking.copy(marking.marking(), n_places); - extrapolator->extrapolate(&extrapolated_marking, t_query); + abstracted_marking.copy(marking.marking(), n_places); + token_elim->eliminate(&abstracted_marking, t_query); - size_t encoded = createMarking(extrapolated_marking); + size_t encoded = createMarking(abstracted_marking); auto& configs = trie.get_data(encoded); for(PetriConfig* c : configs){ if(c->query == t_query) diff --git a/src/PetriEngine/CMakeLists.txt b/src/PetriEngine/CMakeLists.txt index 316cd01d5..fc14e44e6 100644 --- a/src/PetriEngine/CMakeLists.txt +++ b/src/PetriEngine/CMakeLists.txt @@ -17,7 +17,7 @@ add_library(PetriEngine ${HEADER_FILES} STSolver.cpp SuccessorGenerator.cpp TraceReplay.cpp - Extrapolator.cpp + TokenEliminator.cpp options.cpp) target_link_libraries(PetriEngine PRIVATE Colored ColoredReduction Structures Simplification Stubborn Reachability PQL TAR Synthesis) diff --git a/src/PetriEngine/Reachability/ReachabilitySearch.cpp b/src/PetriEngine/Reachability/ReachabilitySearch.cpp index 8a99451c4..c5b1e8722 100644 --- a/src/PetriEngine/Reachability/ReachabilitySearch.cpp +++ b/src/PetriEngine/Reachability/ReachabilitySearch.cpp @@ -91,11 +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 - << "\tTokens Extrapolated: " << extrapolator->tokensExtrapolated() << 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) diff --git a/src/PetriEngine/Extrapolator.cpp b/src/PetriEngine/TokenEliminator.cpp similarity index 94% rename from src/PetriEngine/Extrapolator.cpp rename to src/PetriEngine/TokenEliminator.cpp index fd9685d98..7bd4c99a6 100644 --- a/src/PetriEngine/Extrapolator.cpp +++ b/src/PetriEngine/TokenEliminator.cpp @@ -1,5 +1,5 @@ #include -#include "PetriEngine/Extrapolator.h" +#include "PetriEngine/TokenEliminator.h" #include "PetriEngine/PQL/PlaceUseVisitor.h" #include "PetriEngine/PQL/PredicateCheckers.h" namespace PetriEngine { @@ -124,13 +124,13 @@ namespace PetriEngine { uint8_t direction = 0; }; - void Extrapolator::init(const PetriNet *net, const Condition *query) { + void TokenEliminator::init(const PetriNet *net, const Condition *query) { _net = net; setupProducersAndConsumers(); setupExtBounds(); } - void Extrapolator::setupProducersAndConsumers() { + void TokenEliminator::setupProducersAndConsumers() { _inhibpost.resize(0); _inhibpost.resize(_net->_nplaces); std::vector, std::vector>> tmp_places(_net->_nplaces); @@ -191,7 +191,7 @@ namespace PetriEngine { _prodcons[p].consumers = offset; } - void Extrapolator::setupExtBounds() { + void TokenEliminator::setupExtBounds() { _extBounds.assign(_net->_nplaces, 0); for (uint32_t i = 0; i < _net->_ntransitions; ++i) { uint32_t finv = _net->_transitions[i].inputs; @@ -206,25 +206,25 @@ namespace PetriEngine { } } - std::pair Extrapolator::producers(uint32_t p) const { + 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 Extrapolator::consumers(uint32_t p) const { + std::pair TokenEliminator::consumers(uint32_t p) const { return std::make_pair(&_parcs[_prodcons[p].consumers], &_parcs[_prodcons[p + 1].producers]); } - void Extrapolator::extrapolate(Marking *marking, Condition *query) { + void TokenEliminator::eliminate(Marking *marking, Condition *query) { if (!_enabled) return; if (_doDynamic) { - extrapolateDynamicReachRelevance(marking, query); + eliminateDynamic(marking, query); } else { - extrapolateStaticReachRelevance(marking, query); + eliminateStatic(marking, query); } } - void Extrapolator::findDeadPlacesAndTransitions(const Marking *marking) { + void TokenEliminator::findDeadPlacesAndTransitions(const Marking *marking) { _pflags.resize(_net->_nplaces); std::fill(_pflags.begin(), _pflags.end(), 0); @@ -311,7 +311,7 @@ namespace PetriEngine { } } - void Extrapolator::extrapolateDynamicReachRelevance(Marking *marking, Condition *query) { + void TokenEliminator::eliminateDynamic(Marking * marking, Condition * query) { if (PQL::isLoopSensitive(query->shared_from_this()) || !PQL::isReachability(query)) { return; @@ -333,10 +333,10 @@ namespace PetriEngine { 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) { - // Extrapolating below the upper bound may introduce behaviour + // Going below the upper bound may introduce behaviour uint32_t cur = marking->marking()[i]; uint32_t ex = std::min(cur, _extBounds[i]); - _tokensExtrapolated += cur - ex; + _tokensEliminated += cur - ex; marking->marking()[i] = ex; } } @@ -374,7 +374,7 @@ namespace PetriEngine { } } - void Extrapolator::findDynamicVisiblePlaces(Condition *query) { + void TokenEliminator::findDynamicVisiblePlaces(Condition *query) { PlaceReachabilityDirectionVisitor pv(_net->numberOfPlaces()); PQL::Visitor::visit(&pv, query); @@ -479,7 +479,7 @@ namespace PetriEngine { } } - void Extrapolator::extrapolateStaticReachRelevance(Marking *marking, Condition *query) { + void TokenEliminator::eliminateStatic(Marking * marking, Condition * query) { const std::vector *visible; auto it = _cache.find(query); if (it != _cache.end()) { @@ -491,17 +491,17 @@ namespace PetriEngine { if (!visible->empty()) { for (uint32_t i = 0; i < _net->_nplaces; ++i) { if (!(*visible)[i]) { - // Extrapolating below the upper bound may introduce behaviour + // Going below below the upper bound may introduce behaviour uint32_t cur = marking->marking()[i]; uint32_t ex = std::min(cur, _extBounds[i]); - _tokensExtrapolated += cur - ex; + _tokensEliminated += cur - ex; marking->marking()[i] = ex; } } } } - const std::vector &Extrapolator::findStaticVisiblePlaces(Condition *query) { + 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())); From 433ed4f77141fab1c7ceaa1a50e8a4d2a3a5f28a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 21 Jan 2025 10:06:33 +0100 Subject: [PATCH 24/29] Add separate --token-elim cmd args for CTl and reachability --- include/CTL/CTLEngine.h | 1 + include/CTL/PetriNets/OnTheFlyDG.h | 4 +-- .../Reachability/ReachabilitySearch.h | 15 +++++---- include/PetriEngine/TokenEliminator.h | 4 +-- include/PetriEngine/options.h | 8 +++++ src/CTL/CTLEngine.cpp | 10 ++++-- src/CTL/PetriNets/OnTheFlyDG.cpp | 12 +++---- .../Reachability/ReachabilitySearch.cpp | 5 +-- src/PetriEngine/options.cpp | 33 +++++++++++++++++++ src/main.cpp | 8 +++-- 10 files changed, 77 insertions(+), 23 deletions(-) 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/PetriNets/OnTheFlyDG.h b/include/CTL/PetriNets/OnTheFlyDG.h index 9684c8e82..e410314c2 100644 --- a/include/CTL/PetriNets/OnTheFlyDG.h +++ b/include/CTL/PetriNets/OnTheFlyDG.h @@ -24,7 +24,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph using Condition_ptr = PetriEngine::PQL::Condition_ptr; using Marking = PetriEngine::Structures::State; using TokenEliminator = PetriEngine::TokenEliminator; - OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order); + OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order, TokenEliminator& token_elim); virtual ~OnTheFlyDG(); @@ -59,7 +59,7 @@ class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph Marking working_marking; Marking query_marking; Marking abstracted_marking; - TokenEliminator* token_elim = nullptr; + TokenEliminator& token_elim; uint32_t n_transitions = 0; uint32_t n_places = 0; size_t _markingCount = 0; diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index 456afb88b..561f65d38 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -66,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 { @@ -95,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); @@ -133,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 @@ -182,11 +184,12 @@ namespace PetriEngine { queue.push(r.second, &dc, queries[ss.heurquery].get()); } - if (queries.size() == 1 && usequeries) { - token_elim = new TokenEliminator(); + token_elim = new TokenEliminator(); + if (queries.size() == 1 && usequeries && tokenElim != TokenEliminationMethod::Disabled) { + token_elim->setDynamic(tokenElim == TokenEliminationMethod::Dynamic); token_elim->init(&_net, queries[0].get()); } else { - token_elim = (new TokenEliminator())->disable(); + token_elim->setEnabled(false); } // Search! diff --git a/include/PetriEngine/TokenEliminator.h b/include/PetriEngine/TokenEliminator.h index 9a82af587..9e6e5fa9f 100644 --- a/include/PetriEngine/TokenEliminator.h +++ b/include/PetriEngine/TokenEliminator.h @@ -46,8 +46,8 @@ namespace PetriEngine { return _tokensEliminated; } - TokenEliminator * disable() { - _enabled = false; + TokenEliminator * setEnabled(bool enabled) { + _enabled = enabled; return this; } 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/CTLEngine.cpp b/src/CTL/CTLEngine.cpp index 0002e1cf7..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); @@ -316,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, @@ -327,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/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index 980297bbf..820978ba2 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -19,14 +19,13 @@ 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), 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) { + _redgen(*t_net, std::make_shared(*t_net)), _partial_order(partial_order), token_elim(token_elim) { net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); - token_elim = new TokenEliminator(); } @@ -42,7 +41,6 @@ OnTheFlyDG::~OnTheFlyDG() } delete conf_alloc; delete edge_alloc; - delete token_elim; } Condition::Result OnTheFlyDG::initialEval() @@ -593,7 +591,7 @@ void OnTheFlyDG::setQuery(Condition* query) working_marking.setMarking(nullptr); query_marking.setMarking(nullptr); abstracted_marking.setMarking(nullptr); - token_elim->init(net, query); + token_elim.init(net, query); initialConfiguration(); assert(this->query); } @@ -613,13 +611,13 @@ size_t OnTheFlyDG::maxTokens() const { } size_t OnTheFlyDG::tokensEliminated() const { - return token_elim->tokensEliminated(); + return token_elim.tokensEliminated(); } PetriConfig *OnTheFlyDG::createConfiguration(const Marking& marking, size_t own, Condition* t_query) { abstracted_marking.copy(marking.marking(), n_places); - token_elim->eliminate(&abstracted_marking, t_query); + token_elim.eliminate(&abstracted_marking, t_query); size_t encoded = createMarking(abstracted_marking); auto& configs = trie.get_data(encoded); diff --git a/src/PetriEngine/Reachability/ReachabilitySearch.cpp b/src/PetriEngine/Reachability/ReachabilitySearch.cpp index c5b1e8722..14644aa2d 100644 --- a/src/PetriEngine/Reachability/ReachabilitySearch.cpp +++ b/src/PetriEngine/Reachability/ReachabilitySearch.cpp @@ -128,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) \ @@ -155,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/options.cpp b/src/PetriEngine/options.cpp index 8620fca66..854c198ca 100644 --- a/src/PetriEngine/options.cpp +++ b/src/PetriEngine/options.cpp @@ -206,6 +206,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 +643,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 7eb5231bb..44c6171a0 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -396,6 +396,7 @@ int main(int argc, const char** argv) { options.strategy, options.printstatistics, options.stubbornreduction, + options.tokenElimMethodCTL, querynames, queries, ctl_ids, @@ -543,7 +544,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, @@ -553,7 +555,9 @@ int main(int argc, const char** argv) { options.trace != TraceLevel::None, options.seed(), options.depthRandomWalk, - options.incRandomWalk); + options.incRandomWalk, + std::vector(), + options.tokenElimMethodReach); } } } From 48f2cdb969391fddecb3d05eb0851e8cda3b6536 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 21 Jan 2025 10:39:20 +0100 Subject: [PATCH 25/29] Add a few more comments + clean up --- .../Reachability/ReachabilitySearch.h | 4 ++-- include/PetriEngine/TokenEliminator.h | 13 ++++++++---- src/CTL/PetriNets/OnTheFlyDG.cpp | 5 +++-- src/PetriEngine/TokenEliminator.cpp | 21 +++++++++++++------ src/PetriEngine/options.cpp | 15 +++++++++++++ 5 files changed, 44 insertions(+), 14 deletions(-) diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index 561f65d38..2c4589f41 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -185,9 +185,9 @@ namespace PetriEngine { } token_elim = new TokenEliminator(); - if (queries.size() == 1 && usequeries && tokenElim != TokenEliminationMethod::Disabled) { + if (usequeries && tokenElim != TokenEliminationMethod::Disabled) { token_elim->setDynamic(tokenElim == TokenEliminationMethod::Dynamic); - token_elim->init(&_net, queries[0].get()); + token_elim->init(&_net); } else { token_elim->setEnabled(false); } diff --git a/include/PetriEngine/TokenEliminator.h b/include/PetriEngine/TokenEliminator.h index 9e6e5fa9f..ccb682bc4 100644 --- a/include/PetriEngine/TokenEliminator.h +++ b/include/PetriEngine/TokenEliminator.h @@ -38,7 +38,7 @@ namespace PetriEngine { public: virtual ~TokenEliminator() = default; - void init(const PetriNet *net, const Condition *query); + void init(const PetriNet *net); void eliminate(Marking *marking, Condition *query); @@ -74,6 +74,7 @@ namespace PetriEngine { }; private: + /** Built data structure that makes it faster to go from places to transitions */ void setupProducersAndConsumers(); void setupExtBounds(); @@ -81,21 +82,25 @@ namespace PetriEngine { [[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 = std::getenv("TAPAAL_TOKEN_ELIM") != nullptr; - bool _doDynamic = std::getenv("TAPAAL_TOKEN_ELIM_STATIC") == nullptr; - bool _env_TOKEN_ELIM_DEBUG = std::getenv("TAPAAL_TOKEN_ELIM_DEBUG") != nullptr; + bool _enabled = true; + bool _doDynamic = false; + bool _env_TOKEN_ELIM_DEBUG = false; //std::getenv("TAPAAL_TOKEN_ELIM_DEBUG") != nullptr; // === Net PetriNet const *_net; diff --git a/src/CTL/PetriNets/OnTheFlyDG.cpp b/src/CTL/PetriNets/OnTheFlyDG.cpp index 820978ba2..1f9d3a7d3 100644 --- a/src/CTL/PetriNets/OnTheFlyDG.cpp +++ b/src/CTL/PetriNets/OnTheFlyDG.cpp @@ -20,9 +20,10 @@ using namespace DependencyGraph; namespace PetriNets { 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), token_elim(token_elim) { + _redgen(*t_net, std::make_shared(*t_net)), _partial_order(partial_order) { net = t_net; n_places = t_net->numberOfPlaces(); n_transitions = t_net->numberOfTransitions(); @@ -591,7 +592,7 @@ void OnTheFlyDG::setQuery(Condition* query) working_marking.setMarking(nullptr); query_marking.setMarking(nullptr); abstracted_marking.setMarking(nullptr); - token_elim.init(net, query); + token_elim.init(net); initialConfiguration(); assert(this->query); } diff --git a/src/PetriEngine/TokenEliminator.cpp b/src/PetriEngine/TokenEliminator.cpp index 7bd4c99a6..360da8588 100644 --- a/src/PetriEngine/TokenEliminator.cpp +++ b/src/PetriEngine/TokenEliminator.cpp @@ -3,6 +3,12 @@ #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) {} @@ -124,7 +130,8 @@ namespace PetriEngine { uint8_t direction = 0; }; - void TokenEliminator::init(const PetriNet *net, const Condition *query) { + void TokenEliminator::init(const PetriNet *net) { + _cache.clear(); _net = net; setupProducersAndConsumers(); setupExtBounds(); @@ -324,10 +331,6 @@ namespace PetriEngine { } } - if (before.str() == "00110000000010000000000000001100000000000000000000000101000000001") { - std::cout << "Debugging\n"; - } - findDeadPlacesAndTransitions(marking); findDynamicVisiblePlaces(query); @@ -382,6 +385,7 @@ namespace PetriEngine { 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]; @@ -395,6 +399,7 @@ namespace PetriEngine { } } + // Propagate visibility while (!queue.empty()) { uint32_t p = queue.front(); queue.pop(); @@ -425,6 +430,7 @@ namespace PetriEngine { } } + // 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 @@ -491,7 +497,7 @@ namespace PetriEngine { if (!visible->empty()) { for (uint32_t i = 0; i < _net->_nplaces; ++i) { if (!(*visible)[i]) { - // Going below below the upper bound may introduce behaviour + // 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; @@ -516,6 +522,7 @@ namespace PetriEngine { 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; @@ -524,6 +531,7 @@ namespace PetriEngine { } } + // Propagate visibility while (!queue.empty()) { uint32_t p = queue.back(); queue.pop_back(); @@ -554,6 +562,7 @@ namespace PetriEngine { } } + // 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 diff --git a/src/PetriEngine/options.cpp b/src/PetriEngine/options.cpp index 854c198ca..345a1a8d0 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) { From bf3415b8ea3d8187ef610fccf555b51676c3f8b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 21 Jan 2025 10:44:28 +0100 Subject: [PATCH 26/29] Add file headers --- include/PetriEngine/TokenEliminator.h | 5 +++++ src/PetriEngine/TokenEliminator.cpp | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/include/PetriEngine/TokenEliminator.h b/include/PetriEngine/TokenEliminator.h index ccb682bc4..fbd82958b 100644 --- a/include/PetriEngine/TokenEliminator.h +++ b/include/PetriEngine/TokenEliminator.h @@ -1,3 +1,8 @@ +/** + * Original author(s): + * Nicolaj Ø. Jensen + */ + #ifndef VERIFYPN_TOKENELIMINATOR_H #define VERIFYPN_TOKENELIMINATOR_H diff --git a/src/PetriEngine/TokenEliminator.cpp b/src/PetriEngine/TokenEliminator.cpp index 360da8588..db9a75fec 100644 --- a/src/PetriEngine/TokenEliminator.cpp +++ b/src/PetriEngine/TokenEliminator.cpp @@ -1,7 +1,13 @@ +/** + * 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 From a72d3df438f954395ec1b496a181c60f404cb235 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 21 Jan 2025 13:36:10 +0100 Subject: [PATCH 27/29] Extra clean up --- include/PetriEngine/Reachability/ReachabilitySearch.h | 11 +++++------ src/PetriEngine/CMakeLists.txt | 2 +- src/main.cpp | 8 -------- 3 files changed, 6 insertions(+), 15 deletions(-) diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index 2c4589f41..d424f2b9c 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -116,7 +116,6 @@ namespace PetriEngine { size_t _satisfyingMarking = 0; Structures::State _initial; AbstractHandler& _callback; - TokenEliminator* token_elim = nullptr; // FIXME: Leaked size_t _max_tokens = 0; }; @@ -184,12 +183,12 @@ namespace PetriEngine { queue.push(r.second, &dc, queries[ss.heurquery].get()); } - token_elim = new TokenEliminator(); + TokenEliminator token_elim; if (usequeries && tokenElim != TokenEliminationMethod::Disabled) { - token_elim->setDynamic(tokenElim == TokenEliminationMethod::Dynamic); - token_elim->init(&_net); + token_elim.setDynamic(tokenElim == TokenEliminationMethod::Dynamic); + token_elim.init(&_net); } else { - token_elim->setEnabled(false); + token_elim.setEnabled(false); } // Search! @@ -199,7 +198,7 @@ namespace PetriEngine { while(generator.next(working)){ ss.enabledTransitionsCount[generator.fired()]++; - token_elim->eliminate(&working, queries[ss.heurquery].get()); + 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/src/PetriEngine/CMakeLists.txt b/src/PetriEngine/CMakeLists.txt index fc14e44e6..064883120 100644 --- a/src/PetriEngine/CMakeLists.txt +++ b/src/PetriEngine/CMakeLists.txt @@ -17,7 +17,7 @@ add_library(PetriEngine ${HEADER_FILES} STSolver.cpp SuccessorGenerator.cpp TraceReplay.cpp - TokenEliminator.cpp + TokenEliminator.cpp options.cpp) target_link_libraries(PetriEngine PRIVATE Colored ColoredReduction Structures Simplification Stubborn Reachability PQL TAR Synthesis) diff --git a/src/main.cpp b/src/main.cpp index 44c6171a0..2362a31c5 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -93,14 +93,6 @@ int main(int argc, const char** argv) { std::cout << "Finished parsing model" << std::endl; } - auto workStart = std::chrono::high_resolution_clock::now(); - // When this ptr goes out of scope it will print the time spent - std::shared_ptr defer (nullptr, [&workStart](...){ - auto workEnd = std::chrono::high_resolution_clock::now(); - auto diff = std::chrono::duration_cast(workEnd - workStart).count() / 1000000.0; - std::cout << std::setprecision(6) << "Spent " << diff << " in total" << std::endl; - }); - //----------------------- Parse Query -----------------------// std::vector querynames; auto ctlStarQueries = readQueries(string_set, options, querynames); From dc82a1a5a918276e8fae402efef093eba6feb6bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 21 Jan 2025 14:14:27 +0100 Subject: [PATCH 28/29] Fix compilation issue --- include/PetriEngine/Reachability/ReachabilitySearch.h | 11 ++++------- src/PetriEngine/Reachability/ReachabilitySearch.cpp | 2 +- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/include/PetriEngine/Reachability/ReachabilitySearch.h b/include/PetriEngine/Reachability/ReachabilitySearch.h index d424f2b9c..a2a3a0651 100644 --- a/include/PetriEngine/Reachability/ReachabilitySearch.h +++ b/include/PetriEngine/Reachability/ReachabilitySearch.h @@ -117,6 +117,7 @@ namespace PetriEngine { Structures::State _initial; AbstractHandler& _callback; size_t _max_tokens = 0; + TokenEliminator token_elim{}; }; template @@ -183,13 +184,9 @@ namespace PetriEngine { queue.push(r.second, &dc, queries[ss.heurquery].get()); } - TokenEliminator token_elim; - if (usequeries && tokenElim != TokenEliminationMethod::Disabled) { - token_elim.setDynamic(tokenElim == TokenEliminationMethod::Dynamic); - token_elim.init(&_net); - } else { - token_elim.setEnabled(false); - } + 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()) { diff --git a/src/PetriEngine/Reachability/ReachabilitySearch.cpp b/src/PetriEngine/Reachability/ReachabilitySearch.cpp index 14644aa2d..4b5852be4 100644 --- a/src/PetriEngine/Reachability/ReachabilitySearch.cpp +++ b/src/PetriEngine/Reachability/ReachabilitySearch.cpp @@ -95,7 +95,7 @@ namespace PetriEngine { << "\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 + << "\tTokens Eliminated: " << token_elim.tokensEliminated() << std::endl << "\tmax tokens: " << states->maxTokens() << std::endl; if (statisticsLevel != StatisticsLevel::Full) From 8781cdd00cfb125843dd81b920a6fbc46f6ea041 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 24 Jan 2025 08:42:13 +0100 Subject: [PATCH 29/29] Try fix github action --- .github/workflows/build-linux.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml index 3692c10cd..cdd34bf63 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