Merge lp:~tapaal-ltl/verifypn/reach-stub-new into lp:verifypn

Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 284
Merged at revision: 252
Proposed branch: lp:~tapaal-ltl/verifypn/reach-stub-new
Merge into: lp:verifypn
Diff against target: 6145 lines (+1333/-1200)
29 files modified
CMakeLists.txt (+1/-1)
include/LTL/Algorithm/ModelChecker.h (+37/-33)
include/LTL/Algorithm/NestedDepthFirstSearch.h (+29/-34)
include/LTL/Algorithm/TarjanModelChecker.h (+32/-34)
include/LTL/LTLMain.h (+5/-4)
include/LTL/Structures/BitProductStateSet.h (+4/-4)
include/LTL/Structures/ProductState.h (+9/-1)
include/LTL/Structures/ProductStateFactory.h (+4/-3)
include/LTL/Stubborn/SafeAutStubbornSet.h (+22/-5)
include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h (+1/-1)
include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h (+8/-6)
include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h (+27/-9)
include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h (+74/-81)
include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h (+27/-16)
include/PetriEngine/Reducer.h (+21/-21)
include/PetriEngine/Structures/StateSet.h (+5/-33)
include/PetriEngine/Structures/light_deque.h (+83/-24)
include/PetriEngine/SuccessorGenerator.h (+4/-4)
src/LTL/Algorithm/NestedDepthFirstSearch.cpp (+124/-124)
src/LTL/Algorithm/TarjanModelChecker.cpp (+107/-86)
src/LTL/LTLMain.cpp (+29/-63)
src/LTL/Stubborn/AutomatonStubbornSet.cpp (+1/-1)
src/LTL/Stubborn/SafeAutStubbornSet.cpp (+57/-9)
src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp (+2/-2)
src/PetriEngine/PQL/Expressions.cpp (+403/-414)
src/PetriEngine/Reducer.cpp (+160/-157)
src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp (+23/-1)
src/PetriEngine/TraceReplay.cpp (+4/-4)
src/VerifyPN.cpp (+30/-25)
To merge this branch: bzr merge lp:~tapaal-ltl/verifypn/reach-stub-new
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+409596@code.launchpad.net

Commit message

Adds POR for LTL, improves performance of NDFS.

Passes regression on MCC21 models using competition script.

To post a comment you must log in.
279. By Nikolaj Jensen Ulrik

Probably properly fixed k-bounds in NDFS. Fixes https://bugs.launchpad.net/tapaal/+bug/1947036

280. By Nikolaj Jensen Ulrik

LTL Query simplification more robust against queries without leading A/E quantifier.

281. By Nikolaj Jensen Ulrik

Fixing infinite loop in Tarjan trace generation

282. By Peter G. Jensen <email address hidden>

avoiding double-addition of extra-consume during ruleB trace reconstruction

283. By Nikolaj Jensen Ulrik

extraConsume in the right place

284. By <email address hidden>

increased version number to 4.2.0

Revision history for this message
Jiri Srba (srba) wrote :

Merging to trunk now - small issue with loop at the end in once case but let's address this in 3.9.1 release.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'CMakeLists.txt'
--- CMakeLists.txt 2021-08-11 09:06:51 +0000
+++ CMakeLists.txt 2021-10-17 18:21:15 +0000
@@ -15,7 +15,7 @@
15set(CMAKE_POSITION_INDEPENDENT_CODE ON)15set(CMAKE_POSITION_INDEPENDENT_CODE ON)
1616
1717
18set(VERIFYPN_VERSION 4.1.0)18set(VERIFYPN_VERSION 4.2.0)
19add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")19add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")
2020
21project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)21project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)
2222
=== modified file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h 2021-08-06 09:34:01 +0000
+++ include/LTL/Algorithm/ModelChecker.h 2021-10-17 18:21:15 +0000
@@ -25,7 +25,9 @@
25#include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"25#include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"
26#include "LTL/Structures/BitProductStateSet.h"26#include "LTL/Structures/BitProductStateSet.h"
27#include "LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h"27#include "LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h"
28#include "LTL/Structures/ProductStateFactory.h"
28#include "PetriEngine/options.h"29#include "PetriEngine/options.h"
30#include "PetriEngine/Reducer.h"
2931
30#include <iomanip>32#include <iomanip>
31#include <algorithm>33#include <algorithm>
@@ -37,11 +39,14 @@
37 ModelChecker(const PetriEngine::PetriNet *net,39 ModelChecker(const PetriEngine::PetriNet *net,
38 const PetriEngine::PQL::Condition_ptr &condition,40 const PetriEngine::PQL::Condition_ptr &condition,
39 const Structures::BuchiAutomaton &buchi,41 const Structures::BuchiAutomaton &buchi,
40 SuccessorGen *successorGen,42 SuccessorGen *successorGen, const PetriEngine::Reducer* reducer,
41 std::unique_ptr<Spooler> &&...spooler)43 std::unique_ptr<Spooler> &&...spooler)
42 : net(net), formula(condition)44 : net(net), formula(condition), _reducer(reducer), successorGenerator(
45 std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen,
46 std::move(spooler)...)),
47 _factory(net, buchi, this->successorGenerator->initial_buchi_state())
43 {48 {
44 successorGenerator = std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen, std::move(spooler)...);49// successorGenerator = std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen, std::move(spooler)...);
45 }50 }
4651
47 void setOptions(const options_t &options) {52 void setOptions(const options_t &options) {
@@ -81,11 +86,14 @@
81 << "\tmax tokens: " << stateSet.max_tokens() << std::endl;86 << "\tmax tokens: " << stateSet.max_tokens() << std::endl;
82 }87 }
8388
89 const PetriEngine::Reducer* _reducer;
84 std::unique_ptr<ProductSucGen<SuccessorGen, Spooler...>> successorGenerator;90 std::unique_ptr<ProductSucGen<SuccessorGen, Spooler...>> successorGenerator;
8591
86 const PetriEngine::PetriNet *net;92 const PetriEngine::PetriNet *net;
87 PetriEngine::PQL::Condition_ptr formula;93 PetriEngine::PQL::Condition_ptr formula;
94 //const Structures::BuchiAutomaton *_aut;
88 TraceLevel traceLevel;95 TraceLevel traceLevel;
96 LTL::Structures::ProductStateFactory _factory;
8997
90 size_t _discovered = 0;98 size_t _discovered = 0;
91 bool shortcircuitweak;99 bool shortcircuitweak;
@@ -102,41 +110,37 @@
102 }110 }
103111
104 std::ostream &112 std::ostream &
105 printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os)113 printTransition(size_t transition, std::ostream &os, const LTL::Structures::ProductState* state = nullptr)
106 {114 {
107 if (transition >= std::numeric_limits<ptrie::uint>::max() - 1) {115 if (transition >= std::numeric_limits<ptrie::uint>::max() - 1) {
108 os << indent << "<deadlock/>";116 os << indent << "<deadlock/>";
109 return os;117 return os;
110 }118 }
111 os << indent << "<transition id="119 os << indent << "<transition id="
112 // field width stuff obsolete without büchi state printing.120 // field width stuff obsolete without büchi state printing.
113 //<< std::setw(maxTransName + 2) << std::left121 << std::quoted(net->transitionNames()[transition]);
114 << std::quoted(net->transitionNames()[transition]);122 os << ">";
115 if (traceLevel == TraceLevel::Full) {123 if(_reducer) {
116 os << ">";124 _reducer->extraConsume(os, net->transitionNames()[transition]);
117 os << std::endl;125 }
118 auto [fpre, lpre] = net->preset(transition);126 os << std::endl;
119 for(; fpre < lpre; ++fpre) {127 auto [fpre, lpre] = net->preset(transition);
120 if (fpre->inhibitor) {128 for(; fpre < lpre; ++fpre) {
121 assert(state.marking()[fpre->place] < fpre->tokens);129 if (fpre->inhibitor) {
122 continue;130 assert(state == nullptr || state->marking()[fpre->place] < fpre->tokens);
123 }131 continue;
124 for (size_t i = 0; i < fpre->tokens; ++i) {132 }
125 assert(state.marking()[fpre->place] >= fpre->tokens);133 for (size_t i = 0; i < fpre->tokens; ++i) {
126 os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[fpre->place] << "\"/>\n";134 assert(state == nullptr || state->marking()[fpre->place] >= fpre->tokens);
127 }135 os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[fpre->place] << "\"/>\n";
128 }136 }
129 /*for (size_t i = 0; i < net->numberOfPlaces(); ++i) {137 }
130 for (size_t j = 0; j < state.marking()[i]; ++j) {138 os << indent << "</transition>\n";
131 os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[i] << "\"/>\n";139 if(_reducer)
132 }140 {
133 }*/141 _reducer->postFire(os, net->transitionNames()[transition]);
134 os << indent << "</transition>";142 }
135 }143 return os;
136 else {
137 os << "/>";
138 }
139 return os;
140 }144 }
141 };145 };
142}146}
143147
=== modified file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-08-10 13:44:22 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-10-17 18:21:15 +0000
@@ -22,12 +22,11 @@
22#include "PetriEngine/Structures/StateSet.h"22#include "PetriEngine/Structures/StateSet.h"
23#include "PetriEngine/Structures/State.h"23#include "PetriEngine/Structures/State.h"
24#include "PetriEngine/Structures/Queue.h"24#include "PetriEngine/Structures/Queue.h"
25#include "PetriEngine/Structures/light_deque.h"
25#include "LTL/Structures/ProductStateFactory.h"26#include "LTL/Structures/ProductStateFactory.h"
2627
27#include <ptrie/ptrie_stable.h>
28#include <unordered_set>
29
30namespace LTL {28namespace LTL {
29
31 /**30 /**
32 * Implement the nested DFS algorithm for LTL model checking. Roughly based on versions given in31 * Implement the nested DFS algorithm for LTL model checking. Roughly based on versions given in
33 * <p>32 * <p>
@@ -45,14 +44,13 @@
45 * @tparam W type used for state storage. Use <code>PetriEngine::Structures::TracableStateSet</code> if you want traces,44 * @tparam W type used for state storage. Use <code>PetriEngine::Structures::TracableStateSet</code> if you want traces,
46 * <code>PetriEngine::Structures::StateSet</code> if you don't care (as it is faster).45 * <code>PetriEngine::Structures::StateSet</code> if you don't care (as it is faster).
47 */46 */
48 template<typename SucGen, typename W>47 template<typename SucGen>
49class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {48 class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {
50 public:49 public:
51 NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,50 NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,
52 const Structures::BuchiAutomaton &buchi, SucGen *gen, int kbound)51 const Structures::BuchiAutomaton &buchi, SucGen *gen, const bool print_trace, int kbound, const PetriEngine::Reducer* reducer)
53 : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen),52 : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen, reducer),
54 factory{net, this->successorGenerator->initial_buchi_state()},53 _states(net, kbound), _print_trace(print_trace) {}
55 states(net, kbound) {}
5654
57 bool isSatisfied() override;55 bool isSatisfied() override;
5856
@@ -60,43 +58,40 @@
6058
61 private:59 private:
62 using State = LTL::Structures::ProductState;60 using State = LTL::Structures::ProductState;
6361 std::pair<bool,size_t> mark(State& state, uint8_t);
64 Structures::ProductStateFactory factory;62
65 W states; //StateSet63
66 std::set<size_t> mark1;64 LTL::Structures::BitProductStateSet<> _states;
67 std::set<size_t> mark2;65
66 std::unordered_map<size_t, uint8_t> _markers;
67 //std::vector<uint8_t> _markers;
68 static constexpr uint8_t MARKER1 = 1;
69 static constexpr uint8_t MARKER2 = 2;
70 size_t _mark_count[3] = {0,0,0};
6871
69 struct StackEntry {72 struct StackEntry {
70 size_t id;73 size_t _id;
71 typename SucGen::sucinfo sucinfo;74 typename SucGen::successor_info_t _sucinfo;
72 };75 };
7376
74 State *seed;77 bool _violation = false;
75 bool violation = false;78 const bool _print_trace = false;
7679
77 //Used for printing the trace80 //Used for printing the trace
78 std::stack<std::pair<size_t, size_t>> nested_transitions;81 std::stack<std::pair<size_t, size_t>> _nested_transitions;
7982
80 void dfs();83 void dfs();
8184
82 void ndfs(State &state);85 void ndfs(const State &state, light_deque<StackEntry>& nested_todo);
8386
84 void printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os = std::cout);87 void print_trace(light_deque<StackEntry>& todo, light_deque<StackEntry>& nested_todo, std::ostream &os = std::cout);
85
86 static constexpr bool SaveTrace = std::is_same_v<W, PetriEngine::Structures::TracableStateSet>;
87 };88 };
8889
89 extern template90 extern template
90 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;91 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator>;
9192
92 extern template93 extern template
93 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;94 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator>;
94
95 extern template
96 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
97
98 extern template
99 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
100}95}
10196
102#endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H97#endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H
10398
=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h 2021-08-10 13:44:22 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h 2021-10-17 18:21:15 +0000
@@ -49,62 +49,60 @@
49 TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,49 TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,
50 const Structures::BuchiAutomaton &buchi,50 const Structures::BuchiAutomaton &buchi,
51 SuccessorGen *successorGen,51 SuccessorGen *successorGen,
52 int kbound,52 int kbound, const PetriEngine::Reducer* reducer,
53 std::unique_ptr<Spooler> &&...spooler)53 std::unique_ptr<Spooler> &&...spooler)
54 : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, std::move(spooler)...),54 : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, reducer, std::move(spooler)...),
55 factory(net, this->successorGenerator->initial_buchi_state()),55 _seen(net, kbound)
56 seen(net, kbound)
57 {56 {
58 if (buchi._buchi->num_states() > 65535) {57 if (buchi._buchi->num_states() > 65535) {
59 std::cerr << "Fatal error: cannot handle Büchi automata larger than 2^16 states\n";58 std::cerr << "Fatal error: cannot handle Büchi automata larger than 2^16 states\n";
60 exit(1);59 exit(1);
61 }60 }
62 chash.fill(std::numeric_limits<idx_t>::max());61 _chash.fill(std::numeric_limits<idx_t>::max());
63 }62 }
6463
65 bool isSatisfied() override;64 bool isSatisfied() override;
6665
67 void printStats(std::ostream &os) override66 void printStats(std::ostream &os) override
68 {67 {
69 this->_printStats(os, seen);68 this->_printStats(os, _seen);
70 }69 }
7170
72 private:71 private:
73 using State = LTL::Structures::ProductState;72 using State = LTL::Structures::ProductState;
74 using idx_t = size_t;73 using idx_t = size_t;
75 // 64 MB hash table74 // 64 MB hash table
76 static constexpr idx_t HashSz = 16777216;75 static constexpr idx_t _hash_sz = 16777216;
7776
78 LTL::Structures::ProductStateFactory factory;
7977
80 using StateSet = std::conditional_t<SaveTrace, LTL::Structures::TraceableBitProductStateSet<>, LTL::Structures::BitProductStateSet<>>;78 using StateSet = std::conditional_t<SaveTrace, LTL::Structures::TraceableBitProductStateSet<>, LTL::Structures::BitProductStateSet<>>;
81 static constexpr bool IsSpooling = std::is_same_v<SuccessorGen, SpoolingSuccessorGenerator>;79 static constexpr bool _is_spooling = std::is_same_v<SuccessorGen, SpoolingSuccessorGenerator>;
8280
83 StateSet seen;81 StateSet _seen;
84 std::unordered_set<idx_t> store;82 std::unordered_set<idx_t> _store;
8583
86 // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack84 // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack
87 // corresponding to state. Collisions are resolved using linked list via CEntry::next.85 // corresponding to state. Collisions are resolved using linked list via CEntry::next.
88 std::array<idx_t, HashSz> chash;86 std::array<idx_t, _hash_sz> _chash;
89 static_assert(sizeof(chash) == (1U << 27U));87 static_assert(sizeof(_chash) == (1U << 27U));
9088
91 static inline idx_t hash(idx_t id)89 static inline idx_t hash(idx_t id)
92 {90 {
93 return id % HashSz;91 return id % _hash_sz;
94 }92 }
9593
96 struct PlainCEntry {94 struct PlainCEntry {
97 idx_t lowlink;95 idx_t _lowlink;
98 idx_t stateid;96 idx_t _stateid;
99 idx_t next = std::numeric_limits<idx_t>::max();97 idx_t _next = std::numeric_limits<idx_t>::max();
100 bool dstack = true;98 bool _dstack = true;
10199
102 PlainCEntry(idx_t lowlink, idx_t stateid, idx_t next) : lowlink(lowlink), stateid(stateid), next(next) {}100 PlainCEntry(idx_t lowlink, idx_t stateid, idx_t next) : _lowlink(lowlink), _stateid(stateid), _next(next) {}
103 };101 };
104102
105 struct TracableCEntry : PlainCEntry {103 struct TracableCEntry : PlainCEntry {
106 idx_t lowsource = std::numeric_limits<idx_t>::max();104 idx_t _lowsource = std::numeric_limits<idx_t>::max();
107 idx_t sourcetrans;105 idx_t _sourcetrans;
108106
109 TracableCEntry(idx_t lowlink, idx_t stateid, idx_t next) : PlainCEntry(lowlink, stateid, next) {}107 TracableCEntry(idx_t lowlink, idx_t stateid, idx_t next) : PlainCEntry(lowlink, stateid, next) {}
110 };108 };
@@ -114,24 +112,24 @@
114 PlainCEntry>;112 PlainCEntry>;
115113
116 struct DEntry {114 struct DEntry {
117 idx_t pos; // position in cstack.115 idx_t _pos; // position in cstack.
118116
119 typename SuccessorGen::sucinfo sucinfo;117 typename SuccessorGen::successor_info_t _sucinfo;
120118
121 explicit DEntry(idx_t pos) : pos(pos), sucinfo(SuccessorGen::initial_suc_info()) {}119 explicit DEntry(idx_t pos) : _pos(pos), _sucinfo(SuccessorGen::initial_suc_info()) {}
122 };120 };
123121
124 // master list of state information.122 // master list of state information.
125 std::vector<CEntry> cstack;123 std::vector<CEntry> _cstack;
126 // depth-first search stack, contains current search path.124 // depth-first search stack, contains current search path.
127 std::stack<DEntry> dstack;125 std::stack<DEntry> _dstack;
128 // cstack positions of accepting states in current search path, for quick access.126 // cstack positions of accepting states in current search path, for quick access.
129 std::stack<idx_t> astack;127 std::stack<idx_t> _astack;
130128
131 bool violation = false;129 bool _violation = false;
132 bool invariant_loop = true;130 bool _invariant_loop = true;
133 size_t loopstate = std::numeric_limits<size_t>::max();131 size_t _loop_state = std::numeric_limits<size_t>::max();
134 size_t looptrans = std::numeric_limits<size_t>::max();132 size_t _loop_trans = std::numeric_limits<size_t>::max();
135133
136 void push(State &state, size_t stateid);134 void push(State &state, size_t stateid);
137135
@@ -144,8 +142,8 @@
144 void popCStack();142 void popCStack();
145143
146 void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout);144 void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout);
147
148 };145 };
146
149 extern template147 extern template
150 class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, true>;148 class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, true>;
151149
152150
=== modified file 'include/LTL/LTLMain.h'
--- include/LTL/LTLMain.h 2021-08-03 12:00:44 +0000
+++ include/LTL/LTLMain.h 2021-10-17 18:21:15 +0000
@@ -1,16 +1,16 @@
1/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,1/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
2 * Simon M. Virenfeldt <simon@simwir.dk>2 * Simon M. Virenfeldt <simon@simwir.dk>
3 * 3 *
4 * This program is free software: you can redistribute it and/or modify4 * This program is free software: you can redistribute it and/or modify
5 * it under the terms of the GNU General Public License as published by5 * it under the terms of the GNU General Public License as published by
6 * the Free Software Foundation, either version 3 of the License, or6 * the Free Software Foundation, either version 3 of the License, or
7 * (at your option) any later version.7 * (at your option) any later version.
8 * 8 *
9 * This program is distributed in the hope that it will be useful,9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.12 * GNU General Public License for more details.
13 * 13 *
14 * You should have received a copy of the GNU General Public License14 * You should have received a copy of the GNU General Public License
15 * along with this program. If not, see <http://www.gnu.org/licenses/>.15 * along with this program. If not, see <http://www.gnu.org/licenses/>.
16 */16 */
@@ -26,7 +26,8 @@
26 bool LTLMain(const PetriEngine::PetriNet *net,26 bool LTLMain(const PetriEngine::PetriNet *net,
27 const PetriEngine::PQL::Condition_ptr &query,27 const PetriEngine::PQL::Condition_ptr &query,
28 const std::string &queryName,28 const std::string &queryName,
29 options_t &options);29 options_t &options,
30 const PetriEngine::Reducer* reducer);
30}31}
3132
32#endif //VERIFYPN_LTLMAIN_H33#endif //VERIFYPN_LTLMAIN_H
3334
=== modified file 'include/LTL/Structures/BitProductStateSet.h'
--- include/LTL/Structures/BitProductStateSet.h 2021-08-10 13:44:22 +0000
+++ include/LTL/Structures/BitProductStateSet.h 2021-10-17 18:21:15 +0000
@@ -1,16 +1,16 @@
1/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,1/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
2 * Simon M. Virenfeldt <simon@simwir.dk>2 * Simon M. Virenfeldt <simon@simwir.dk>
3 * 3 *
4 * This program is free software: you can redistribute it and/or modify4 * This program is free software: you can redistribute it and/or modify
5 * it under the terms of the GNU General Public License as published by5 * it under the terms of the GNU General Public License as published by
6 * the Free Software Foundation, either version 3 of the License, or6 * the Free Software Foundation, either version 3 of the License, or
7 * (at your option) any later version.7 * (at your option) any later version.
8 * 8 *
9 * This program is distributed in the hope that it will be useful,9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.12 * GNU General Public License for more details.
13 * 13 *
14 * You should have received a copy of the GNU General Public License14 * You should have received a copy of the GNU General Public License
15 * along with this program. If not, see <http://www.gnu.org/licenses/>.15 * along with this program. If not, see <http://www.gnu.org/licenses/>.
16 */16 */
@@ -64,7 +64,7 @@
64 template<uint8_t nbits = 16>64 template<uint8_t nbits = 16>
65 class BitProductStateSet : public ProductStateSetInterface {65 class BitProductStateSet : public ProductStateSetInterface {
66 public:66 public:
67 explicit BitProductStateSet(const PetriEngine::PetriNet *net, int kbound = 0, size_t nplaces = -1)67 explicit BitProductStateSet(const PetriEngine::PetriNet *net, int kbound = 0)
68 : markings(*net, kbound, net->numberOfPlaces())68 : markings(*net, kbound, net->numberOfPlaces())
69 {69 {
70 }70 }
7171
=== modified file 'include/LTL/Structures/ProductState.h'
--- include/LTL/Structures/ProductState.h 2021-04-29 13:19:53 +0000
+++ include/LTL/Structures/ProductState.h 2021-10-17 18:21:15 +0000
@@ -19,6 +19,7 @@
19#define VERIFYPN_PRODUCTSTATE_H19#define VERIFYPN_PRODUCTSTATE_H
2020
21#include "PetriEngine/Structures/State.h"21#include "PetriEngine/Structures/State.h"
22#include "LTL/Structures/BuchiAutomaton.h"
2223
23namespace LTL {24namespace LTL {
24 template <class SuccessorGen>25 template <class SuccessorGen>
@@ -32,7 +33,7 @@
32 */33 */
33 class ProductState : public PetriEngine::Structures::State {34 class ProductState : public PetriEngine::Structures::State {
34 public:35 public:
35 ProductState() : PetriEngine::Structures::State() {}36 explicit ProductState(const BuchiAutomaton* aut = nullptr) : PetriEngine::Structures::State(), _aut(aut) {}
3637
37 void setMarking(PetriEngine::MarkVal* marking, size_t nplaces)38 void setMarking(PetriEngine::MarkVal* marking, size_t nplaces)
38 {39 {
@@ -74,10 +75,17 @@
74 bool operator!=(const ProductState &rhs) const {75 bool operator!=(const ProductState &rhs) const {
75 return !(rhs == *this);76 return !(rhs == *this);
76 }77 }
78
79 [[nodiscard]] bool is_accepting() const {
80 assert(_aut);
81 return _aut->_buchi->state_is_accepting(getBuchiState());
82 }
83
77 private:84 private:
78 template <typename T>85 template <typename T>
79 friend class LTL::ProductSuccessorGenerator;86 friend class LTL::ProductSuccessorGenerator;
80 size_t buchi_state_idx;87 size_t buchi_state_idx;
88 const LTL::Structures::BuchiAutomaton *_aut = nullptr;
81 };89 };
82}90}
8391
8492
=== modified file 'include/LTL/Structures/ProductStateFactory.h'
--- include/LTL/Structures/ProductStateFactory.h 2021-04-29 07:47:52 +0000
+++ include/LTL/Structures/ProductStateFactory.h 2021-10-17 18:21:15 +0000
@@ -25,14 +25,14 @@
25namespace LTL::Structures{25namespace LTL::Structures{
26 class ProductStateFactory {26 class ProductStateFactory {
27 public:27 public:
28 ProductStateFactory(const PetriEngine::PetriNet *net, size_t initial_buchi_state)28 ProductStateFactory(const PetriEngine::PetriNet *net, const BuchiAutomaton& aut, size_t initial_buchi_state)
29 : net(net), buchi_init(initial_buchi_state) {}29 : net(net), _aut(aut), buchi_init(initial_buchi_state) {}
3030
31 ProductState newState() {31 ProductState newState() {
32 auto buf = new PetriEngine::MarkVal[net->numberOfPlaces()+1];32 auto buf = new PetriEngine::MarkVal[net->numberOfPlaces()+1];
33 std::copy(net->initial(), net->initial() + net->numberOfPlaces(), buf);33 std::copy(net->initial(), net->initial() + net->numberOfPlaces(), buf);
34 buf[net->numberOfPlaces()] = 0;34 buf[net->numberOfPlaces()] = 0;
35 ProductState state;35 ProductState state{&_aut};
36 state.setMarking(buf, net->numberOfPlaces());36 state.setMarking(buf, net->numberOfPlaces());
37 state.setBuchiState(buchi_init);37 state.setBuchiState(buchi_init);
38 return state;38 return state;
@@ -40,6 +40,7 @@
4040
41 private:41 private:
42 const PetriEngine::PetriNet *net;42 const PetriEngine::PetriNet *net;
43 const LTL::Structures::BuchiAutomaton _aut;
43 const size_t buchi_init;44 const size_t buchi_init;
44 };45 };
45}46}
4647
=== modified file 'include/LTL/Stubborn/SafeAutStubbornSet.h'
--- include/LTL/Stubborn/SafeAutStubbornSet.h 2021-05-13 09:19:31 +0000
+++ include/LTL/Stubborn/SafeAutStubbornSet.h 2021-10-17 18:21:15 +0000
@@ -48,23 +48,40 @@
48 StubbornSet::reset();48 StubbornSet::reset();
49 memset(_unsafe.get(), false, sizeof(bool) * _net.numberOfTransitions());49 memset(_unsafe.get(), false, sizeof(bool) * _net.numberOfTransitions());
50 _bad = false;50 _bad = false;
51 _has_enabled_stubborn = false;
52 }
53
54 void set_buchi_conds(PetriEngine::PQL::Condition_ptr ret_cond,
55 PetriEngine::PQL::Condition_ptr prog_cond,
56 PetriEngine::PQL::Condition_ptr sink_cond) {
57 _ret_cond = ret_cond;
58 _prog_cond = prog_cond;
59 _sink_cond = sink_cond;
51 }60 }
5261
53 protected:62 protected:
54 void addToStub(uint32_t t) override63 void addToStub(uint32_t t) override
55 {64 {
56 //refinement of bad: can manually check whether firing t would violate some progressing formula.65 // potential refinement of bad: can manually check whether firing t would violate some progressing formula.
57 if (_unsafe[t] && _enabled[t]) {66 if (_enabled[t]) {
58 _bad = true;67 _has_enabled_stubborn = true;
59 return;68 if (_unsafe[t]) {
69 _bad = true;
70 return;
71 }
60 }72 }
61 //TODO check safe-ness
62 StubbornSet::addToStub(t);73 StubbornSet::addToStub(t);
63 }74 }
6475
65 private:76 private:
66 std::unique_ptr<bool[]> _unsafe;77 std::unique_ptr<bool[]> _unsafe;
67 bool _bad = false;78 bool _bad = false;
79 bool _has_enabled_stubborn = false;
80 PetriEngine::PQL::Condition_ptr _ret_cond;
81 PetriEngine::PQL::Condition_ptr _prog_cond;
82 PetriEngine::PQL::Condition_ptr _sink_cond;
83
84 void _print_debug();
68 };85 };
69}86}
7087
7188
=== modified file 'include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h 2021-04-14 09:38:34 +0000
+++ include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h 2021-10-17 18:21:15 +0000
@@ -78,6 +78,7 @@
78 {78 {
79 return (bool) aut._buchi->prop_weak();79 return (bool) aut._buchi->prop_weak();
80 }80 }
81
81 size_t buchiStates() { return aut._buchi->num_states(); }82 size_t buchiStates() { return aut._buchi->num_states(); }
8283
83 Structures::BuchiAutomaton aut;84 Structures::BuchiAutomaton aut;
@@ -91,7 +92,6 @@
91 }92 }
92 };93 };
9394
94
95 bool has_invariant_self_loop(size_t state) {95 bool has_invariant_self_loop(size_t state) {
96 if (self_loops[state] != InvariantSelfLoop::UNKNOWN)96 if (self_loops[state] != InvariantSelfLoop::UNKNOWN)
97 return self_loops[state] == InvariantSelfLoop::TRUE;97 return self_loops[state] == InvariantSelfLoop::TRUE;
9898
=== modified file 'include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h 2021-04-29 13:19:53 +0000
+++ include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h 2021-10-17 18:21:15 +0000
@@ -48,6 +48,8 @@
4848
49 }49 }
5050
51 const PetriEngine::PetriNet& net() const { return *_net; }
52
51 [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); };53 [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); };
5254
53 bool next(LTL::Structures::ProductState &state)55 bool next(LTL::Structures::ProductState &state)
@@ -89,12 +91,12 @@
89 auto buf = new PetriEngine::MarkVal[_net->numberOfPlaces() + 1];91 auto buf = new PetriEngine::MarkVal[_net->numberOfPlaces() + 1];
90 std::copy(_net->initial(), _net->initial() + _net->numberOfPlaces(), buf);92 std::copy(_net->initial(), _net->initial() + _net->numberOfPlaces(), buf);
91 buf[_net->numberOfPlaces()] = initial_buchi_state();93 buf[_net->numberOfPlaces()] = initial_buchi_state();
92 LTL::Structures::ProductState state;94 LTL::Structures::ProductState state{&buchi.aut};
93 state.setMarking(buf, _net->numberOfPlaces());95 state.setMarking(buf, _net->numberOfPlaces());
94 //state.setBuchiState(initial_buchi_state());96 //state.setBuchiState(initial_buchi_state());
95 buchi.prepare(state.getBuchiState());97 buchi.prepare(state.getBuchiState());
96 while (next_buchi_succ(state)) {98 while (next_buchi_succ(state)) {
97 states.emplace_back();99 states.emplace_back(&buchi.aut);
98 states.back().setMarking(new PetriEngine::MarkVal[_net->numberOfPlaces() + 1], _net->numberOfPlaces());100 states.back().setMarking(new PetriEngine::MarkVal[_net->numberOfPlaces() + 1], _net->numberOfPlaces());
99 std::copy(state.marking(), state.marking() + _net->numberOfPlaces(), states.back().marking());101 std::copy(state.marking(), state.marking() + _net->numberOfPlaces(), states.back().marking());
100 states.back().setBuchiState(state.getBuchiState());102 states.back().setBuchiState(state.getBuchiState());
@@ -112,7 +114,7 @@
112 * @param state the source state to generate successors from114 * @param state the source state to generate successors from
113 * @param sucinfo the point in the iteration to start from, as returned by `next`.115 * @param sucinfo the point in the iteration to start from, as returned by `next`.
114 */116 */
115 virtual void prepare(const LTL::Structures::ProductState *state, typename SuccessorGen::sucinfo &sucinfo)117 virtual void prepare(const LTL::Structures::ProductState *state, typename SuccessorGen::successor_info_t &sucinfo)
116 {118 {
117 _successor_generator->prepare(state, sucinfo);119 _successor_generator->prepare(state, sucinfo);
118 fresh_marking = sucinfo.fresh();120 fresh_marking = sucinfo.fresh();
@@ -139,7 +141,7 @@
139 * @return `true` if a successor was successfully generated, `false` otherwise.141 * @return `true` if a successor was successfully generated, `false` otherwise.
140 * @warning do not use the same State for both prepare and next, this will cause wildly incorrect behaviour!142 * @warning do not use the same State for both prepare and next, this will cause wildly incorrect behaviour!
141 */143 */
142 bool next(Structures::ProductState &state, typename SuccessorGen::sucinfo &sucinfo)144 bool next(Structures::ProductState &state, typename SuccessorGen::successor_info_t &sucinfo)
143 {145 {
144 if (fresh_marking) {146 if (fresh_marking) {
145 fresh_marking = false;147 fresh_marking = false;
@@ -182,7 +184,7 @@
182 size_t fired() const { return _successor_generator->fired(); }184 size_t fired() const { return _successor_generator->fired(); }
183185
184 //template<typename T = std::enable_if_t<std::is_same_v<SuccessorGen, PetriEngine::ReducingSuccessorGenerator>, void>>186 //template<typename T = std::enable_if_t<std::is_same_v<SuccessorGen, PetriEngine::ReducingSuccessorGenerator>, void>>
185 void generateAll(LTL::Structures::ProductState *parent, typename SuccessorGen::sucinfo &sucinfo)187 void generateAll(LTL::Structures::ProductState *parent, typename SuccessorGen::successor_info_t &sucinfo)
186 {188 {
187 if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {189 if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
188 _successor_generator->generate_all(parent, sucinfo);190 _successor_generator->generate_all(parent, sucinfo);
@@ -221,7 +223,7 @@
221 }223 }
222 }224 }
223225
224 void pop(const typename SuccessorGen::sucinfo &sucinfo) {226 void pop(const typename SuccessorGen::successor_info_t &sucinfo) {
225 if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {227 if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
226 _successor_generator->pop(sucinfo);228 _successor_generator->pop(sucinfo);
227 }229 }
228230
=== modified file 'include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h 2021-08-04 08:13:25 +0000
+++ include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h 2021-10-17 18:21:15 +0000
@@ -49,7 +49,7 @@
49 std::transform(std::begin(buchi.ap_info), std::end(buchi.ap_info), std::begin(aps),49 std::transform(std::begin(buchi.ap_info), std::end(buchi.ap_info), std::begin(aps),
50 [](const std::pair<int, AtomicProposition> &pair) { return pair.second; });50 [](const std::pair<int, AtomicProposition> &pair) { return pair.second; });
51 for (unsigned state = 0; state < buchi._buchi->num_states(); ++state) {51 for (unsigned state = 0; state < buchi._buchi->num_states(); ++state) {
52 if (buchi._buchi->state_is_accepting(state)) continue;52 //if (buchi._buchi->state_is_accepting(state)) continue;
5353
54 bdd retarding = bddfalse;54 bdd retarding = bddfalse;
55 bdd progressing = bddfalse;55 bdd progressing = bddfalse;
@@ -61,16 +61,32 @@
61 progressing |= e.cond;61 progressing |= e.cond;
62 }62 }
63 }63 }
64 if ((retarding | progressing) == bddtrue) {64 bdd sink_prop = bdd_not(retarding | progressing);
65 _reach_states.insert(std::make_pair(state, BuchiEdge{progressing, toPQL(spot::bdd_to_formula(progressing, buchi.dict), aps)}));65 auto prog_cond = toPQL(spot::bdd_to_formula(progressing, buchi.dict), aps);
66 }66 auto ret_cond = toPQL(spot::bdd_to_formula(retarding, buchi.dict), aps);
67 auto sink_cond = sink_prop == bdd_false()
68 ? PetriEngine::PQL::BooleanCondition::FALSE_CONSTANT
69 : std::make_shared<PetriEngine::PQL::NotCondition>(
70 std::make_shared<PetriEngine::PQL::OrCondition>(prog_cond, ret_cond)
71 );
72 _reach_states.insert(std::make_pair(
73 state,
74 BuchiEdge{progressing | sink_prop,
75 ret_cond,
76 prog_cond,
77 sink_cond}));
67 }78 }
68 }79 }
6980
70 void prepare(const LTL::Structures::ProductState *state, typename S::sucinfo &sucinfo) override81 void prepare(const LTL::Structures::ProductState *state, typename S::successor_info_t &sucinfo) override
71 {82 {
72 if (auto suc = _reach_states.find(state->getBuchiState()); suc != std::end(_reach_states) && !this->guard_valid(*state, suc->second.bddCond)) {83 auto suc = _reach_states.find(state->getBuchiState());
73 (dynamic_cast<PetriEngine::StubbornSet*>(_reach.get()))->setQuery(suc->second.cond.get());84 // assert valid since all states are reducible when considering
85 // the sink progressing formula and key transitions in accepting states.
86 assert(suc != std::end(_reach_states));
87 if (suc != std::end(_reach_states) && !this->guard_valid(*state, suc->second.bddCond)) {
88 //_reach->setQuery(suc->second.prog_cond.get());
89 _reach->set_buchi_conds(suc->second.ret_cond, suc->second.prog_cond, suc->second.pseudo_sink_cond);
74 set_spooler(_reach.get());90 set_spooler(_reach.get());
75 }91 }
76 else {92 else {
@@ -92,11 +108,13 @@
92108
93 struct BuchiEdge{109 struct BuchiEdge{
94 bdd bddCond;110 bdd bddCond;
95 PetriEngine::PQL::Condition_ptr cond;111 PetriEngine::PQL::Condition_ptr ret_cond;
112 PetriEngine::PQL::Condition_ptr prog_cond;
113 PetriEngine::PQL::Condition_ptr pseudo_sink_cond;
96 };114 };
97115
98 std::unique_ptr<Spooler> _fallback_spooler;116 std::unique_ptr<Spooler> _fallback_spooler;
99 std::unique_ptr<LTL::SuccessorSpooler> _reach;117 std::unique_ptr<LTL::SafeAutStubbornSet> _reach;
100 std::unordered_map<size_t, BuchiEdge> _reach_states;118 std::unordered_map<size_t, BuchiEdge> _reach_states;
101 std::vector<PetriEngine::PQL::Condition_ptr> _progressing_formulae;119 std::vector<PetriEngine::PQL::Condition_ptr> _progressing_formulae;
102120
103121
=== modified file 'include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h 2021-04-29 07:47:52 +0000
+++ include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h 2021-10-17 18:21:15 +0000
@@ -25,114 +25,107 @@
25#include "PetriEngine/Stubborn/StubbornSet.h"25#include "PetriEngine/Stubborn/StubbornSet.h"
2626
27namespace LTL {27namespace LTL {
28 /**
29 * type holding sufficient information to resume successor generation for a state from a given point.
30 */
31 struct successor_info {
32 uint32_t pcounter;
33 uint32_t tcounter;
34 size_t buchi_state;
35 size_t last_state;
36
37 friend bool operator==(const successor_info &lhs, const successor_info &rhs)
38 {
39 return lhs.pcounter == rhs.pcounter &&
40 lhs.tcounter == rhs.tcounter &&
41 lhs.buchi_state == rhs.buchi_state &&
42 lhs.last_state == rhs.last_state;
43 }
44
45 friend bool operator!=(const successor_info &lhs, const successor_info &rhs)
46 {
47 return !(rhs == lhs);
48 }
49
50 inline bool has_pcounter() const
51 {
52 return pcounter != NoPCounter;
53 }
54
55 inline bool has_tcounter() const
56 {
57 return tcounter != NoTCounter;
58 }
59
60 inline bool has_buchistate() const
61 {
62 return buchi_state != NoBuchiState;
63 }
64
65 inline bool has_prev_state() const
66 {
67 return last_state != NoLastState;
68 }
69
70 [[nodiscard]] inline bool fresh() const
71 {
72 return pcounter == NoPCounter && tcounter == NoTCounter;
73 }
74
75 static constexpr auto NoPCounter = 0;
76 static constexpr auto NoTCounter = std::numeric_limits<uint32_t>::max();
77 static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();
78 static constexpr auto NoLastState = std::numeric_limits<size_t>::max();
79 };
8028
81 class ResumingSuccessorGenerator : public PetriEngine::SuccessorGenerator {29 class ResumingSuccessorGenerator : public PetriEngine::SuccessorGenerator {
82 public:30 public:
8331
32 struct successor_info_t {
33 uint32_t pcounter;
34 uint32_t tcounter;
35 size_t buchi_state;
36 size_t last_state;
37
38 friend bool operator==(const successor_info_t &lhs, const successor_info_t &rhs) {
39 return lhs.pcounter == rhs.pcounter &&
40 lhs.tcounter == rhs.tcounter &&
41 lhs.buchi_state == rhs.buchi_state &&
42 lhs.last_state == rhs.last_state;
43 }
44
45 friend bool operator!=(const successor_info_t &lhs, const successor_info_t &rhs) {
46 return !(rhs == lhs);
47 }
48
49 bool has_pcounter() const {
50 return pcounter != NoPCounter;
51 }
52
53 bool has_tcounter() const {
54 return tcounter != NoTCounter;
55 }
56
57 bool has_buchistate() const {
58 return buchi_state != NoBuchiState;
59 }
60
61 bool has_prev_state() const {
62 return last_state != NoLastState;
63 }
64
65 size_t state() const {
66 return last_state;
67 }
68
69 size_t transition() const {
70 return tcounter - 1;
71 }
72
73 [[nodiscard]] bool fresh() const {
74 return pcounter == NoPCounter && tcounter == NoTCounter;
75 }
76
77 static constexpr auto NoPCounter = 0;
78 static constexpr auto NoTCounter = std::numeric_limits<uint32_t>::max();
79 static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();
80 static constexpr auto NoLastState = std::numeric_limits<size_t>::max();
81 };
82 public:
83
84 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net);84 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net);
8585
86 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net, const std::shared_ptr<PetriEngine::StubbornSet> &);86 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net, const std::shared_ptr<PetriEngine::StubbornSet> &);
8787
88 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,88 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,
89 std::vector<std::shared_ptr<PetriEngine::PQL::Condition> > &queries);89 std::vector<std::shared_ptr<PetriEngine::PQL::Condition> > &queries);
9090
91 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,91 ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,
92 const std::shared_ptr<PetriEngine::PQL::Condition> &query);92 const std::shared_ptr<PetriEngine::PQL::Condition> &query);
9393
94 ~ResumingSuccessorGenerator() override = default;94 ~ResumingSuccessorGenerator() override = default;
9595
96 void prepare(const PetriEngine::Structures::State *state, const successor_info &sucinfo);96 void prepare(const PetriEngine::Structures::State *state, const successor_info_t &sucinfo);
9797
9898 bool next(PetriEngine::Structures::State &write, successor_info_t &sucinfo) {
99 bool next(PetriEngine::Structures::State &write, successor_info &sucinfo)
100 {
101 bool has_suc = PetriEngine::SuccessorGenerator::next(write);99 bool has_suc = PetriEngine::SuccessorGenerator::next(write);
102 getSuccInfo(sucinfo);100 get_succ_info(sucinfo);
103 return has_suc;101 return has_suc;
104 }102 }
105103
106 uint32_t fired() const104 uint32_t fired() const {
107 {
108 return _suc_tcounter - 1;105 return _suc_tcounter - 1;
109 }106 }
110107
111 const PetriEngine::MarkVal *getParent() const108 const PetriEngine::MarkVal *get_parent() const {
112 {
113 return _parent->marking();109 return _parent->marking();
114 }110 }
115111
116112 size_t last_transition() const {
117 size_t last_transition() const
118 {
119 return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() :113 return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() :
120 _suc_tcounter - 1;114 _suc_tcounter - 1;
121 }115 }
122116
123 using sucinfo = successor_info;117 static constexpr successor_info_t _initial_suc_info{
124118 successor_info_t::NoPCounter,
125 static constexpr sucinfo _initial_suc_info{119 successor_info_t::NoTCounter,
126 successor_info::NoPCounter,120 successor_info_t::NoBuchiState,
127 successor_info::NoTCounter,121 successor_info_t::NoLastState};
128 successor_info::NoBuchiState,122
129 successor_info::NoLastState123 static constexpr auto initial_suc_info() {
130 };124 return _initial_suc_info;
131125 }
132 static constexpr auto initial_suc_info() { return _initial_suc_info; }
133126
134 private:127 private:
135 void getSuccInfo(successor_info &sucinfo) const;128 void get_succ_info(successor_info_t &sucinfo) const;
136129
137 //friend class ReducingSuccessorGenerator;130 //friend class ReducingSuccessorGenerator;
138 };131 };
139132
=== modified file 'include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h 2021-04-30 07:02:31 +0000
+++ include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h 2021-10-17 18:21:15 +0000
@@ -1,16 +1,16 @@
1/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,1/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
2 * Simon M. Virenfeldt <simon@simwir.dk>2 * Simon M. Virenfeldt <simon@simwir.dk>
3 * 3 *
4 * This program is free software: you can redistribute it and/or modify4 * This program is free software: you can redistribute it and/or modify
5 * it under the terms of the GNU General Public License as published by5 * it under the terms of the GNU General Public License as published by
6 * the Free Software Foundation, either version 3 of the License, or6 * the Free Software Foundation, either version 3 of the License, or
7 * (at your option) any later version.7 * (at your option) any later version.
8 * 8 *
9 * This program is distributed in the hope that it will be useful,9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.12 * GNU General Public License for more details.
13 * 13 *
14 * You should have received a copy of the GNU General Public License14 * You should have received a copy of the GNU General Public License
15 * along with this program. If not, see <http://www.gnu.org/licenses/>.15 * along with this program. If not, see <http://www.gnu.org/licenses/>.
16 */16 */
@@ -34,18 +34,27 @@
34 _statebuf.setMarking(new PetriEngine::MarkVal[net->numberOfPlaces() + 1], net->numberOfPlaces());34 _statebuf.setMarking(new PetriEngine::MarkVal[net->numberOfPlaces() + 1], net->numberOfPlaces());
35 }35 }
3636
37 struct sucinfo {37 struct successor_info_t {
38 SuccessorQueue<> successors;38 SuccessorQueue<> successors;
39 size_t buchi_state;39 size_t buchi_state;
40 size_t last_state;40 size_t last_state;
4141 size_t _transition;
42 sucinfo(size_t buchiState, size_t lastState) : buchi_state(buchiState), last_state(lastState) {}42
4343 successor_info_t(size_t buchiState, size_t lastState) : buchi_state(buchiState), last_state(lastState) {}
44 [[nodiscard]] inline bool has_prev_state() const44
45 [[nodiscard]] bool has_prev_state() const
45 {46 {
46 return last_state != NoLastState;47 return last_state != NoLastState;
47 }48 }
4849
50 size_t state() const {
51 return last_state;
52 }
53
54 size_t transition() const {
55 return _transition;
56 }
57
49 [[nodiscard]] bool fresh() const { return buchi_state == NoBuchiState && last_state == NoLastState; }58 [[nodiscard]] bool fresh() const { return buchi_state == NoBuchiState && last_state == NoLastState; }
5059
51 static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();60 static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();
@@ -62,9 +71,9 @@
62 _heuristic = heuristic;71 _heuristic = heuristic;
63 }72 }
6473
65 [[nodiscard]] static sucinfo initial_suc_info()74 [[nodiscard]] static successor_info_t initial_suc_info()
66 {75 {
67 return sucinfo{sucinfo::NoBuchiState, sucinfo::NoLastState};76 return successor_info_t{successor_info_t::NoBuchiState, successor_info_t::NoLastState};
68 }77 }
6978
70 bool prepare(const PetriEngine::Structures::State *state)79 bool prepare(const PetriEngine::Structures::State *state)
@@ -78,14 +87,15 @@
78 }87 }
7988
8089
81 void prepare(const Structures::ProductState *state, sucinfo &sucinfo)90 void prepare(const Structures::ProductState *state, successor_info_t &sucinfo)
82 {91 {
83 assert(_spooler != nullptr);92 assert(_spooler != nullptr);
8493
85 PetriEngine::SuccessorGenerator::prepare(state);94 PetriEngine::SuccessorGenerator::prepare(state);
86 if (sucinfo.successors == nullptr) {95 if (sucinfo.successors == nullptr) {
87 uint32_t tid;96 uint32_t tid;
88 _spooler->prepare(state);97 bool res = _spooler->prepare(state);
98 //assert(!res/* || !_net.deadlocked(state->marking())*/);
89 if (!_heuristic || !_heuristic->has_heuristic(*state)) {99 if (!_heuristic || !_heuristic->has_heuristic(*state)) {
90 uint32_t nsuc = 0;100 uint32_t nsuc = 0;
91 // generate list of transitions that generate a successor.101 // generate list of transitions that generate a successor.
@@ -95,7 +105,7 @@
95 assert(nsuc <= _net.numberOfTransitions());105 assert(nsuc <= _net.numberOfTransitions());
96 }106 }
97 sucinfo.successors = SuccessorQueue(_transbuf.get(), nsuc);107 sucinfo.successors = SuccessorQueue(_transbuf.get(), nsuc);
98108 assert((res && !sucinfo.successors.empty()) || !res);
99 } else {109 } else {
100 // list of (transition, weight)110 // list of (transition, weight)
101 _heuristic->prepare(*state);111 _heuristic->prepare(*state);
@@ -113,7 +123,7 @@
113 }123 }
114 }124 }
115 }125 }
116 bool next(Structures::ProductState &state, sucinfo &sucinfo)126 bool next(Structures::ProductState &state, successor_info_t &sucinfo)
117 {127 {
118 assert(sucinfo.successors != nullptr);128 assert(sucinfo.successors != nullptr);
119 if (sucinfo.successors.empty()) {129 if (sucinfo.successors.empty()) {
@@ -124,6 +134,7 @@
124 return false;134 return false;
125 }135 }
126 _last = sucinfo.successors.front();136 _last = sucinfo.successors.front();
137 sucinfo._transition = _last;
127#ifndef NDEBUG138#ifndef NDEBUG
128 //std::cerr << "Firing " << _net.transitionNames()[_last] << std::endl;139 //std::cerr << "Firing " << _net.transitionNames()[_last] << std::endl;
129#endif140#endif
@@ -134,7 +145,7 @@
134145
135 [[nodiscard]] uint32_t fired() const { return _last; }146 [[nodiscard]] uint32_t fired() const { return _last; }
136147
137 void generate_all(LTL::Structures::ProductState *parent, sucinfo &sucinfo)148 void generate_all(LTL::Structures::ProductState *parent, successor_info_t &sucinfo)
138 {149 {
139 assert(_spooler != nullptr);150 assert(_spooler != nullptr);
140 assert(sucinfo.successors != nullptr);151 assert(sucinfo.successors != nullptr);
@@ -200,7 +211,7 @@
200 _heuristic->push(fired());211 _heuristic->push(fired());
201 }212 }
202213
203 void pop(const sucinfo &sc) {214 void pop(const successor_info_t &sc) {
204 if (_heuristic && sc.successors.has_consumed())215 if (_heuristic && sc.successors.has_consumed())
205 _heuristic->pop(sc.successors.last_pop());216 _heuristic->pop(sc.successors.last_pop());
206 }217 }
207218
=== modified file 'include/PetriEngine/Reducer.h'
--- include/PetriEngine/Reducer.h 2021-07-07 13:19:23 +0000
+++ include/PetriEngine/Reducer.h 2021-10-17 18:21:15 +0000
@@ -1,4 +1,4 @@
1/* 1/*
2 * File: Reducer.h2 * File: Reducer.h
3 * Author: srba3 * Author: srba
4 *4 *
@@ -19,34 +19,34 @@
19namespace PetriEngine {19namespace PetriEngine {
2020
21 using ArcIter = std::vector<Arc>::iterator;21 using ArcIter = std::vector<Arc>::iterator;
22 22
23 class PetriNetBuilder;23 class PetriNetBuilder;
24 24
25 class QueryPlaceAnalysisContext : public PQL::AnalysisContext {25 class QueryPlaceAnalysisContext : public PQL::AnalysisContext {
26 std::vector<uint32_t> _placeInQuery;26 std::vector<uint32_t> _placeInQuery;
27 bool _deadlock;27 bool _deadlock;
28 public:28 public:
2929
30 QueryPlaceAnalysisContext(const std::unordered_map<std::string, uint32_t>& pnames, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net) 30 QueryPlaceAnalysisContext(const std::unordered_map<std::string, uint32_t>& pnames, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net)
31 : PQL::AnalysisContext(pnames, tnames, net) {31 : PQL::AnalysisContext(pnames, tnames, net) {
32 _placeInQuery.resize(_placeNames.size(), 0);32 _placeInQuery.resize(_placeNames.size(), 0);
33 _deadlock = false;33 _deadlock = false;
34 };34 };
35 35
36 virtual ~QueryPlaceAnalysisContext()36 virtual ~QueryPlaceAnalysisContext()
37 {37 {
38 }38 }
39 39
40 uint32_t* getQueryPlaceCount(){40 uint32_t* getQueryPlaceCount(){
41 return _placeInQuery.data();41 return _placeInQuery.data();
42 }42 }
4343
44 bool hasDeadlock() { return _deadlock; }44 bool hasDeadlock() { return _deadlock; }
45 45
46 virtual void setHasDeadlock() override {46 virtual void setHasDeadlock() override {
47 _deadlock = true;47 _deadlock = true;
48 };48 };
49 49
50 ResolutionResult resolve(const std::string& identifier, bool place) override {50 ResolutionResult resolve(const std::string& identifier, bool place) override {
51 if(!place) return PQL::AnalysisContext::resolve(identifier, false);51 if(!place) return PQL::AnalysisContext::resolve(identifier, false);
52 ResolutionResult result;52 ResolutionResult result;
@@ -61,7 +61,7 @@
61 _placeInQuery[i]++;61 _placeInQuery[i]++;
62 return result;62 return result;
63 }63 }
64 64
65 return result;65 return result;
66 }66 }
6767
@@ -70,7 +70,7 @@
70 struct ExpandedArc70 struct ExpandedArc
71 {71 {
72 ExpandedArc(std::string place, size_t weight) : place(place), weight(weight) {}72 ExpandedArc(std::string place, size_t weight) : place(place), weight(weight) {}
73 73
74 friend std::ostream& operator<<(std::ostream& os, ExpandedArc const & ea) {74 friend std::ostream& operator<<(std::ostream& os, ExpandedArc const & ea) {
75 for(size_t i = 0; i < ea.weight; ++i)75 for(size_t i = 0; i < ea.weight; ++i)
76 {76 {
@@ -78,18 +78,18 @@
78 }78 }
79 return os;79 return os;
80 }80 }
81 81
82 std::string place; 82 std::string place;
83 size_t weight;83 size_t weight;
84 };84 };
85 85
86 class Reducer {86 class Reducer {
87 public:87 public:
88 Reducer(PetriNetBuilder*);88 Reducer(PetriNetBuilder*);
89 ~Reducer();89 ~Reducer();
90 void Print(QueryPlaceAnalysisContext& context); // prints the net, just for debugging90 void Print(QueryPlaceAnalysisContext& context); // prints the net, just for debugging
91 void Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reductions);91 void Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reductions);
92 92
93 size_t RemovedTransitions() const {93 size_t RemovedTransitions() const {
94 return _removedTransitions;94 return _removedTransitions;
95 }95 }
@@ -115,9 +115,9 @@
115 << "Applications of rule K: " << _ruleK << std::endl;115 << "Applications of rule K: " << _ruleK << std::endl;
116 }116 }
117117
118 void postFire(std::ostream&, const std::string& transition);118 void postFire(std::ostream&, const std::string& transition) const;
119 void extraConsume(std::ostream&, const std::string& transition);119 void extraConsume(std::ostream&, const std::string& transition) const;
120 void initFire(std::ostream&);120 void initFire(std::ostream&) const;
121121
122 private:122 private:
123 size_t _removedTransitions = 0;123 size_t _removedTransitions = 0;
@@ -146,7 +146,7 @@
146146
147 std::string getTransitionName(uint32_t transition);147 std::string getTransitionName(uint32_t transition);
148 std::string getPlaceName(uint32_t place);148 std::string getPlaceName(uint32_t place);
149 149
150 PetriEngine::Transition& getTransition(uint32_t transition);150 PetriEngine::Transition& getTransition(uint32_t transition);
151 ArcIter getOutArc(PetriEngine::Transition&, uint32_t place);151 ArcIter getOutArc(PetriEngine::Transition&, uint32_t place);
152 ArcIter getInArc(uint32_t place, PetriEngine::Transition&);152 ArcIter getInArc(uint32_t place, PetriEngine::Transition&);
@@ -154,14 +154,14 @@
154 void skipTransition(uint32_t);154 void skipTransition(uint32_t);
155 void skipPlace(uint32_t);155 void skipPlace(uint32_t);
156 std::string newTransName();156 std::string newTransName();
157 157
158 bool consistent();158 bool consistent();
159 bool hasTimedout() const {159 bool hasTimedout() const {
160 auto end = std::chrono::high_resolution_clock::now();160 auto end = std::chrono::high_resolution_clock::now();
161 auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _timer);161 auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _timer);
162 return (diff.count() >= _timeout);162 return (diff.count() >= _timeout);
163 }163 }
164 164
165 std::vector<std::string> _initfire;165 std::vector<std::string> _initfire;
166 std::unordered_map<std::string, std::vector<std::string>> _postfire;166 std::unordered_map<std::string, std::vector<std::string>> _postfire;
167 std::unordered_map<std::string, std::vector<ExpandedArc>> _extraconsume;167 std::unordered_map<std::string, std::vector<ExpandedArc>> _extraconsume;
@@ -171,7 +171,7 @@
171 std::vector<uint32_t> _skipped_trans;171 std::vector<uint32_t> _skipped_trans;
172 };172 };
173173
174 174
175175
176176
177}177}
178178
=== modified file 'include/PetriEngine/Structures/StateSet.h'
--- include/PetriEngine/Structures/StateSet.h 2021-04-29 07:47:52 +0000
+++ include/PetriEngine/Structures/StateSet.h 2021-10-17 18:21:15 +0000
@@ -42,10 +42,11 @@
42 _maxPlaceBound = std::vector<uint32_t>(net.numberOfPlaces(), 0);42 _maxPlaceBound = std::vector<uint32_t>(net.numberOfPlaces(), 0);
43 _sp = binarywrapper_t(sizeof(uint32_t) * _nplaces * 8);43 _sp = binarywrapper_t(sizeof(uint32_t) * _nplaces * 8);
44 }44 }
45 virtual ~StateSetInterface()45
46 {46 virtual ~StateSetInterface()
47 _sp.release();47 {
48 }48 _sp.release();
49 }
49 50
50 virtual std::pair<bool, size_t> add(const State& state) = 0;51 virtual std::pair<bool, size_t> add(const State& state) = 0;
51 52
@@ -59,10 +60,6 @@
59 60
60 virtual std::pair<size_t, size_t> getHistory(size_t markingid) = 0;61 virtual std::pair<size_t, size_t> getHistory(size_t markingid) = 0;
6162
62 virtual void setHistory2(size_t id, size_t transition) = 0;
63
64 virtual std::pair<size_t, size_t> getHistory2(size_t markingid) = 0;
65
66 protected:63 protected:
67 size_t _discovered;64 size_t _discovered;
68 uint32_t _kbound;65 uint32_t _kbound;
@@ -235,14 +232,6 @@
235 return std::make_pair(0,0); 232 return std::make_pair(0,0);
236 }233 }
237234
238 virtual void setHistory2(size_t id, size_t transition) override {}
239
240 virtual std::pair<size_t, size_t> getHistory2(size_t markingid) override
241 {
242 assert(false);
243 return std::make_pair(std::numeric_limits<std::size_t>::max(), std::numeric_limits<std::size_t>::max());
244 }
245
246 private:235 private:
247 ptrie_t _trie;236 ptrie_t _trie;
248 };237 };
@@ -254,8 +243,6 @@
254 {243 {
255 ptrie::uint parent;244 ptrie::uint parent;
256 ptrie::uint transition = std::numeric_limits<ptrie::uint>::max();245 ptrie::uint transition = std::numeric_limits<ptrie::uint>::max();
257 ptrie::uint parent2;
258 ptrie::uint transition2 = std::numeric_limits<ptrie::uint>::max();
259 };246 };
260 247
261 private:248 private:
@@ -301,21 +288,6 @@
301 return std::pair<size_t, size_t>(t.parent, t.transition);288 return std::pair<size_t, size_t>(t.parent, t.transition);
302 }289 }
303290
304 virtual void setHistory2(size_t id, size_t transition) override {
305 traceable_t &t = _trie.get_data(id);
306 t.parent2 = _parent;
307 t.transition2 = transition;
308 }
309
310 virtual std::pair<size_t, size_t> getHistory2(size_t markingid) override {
311 traceable_t &t = _trie.get_data(markingid);
312 return std::pair<size_t, size_t>(t.parent2, t.transition2);
313 }
314
315 void setParent(size_t id) {
316 _parent = id;
317 }
318
319 private:291 private:
320 ptrie_t _trie;292 ptrie_t _trie;
321 size_t _parent = 0;293 size_t _parent = 0;
322294
=== modified file 'include/PetriEngine/Structures/light_deque.h'
--- include/PetriEngine/Structures/light_deque.h 2021-03-23 14:10:04 +0000
+++ include/PetriEngine/Structures/light_deque.h 2021-10-17 18:21:15 +0000
@@ -1,4 +1,4 @@
1/* 1/*
2 * File: light_deque.h2 * File: light_deque.h
3 * Author: Peter G. Jensen <pgj@cs.aau.dk>3 * Author: Peter G. Jensen <pgj@cs.aau.dk>
4 *4 *
@@ -18,30 +18,40 @@
18 size_t _front = 0;18 size_t _front = 0;
19 size_t _back = 0;19 size_t _back = 0;
20 size_t _size = 0;20 size_t _size = 0;
21 std::unique_ptr<T[]> _data;21 T* _data = nullptr;
22 public:22 public:
23 light_deque(size_t initial_size = 64)23 light_deque(size_t initial_size = 64)
24 {24 {
25 if(initial_size == 0) initial_size = 1;25 if(initial_size == 0) initial_size = 1;
26 _data.reset(new T[initial_size]);26 _data = (T*)new uint8_t[initial_size*sizeof(T)]; // TODO, revisit with cast and initialization
27 _size = initial_size;27 _size = initial_size;
28 }28 }
2929
30 light_deque<T> &operator=(const light_deque<T> &other) {30 light_deque<T> &operator=(const light_deque<T> &other) {
31 _front = other._front;31 for(auto& e : *this)
32 _back = other._back;32 e.~T();
33 delete[] (uint8_t*)_data;
34 _front = 0;
35 _back = 0;
33 _size = other.size();36 _size = other.size();
34 _data.reset(new T[_size]);37 _data = (T*)new uint8_t[_size*sizeof(T)];
35 memcpy(_data.get(), other._data.get(), _size * sizeof(T));38 for(auto& e : other)
39 push_back(e);
36 return *this;40 return *this;
37 }41 }
3842
39 light_deque(light_deque &&) noexcept = default;43 ~light_deque() {
40 light_deque &operator=(light_deque &&) noexcept = default;44 for(auto& e : *this)
45 {
46 e.~T();
47 }
48 delete[] (uint8_t*)_data;
49 _data = nullptr;
50 }
4151
42 void push_back(const T& element)52 void push_back(const T& element)
43 {53 {
44 _data.get()[_back] = element;54 new (&_data[_back]) T(element);
45 ++_back;55 ++_back;
46 if(_back == _size)56 if(_back == _size)
47 {57 {
@@ -51,7 +61,7 @@
5161
52 void push_back(T&& element)62 void push_back(T&& element)
53 {63 {
54 _data.get()[_back] = element;64 new (&_data[_back]) T(std::move(element));
55 ++_back;65 ++_back;
56 if(_back == _size) {66 if(_back == _size) {
57 expand();67 expand();
@@ -62,39 +72,88 @@
62 {72 {
63 return _front == _back;73 return _front == _back;
64 }74 }
65 75
66 size_t size() const76 size_t size() const
67 {77 {
68 return _back - _front;78 return _back - _front;
69 }79 }
70 80
71 T front() const81 const T& front() const
72 {82 {
73 return _data.get()[_front];83 return _data[_front];
74 }84 }
75 const T& front() {85
76 return _data.get()[_front];86 T& front() {
87 return _data[_front];
88 }
89
90 const T& back() const
91 {
92 return _data[_back - 1];
93 }
94
95 T& back() {
96 return _data[_back - 1];
77 }97 }
7898
79 void pop_front()99 void pop_front()
80 {100 {
101 _data[_front].~T();
81 ++_front;102 ++_front;
82 if(_front >= _back)103 if(_front >= _back)
83 {104 {
84 _front = _back = 0;105 _front = _back = 0;
85 }106 }
86 }107 }
87 108
109 void pop_back()
110 {
111 if(_back > _front)
112 {
113 --_back;
114 _data[_back].~T();
115 }
116 if(_back == _front)
117 clear();
118 }
119
88 void clear()120 void clear()
89 {121 {
122 for(auto& e : *this)
123 e.~T();
90 _front = _back = 0;124 _front = _back = 0;
91 }125 }
92 private:126
127 T* begin() {
128 return &front();
129 }
130
131 T* end() {
132 return &_data[_back];
133 }
134
135 const T* begin() const {
136 return &front();
137 }
138
139 const T* end() const {
140 return &_data[_back];
141 }
142
143 private:
93 void expand() {144 void expand() {
94 std::unique_ptr<T[]> ndata(new T[_size*2]);145 T* ndata = (T*)new uint8_t[_size*2*sizeof(T)];
95 memcpy(ndata.get(), _data.get(), _size*sizeof(T));146 size_t n = 0;
147 for(auto& e : *this)
148 {
149 new (ndata + n) T(std::move(e));
150 ++n;
151 }
96 _size *= 2;152 _size *= 2;
97 _data.swap(ndata);153 _back = (_back - _front);
154 _front = 0;
155 std::swap(_data, ndata);
156 delete[] (uint8_t*)ndata;
98 }157 }
99};158};
100159
101160
=== modified file 'include/PetriEngine/SuccessorGenerator.h'
--- include/PetriEngine/SuccessorGenerator.h 2021-03-19 11:48:52 +0000
+++ include/PetriEngine/SuccessorGenerator.h 2021-10-17 18:21:15 +0000
@@ -4,7 +4,7 @@
4 * and open the template in the editor.4 * and open the template in the editor.
5 */5 */
66
7/* 7/*
8 * File: SuccessorGenerator.h8 * File: SuccessorGenerator.h
9 * Author: Peter G. Jensen9 * Author: Peter G. Jensen
10 *10 *
@@ -32,13 +32,15 @@
32 virtual bool next(Structures::State& write);32 virtual bool next(Structures::State& write);
33 uint32_t fired() const33 uint32_t fired() const
34 {34 {
35 return _suc_tcounter -1;35 return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() : _suc_tcounter - 1;
36 }36 }
3737
38 const MarkVal* getParent() const {38 const MarkVal* getParent() const {
39 return _parent->marking();39 return _parent->marking();
40 }40 }
4141
42 const PetriNet& net() const { return _net; }
43
42 void reset();44 void reset();
4345
44 /**46 /**
@@ -64,8 +66,6 @@
64 */66 */
65 void producePostset(Structures::State& write, uint32_t t);67 void producePostset(Structures::State& write, uint32_t t);
6668
67 size_t last_transition() const { return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() : _suc_tcounter - 1; }
68
69protected:69protected:
70 const PetriNet& _net;70 const PetriNet& _net;
7171
7272
=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-08-10 13:44:22 +0000
+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-10-17 18:21:15 +0000
@@ -18,186 +18,186 @@
18#include "LTL/Algorithm/NestedDepthFirstSearch.h"18#include "LTL/Algorithm/NestedDepthFirstSearch.h"
1919
20namespace LTL {20namespace LTL {
21 template<typename S, typename W>21 template<typename S>
22 bool NestedDepthFirstSearch<S, W>::isSatisfied()22 bool NestedDepthFirstSearch<S>::isSatisfied()
23 {23 {
24 this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;24 this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;
25 dfs();25 dfs();
26 return !violation;26 return !_violation;
27 }27 }
2828
29 template<typename S, typename W>29 template<typename S>
30 void NestedDepthFirstSearch<S, W>::dfs()30 std::pair<bool,size_t> NestedDepthFirstSearch<S>::mark(State& state, const uint8_t MARKER)
31 {31 {
32 std::stack<size_t> call_stack;32 auto[_, stateid] = _states.add(state);
33 std::stack<StackEntry> todo;33 if (stateid == std::numeric_limits<size_t>::max()) {
3434 return std::make_pair(false, stateid);
35 State working = factory.newState();35 }
36 State curState = factory.newState();36
3737 auto r = _markers[stateid];
38 {38 _markers[stateid] = (MARKER | r);
3939 const bool is_new = (r & MARKER) == 0;
40 if(is_new)
41 {
42 ++_mark_count[MARKER];
43 ++this->_discovered;
44 }
45 return std::make_pair(is_new, stateid);
46 }
47
48 template<typename S>
49 void NestedDepthFirstSearch<S>::dfs()
50 {
51
52 light_deque<StackEntry> todo;
53 light_deque<StackEntry> nested_todo;
54
55 State working = this->_factory.newState();
56 State curState = this->_factory.newState();
57
58 {
40 std::vector<State> initial_states = this->successorGenerator->makeInitialState();59 std::vector<State> initial_states = this->successorGenerator->makeInitialState();
41 for (auto &state : initial_states) {60 for (auto &state : initial_states) {
42 auto res = states.add(state);61 auto res = _states.add(state);
43 if (res.first) {62 if (res.first) {
44 assert(res.first);63 todo.push_back(StackEntry{res.second, S::initial_suc_info()});
45 todo.push(StackEntry{res.second, S::initial_suc_info()});64 ++this->_discovered;
46 this->_discovered++;
47 }65 }
48 }66 }
49 }67 }
5068
51 while (!todo.empty()) {69 while (!todo.empty()) {
52 auto &top = todo.top();70 auto &top = todo.back();
53 states.decode(curState, top.id);71 _states.decode(curState, top._id);
54 this->successorGenerator->prepare(&curState, top.sucinfo);72 this->successorGenerator->prepare(&curState, top._sucinfo);
55 if (top.sucinfo.has_prev_state()) {73 if (top._sucinfo.has_prev_state()) {
56 states.decode(working, top.sucinfo.last_state);74 _states.decode(working, top._sucinfo.last_state);
57 }75 }
58 if (!this->successorGenerator->next(working, top.sucinfo)) {76 if (!this->successorGenerator->next(working, top._sucinfo)) {
59 // no successor77 // no successor
60 todo.pop();78 if (curState.is_accepting()) {
61 if (this->successorGenerator->isAccepting(curState)) {79 if(this->successorGenerator->has_invariant_self_loop(curState))
62 seed = &curState;80 _violation = true;
63 ndfs(curState);81 else
64 if (violation) {82 ndfs(curState, nested_todo);
65 if constexpr (SaveTrace) {83 if (_violation) {
66 std::stack<std::pair<size_t, size_t>> transitions;84 if (_print_trace) {
67 size_t next = top.id;85 print_trace(todo, nested_todo);
68 states.decode(working, next);
69 while (!this->successorGenerator->isInitialState(working)) {
70 auto[parent, transition] = states.getHistory(next);
71 transitions.push(std::make_pair(parent, transition));
72 next = parent;
73 states.decode(working, next);
74 }
75 printTrace(transitions);
76 }86 }
77 return;87 return;
78 }88 }
79 }89 }
90 todo.pop_back();
80 } else {91 } else {
81 auto[_, stateid] = states.add(working);92 auto [is_new, stateid] = mark(working, MARKER1);
82 if (stateid == std::numeric_limits<size_t>::max()) {93 if (stateid == std::numeric_limits<size_t>::max()) {
83 continue;94 continue;
84 }95 }
85 auto[it, is_new] = mark1.insert(stateid);96 top._sucinfo.last_state = stateid;
86 top.sucinfo.last_state = stateid;
87 if (is_new) {97 if (is_new) {
88 if constexpr (SaveTrace) {98 ++this->_discovered;
89 states.setParent(top.id);99 if(this->successorGenerator->isAccepting(curState) &&
90 states.setHistory(stateid, this->successorGenerator->fired());100 this->successorGenerator->has_invariant_self_loop(curState))
101 {
102 _violation = true;
103 if(_print_trace)
104 print_trace(todo, nested_todo);
105 return;
91 }106 }
92 this->_discovered++;107 todo.push_back(StackEntry{stateid, S::initial_suc_info()});
93 todo.push(StackEntry{stateid, S::initial_suc_info()});
94 }108 }
95 }109 }
96 }110 }
97 }111 }
98112
99 template<typename S, typename W>113 template<typename S>
100 void NestedDepthFirstSearch<S, W>::ndfs(State &state)114 void NestedDepthFirstSearch<S>::ndfs(const State &state, light_deque<StackEntry>& nested_todo)
101 {115 {
102 std::stack<StackEntry> todo;116
103117 State working = this->_factory.newState();
104 State working = factory.newState();118 State curState = this->_factory.newState();
105 State curState = factory.newState();119
106120 nested_todo.push_back(StackEntry{_states.add(state).second, S::initial_suc_info()});
107 todo.push(StackEntry{states.add(state).second, S::initial_suc_info()});121
108122 while (!nested_todo.empty()) {
109 while (!todo.empty()) {123 auto &top = nested_todo.back();
110 auto &top = todo.top();124 _states.decode(curState, top._id);
111 states.decode(curState, top.id);125 this->successorGenerator->prepare(&curState, top._sucinfo);
112 this->successorGenerator->prepare(&curState, top.sucinfo);126 if (top._sucinfo.has_prev_state()) {
113 if (top.sucinfo.has_prev_state()) {127 _states.decode(working, top._sucinfo.last_state);
114 states.decode(working, top.sucinfo.last_state);
115 }128 }
116 if (!this->successorGenerator->next(working, top.sucinfo)) {129 if (!this->successorGenerator->next(working, top._sucinfo)) {
117 todo.pop();130 nested_todo.pop_back();
118 } else {131 } else {
119 if (this->is_weak && !this->successorGenerator->isAccepting(working)) {132 if (this->is_weak && !this->successorGenerator->isAccepting(working)) {
120 continue;133 continue;
121 }134 }
122 if (working == *seed) {135 if (working == state) {
123 violation = true;136 _violation = true;
124 if constexpr (SaveTrace) {
125 auto[_, stateid] = states.add(working);
126 auto seedId = stateid;
127 states.setHistory2(stateid, this->successorGenerator->fired());
128 size_t next = stateid;
129 // follow trace until back at seed state.
130 do {
131 auto[state, transition] = states.getHistory2(next);
132 nested_transitions.push(std::make_pair(state, transition));
133 next = state;
134 } while (next != seedId);
135 }
136 return;137 return;
137 }138 }
138 auto[_, stateid] = states.add(working);139 auto [is_new, stateid] = mark(working, MARKER2);
139 if (stateid == std::numeric_limits<size_t>::max()) {140 if (stateid == std::numeric_limits<size_t>::max())
140 continue;141 continue;
141 }142 top._sucinfo.last_state = stateid;
142 auto[it, is_new] = mark2.insert(stateid);
143 top.sucinfo.last_state = stateid;
144 if (is_new) {143 if (is_new) {
145 if constexpr (SaveTrace) {144 nested_todo.push_back(StackEntry{stateid, S::initial_suc_info()});
146 states.setParent(top.id);
147 states.setHistory2(stateid, this->successorGenerator->fired());
148 }
149 this->_discovered++;
150 todo.push(StackEntry{stateid, S::initial_suc_info()});
151 }145 }
152
153 }146 }
154 }147 }
155 }148 }
156149
157 template<typename S, typename W>150 template<typename S>
158 void NestedDepthFirstSearch<S, W>::printStats(std::ostream &os)151 void NestedDepthFirstSearch<S>::printStats(std::ostream &os)
159 {152 {
160 std::cout << "STATS:\n"153 std::cout << "STATS:\n"
161 << "\tdiscovered states: " << states.discovered() << std::endl154 << "\tdiscovered states: " << _states.discovered() << std::endl
162 << "\tmax tokens: " << states.max_tokens() << std::endl155 << "\tmax tokens: " << _states.max_tokens() << std::endl
163 << "\texplored states: " << mark1.size() << std::endl156 << "\texplored states: " << _mark_count[MARKER1] << std::endl
164 << "\texplored states (nested): " << mark2.size() << std::endl;157 << "\texplored states (nested): " << _mark_count[MARKER2] << std::endl;
165 }158 }
166159
167160
168 template<typename S, typename W>161 template<typename S>
169 void NestedDepthFirstSearch<S, W>::printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os)162 void NestedDepthFirstSearch<S>::print_trace(light_deque<StackEntry>& _todo, light_deque<StackEntry>& _nested_todo, std::ostream &os)
170 {163 {
171 State state = factory.newState();
172 os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"164 os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
173 "<trace>\n";165 "<trace>\n";
174 while (!transitions.empty()) {166 if(this->_reducer)
175 auto[stateid, transition] = transitions.top();167 this->_reducer->initFire(os);
176 states.decode(state, stateid);168 size_t loop_id = std::numeric_limits<size_t>::max();
177 this->printTransition(transition, state, os) << std::endl;169 // last element of todo-stack always has a "garbage" transition, it is the
178 transitions.pop();170 // current working element OR first element of nested.
171
172 if(!_todo.empty())
173 _todo.pop_back();
174 if(!_nested_todo.empty()) {
175 // here the last state is significant
176 // of the successor is the check that demonstrates the violation.
177 loop_id = _nested_todo.back()._id;
178 _nested_todo.pop_back();
179 }179 }
180 this->printLoop(os);
181 while (!nested_transitions.empty()) {
182 auto[stateid, transition] = nested_transitions.top();
183 states.decode(state, stateid);
184180
185 this->printTransition(transition, state, os) << std::endl;181 for(auto* stck : {&_todo, &_nested_todo})
186 nested_transitions.pop();182 {
183 while(!(*stck).empty())
184 {
185 auto& top = (*stck).front();
186 if(top._id == loop_id)
187 {
188 this->printLoop(os);
189 loop_id = std::numeric_limits<size_t>::max();
190 }
191 this->printTransition(top._sucinfo.transition(), os) << std::endl;
192 (*stck).pop_front();
193 }
187 }194 }
188 os << std::endl << "</trace>" << std::endl;195 os << std::endl << "</trace>" << std::endl;
189 }196 }
190197
191 template198 template
192 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;199 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator>;
193200
194 template201 template
195 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;202 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator>;
196
197 template
198 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
199
200 template
201 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
202
203}203}
204204
=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
--- src/LTL/Algorithm/TarjanModelChecker.cpp 2021-08-10 13:44:22 +0000
+++ src/LTL/Algorithm/TarjanModelChecker.cpp 2021-10-17 18:21:15 +0000
@@ -24,50 +24,62 @@
24 {24 {
25 this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;25 this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;
26 std::vector<State> initial_states = this->successorGenerator->makeInitialState();26 std::vector<State> initial_states = this->successorGenerator->makeInitialState();
27 State working = factory.newState();27 State working = this->_factory.newState();
28 State parent = factory.newState();28 State parent = this->_factory.newState();
29 for (auto &state : initial_states) {29 for (auto &state : initial_states) {
30 const auto res = seen.add(state);30 const auto res = _seen.add(state);
31 if (res.first) {31 if (res.first) {
32 push(state, res.second);32 push(state, res.second);
33 }33 }
34 while (!dstack.empty() && !violation) {34 while (!_dstack.empty() && !_violation) {
35 DEntry &dtop = dstack.top();35 DEntry &dtop = _dstack.top();
36 // write next successor state to working.36 // write next successor state to working.
37 if (!nexttrans(working, parent, dtop)) {37 if (!nexttrans(working, parent, dtop)) {
38 ++this->stats.expanded;38 ++this->stats.expanded;
39#ifndef NDEBUG
40 std::cerr << "backtrack\n";
41#endif
39 pop();42 pop();
40 continue;43 continue;
41 }44 }
45 auto fired = this->successorGenerator->fired();
46#ifndef NDEBUG
47 if (fired >= std::numeric_limits<uint32_t>::max() - 3) {
48 std::cerr << "looping\n";
49 }
50 else {
51 //state.print(*this->net, std::cerr); std::cerr << ": <transition id='" << this->net->transitionNames()[fired] << "'>" << std::endl ;
52 }
53#endif
42 ++this->stats.explored;54 ++this->stats.explored;
43 const auto[isnew, stateid] = seen.add(working);55 const auto[isnew, stateid] = _seen.add(working);
44 if (stateid == std::numeric_limits<idx_t>::max()) {56 if (stateid == std::numeric_limits<idx_t>::max()) {
45 continue;57 continue;
46 }58 }
4759
48 if constexpr (SaveTrace) {60 if constexpr (SaveTrace) {
49 if (isnew) {61 if (isnew) {
50 seen.setHistory(stateid, this->successorGenerator->fired());62 _seen.setHistory(stateid, this->successorGenerator->fired());
51 }63 }
52 }64 }
5365
54 dtop.sucinfo.last_state = stateid;66 dtop._sucinfo.last_state = stateid;
5567
56 // lookup successor in 'hash' table68 // lookup successor in 'hash' table
57 auto suc_pos = chash[hash(stateid)];69 auto suc_pos = _chash[hash(stateid)];
58 auto marking = seen.getMarkingId(stateid);70 auto marking = _seen.getMarkingId(stateid);
59 while (suc_pos != std::numeric_limits<idx_t>::max() && cstack[suc_pos].stateid != stateid) {71 while (suc_pos != std::numeric_limits<idx_t>::max() && _cstack[suc_pos]._stateid != stateid) {
60 if constexpr (IsSpooling) {72 if constexpr (_is_spooling) {
61 if (cstack[suc_pos].dstack && seen.getMarkingId(cstack[suc_pos].stateid) == marking) {73 if (_cstack[suc_pos]._dstack && _seen.getMarkingId(_cstack[suc_pos]._stateid) == marking) {
62 this->successorGenerator->generateAll(&parent, dtop.sucinfo);74 this->successorGenerator->generateAll(&parent, dtop._sucinfo);
63 }75 }
64 }76 }
65 suc_pos = cstack[suc_pos].next;77 suc_pos = _cstack[suc_pos]._next;
66 }78 }
67 if (suc_pos != std::numeric_limits<idx_t>::max()) {79 if (suc_pos != std::numeric_limits<idx_t>::max()) {
68 if constexpr (IsSpooling) {80 if constexpr (_is_spooling) {
69 if (cstack[suc_pos].dstack) {81 if (_cstack[suc_pos]._dstack) {
70 this->successorGenerator->generateAll(&parent, dtop.sucinfo);82 this->successorGenerator->generateAll(&parent, dtop._sucinfo);
71 }83 }
72 }84 }
73 // we found the successor, i.e. there's a loop!85 // we found the successor, i.e. there's a loop!
@@ -75,24 +87,24 @@
75 update(suc_pos);87 update(suc_pos);
76 continue;88 continue;
77 }89 }
78 if (store.find(stateid) == std::end(store)) {90 if (_store.find(stateid) == std::end(_store)) {
79 push(working, stateid);91 push(working, stateid);
80 }92 }
81 }93 }
82 if constexpr (SaveTrace) {94 if constexpr (SaveTrace) {
83 // print counter-example if it exists.95 // print counter-example if it exists.
84 if (violation) {96 if (_violation) {
85 std::stack<DEntry> revstack;97 std::stack<DEntry> revstack;
86 while (!dstack.empty()) {98 while (!_dstack.empty()) {
87 revstack.push(std::move(dstack.top()));99 revstack.push(std::move(_dstack.top()));
88 dstack.pop();100 _dstack.pop();
89 }101 }
90 printTrace(std::move(revstack));102 printTrace(std::move(revstack));
91 return false;103 return false;
92 }104 }
93 }105 }
94 }106 }
95 return !violation;107 return !_violation;
96 }108 }
97109
98 /**110 /**
@@ -101,20 +113,19 @@
101 */113 */
102 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>114 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
103 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::push(State &state, size_t stateid) {115 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::push(State &state, size_t stateid) {
104 const auto ctop = static_cast<idx_t>(cstack.size());116 const auto ctop = static_cast<idx_t>(_cstack.size());
105 const auto h = hash(stateid);117 const auto h = hash(stateid);
106 cstack.emplace_back(ctop, stateid, chash[h]);118 _cstack.emplace_back(ctop, stateid, _chash[h]);
107 chash[h] = ctop;119 _chash[h] = ctop;
108 dstack.push(DEntry{ctop});120 _dstack.push(DEntry{ctop});
109 if (this->successorGenerator->isAccepting(state)) {121 if (this->successorGenerator->isAccepting(state)) {
110 astack.push(ctop);122 _astack.push(ctop);
111 if (this->successorGenerator->has_invariant_self_loop(state) && !SaveTrace){123 if (this->successorGenerator->has_invariant_self_loop(state)){
112 //std::cerr << "Invariant self loop found. Violation is true" << std::endl;124 _violation = true;
113 violation = true;125 _invariant_loop = true;
114 invariant_loop = true;
115 }126 }
116 }127 }
117 if constexpr (IsSpooling) {128 if constexpr (_is_spooling) {
118 this->successorGenerator->push();129 this->successorGenerator->push();
119 }130 }
120 }131 }
@@ -122,27 +133,27 @@
122 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>133 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
123 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::pop()134 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::pop()
124 {135 {
125 const auto p = dstack.top().pos;136 const auto p = _dstack.top()._pos;
126 dstack.pop();137 _dstack.pop();
127 cstack[p].dstack = false;138 _cstack[p]._dstack = false;
128 if (cstack[p].lowlink == p) {139 if (_cstack[p]._lowlink == p) {
129 while (cstack.size() > p) {140 while (_cstack.size() > p) {
130 popCStack();141 popCStack();
131 }142 }
132 } else if (this->is_weak) {143 } else if (this->is_weak) {
133 State state = factory.newState();144 State state = this->_factory.newState();
134 seen.decode(state, cstack[p].stateid);145 _seen.decode(state, _cstack[p]._stateid);
135 if (!this->successorGenerator->isAccepting(state)) {146 if (!this->successorGenerator->isAccepting(state)) {
136 popCStack();147 popCStack();
137 }148 }
138 }149 }
139 if (!astack.empty() && p == astack.top()) {150 if (!_astack.empty() && p == _astack.top()) {
140 astack.pop();151 _astack.pop();
141 }152 }
142 if (!dstack.empty()) {153 if (!_dstack.empty()) {
143 update(p);154 update(p);
144 if constexpr (IsSpooling) {155 if constexpr (_is_spooling) {
145 this->successorGenerator->pop(dstack.top().sucinfo);156 this->successorGenerator->pop(_dstack.top()._sucinfo);
146 }157 }
147 }158 }
148 }159 }
@@ -150,28 +161,28 @@
150 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>161 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
151 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::popCStack()162 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::popCStack()
152 {163 {
153 auto h = hash(cstack.back().stateid);164 auto h = hash(_cstack.back()._stateid);
154 store.insert(cstack.back().stateid);165 _store.insert(_cstack.back()._stateid);
155 chash[h] = cstack.back().next;166 _chash[h] = _cstack.back()._next;
156 cstack.pop_back();167 _cstack.pop_back();
157 }168 }
158169
159 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>170 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
160 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::update(idx_t to)171 void TarjanModelChecker<S, G, SaveTrace, Spooler...>::update(idx_t to)
161 {172 {
162 const auto from = dstack.top().pos;173 const auto from = _dstack.top()._pos;
163 assert(cstack[to].lowlink != std::numeric_limits<idx_t>::max() && cstack[from].lowlink != std::numeric_limits<idx_t>::max());174 assert(_cstack[to]._lowlink != std::numeric_limits<idx_t>::max() && _cstack[from]._lowlink != std::numeric_limits<idx_t>::max());
164 if (cstack[to].lowlink <= cstack[from].lowlink) {175 if (_cstack[to]._lowlink <= _cstack[from]._lowlink) {
165 // we have now found a loop into earlier seen component cstack[to].lowlink.176 // we have now found a loop into earlier seen component cstack[to].lowlink.
166 // if this earlier component precedes an accepting state,177 // if this earlier component precedes an accepting state,
167 // the found loop is accepting and thus a violation.178 // the found loop is accepting and thus a violation.
168 violation = (!astack.empty() && to <= astack.top());179 _violation = (!_astack.empty() && to <= _astack.top());
169 // either way update the component ID of the state we came from.180 // either way update the component ID of the state we came from.
170 cstack[from].lowlink = cstack[to].lowlink;181 _cstack[from]._lowlink = _cstack[to]._lowlink;
171 if constexpr (SaveTrace) {182 if constexpr (SaveTrace) {
172 loopstate = cstack[from].stateid;183 _loop_state = _cstack[to]._stateid;
173 looptrans = this->successorGenerator->fired();184 _loop_trans = this->successorGenerator->fired();
174 cstack[from].lowsource = to;185 _cstack[from]._lowsource = to;
175186
176 }187 }
177 }188 }
@@ -180,13 +191,13 @@
180 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>191 template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
181 bool TarjanModelChecker<S, G, SaveTrace, Spooler...>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem)192 bool TarjanModelChecker<S, G, SaveTrace, Spooler...>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem)
182 {193 {
183 seen.decode(parent, cstack[delem.pos].stateid);194 _seen.decode(parent, _cstack[delem._pos]._stateid);
184 this->successorGenerator->prepare(&parent, delem.sucinfo);195 this->successorGenerator->prepare(&parent, delem._sucinfo);
185 // ensure that `state` buffer contains the correct state for Büchi successor generation.196 // ensure that `state` buffer contains the correct state for Büchi successor generation.
186 if (delem.sucinfo.has_prev_state()) {197 if (delem._sucinfo.has_prev_state()) {
187 seen.decode(state, delem.sucinfo.last_state);198 _seen.decode(state, delem._sucinfo.last_state);
188 }199 }
189 auto res = this->successorGenerator->next(state, delem.sucinfo);200 auto res = this->successorGenerator->next(state, delem._sucinfo);
190 return res;201 return res;
191 }202 }
192203
@@ -196,39 +207,49 @@
196 if constexpr (!SaveTrace) {207 if constexpr (!SaveTrace) {
197 return;208 return;
198 } else {209 } else {
199 assert(violation);210 assert(_violation);
200 State state = factory.newState();
201 os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"211 os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
202 "<trace>\n";212 "<trace>\n";
203 if (cstack[dstack.top().pos].stateid == loopstate) this->printLoop(os);213 this->_reducer->initFire(os);
204 cstack[dstack.top().pos].lowlink = std::numeric_limits<idx_t>::max();214 if (_cstack[dstack.top()._pos]._stateid == _loop_state)
215 this->printLoop(os);
205 dstack.pop();216 dstack.pop();
206 unsigned long p;217 unsigned long p;
218 bool had_deadlock = false;
207 // print (reverted) dstack219 // print (reverted) dstack
208 while (!dstack.empty()) {220 while (!dstack.empty()) {
209 p = dstack.top().pos;221 p = dstack.top()._pos;
210 auto stateid = cstack[p].stateid;
211 auto[parent, tid] = seen.getHistory(stateid);
212 seen.decode(state, parent);
213
214 if (stateid == loopstate) this->printLoop(os);
215 this->printTransition(tid, state, os) << '\n';
216
217 cstack[p].lowlink = std::numeric_limits<idx_t>::max();
218 dstack.pop();222 dstack.pop();
223 auto stateid = _cstack[p]._stateid;
224 auto[parent, tid] = _seen.getHistory(stateid);
225 this->printTransition(tid, os) << '\n';
226 if(tid >= std::numeric_limits<ptrie::uint>::max() - 1)
227 {
228 had_deadlock = true;
229 break;
230 }
231 if(_cstack[p]._stateid == _loop_state)
232 this->printLoop(os);
233 _cstack[p]._lowlink = std::numeric_limits<idx_t>::max();
219 }234 }
220 // follow previously found back edges via lowsource until back in dstack.235 // follow previously found back edges via lowsource until back in dstack.
221 assert(cstack[p].lowsource != std::numeric_limits<idx_t>::max());236 if(_cstack[p]._lowsource != std::numeric_limits<idx_t>::max() && !had_deadlock)
222 p = cstack[p].lowsource;237 {
223 while (cstack[p].lowlink != std::numeric_limits<idx_t>::max()) {238 p = _cstack[p]._lowsource;
224 auto[parent, tid] = seen.getHistory(cstack[p].stateid);239 while (_cstack[p]._lowlink != std::numeric_limits<idx_t>::max()) {
225 seen.decode(state, parent);240 auto[parent, tid] = _seen.getHistory(_cstack[p]._stateid);
226 this->printTransition(tid, state, os) << '\n';241 this->printTransition(tid, os) << '\n';
227 assert(cstack[p].lowsource != std::numeric_limits<idx_t>::max());242 if(tid >= std::numeric_limits<ptrie::uint>::max() - 1)
228 p = cstack[p].lowsource;243 {
244 had_deadlock = true;
245 break;
246 }
247 assert(_cstack[p]._lowsource != std::numeric_limits<idx_t>::max());
248 p = _cstack[p]._lowsource;
249 }
250 if(!had_deadlock)
251 this->printTransition(_loop_trans, os) << '\n';
229 }252 }
230 seen.decode(state, loopstate);
231 this->printTransition(looptrans, state, os) << '\n';
232253
233 os << "</trace>" << std::endl;254 os << "</trace>" << std::endl;
234 }255 }
235256
=== modified file 'src/LTL/LTLMain.cpp'
--- src/LTL/LTLMain.cpp 2021-08-10 13:44:22 +0000
+++ src/LTL/LTLMain.cpp 2021-10-17 18:21:15 +0000
@@ -71,9 +71,7 @@
71 }71 }
7272
73 template<typename Checker>73 template<typename Checker>
74 Result _verify(const PetriNet *net,74 Result _verify(std::unique_ptr<Checker> checker,
75 Condition_ptr &negatedQuery,
76 std::unique_ptr<Checker> checker,
77 const options_t &options)75 const options_t &options)
78 {76 {
79 Result result;77 Result result;
@@ -110,15 +108,14 @@
110 bool LTLMain(const PetriNet *net,108 bool LTLMain(const PetriNet *net,
111 const Condition_ptr &query,109 const Condition_ptr &query,
112 const std::string &queryName,110 const std::string &queryName,
113 options_t &options)111 options_t &options, const Reducer* reducer)
114 {112 {
115 auto res = to_ltl(query);
116 Condition_ptr negated_formula = res.first;
117 bool negate_answer = res.second;
118113
119 // force AP compress off for Büchi prints114 // force AP compress off for Büchi prints
120 options.ltl_compress_aps = options.buchi_out_file.empty() ? options.ltl_compress_aps : APCompression::None;115 options.ltl_compress_aps = options.buchi_out_file.empty() ? options.ltl_compress_aps : APCompression::None;
121116
117 auto [negated_formula, negate_answer] = to_ltl(query);
118
122 Structures::BuchiAutomaton automaton = makeBuchiAutomaton(negated_formula, options);119 Structures::BuchiAutomaton automaton = makeBuchiAutomaton(negated_formula, options);
123 if (!options.buchi_out_file.empty()) {120 if (!options.buchi_out_file.empty()) {
124 automaton.output_buchi(options.buchi_out_file, options.buchi_out_type);121 automaton.output_buchi(options.buchi_out_file, options.buchi_out_type);
@@ -127,7 +124,7 @@
127 bool is_visible_stub = options.stubbornreduction124 bool is_visible_stub = options.stubbornreduction
128 && (options.ltl_por == LTLPartialOrder::Visible || options.ltl_por == LTLPartialOrder::VisibleReach)125 && (options.ltl_por == LTLPartialOrder::Visible || options.ltl_por == LTLPartialOrder::VisibleReach)
129 && !net->has_inhibitor()126 && !net->has_inhibitor()
130 && !negated_formula->containsNext();127 && !negated_formula->containsNext();
131 bool is_autreach_stub = options.stubbornreduction128 bool is_autreach_stub = options.stubbornreduction
132 && (options.ltl_por == LTLPartialOrder::AutomatonReach ||129 && (options.ltl_por == LTLPartialOrder::AutomatonReach ||
133 options.ltl_por == LTLPartialOrder::VisibleReach)130 options.ltl_por == LTLPartialOrder::VisibleReach)
@@ -149,39 +146,17 @@
149 spooler = std::make_unique<EnabledSpooler>(net, gen);146 spooler = std::make_unique<EnabledSpooler>(net, gen);
150 gen.setSpooler(spooler.get());147 gen.setSpooler(spooler.get());
151 gen.setHeuristic(heuristic.get());148 gen.setHeuristic(heuristic.get());
149 result = _verify(
150 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator>>(
151 net, negated_formula, automaton, &gen, options.trace != TraceLevel::None, options.kbound, reducer),
152 options);
152153
153 if (options.trace != TraceLevel::None) {
154 result = _verify(
155 net, negated_formula,
156 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
157 net, negated_formula, automaton, &gen,
158 options.kbound),
159 options);
160 } else {
161 result = _verify(
162 net, negated_formula,
163 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
164 net, negated_formula, automaton, &gen,
165 options.kbound),
166 options);
167 }
168 } else {154 } else {
169 ResumingSuccessorGenerator gen{net};155 ResumingSuccessorGenerator gen{net};
170 if (options.trace != TraceLevel::None) {156 result = _verify(
171 result = _verify(157 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator>>(
172 net, negated_formula,158 net, negated_formula, automaton, &gen, options.trace != TraceLevel::None, options.kbound, reducer),
173 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(159 options);
174 net, negated_formula, automaton, &gen,
175 options.kbound),
176 options);
177 } else {
178 result = _verify(
179 net, negated_formula,
180 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
181 net, negated_formula, automaton, &gen,
182 options.kbound),
183 options);
184 }
185 }160 }
186 break;161 break;
187162
@@ -191,7 +166,6 @@
191 // Running default, BestFS, or RDFS search strategy so use spooling successor generator to enable heuristics.166 // Running default, BestFS, or RDFS search strategy so use spooling successor generator to enable heuristics.
192 SpoolingSuccessorGenerator gen{net, negated_formula};167 SpoolingSuccessorGenerator gen{net, negated_formula};
193 if (is_visible_stub) {168 if (is_visible_stub) {
194 std::cout << "Running stubborn version!" << std::endl;
195 spooler = std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula);169 spooler = std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula);
196 } else if (is_buchi_stub) {170 } else if (is_buchi_stub) {
197 spooler = std::make_unique<AutomatonStubbornSet>(*net, automaton);171 spooler = std::make_unique<AutomatonStubbornSet>(*net, automaton);
@@ -211,68 +185,62 @@
211185
212 if (options.trace != TraceLevel::None) {186 if (options.trace != TraceLevel::None) {
213 if (is_autreach_stub && is_visible_stub) {187 if (is_autreach_stub && is_visible_stub) {
214 result = _verify(net, negated_formula,188 result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>>(
215 std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>>(
216 net,189 net,
217 negated_formula,190 negated_formula,
218 automaton,191 automaton,
219 &gen,192 &gen,
220 options.kbound,193 options.kbound, reducer,
221 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),194 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
222 options);195 options);
223 }196 }
224 else if (is_autreach_stub && !is_visible_stub) {197 else if (is_autreach_stub && !is_visible_stub) {
225 result = _verify(net, negated_formula,198 result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, EnabledSpooler>>(
226 std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, EnabledSpooler>>(
227 net,199 net,
228 negated_formula,200 negated_formula,
229 automaton,201 automaton,
230 &gen,202 &gen,
231 options.kbound,203 options.kbound, reducer,
232 std::make_unique<EnabledSpooler>(net, gen)),204 std::make_unique<EnabledSpooler>(net, gen)),
233 options);205 options);
234 }206 }
235 else {207 else {
236 result = _verify(net, negated_formula,208 result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, true>>(
237 std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, true>>(
238 net,209 net,
239 negated_formula,210 negated_formula,
240 automaton,211 automaton,
241 &gen,212 &gen,
242 options.kbound),213 options.kbound, reducer),
243 options);214 options);
244 }215 }
245 } else {216 } else {
246217
247 if (is_autreach_stub && is_visible_stub) {218 if (is_autreach_stub && is_visible_stub) {
248 result = _verify(net, negated_formula,219 result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>>(
249 std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>>(
250 net,220 net,
251 negated_formula,221 negated_formula,
252 automaton,222 automaton,
253 &gen,223 &gen,
254 options.kbound,224 options.kbound, reducer,
255 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),225 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
256 options);226 options);
257 } else if (is_autreach_stub && !is_visible_stub) {227 } else if (is_autreach_stub && !is_visible_stub) {
258 result = _verify(net, negated_formula,228 result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, EnabledSpooler>>(
259 std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, EnabledSpooler>>(
260 net,229 net,
261 negated_formula,230 negated_formula,
262 automaton,231 automaton,
263 &gen,232 &gen,
264 options.kbound,233 options.kbound, reducer,
265 std::make_unique<EnabledSpooler>(net, gen)),234 std::make_unique<EnabledSpooler>(net, gen)),
266 options);235 options);
267 }236 }
268 else {237 else {
269 result = _verify(net, negated_formula,238 result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, false>>(
270 std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, false>>(
271 net,239 net,
272 negated_formula,240 negated_formula,
273 automaton,241 automaton,
274 &gen,242 &gen,
275 options.kbound),243 options.kbound, reducer),
276 options);244 options);
277 }245 }
278 }246 }
@@ -281,22 +249,20 @@
281249
282 // no spooling needed, thus use resuming successor generation250 // no spooling needed, thus use resuming successor generation
283 if (options.trace != TraceLevel::None) {251 if (options.trace != TraceLevel::None) {
284 result = _verify(net, negated_formula,252 result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, true>>(
285 std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, true>>(
286 net,253 net,
287 negated_formula,254 negated_formula,
288 automaton,255 automaton,
289 &gen,256 &gen,
290 options.kbound),257 options.kbound, reducer),
291 options);258 options);
292 } else {259 } else {
293 result = _verify(net, negated_formula,260 result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, false>>(
294 std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, false>>(
295 net,261 net,
296 negated_formula,262 negated_formula,
297 automaton,263 automaton,
298 &gen,264 &gen,
299 options.kbound),265 options.kbound, reducer),
300 options);266 options);
301 }267 }
302 }268 }
303269
=== modified file 'src/LTL/Stubborn/AutomatonStubbornSet.cpp'
--- src/LTL/Stubborn/AutomatonStubbornSet.cpp 2021-04-29 13:19:53 +0000
+++ src/LTL/Stubborn/AutomatonStubbornSet.cpp 2021-10-17 18:21:15 +0000
@@ -28,7 +28,7 @@
28 public:28 public:
29 NondeterministicConjunctionVisitor(AutomatonStubbornSet &stubbornSet) :29 NondeterministicConjunctionVisitor(AutomatonStubbornSet &stubbornSet) :
30 InterestingLTLTransitionVisitor(stubbornSet, false),30 InterestingLTLTransitionVisitor(stubbornSet, false),
31 _stubborn(stubbornSet), _net(stubbornSet._net) {}31 _net(stubbornSet._net), _stubborn(stubbornSet){}
3232
33 protected:33 protected:
34 static constexpr auto PresetBad = StubbornSet::PresetBad;34 static constexpr auto PresetBad = StubbornSet::PresetBad;
3535
=== modified file 'src/LTL/Stubborn/SafeAutStubbornSet.cpp'
--- src/LTL/Stubborn/SafeAutStubbornSet.cpp 2021-05-13 09:19:31 +0000
+++ src/LTL/Stubborn/SafeAutStubbornSet.cpp 2021-10-17 18:21:15 +0000
@@ -16,6 +16,7 @@
16 */16 */
1717
18#include "LTL/Stubborn/SafeAutStubbornSet.h"18#include "LTL/Stubborn/SafeAutStubbornSet.h"
19#include "LTL/Stubborn/VisibleTransitionVisitor.h"
1920
20namespace LTL {21namespace LTL {
21 using namespace PetriEngine;22 using namespace PetriEngine;
@@ -28,37 +29,84 @@
2829
29 constructEnabled();30 constructEnabled();
30 if (_ordering.empty()) {31 if (_ordering.empty()) {
32 _print_debug();
31 return false;33 return false;
32 }34 }
33 if (_ordering.size() == 1) {35 if (_ordering.size() == 1) {
34 _stubborn[_ordering.front()] = true;36 _stubborn[_ordering.front()] = true;
37 _print_debug();
35 return true;38 return true;
36 }39 }
3740
41 InterestingLTLTransitionVisitor unsafe{*this, false};
38 InterestingTransitionVisitor interesting{*this, false};42 InterestingTransitionVisitor interesting{*this, false};
3943
40 for (auto &q : _queries) {44 PQL::EvaluationContext ctx((*_parent).marking(), &_net);
41 q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));45 _prog_cond->evalAndSet(ctx);
42 q->visit(interesting);46 _sink_cond->evalAndSet(ctx);
43 }47 _prog_cond->visit(unsafe);
48 _sink_cond->visit(unsafe);
49
50 //_ret_cond->evalAndSet(ctx);
51 //(std::make_shared<PetriEngine::PQL::NotCondition>(_ret_cond))->visit(interesting);
52
44 assert(!_bad);53 assert(!_bad);
4554
46 _unsafe.swap(_stubborn);55 _unsafe.swap(_stubborn);
56 _has_enabled_stubborn = false;
47 //memset(_stubborn.get(), false, sizeof(bool) * _net.numberOfTransitions());57 //memset(_stubborn.get(), false, sizeof(bool) * _net.numberOfTransitions());
48 _unprocessed.clear();58 _unprocessed.clear();
49 memset(_places_seen.get(), 0, _net.numberOfPlaces());59 memset(_places_seen.get(), 0, _net.numberOfPlaces());
5060
51 assert(_unprocessed.empty());61 assert(_unprocessed.empty());
5262
53 for (auto &q : _queries) {63
54 q->visit(interesting);64
65 // sink condition is not interesting, just unsafe.
66 _prog_cond->visit(interesting);
67 //_sink_cond->visit(interesting);
68 closure();
69 if (_bad) {
70 // abort
71 set_all_stubborn();
72 _print_debug();
73 return true;
74 }
75 // accepting states need key transition. add firs t enabled by index.
76 if (state->is_accepting() && !_has_enabled_stubborn) {
77 //set_all_stubborn();
78 //_print_debug();
79 //return true;
80 addToStub(_ordering.front());
55 closure();81 closure();
82/* for (int i = 0; i < _net.numberOfPlaces(); ++i) {
83 if (_enabled[i]) {
84 addToStub(i);
85 closure();
86 break;
87 }
88 }*/
56 if (_bad) {89 if (_bad) {
57 // abort
58 set_all_stubborn();90 set_all_stubborn();
59 return true;
60 }91 }
61 }92 }
93 _print_debug();
62 return true;94 return true;
63 }95 }
64}
65\ No newline at end of file96\ No newline at end of file
97
98 void SafeAutStubbornSet::_print_debug() {
99#ifndef NDEBUG
100 float num_stubborn = 0;
101 float num_enabled = 0;
102 float num_enabled_stubborn = 0;
103 for (int i = 0; i < _net.numberOfTransitions(); ++i) {
104 if (_stubborn[i]) ++num_stubborn;
105 if (_enabled[i]) ++num_enabled;
106 if (_stubborn[i] && _enabled[i]) ++num_enabled_stubborn;
107 }
108 std::cerr << "Enabled: " << num_enabled << "/" << _net.numberOfTransitions() << " (" << num_enabled/_net.numberOfTransitions()*100.0 << "%),\t\t "
109 << "Stubborn: " << num_stubborn << "/" << _net.numberOfTransitions() << " (" << num_stubborn/_net.numberOfTransitions()*100.0 << "%),\t\t "
110 << "Enabled stubborn: " << num_enabled_stubborn << "/" << num_enabled << " (" << num_enabled_stubborn/num_enabled*100.0 << "%)" << std::endl;
111#endif
112 }
113}
66114
=== modified file 'src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp'
--- src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp 2021-04-29 07:47:52 +0000
+++ src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp 2021-10-17 18:21:15 +0000
@@ -34,13 +34,13 @@
34 }34 }
3535
3636
37 void ResumingSuccessorGenerator::prepare(const Structures::State* state, const successor_info &sucinfo) {37 void ResumingSuccessorGenerator::prepare(const Structures::State* state, const successor_info_t &sucinfo) {
38 SuccessorGenerator::prepare(state);38 SuccessorGenerator::prepare(state);
39 _suc_pcounter = sucinfo.pcounter;39 _suc_pcounter = sucinfo.pcounter;
40 _suc_tcounter = sucinfo.tcounter;40 _suc_tcounter = sucinfo.tcounter;
41 }41 }
4242
43 void ResumingSuccessorGenerator::getSuccInfo(successor_info &sucinfo) const {43 void ResumingSuccessorGenerator::get_succ_info(successor_info_t &sucinfo) const {
44 sucinfo.pcounter = _suc_pcounter;44 sucinfo.pcounter = _suc_pcounter;
45 sucinfo.tcounter = _suc_tcounter;45 sucinfo.tcounter = _suc_tcounter;
46 }46 }
4747
=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp 2021-08-21 10:20:38 +0000
+++ src/PetriEngine/PQL/Expressions.cpp 2021-10-17 18:21:15 +0000
@@ -3,17 +3,17 @@
3 * Thomas Søndersø Nielsen <primogens@gmail.com>,3 * Thomas Søndersø Nielsen <primogens@gmail.com>,
4 * Lars Kærlund Østergaard <larsko@gmail.com>,4 * Lars Kærlund Østergaard <larsko@gmail.com>,
5 * Peter Gjøl Jensen <root@petergjoel.dk>5 * Peter Gjøl Jensen <root@petergjoel.dk>
6 * 6 *
7 * This program is free software: you can redistribute it and/or modify7 * This program is free software: you can redistribute it and/or modify
8 * it under the terms of the GNU General Public License as published by8 * it under the terms of the GNU General Public License as published by
9 * the Free Software Foundation, either version 3 of the License, or9 * the Free Software Foundation, either version 3 of the License, or
10 * (at your option) any later version.10 * (at your option) any later version.
11 * 11 *
12 * This program is distributed in the hope that it will be useful,12 * This program is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.15 * GNU General Public License for more details.
16 * 16 *
17 * You should have received a copy of the GNU General Public License17 * You should have received a copy of the GNU General Public License
18 * along with this program. If not, see <http://www.gnu.org/licenses/>.18 * along with this program. If not, see <http://www.gnu.org/licenses/>.
19 */19 */
@@ -38,7 +38,7 @@
3838
39namespace PetriEngine {39namespace PetriEngine {
40 namespace PQL {40 namespace PQL {
41 41
42 std::ostream& generateTabs(std::ostream& out, uint32_t tabs) {42 std::ostream& generateTabs(std::ostream& out, uint32_t tabs) {
4343
44 for(uint32_t i = 0; i < tabs; i++) {44 for(uint32_t i = 0; i < tabs; i++) {
@@ -46,7 +46,7 @@
46 }46 }
47 return out;47 return out;
48 }48 }
49 49
50 /** FOR COMPILING AND CONSTRUCTING LOGICAL OPERATORS **/50 /** FOR COMPILING AND CONSTRUCTING LOGICAL OPERATORS **/
5151
52 template<typename T>52 template<typename T>
@@ -61,7 +61,7 @@
61 _conds.emplace_back(ptr);61 _conds.emplace_back(ptr);
62 }62 }
63 else if (auto comp = std::dynamic_pointer_cast<CompareCondition>(ptr))63 else if (auto comp = std::dynamic_pointer_cast<CompareCondition>(ptr))
64 { 64 {
65 if((std::is_same<T, AndCondition>::value && std::dynamic_pointer_cast<NotEqualCondition>(ptr)) ||65 if((std::is_same<T, AndCondition>::value && std::dynamic_pointer_cast<NotEqualCondition>(ptr)) ||
66 (std::is_same<T, OrCondition>::value && std::dynamic_pointer_cast<EqualCondition>(ptr)))66 (std::is_same<T, OrCondition>::value && std::dynamic_pointer_cast<EqualCondition>(ptr)))
67 {67 {
@@ -113,7 +113,7 @@
113 }113 }
114 else114 else
115 {115 {
116 _conds.emplace_back(ptr); 116 _conds.emplace_back(ptr);
117 }117 }
118 }118 }
119 else119 else
@@ -122,7 +122,7 @@
122 }122 }
123123
124 }124 }
125 125
126 template<typename T, bool K>126 template<typename T, bool K>
127 Condition_ptr makeLog(const std::vector<Condition_ptr>& conds, bool aggressive)127 Condition_ptr makeLog(const std::vector<Condition_ptr>& conds, bool aggressive)
128 {128 {
@@ -138,28 +138,28 @@
138 return BooleanCondition::getShared(K);138 return BooleanCondition::getShared(K);
139 return res;139 return res;
140 }140 }
141 141
142 Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr) 142 Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr)
143 { return makeLog<OrCondition,false>(cptr, true); }143 { return makeLog<OrCondition,false>(cptr, true); }
144 Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr) 144 Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr)
145 { return makeLog<AndCondition,true>(cptr, true); }145 { return makeLog<AndCondition,true>(cptr, true); }
146 Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) { 146 Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) {
147 std::vector<Condition_ptr> cnds{a,b};147 std::vector<Condition_ptr> cnds{a,b};
148 return makeLog<OrCondition,false>(cnds, true); 148 return makeLog<OrCondition,false>(cnds, true);
149 }149 }
150 Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b) 150 Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b)
151 { 151 {
152 std::vector<Condition_ptr> cnds{a,b};152 std::vector<Condition_ptr> cnds{a,b};
153 return makeLog<AndCondition,true>(cnds, true); 153 return makeLog<AndCondition,true>(cnds, true);
154 }154 }
155 155
156 156
157 // CONSTANTS157 // CONSTANTS
158 Condition_ptr BooleanCondition::FALSE_CONSTANT = std::make_shared<BooleanCondition>(false);158 Condition_ptr BooleanCondition::FALSE_CONSTANT = std::make_shared<BooleanCondition>(false);
159 Condition_ptr BooleanCondition::TRUE_CONSTANT = std::make_shared<BooleanCondition>(true);159 Condition_ptr BooleanCondition::TRUE_CONSTANT = std::make_shared<BooleanCondition>(true);
160 Condition_ptr DeadlockCondition::DEADLOCK = std::make_shared<DeadlockCondition>();160 Condition_ptr DeadlockCondition::DEADLOCK = std::make_shared<DeadlockCondition>();
161 161
162 162
163 Condition_ptr BooleanCondition::getShared(bool val)163 Condition_ptr BooleanCondition::getShared(bool val)
164 {164 {
165 if(val)165 if(val)
@@ -178,7 +178,7 @@
178 out << op() << " ";178 out << op() << " ";
179 _cond->toTAPAALQuery(out,context);179 _cond->toTAPAALQuery(out,context);
180 }180 }
181 181
182 void UntilCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {182 void UntilCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
183 out << op() << " (";183 out << op() << " (";
184 _cond1->toTAPAALQuery(out, context);184 _cond1->toTAPAALQuery(out, context);
@@ -186,7 +186,7 @@
186 _cond2->toTAPAALQuery(out,context);186 _cond2->toTAPAALQuery(out,context);
187 out << ")";187 out << ")";
188 }188 }
189 189
190 void LogicalCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {190 void LogicalCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
191 out << "(";191 out << "(";
192 _conds[0]->toTAPAALQuery(out, context);192 _conds[0]->toTAPAALQuery(out, context);
@@ -197,7 +197,7 @@
197 }197 }
198 out << ")";198 out << ")";
199 }199 }
200 200
201 void CompareConjunction::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {201 void CompareConjunction::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
202 out << "(";202 out << "(";
203 if(_negated) out << "!";203 if(_negated) out << "!";
@@ -205,11 +205,11 @@
205 for(auto& c : _constraints)205 for(auto& c : _constraints)
206 {206 {
207 if(!first) out << " and ";207 if(!first) out << " and ";
208 if(c._lower != 0) 208 if(c._lower != 0)
209 out << "(" << c._lower << " <= " << context.netName << "." << c._name << ")";209 out << "(" << c._lower << " <= " << context.netName << "." << c._name << ")";
210 if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max()) 210 if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())
211 out << " and ";211 out << " and ";
212 if(c._lower != 0) 212 if(c._lower != 0)
213 out << "(" << c._upper << " >= " << context.netName << "." << c._name << ")";213 out << "(" << c._upper << " >= " << context.netName << "." << c._name << ")";
214 first = false;214 first = false;
215 }215 }
@@ -270,7 +270,7 @@
270 }270 }
271 out << ")";271 out << ")";
272 }272 }
273 273
274 /******************** opTAPAAL ********************/274 /******************** opTAPAAL ********************/
275275
276 std::string EqualCondition::opTAPAAL() const {276 std::string EqualCondition::opTAPAAL() const {
@@ -405,16 +405,16 @@
405 void SimpleQuantifierCondition::analyze(AnalysisContext& context) {405 void SimpleQuantifierCondition::analyze(AnalysisContext& context) {
406 _cond->analyze(context);406 _cond->analyze(context);
407 }407 }
408 408
409 void UntilCondition::analyze(AnalysisContext& context) {409 void UntilCondition::analyze(AnalysisContext& context) {
410 _cond1->analyze(context);410 _cond1->analyze(context);
411 _cond2->analyze(context);411 _cond2->analyze(context);
412 }412 }
413 413
414 void LogicalCondition::analyze(AnalysisContext& context) {414 void LogicalCondition::analyze(AnalysisContext& context) {
415 for(auto& c : _conds) c->analyze(context);415 for(auto& c : _conds) c->analyze(context);
416 }416 }
417 417
418 void UnfoldedFireableCondition::_analyze(AnalysisContext& context)418 void UnfoldedFireableCondition::_analyze(AnalysisContext& context)
419 {419 {
420 std::vector<Condition_ptr> conds;420 std::vector<Condition_ptr> conds;
@@ -425,7 +425,7 @@
425 _name.length());425 _name.length());
426 context.reportError(error);426 context.reportError(error);
427 return;427 return;
428 } 428 }
429429
430 assert(_name.compare(context.net()->transitionNames()[result.offset]) == 0);430 assert(_name.compare(context.net()->transitionNames()[result.offset]) == 0);
431 auto preset = context.net()->preset(result.offset);431 auto preset = context.net()->preset(result.offset);
@@ -462,9 +462,9 @@
462 ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());462 ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
463 coloredContext->reportError(error);463 coloredContext->reportError(error);
464 return;464 return;
465 } 465 }
466 if(names.size() < 1){466 if(names.size() < 1){
467 //If the transition points to empty vector we know that it has 467 //If the transition points to empty vector we know that it has
468 //no legal bindings and can never fire468 //no legal bindings and can never fire
469 _compiled = std::make_shared<BooleanCondition>(false);469 _compiled = std::make_shared<BooleanCondition>(false);
470 _compiled->analyze(context);470 _compiled->analyze(context);
@@ -497,7 +497,7 @@
497 _expr1->analyze(context);497 _expr1->analyze(context);
498 _expr2->analyze(context);498 _expr2->analyze(context);
499 }499 }
500 500
501 void NotCondition::analyze(AnalysisContext& context) {501 void NotCondition::analyze(AnalysisContext& context) {
502 _cond->analyze(context);502 _cond->analyze(context);
503 }503 }
@@ -639,7 +639,7 @@
639 }639 }
640 _compiled->analyze(context);640 _compiled->analyze(context);
641 }641 }
642 642
643 void UnfoldedUpperBoundsCondition::analyze(AnalysisContext& c)643 void UnfoldedUpperBoundsCondition::analyze(AnalysisContext& c)
644 {644 {
645 for(auto& p : _places)645 for(auto& p : _places)
@@ -833,7 +833,7 @@
833 setUpperBound(value(context.marking()));833 setUpperBound(value(context.marking()));
834 return _max <= _bound ? RTRUE : RUNKNOWN;834 return _max <= _bound ? RTRUE : RUNKNOWN;
835 }835 }
836 836
837 /******************** Evaluation - save result ********************/837 /******************** Evaluation - save result ********************/
838 Condition::Result SimpleQuantifierCondition::evalAndSet(const EvaluationContext& context) {838 Condition::Result SimpleQuantifierCondition::evalAndSet(const EvaluationContext& context) {
839 return RUNKNOWN;839 return RUNKNOWN;
@@ -880,14 +880,14 @@
880 setSatisfied(res);880 setSatisfied(res);
881 return res;881 return res;
882 }882 }
883 883
884 Condition::Result UntilCondition::evalAndSet(const EvaluationContext& context) {884 Condition::Result UntilCondition::evalAndSet(const EvaluationContext& context) {
885 auto r2 = _cond2->evalAndSet(context);885 auto r2 = _cond2->evalAndSet(context);
886 if(r2 != RFALSE) return r2;886 if(r2 != RFALSE) return r2;
887 auto r1 = _cond1->evalAndSet(context);887 auto r1 = _cond1->evalAndSet(context);
888 if(r1 == RFALSE) return RFALSE;888 if(r1 == RFALSE) return RFALSE;
889 return RUNKNOWN;889 return RUNKNOWN;
890 } 890 }
891891
892 int Expr::evalAndSet(const EvaluationContext& context) {892 int Expr::evalAndSet(const EvaluationContext& context) {
893 int r = evaluate(context);893 int r = evaluate(context);
@@ -939,7 +939,7 @@
939 setSatisfied(res);939 setSatisfied(res);
940 return res;940 return res;
941 }941 }
942 942
943 Condition::Result CompareCondition::evalAndSet(const EvaluationContext& context) {943 Condition::Result CompareCondition::evalAndSet(const EvaluationContext& context) {
944 int v1 = _expr1->evalAndSet(context);944 int v1 = _expr1->evalAndSet(context);
945 int v2 = _expr2->evalAndSet(context);945 int v2 = _expr2->evalAndSet(context);
@@ -966,7 +966,7 @@
966 setSatisfied(context.net()->deadlocked(context.marking()));966 setSatisfied(context.net()->deadlocked(context.marking()));
967 return isSatisfied() ? RTRUE : RFALSE;967 return isSatisfied() ? RTRUE : RFALSE;
968 }968 }
969 969
970 Condition::Result UnfoldedUpperBoundsCondition::evalAndSet(const EvaluationContext& context)970 Condition::Result UnfoldedUpperBoundsCondition::evalAndSet(const EvaluationContext& context)
971 {971 {
972 auto res = evaluate(context);972 auto res = evaluate(context);
@@ -990,12 +990,12 @@
990 {990 {
991 ctx.accept<decltype(this)>(this);991 ctx.accept<decltype(this)>(this);
992 }992 }
993 993
994 void EXCondition::visit(Visitor& ctx) const994 void EXCondition::visit(Visitor& ctx) const
995 {995 {
996 ctx.accept<decltype(this)>(this);996 ctx.accept<decltype(this)>(this);
997 }997 }
998 998
999 void EFCondition::visit(Visitor& ctx) const999 void EFCondition::visit(Visitor& ctx) const
1000 {1000 {
1001 ctx.accept<decltype(this)>(this);1001 ctx.accept<decltype(this)>(this);
@@ -1004,7 +1004,7 @@
1004 void AUCondition::visit(Visitor& ctx) const1004 void AUCondition::visit(Visitor& ctx) const
1005 {1005 {
1006 ctx.accept<decltype(this)>(this);1006 ctx.accept<decltype(this)>(this);
1007 } 1007 }
10081008
1009 void AXCondition::visit(Visitor& ctx) const1009 void AXCondition::visit(Visitor& ctx) const
1010 {1010 {
@@ -1014,7 +1014,7 @@
1014 void AFCondition::visit(Visitor& ctx) const1014 void AFCondition::visit(Visitor& ctx) const
1015 {1015 {
1016 ctx.accept<decltype(this)>(this);1016 ctx.accept<decltype(this)>(this);
1017 } 1017 }
10181018
1019 void AGCondition::visit(Visitor& ctx) const1019 void AGCondition::visit(Visitor& ctx) const
1020 {1020 {
@@ -1060,7 +1060,7 @@
1060 {1060 {
1061 ctx.accept<decltype(this)>(this);1061 ctx.accept<decltype(this)>(this);
1062 }1062 }
1063 1063
1064 void EqualCondition::visit(Visitor& ctx) const1064 void EqualCondition::visit(Visitor& ctx) const
1065 {1065 {
1066 ctx.accept<decltype(this)>(this);1066 ctx.accept<decltype(this)>(this);
@@ -1075,22 +1075,22 @@
1075 {1075 {
1076 ctx.accept<decltype(this)>(this);1076 ctx.accept<decltype(this)>(this);
1077 }1077 }
1078 1078
1079 void LessThanOrEqualCondition::visit(Visitor& ctx) const1079 void LessThanOrEqualCondition::visit(Visitor& ctx) const
1080 {1080 {
1081 ctx.accept<decltype(this)>(this);1081 ctx.accept<decltype(this)>(this);
1082 }1082 }
1083 1083
1084 void LessThanCondition::visit(Visitor& ctx) const1084 void LessThanCondition::visit(Visitor& ctx) const
1085 {1085 {
1086 ctx.accept<decltype(this)>(this);1086 ctx.accept<decltype(this)>(this);
1087 }1087 }
1088 1088
1089 void BooleanCondition::visit(Visitor& ctx) const1089 void BooleanCondition::visit(Visitor& ctx) const
1090 {1090 {
1091 ctx.accept<decltype(this)>(this);1091 ctx.accept<decltype(this)>(this);
1092 }1092 }
1093 1093
1094 void DeadlockCondition::visit(Visitor& ctx) const1094 void DeadlockCondition::visit(Visitor& ctx) const
1095 {1095 {
1096 ctx.accept<decltype(this)>(this);1096 ctx.accept<decltype(this)>(this);
@@ -1143,7 +1143,7 @@
1143 else1143 else
1144 ctx.accept<decltype(this)>(this);1144 ctx.accept<decltype(this)>(this);
1145 }1145 }
1146 1146
1147 void UnfoldedFireableCondition::visit(Visitor& ctx) const1147 void UnfoldedFireableCondition::visit(Visitor& ctx) const
1148 {1148 {
1149 if(_compiled)1149 if(_compiled)
@@ -1152,12 +1152,12 @@
1152 ctx.accept<decltype(this)>(this);1152 ctx.accept<decltype(this)>(this);
1153 }1153 }
11541154
1155 1155
1156 void UnfoldedUpperBoundsCondition::visit(Visitor& ctx) const1156 void UnfoldedUpperBoundsCondition::visit(Visitor& ctx) const
1157 {1157 {
1158 ctx.accept<decltype(this)>(this);1158 ctx.accept<decltype(this)>(this);
1159 }1159 }
1160 1160
1161 void LiteralExpr::visit(Visitor& ctx) const1161 void LiteralExpr::visit(Visitor& ctx) const
1162 {1162 {
1163 ctx.accept<decltype(this)>(this);1163 ctx.accept<decltype(this)>(this);
@@ -1393,7 +1393,7 @@
1393 int MultiplyExpr::apply(int v1, int v2) const {1393 int MultiplyExpr::apply(int v1, int v2) const {
1394 return v1 * v2;1394 return v1 * v2;
1395 }1395 }
1396 1396
1397 /******************** Apply (CompareCondition subclasses) ********************/1397 /******************** Apply (CompareCondition subclasses) ********************/
13981398
1399 bool EqualCondition::apply(int v1, int v2) const {1399 bool EqualCondition::apply(int v1, int v2) const {
@@ -1425,7 +1425,7 @@
1425 std::string MultiplyExpr::op() const {1425 std::string MultiplyExpr::op() const {
1426 return "*";1426 return "*";
1427 }1427 }
1428 1428
1429 /******************** Op (QuantifierCondition subclasses) ********************/1429 /******************** Op (QuantifierCondition subclasses) ********************/
14301430
1431 std::string ACondition::op() const {1431 std::string ACondition::op() const {
@@ -1447,27 +1447,27 @@
1447 std::string XCondition::op() const {1447 std::string XCondition::op() const {
1448 return "X";1448 return "X";
1449 }1449 }
1450 1450
1451 std::string EXCondition::op() const {1451 std::string EXCondition::op() const {
1452 return "EX";1452 return "EX";
1453 }1453 }
1454 1454
1455 std::string EGCondition::op() const {1455 std::string EGCondition::op() const {
1456 return "EG";1456 return "EG";
1457 }1457 }
1458 1458
1459 std::string EFCondition::op() const {1459 std::string EFCondition::op() const {
1460 return "EF";1460 return "EF";
1461 }1461 }
1462 1462
1463 std::string AXCondition::op() const {1463 std::string AXCondition::op() const {
1464 return "AX";1464 return "AX";
1465 }1465 }
1466 1466
1467 std::string AGCondition::op() const {1467 std::string AGCondition::op() const {
1468 return "AG";1468 return "AG";
1469 }1469 }
1470 1470
1471 std::string AFCondition::op() const {1471 std::string AFCondition::op() const {
1472 return "AF";1472 return "AF";
1473 }1473 }
@@ -1481,11 +1481,11 @@
1481 std::string EUCondition::op() const {1481 std::string EUCondition::op() const {
1482 return "E";1482 return "E";
1483 }1483 }
1484 1484
1485 std::string AUCondition::op() const {1485 std::string AUCondition::op() const {
1486 return "A";1486 return "A";
1487 }1487 }
1488 1488
1489 /******************** Op (LogicalCondition subclasses) ********************/1489 /******************** Op (LogicalCondition subclasses) ********************/
14901490
1491 std::string AndCondition::op() const {1491 std::string AndCondition::op() const {
@@ -1514,7 +1514,7 @@
1514 return "<=";1514 return "<=";
1515 }1515 }
15161516
1517 /******************** free of places ********************/ 1517 /******************** free of places ********************/
15181518
1519 bool NaryExpr::placeFree() const1519 bool NaryExpr::placeFree() const
1520 {1520 {
@@ -1523,18 +1523,18 @@
1523 return false;1523 return false;
1524 return true;1524 return true;
1525 }1525 }
1526 1526
1527 bool CommutativeExpr::placeFree() const1527 bool CommutativeExpr::placeFree() const
1528 {1528 {
1529 if(_ids.size() > 0) return false;1529 if(_ids.size() > 0) return false;
1530 return NaryExpr::placeFree();1530 return NaryExpr::placeFree();
1531 }1531 }
1532 1532
1533 bool MinusExpr::placeFree() const1533 bool MinusExpr::placeFree() const
1534 {1534 {
1535 return _expr->placeFree();1535 return _expr->placeFree();
1536 }1536 }
1537 1537
1538 /******************** Expr::type() implementation ********************/1538 /******************** Expr::type() implementation ********************/
15391539
1540 Expr::Types PlusExpr::type() const {1540 Expr::Types PlusExpr::type() const {
@@ -1610,17 +1610,17 @@
1610 return 0;1610 return 0;
1611 }1611 }
16121612
1613 uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const 1613 uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const
1614 {1614 {
1615 size_t tmp = 0;1615 size_t tmp = 0;
1616 for(auto& p : _places)1616 for(auto& p : _places)
1617 {1617 {
1618 tmp += context.marking()[p._place];1618 tmp += context.marking()[p._place];
1619 }1619 }
1620 1620
1621 return _max - tmp;1621 return _max - tmp;
1622 }1622 }
1623 1623
1624 uint32_t EFCondition::distance(DistanceContext& context) const {1624 uint32_t EFCondition::distance(DistanceContext& context) const {
1625 return _cond->distance(context);1625 return _cond->distance(context);
1626 }1626 }
@@ -1636,14 +1636,14 @@
1636 uint32_t EUCondition::distance(DistanceContext& context) const {1636 uint32_t EUCondition::distance(DistanceContext& context) const {
1637 return _cond2->distance(context);1637 return _cond2->distance(context);
1638 }1638 }
1639 1639
1640 uint32_t AFCondition::distance(DistanceContext& context) const {1640 uint32_t AFCondition::distance(DistanceContext& context) const {
1641 context.negate();1641 context.negate();
1642 uint32_t retval = _cond->distance(context);1642 uint32_t retval = _cond->distance(context);
1643 context.negate();1643 context.negate();
1644 return retval;1644 return retval;
1645 }1645 }
1646 1646
1647 uint32_t AXCondition::distance(DistanceContext& context) const {1647 uint32_t AXCondition::distance(DistanceContext& context) const {
1648 context.negate();1648 context.negate();
1649 uint32_t retval = _cond->distance(context);1649 uint32_t retval = _cond->distance(context);
@@ -1665,7 +1665,7 @@
1665 context.negate();1665 context.negate();
1666 return r1 + r2;1666 return r1 + r2;
1667 }1667 }
1668 1668
1669 uint32_t CompareConjunction::distance(DistanceContext& context) const {1669 uint32_t CompareConjunction::distance(DistanceContext& context) const {
1670 uint32_t d = 0;1670 uint32_t d = 0;
1671 auto neg = context.negated() != _negated;1671 auto neg = context.negated() != _negated;
@@ -1691,7 +1691,7 @@
1691 else d = std::min(d, d2);1691 else d = std::min(d, d2);
1692 first = false;1692 first = false;
1693 }1693 }
1694 1694
1695 if(c._lower != 0)1695 if(c._lower != 0)
1696 {1696 {
1697 auto d2 = delta<LessThanOrEqualCondition>(c._upper, pv, neg);1697 auto d2 = delta<LessThanOrEqualCondition>(c._upper, pv, neg);
@@ -1739,35 +1739,35 @@
1739 int d;1739 int d;
1740 unsigned int p;1740 unsigned int p;
1741 };1741 };
1742 1742
1743 uint32_t LessThanOrEqualCondition::distance(DistanceContext& context) const {1743 uint32_t LessThanOrEqualCondition::distance(DistanceContext& context) const {
1744 return _distance(context, delta<LessThanOrEqualCondition>);1744 return _distance(context, delta<LessThanOrEqualCondition>);
1745 }1745 }
1746 1746
1747 uint32_t LessThanCondition::distance(DistanceContext& context) const {1747 uint32_t LessThanCondition::distance(DistanceContext& context) const {
1748 return _distance(context, delta<LessThanCondition>);1748 return _distance(context, delta<LessThanCondition>);
1749 }1749 }
1750 1750
1751 uint32_t NotEqualCondition::distance(DistanceContext& context) const {1751 uint32_t NotEqualCondition::distance(DistanceContext& context) const {
1752 return _distance(context, delta<NotEqualCondition>);1752 return _distance(context, delta<NotEqualCondition>);
1753 }1753 }
1754 1754
1755 uint32_t EqualCondition::distance(DistanceContext& context) const {1755 uint32_t EqualCondition::distance(DistanceContext& context) const {
1756 return _distance(context, delta<EqualCondition>);1756 return _distance(context, delta<EqualCondition>);
1757 }1757 }
17581758
1759 /******************** BIN output ********************/1759 /******************** BIN output ********************/
1760 1760
1761 void LiteralExpr::toBinary(std::ostream& out) const {1761 void LiteralExpr::toBinary(std::ostream& out) const {
1762 out.write("l", sizeof(char));1762 out.write("l", sizeof(char));
1763 out.write(reinterpret_cast<const char*>(&_value), sizeof(int));1763 out.write(reinterpret_cast<const char*>(&_value), sizeof(int));
1764 }1764 }
1765 1765
1766 void UnfoldedIdentifierExpr::toBinary(std::ostream& out) const {1766 void UnfoldedIdentifierExpr::toBinary(std::ostream& out) const {
1767 out.write("i", sizeof(char));1767 out.write("i", sizeof(char));
1768 out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int)); 1768 out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int));
1769 }1769 }
1770 1770
1771 void MinusExpr::toBinary(std::ostream& out) const1771 void MinusExpr::toBinary(std::ostream& out) const
1772 {1772 {
1773 auto e1 = std::make_shared<PQL::LiteralExpr>(0);1773 auto e1 = std::make_shared<PQL::LiteralExpr>(0);
@@ -1776,7 +1776,7 @@
1776 exprs.push_back(_expr);1776 exprs.push_back(_expr);
1777 PQL::SubtractExpr(std::move(exprs)).toBinary(out);1777 PQL::SubtractExpr(std::move(exprs)).toBinary(out);
1778 }1778 }
1779 1779
1780 void SubtractExpr::toBinary(std::ostream& out) const {1780 void SubtractExpr::toBinary(std::ostream& out) const {
1781 out.write("-", sizeof(char));1781 out.write("-", sizeof(char));
1782 uint32_t size = _exprs.size();1782 uint32_t size = _exprs.size();
@@ -1799,7 +1799,7 @@
1799 for(auto& e : _exprs)1799 for(auto& e : _exprs)
1800 e->toBinary(out);1800 e->toBinary(out);
1801 }1801 }
1802 1802
1803 void SimpleQuantifierCondition::toBinary(std::ostream& out) const1803 void SimpleQuantifierCondition::toBinary(std::ostream& out) const
1804 {1804 {
1805 auto path = getPath();1805 auto path = getPath();
@@ -1818,7 +1818,7 @@
1818 _cond1->toBinary(out);1818 _cond1->toBinary(out);
1819 _cond2->toBinary(out);1819 _cond2->toBinary(out);
1820 }1820 }
1821 1821
1822 void LogicalCondition::toBinary(std::ostream& out) const1822 void LogicalCondition::toBinary(std::ostream& out) const
1823 {1823 {
1824 auto path = getPath();1824 auto path = getPath();
@@ -1829,7 +1829,7 @@
1829 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));1829 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
1830 for(auto& c : _conds) c->toBinary(out);1830 for(auto& c : _conds) c->toBinary(out);
1831 }1831 }
1832 1832
1833 void CompareConjunction::toBinary(std::ostream& out) const1833 void CompareConjunction::toBinary(std::ostream& out) const
1834 {1834 {
1835 auto path = getPath();1835 auto path = getPath();
@@ -1841,12 +1841,12 @@
1841 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));1841 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
1842 for(auto& c : _constraints)1842 for(auto& c : _constraints)
1843 {1843 {
1844 out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t)); 1844 out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));
1845 out.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));1845 out.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));
1846 out.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));1846 out.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));
1847 }1847 }
1848 }1848 }
1849 1849
1850 void CompareCondition::toBinary(std::ostream& out) const1850 void CompareCondition::toBinary(std::ostream& out) const
1851 {1851 {
1852 auto path = getPath();1852 auto path = getPath();
@@ -1859,7 +1859,7 @@
1859 _expr1->toBinary(out);1859 _expr1->toBinary(out);
1860 _expr2->toBinary(out);1860 _expr2->toBinary(out);
1861 }1861 }
1862 1862
1863 void DeadlockCondition::toBinary(std::ostream& out) const1863 void DeadlockCondition::toBinary(std::ostream& out) const
1864 {1864 {
1865 auto path = getPath();1865 auto path = getPath();
@@ -1867,7 +1867,7 @@
1867 out.write(reinterpret_cast<const char*>(&path), sizeof(Path));1867 out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1868 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));1868 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1869 }1869 }
1870 1870
1871 void BooleanCondition::toBinary(std::ostream& out) const1871 void BooleanCondition::toBinary(std::ostream& out) const
1872 {1872 {
1873 auto path = getPath();1873 auto path = getPath();
@@ -1876,24 +1876,24 @@
1876 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));1876 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1877 out.write(reinterpret_cast<const char*>(&value), sizeof(bool));1877 out.write(reinterpret_cast<const char*>(&value), sizeof(bool));
1878 }1878 }
1879 1879
1880 void UnfoldedUpperBoundsCondition::toBinary(std::ostream& out) const1880 void UnfoldedUpperBoundsCondition::toBinary(std::ostream& out) const
1881 {1881 {
1882 auto path = getPath();1882 auto path = getPath();
1883 auto quant = Quantifier::UPPERBOUNDS;1883 auto quant = Quantifier::UPPERBOUNDS;
1884 out.write(reinterpret_cast<const char*>(&path), sizeof(Path));1884 out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1885 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier)); 1885 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1886 uint32_t size = _places.size();1886 uint32_t size = _places.size();
1887 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t)); 1887 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
1888 out.write(reinterpret_cast<const char*>(&_max), sizeof(double)); 1888 out.write(reinterpret_cast<const char*>(&_max), sizeof(double));
1889 out.write(reinterpret_cast<const char*>(&_offset), sizeof(double)); 1889 out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));
1890 for(auto& b : _places)1890 for(auto& b : _places)
1891 {1891 {
1892 out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t)); 1892 out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));
1893 out.write(reinterpret_cast<const char*>(&b._max), sizeof(double));1893 out.write(reinterpret_cast<const char*>(&b._max), sizeof(double));
1894 }1894 }
1895 }1895 }
1896 1896
1897 void NotCondition::toBinary(std::ostream& out) const1897 void NotCondition::toBinary(std::ostream& out) const
1898 {1898 {
1899 auto path = getPath();1899 auto path = getPath();
@@ -1902,9 +1902,9 @@
1902 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));1902 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1903 _cond->toBinary(out);1903 _cond->toBinary(out);
1904 }1904 }
1905 1905
1906 /******************** CTL Output ********************/ 1906 /******************** CTL Output ********************/
1907 1907
1908 void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {1908 void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
1909 generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";1909 generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
1910 }1910 }
@@ -1929,14 +1929,14 @@
1929 ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());1929 ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
1930 coloredContext->reportError(error);1930 coloredContext->reportError(error);
1931 return;1931 return;
1932 } 1932 }
1933 if(names.size() < 1){1933 if(names.size() < 1){
1934 //If the transition points to empty vector we know that it has 1934 //If the transition points to empty vector we know that it has
1935 //no legal bindings and can never fire1935 //no legal bindings and can never fire
1936 out << "<false/>";1936 out << "<false/>";
1937 return;1937 return;
1938 }1938 }
1939 1939
1940 out << "<is-fireable>";1940 out << "<is-fireable>";
1941 for (auto& unfoldedName : names) {1941 for (auto& unfoldedName : names) {
1942 out << "<transition>" + unfoldedName << "</transition>";1942 out << "<transition>" + unfoldedName << "</transition>";
@@ -1944,14 +1944,14 @@
1944 out << "</is-fireable>";1944 out << "</is-fireable>";
1945 }1945 }
1946 }1946 }
1947 1947
1948 void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {1948 void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
1949 if (tokencount) {1949 if (tokencount) {
1950 generateTabs(out,tabs) << "<place>" << _name << "</place>\n";1950 generateTabs(out,tabs) << "<place>" << _name << "</place>\n";
1951 }1951 }
1952 else1952 else
1953 {1953 {
1954 generateTabs(out,tabs) << "<tokens-count>\n"; 1954 generateTabs(out,tabs) << "<tokens-count>\n";
1955 generateTabs(out,tabs+1) << "<place>" << _name << "</place>\n";1955 generateTabs(out,tabs+1) << "<place>" << _name << "</place>\n";
1956 generateTabs(out,tabs) << "</tokens-count>\n";1956 generateTabs(out,tabs) << "</tokens-count>\n";
1957 }1957 }
@@ -1963,7 +1963,7 @@
1963 }1963 }
1964 else1964 else
1965 {1965 {
1966 out << "<tokens-count>\n"; 1966 out << "<tokens-count>\n";
1967 out << "<place>" << _name << "</place>\n";1967 out << "<place>" << _name << "</place>\n";
1968 out << "</tokens-count>\n";1968 out << "</tokens-count>\n";
1969 }1969 }
@@ -1977,9 +1977,9 @@
1977 ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());1977 ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
1978 coloredContext->reportError(error);1978 coloredContext->reportError(error);
1979 return;1979 return;
1980 } 1980 }
1981 1981
1982 1982
1983 out << "<tokens-count>\n";1983 out << "<tokens-count>\n";
1984 for (auto& unfoldedName : names) {1984 for (auto& unfoldedName : names) {
1985 out << "<place>" << unfoldedName.second << "</place>\n";1985 out << "<place>" << unfoldedName.second << "</place>\n";
@@ -1991,19 +1991,19 @@
1991 }1991 }
1992 else1992 else
1993 {1993 {
1994 out << "<tokens-count>\n"; 1994 out << "<tokens-count>\n";
1995 out << "<place>" << _name << "</place>\n";1995 out << "<place>" << _name << "</place>\n";
1996 out << "</tokens-count>\n";1996 out << "</tokens-count>\n";
1997 }1997 }
1998 }1998 }
1999 }1999 }
2000 2000
2001 void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {2001 void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
2002 if (tokencount) {2002 if (tokencount) {
2003 for(auto& e : _exprs) e->toXML(ss,tabs, tokencount);2003 for(auto& e : _exprs) e->toXML(ss,tabs, tokencount);
2004 return;2004 return;
2005 }2005 }
2006 2006
2007 if(tk) {2007 if(tk) {
2008 generateTabs(ss,tabs) << "<tokens-count>\n";2008 generateTabs(ss,tabs) << "<tokens-count>\n";
2009 for(auto& e : _ids) generateTabs(ss,tabs+1) << "<place>" << e.second << "</place>\n";2009 for(auto& e : _ids) generateTabs(ss,tabs+1) << "<place>" << e.second << "</place>\n";
@@ -2015,9 +2015,9 @@
2015 generateTabs(ss,tabs+1) << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";2015 generateTabs(ss,tabs+1) << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";
2016 for(auto& i : _ids)2016 for(auto& i : _ids)
2017 {2017 {
2018 generateTabs(ss,tabs+1) << "<tokens-count>\n"; 2018 generateTabs(ss,tabs+1) << "<tokens-count>\n";
2019 generateTabs(ss,tabs+2) << "<place>" << i.second << "</place>\n";2019 generateTabs(ss,tabs+2) << "<place>" << i.second << "</place>\n";
2020 generateTabs(ss,tabs+1) << "</tokens-count>\n"; 2020 generateTabs(ss,tabs+1) << "</tokens-count>\n";
2021 }2021 }
2022 for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);2022 for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);
2023 generateTabs(ss,tabs) << "</integer-sum>\n";2023 generateTabs(ss,tabs) << "</integer-sum>\n";
@@ -2028,7 +2028,7 @@
2028 for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);2028 for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);
2029 return;2029 return;
2030 }2030 }
2031 2031
2032 if(tk) {2032 if(tk) {
2033 out << "<tokens-count>\n";2033 out << "<tokens-count>\n";
2034 for(auto& e : _ids) out << "<place>" << e.second << "</place>\n";2034 for(auto& e : _ids) out << "<place>" << e.second << "</place>\n";
@@ -2040,14 +2040,14 @@
2040 out << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";2040 out << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";
2041 for(auto& i : _ids)2041 for(auto& i : _ids)
2042 {2042 {
2043 out << "<tokens-count>\n"; 2043 out << "<tokens-count>\n";
2044 out << "<place>" << i.second << "</place>\n";2044 out << "<place>" << i.second << "</place>\n";
2045 out << "</tokens-count>\n"; 2045 out << "</tokens-count>\n";
2046 }2046 }
2047 for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);2047 for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);
2048 out << "</integer-sum>\n";2048 out << "</integer-sum>\n";
2049 }2049 }
2050 2050
2051 void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {2051 void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
2052 generateTabs(ss,tabs) << "<integer-difference>\n";2052 generateTabs(ss,tabs) << "<integer-difference>\n";
2053 for(auto& e : _exprs) e->toXML(ss,tabs+1);2053 for(auto& e : _exprs) e->toXML(ss,tabs+1);
@@ -2059,7 +2059,7 @@
2059 for(auto& e : _exprs) e->toCompactXML(out,tabs, context);2059 for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
2060 out << "</integer-difference>\n";2060 out << "</integer-difference>\n";
2061 }2061 }
2062 2062
2063 void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {2063 void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
2064 generateTabs(ss,tabs) << "<integer-product>\n";2064 generateTabs(ss,tabs) << "<integer-product>\n";
2065 for(auto& e : _exprs) e->toXML(ss,tabs+1);2065 for(auto& e : _exprs) e->toXML(ss,tabs+1);
@@ -2071,13 +2071,13 @@
2071 for(auto& e : _exprs) e->toCompactXML(out,tabs, context);2071 for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
2072 out << "</integer-product>\n";2072 out << "</integer-product>\n";
2073 }2073 }
2074 2074
2075 void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {2075 void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
2076 2076
2077 generateTabs(out,tabs) << "<integer-product>\n";2077 generateTabs(out,tabs) << "<integer-product>\n";
2078 _expr->toXML(out,tabs+1);2078 _expr->toXML(out,tabs+1);
2079 generateTabs(out,tabs+1) << "<integer-difference>\n" ; generateTabs(out,tabs+2) <<2079 generateTabs(out,tabs+1) << "<integer-difference>\n" ; generateTabs(out,tabs+2) <<
2080 "<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) << 2080 "<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) <<
2081 "<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<2081 "<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<
2082 "</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";2082 "</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";
2083 }2083 }
@@ -2086,11 +2086,11 @@
2086 out << "<integer-product>\n";2086 out << "<integer-product>\n";
2087 _expr->toCompactXML(out,tabs, context);2087 _expr->toCompactXML(out,tabs, context);
2088 out << "<integer-difference>\n" ; out <<2088 out << "<integer-difference>\n" ; out <<
2089 "<integer-constant>0</integer-constant>\n" ; out << 2089 "<integer-constant>0</integer-constant>\n" ; out <<
2090 "<integer-constant>1</integer-constant>\n" ; out <<2090 "<integer-constant>1</integer-constant>\n" ; out <<
2091 "</integer-difference>\n" ; out << "</integer-product>\n";2091 "</integer-difference>\n" ; out << "</integer-product>\n";
2092 }2092 }
2093 2093
2094 void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {2094 void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {
2095 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";2095 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";
2096 _cond->toXML(out,tabs+2);2096 _cond->toXML(out,tabs+2);
@@ -2103,66 +2103,66 @@
2103 out << "</next>\n" ; out << "</exists-path>\n";2103 out << "</next>\n" ; out << "</exists-path>\n";
2104 }2104 }
21052105
2106 void AXCondition::toXML(std::ostream& out,uint32_t tabs) const { 2106 void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {
2107 generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";2107 generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";
2108 _cond->toXML(out,tabs+2); 2108 _cond->toXML(out,tabs+2);
2109 generateTabs(out,tabs+1) << "</next>\n"; generateTabs(out,tabs) << "</all-paths>\n";2109 generateTabs(out,tabs+1) << "</next>\n"; generateTabs(out,tabs) << "</all-paths>\n";
2110 }2110 }
21112111
2112 void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2112 void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2113 out << "<all-paths>\n" ;out << "<next>\n";2113 out << "<all-paths>\n" ;out << "<next>\n";
2114 _cond->toCompactXML(out,tabs+2, context);2114 _cond->toCompactXML(out,tabs+2, context);
2115 out << "</next>\n" ; out << "</all-paths>\n";2115 out << "</next>\n" ; out << "</all-paths>\n";
2116 }2116 }
2117 2117
2118 void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {2118 void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {
2119 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";2119 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
2120 _cond->toXML(out,tabs+2);2120 _cond->toXML(out,tabs+2);
2121 generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";2121 generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
2122 }2122 }
21232123
2124 void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2124 void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2125 out << "<exists-path>\n" ;out << "<finally>\n";2125 out << "<exists-path>\n" ;out << "<finally>\n";
2126 _cond->toCompactXML(out,tabs+2, context);2126 _cond->toCompactXML(out,tabs+2, context);
2127 out << "</finally>\n" ; out << "</exists-path>\n";2127 out << "</finally>\n" ; out << "</exists-path>\n";
2128 }2128 }
2129 2129
2130 void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {2130 void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {
2131 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";2131 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
2132 _cond->toXML(out,tabs+2);2132 _cond->toXML(out,tabs+2);
2133 generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";2133 generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
2134 }2134 }
21352135
2136 void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2136 void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2137 out << "<all-paths>\n" ;out << "<finally>\n";2137 out << "<all-paths>\n" ;out << "<finally>\n";
2138 _cond->toCompactXML(out,tabs+2, context);2138 _cond->toCompactXML(out,tabs+2, context);
2139 out << "</finally>\n" ; out << "</all-paths>\n";2139 out << "</finally>\n" ; out << "</all-paths>\n";
2140 }2140 }
2141 2141
2142 void EGCondition::toXML(std::ostream& out,uint32_t tabs) const { 2142 void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {
2143 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";2143 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
2144 _cond->toXML(out,tabs+2); 2144 _cond->toXML(out,tabs+2);
2145 generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";2145 generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
2146 }2146 }
21472147
2148 void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2148 void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2149 out << "<exists-path>\n" ;out << "<globally>\n";2149 out << "<exists-path>\n" ;out << "<globally>\n";
2150 _cond->toCompactXML(out,tabs+2, context);2150 _cond->toCompactXML(out,tabs+2, context);
2151 out << "</globally>\n" ; out << "</exists-path>\n";2151 out << "</globally>\n" ; out << "</exists-path>\n";
2152 }2152 }
2153 2153
2154 void AGCondition::toXML(std::ostream& out,uint32_t tabs) const { 2154 void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {
2155 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";2155 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
2156 _cond->toXML(out,tabs+2);2156 _cond->toXML(out,tabs+2);
2157 generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";2157 generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
2158 }2158 }
21592159
2160 void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2160 void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2161 out << "<all-paths>\n" ;out << "<globally>\n";2161 out << "<all-paths>\n" ;out << "<globally>\n";
2162 _cond->toCompactXML(out,tabs+2, context);2162 _cond->toCompactXML(out,tabs+2, context);
2163 out << "</globally>\n" ; out << "</all-paths>\n";2163 out << "</globally>\n" ; out << "</all-paths>\n";
2164 }2164 }
2165 2165
2166 void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {2166 void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {
2167 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";2167 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
2168 _cond1->toXML(out,tabs+3);2168 _cond1->toXML(out,tabs+3);
@@ -2171,14 +2171,14 @@
2171 generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";2171 generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
2172 }2172 }
21732173
2174 void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2174 void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2175 out << "<exists-path>\n" ; out << "<until>\n" ; out << "<before>\n";2175 out << "<exists-path>\n" ; out << "<until>\n" ; out << "<before>\n";
2176 _cond1->toCompactXML(out,tabs+2, context);2176 _cond1->toCompactXML(out,tabs+2, context);
2177 out << "</before>\n" ; out << "<reach>\n";2177 out << "</before>\n" ; out << "<reach>\n";
2178 _cond2->toCompactXML(out,tabs+2, context);2178 _cond2->toCompactXML(out,tabs+2, context);
2179 out << "</reach>\n" ; out << "</until>\n" ; out << "</exists-path>\n";2179 out << "</reach>\n" ; out << "</until>\n" ; out << "</exists-path>\n";
2180 }2180 }
2181 2181
2182 void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {2182 void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {
2183 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";2183 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
2184 _cond1->toXML(out,tabs+3);2184 _cond1->toXML(out,tabs+3);
@@ -2187,7 +2187,7 @@
2187 generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";2187 generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
2188 }2188 }
21892189
2190 void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2190 void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2191 out << "<all-paths>\n" ; out << "<until>\n" ; out << "<before>\n";2191 out << "<all-paths>\n" ; out << "<until>\n" ; out << "<before>\n";
2192 _cond1->toCompactXML(out,tabs+2, context);2192 _cond1->toCompactXML(out,tabs+2, context);
2193 out << "</before>\n" ; out << "<reach>\n";2193 out << "</before>\n" ; out << "<reach>\n";
@@ -2201,7 +2201,7 @@
2201 generateTabs(out, tabs) << "</all-paths>\n";2201 generateTabs(out, tabs) << "</all-paths>\n";
2202 }2202 }
22032203
2204 void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2204 void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2205 out << "<all-paths>\n" ;2205 out << "<all-paths>\n" ;
2206 _cond->toCompactXML(out,tabs+2, context);2206 _cond->toCompactXML(out,tabs+2, context);
2207 out << "</all-paths>\n";2207 out << "</all-paths>\n";
@@ -2213,7 +2213,7 @@
2213 generateTabs(out, tabs) << "</exists-path>\n";2213 generateTabs(out, tabs) << "</exists-path>\n";
2214 }2214 }
22152215
2216 void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2216 void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2217 out << "<exists-path>\n" ;2217 out << "<exists-path>\n" ;
2218 _cond->toCompactXML(out,tabs+2, context);2218 _cond->toCompactXML(out,tabs+2, context);
2219 out << "</exists-path>\n";2219 out << "</exists-path>\n";
@@ -2225,7 +2225,7 @@
2225 generateTabs(out, tabs) << "</finally>\n";2225 generateTabs(out, tabs) << "</finally>\n";
2226 }2226 }
22272227
2228 void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2228 void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2229 out << "<finally>\n" ;2229 out << "<finally>\n" ;
2230 _cond->toCompactXML(out,tabs+2, context);2230 _cond->toCompactXML(out,tabs+2, context);
2231 out << "</finally>\n";2231 out << "</finally>\n";
@@ -2237,7 +2237,7 @@
2237 generateTabs(out, tabs) << "</globally>\n";2237 generateTabs(out, tabs) << "</globally>\n";
2238 }2238 }
22392239
2240 void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2240 void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2241 out << "<globally>\n" ;2241 out << "<globally>\n" ;
2242 _cond->toCompactXML(out,tabs+2, context);2242 _cond->toCompactXML(out,tabs+2, context);
2243 out << "</globally>\n";2243 out << "</globally>\n";
@@ -2249,7 +2249,7 @@
2249 generateTabs(out, tabs) << "</next>\n";2249 generateTabs(out, tabs) << "</next>\n";
2250 }2250 }
22512251
2252 void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2252 void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2253 out << "<next>\n" ;2253 out << "<next>\n" ;
2254 _cond->toCompactXML(out,tabs+2, context);2254 _cond->toCompactXML(out,tabs+2, context);
2255 out << "</next>\n";2255 out << "</next>\n";
@@ -2263,7 +2263,7 @@
2263 generateTabs(out,tabs+1) << "</reach>\n" ; generateTabs(out,tabs) << "</until>\n" ;2263 generateTabs(out,tabs+1) << "</reach>\n" ; generateTabs(out,tabs) << "</until>\n" ;
2264 }2264 }
22652265
2266 void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2266 void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2267 out << "<until>\n" ; out << "<before>\n";2267 out << "<until>\n" ; out << "<before>\n";
2268 _cond1->toCompactXML(out,tabs+2, context);2268 _cond1->toCompactXML(out,tabs+2, context);
2269 out << "</before>\n" ; out << "<reach>\n";2269 out << "</before>\n" ; out << "<reach>\n";
@@ -2298,12 +2298,12 @@
2298 }2298 }
2299 for(size_t i = _conds.size() - 1; i > 1; --i)2299 for(size_t i = _conds.size() - 1; i > 1; --i)
2300 {2300 {
2301 generateTabs(out,tabs + i) << "</conjunction>\n"; 2301 generateTabs(out,tabs + i) << "</conjunction>\n";
2302 }2302 }
2303 generateTabs(out,tabs) << "</conjunction>\n"; 2303 generateTabs(out,tabs) << "</conjunction>\n";
2304 }2304 }
23052305
2306 void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2306 void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2307 if(_conds.size() == 0)2307 if(_conds.size() == 0)
2308 {2308 {
2309 BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);2309 BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
@@ -2330,11 +2330,11 @@
2330 }2330 }
2331 for(size_t i = _conds.size() - 1; i > 1; --i)2331 for(size_t i = _conds.size() - 1; i > 1; --i)
2332 {2332 {
2333 out << "</conjunction>\n"; 2333 out << "</conjunction>\n";
2334 }2334 }
2335 out << "</conjunction>\n"; 2335 out << "</conjunction>\n";
2336 }2336 }
2337 2337
2338 void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {2338 void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {
2339 if(_conds.size() == 0)2339 if(_conds.size() == 0)
2340 {2340 {
@@ -2362,12 +2362,12 @@
2362 }2362 }
2363 for(size_t i = _conds.size() - 1; i > 1; --i)2363 for(size_t i = _conds.size() - 1; i > 1; --i)
2364 {2364 {
2365 generateTabs(out,tabs + i) << "</disjunction>\n"; 2365 generateTabs(out,tabs + i) << "</disjunction>\n";
2366 }2366 }
2367 generateTabs(out,tabs) << "</disjunction>\n"; 2367 generateTabs(out,tabs) << "</disjunction>\n";
2368 }2368 }
23692369
2370 void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2370 void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2371 if(_conds.size() == 0)2371 if(_conds.size() == 0)
2372 {2372 {
2373 BooleanCondition::FALSE_CONSTANT->toCompactXML(out,tabs, context);2373 BooleanCondition::FALSE_CONSTANT->toCompactXML(out,tabs, context);
@@ -2394,9 +2394,9 @@
2394 }2394 }
2395 for(size_t i = _conds.size() - 1; i > 1; --i)2395 for(size_t i = _conds.size() - 1; i > 1; --i)
2396 {2396 {
2397 out << "</disjunction>\n"; 2397 out << "</disjunction>\n";
2398 }2398 }
2399 out << "</disjunction>\n"; 2399 out << "</disjunction>\n";
2400 }2400 }
24012401
2402 void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const2402 void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const
@@ -2405,10 +2405,10 @@
2405 if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toXML(out, tabs);2405 if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toXML(out, tabs);
2406 else2406 else
2407 {2407 {
2408 bool single = _constraints.size() == 1 && 2408 bool single = _constraints.size() == 1 &&
2409 (_constraints[0]._lower == 0 ||2409 (_constraints[0]._lower == 0 ||
2410 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());2410 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
2411 if(!single) 2411 if(!single)
2412 generateTabs(out,tabs) << "<conjunction>\n";2412 generateTabs(out,tabs) << "<conjunction>\n";
2413 for(auto& c : _constraints)2413 for(auto& c : _constraints)
2414 {2414 {
@@ -2419,7 +2419,7 @@
2419 generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";2419 generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";
2420 generateTabs(out,tabs+2) << "</tokens-count>\n";2420 generateTabs(out,tabs+2) << "</tokens-count>\n";
2421 generateTabs(out,tabs+2) << "<integer-constant>" << c._lower << "</integer-constant>\n";2421 generateTabs(out,tabs+2) << "<integer-constant>" << c._lower << "</integer-constant>\n";
2422 generateTabs(out,tabs+1) << "</integer-ge>\n"; 2422 generateTabs(out,tabs+1) << "</integer-ge>\n";
2423 }2423 }
2424 if(c._upper != std::numeric_limits<uint32_t>::max())2424 if(c._upper != std::numeric_limits<uint32_t>::max())
2425 {2425 {
@@ -2428,7 +2428,7 @@
2428 generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";2428 generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";
2429 generateTabs(out,tabs+2) << "</tokens-count>\n";2429 generateTabs(out,tabs+2) << "</tokens-count>\n";
2430 generateTabs(out,tabs+2) << "<integer-constant>" << c._upper << "</integer-constant>\n";2430 generateTabs(out,tabs+2) << "<integer-constant>" << c._upper << "</integer-constant>\n";
2431 generateTabs(out,tabs+1) << "</integer-le>\n"; 2431 generateTabs(out,tabs+1) << "</integer-le>\n";
2432 }2432 }
2433 }2433 }
2434 if(!single)2434 if(!single)
@@ -2437,15 +2437,15 @@
2437 if(_negated) generateTabs(out,--tabs) << "</negation>";2437 if(_negated) generateTabs(out,--tabs) << "</negation>";
2438 }2438 }
24392439
2440 void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2440 void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2441 if(_negated) out << "<negation>";2441 if(_negated) out << "<negation>";
2442 if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);2442 if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
2443 else2443 else
2444 {2444 {
2445 bool single = _constraints.size() == 1 && 2445 bool single = _constraints.size() == 1 &&
2446 (_constraints[0]._lower == 0 ||2446 (_constraints[0]._lower == 0 ||
2447 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());2447 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
2448 if(!single) 2448 if(!single)
2449 out << "<conjunction>\n";2449 out << "<conjunction>\n";
2450 for(auto& c : _constraints)2450 for(auto& c : _constraints)
2451 {2451 {
@@ -2456,7 +2456,7 @@
2456 out << "<place>" << c._name << "</place>\n";2456 out << "<place>" << c._name << "</place>\n";
2457 out << "</tokens-count>\n";2457 out << "</tokens-count>\n";
2458 out << "<integer-constant>" << c._lower << "</integer-constant>\n";2458 out << "<integer-constant>" << c._lower << "</integer-constant>\n";
2459 out << "</integer-ge>\n"; 2459 out << "</integer-ge>\n";
2460 }2460 }
2461 if(c._upper != std::numeric_limits<uint32_t>::max())2461 if(c._upper != std::numeric_limits<uint32_t>::max())
2462 {2462 {
@@ -2465,104 +2465,104 @@
2465 out << "<place>" << c._name << "</place>\n";2465 out << "<place>" << c._name << "</place>\n";
2466 out << "</tokens-count>\n";2466 out << "</tokens-count>\n";
2467 out << "<integer-constant>" << c._upper << "</integer-constant>\n";2467 out << "<integer-constant>" << c._upper << "</integer-constant>\n";
2468 out << "</integer-le>\n"; 2468 out << "</integer-le>\n";
2469 }2469 }
2470 }2470 }
2471 if(!single)2471 if(!single)
2472 out << "</conjunction>\n";2472 out << "</conjunction>\n";
2473 }2473 }
2474 if(_negated) out << "</negation>"; 2474 if(_negated) out << "</negation>";
2475 }2475 }
24762476
2477 void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {2477 void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
2478 generateTabs(out,tabs) << "<integer-eq>\n";2478 generateTabs(out,tabs) << "<integer-eq>\n";
2479 _expr1->toXML(out,tabs+1);2479 _expr1->toXML(out,tabs+1);
2480 _expr2->toXML(out,tabs+1);2480 _expr2->toXML(out,tabs+1);
2481 generateTabs(out,tabs) << "</integer-eq>\n"; 2481 generateTabs(out,tabs) << "</integer-eq>\n";
2482 }2482 }
24832483
2484 void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2484 void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2485 out << "<integer-eq>\n";2485 out << "<integer-eq>\n";
2486 _expr1->toCompactXML(out,tabs, context);2486 _expr1->toCompactXML(out,tabs, context);
2487 _expr2->toCompactXML(out,tabs, context);2487 _expr2->toCompactXML(out,tabs, context);
2488 out << "</integer-eq>\n";2488 out << "</integer-eq>\n";
2489 }2489 }
2490 2490
2491 void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {2491 void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
2492 generateTabs(out,tabs) << "<integer-ne>\n";2492 generateTabs(out,tabs) << "<integer-ne>\n";
2493 _expr1->toXML(out,tabs+1);2493 _expr1->toXML(out,tabs+1);
2494 _expr2->toXML(out,tabs+1);2494 _expr2->toXML(out,tabs+1);
2495 generateTabs(out,tabs) << "</integer-ne>\n"; 2495 generateTabs(out,tabs) << "</integer-ne>\n";
2496 }2496 }
24972497
2498 void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2498 void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2499 out << "<integer-ne>\n";2499 out << "<integer-ne>\n";
2500 _expr1->toCompactXML(out,tabs, context);2500 _expr1->toCompactXML(out,tabs, context);
2501 _expr2->toCompactXML(out,tabs, context);2501 _expr2->toCompactXML(out,tabs, context);
2502 out << "</integer-ne>\n";2502 out << "</integer-ne>\n";
2503 }2503 }
2504 2504
2505 void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {2505 void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {
2506 generateTabs(out,tabs) << "<integer-lt>\n";2506 generateTabs(out,tabs) << "<integer-lt>\n";
2507 _expr1->toXML(out,tabs+1);2507 _expr1->toXML(out,tabs+1);
2508 _expr2->toXML(out,tabs+1);2508 _expr2->toXML(out,tabs+1);
2509 generateTabs(out,tabs) << "</integer-lt>\n"; 2509 generateTabs(out,tabs) << "</integer-lt>\n";
2510 }2510 }
25112511
2512 void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2512 void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2513 out << "<integer-lt>\n";2513 out << "<integer-lt>\n";
2514 _expr1->toCompactXML(out,tabs, context);2514 _expr1->toCompactXML(out,tabs, context);
2515 _expr2->toCompactXML(out,tabs, context);2515 _expr2->toCompactXML(out,tabs, context);
2516 out << "</integer-lt>\n";2516 out << "</integer-lt>\n";
2517 }2517 }
2518 2518
2519 void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {2519 void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
2520 generateTabs(out,tabs) << "<integer-le>\n";2520 generateTabs(out,tabs) << "<integer-le>\n";
2521 _expr1->toXML(out,tabs+1);2521 _expr1->toXML(out,tabs+1);
2522 _expr2->toXML(out,tabs+1);2522 _expr2->toXML(out,tabs+1);
2523 generateTabs(out,tabs) << "</integer-le>\n"; 2523 generateTabs(out,tabs) << "</integer-le>\n";
2524 }2524 }
25252525
2526 void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2526 void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2527 out << "<integer-le>\n";2527 out << "<integer-le>\n";
2528 _expr1->toCompactXML(out,tabs, context);2528 _expr1->toCompactXML(out,tabs, context);
2529 _expr2->toCompactXML(out,tabs, context);2529 _expr2->toCompactXML(out,tabs, context);
2530 out << "</integer-le>\n";2530 out << "</integer-le>\n";
2531 }2531 }
2532 2532
2533 void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {2533 void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {
2534 2534
2535 generateTabs(out,tabs) << "<negation>\n";2535 generateTabs(out,tabs) << "<negation>\n";
2536 _cond->toXML(out,tabs+1);2536 _cond->toXML(out,tabs+1);
2537 generateTabs(out,tabs) << "</negation>\n"; 2537 generateTabs(out,tabs) << "</negation>\n";
2538 }2538 }
25392539
2540 void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2540 void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2541 out << "<negation>\n";2541 out << "<negation>\n";
2542 _cond->toCompactXML(out,tabs, context);2542 _cond->toCompactXML(out,tabs, context);
2543 out << "</negation>\n";2543 out << "</negation>\n";
2544 }2544 }
2545 2545
2546 void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const { 2546 void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {
2547 generateTabs(out,tabs) << "<" << 2547 generateTabs(out,tabs) << "<" <<
2548 (value ? "true" : "false")2548 (value ? "true" : "false")
2549 << "/>\n"; 2549 << "/>\n";
2550 }2550 }
25512551
2552 void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2552 void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2553 out << "<" << 2553 out << "<" <<
2554 (value ? "true" : "false")2554 (value ? "true" : "false")
2555 << "/>\n"; 2555 << "/>\n";
2556 }2556 }
2557 2557
2558 void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {2558 void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {
2559 generateTabs(out,tabs) << "<deadlock/>\n"; 2559 generateTabs(out,tabs) << "<deadlock/>\n";
2560 }2560 }
25612561
2562 void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2562 void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2563 out << "<deadlock/>\n";2563 out << "<deadlock/>\n";
2564 }2564 }
2565 2565
2566 void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {2566 void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {
2567 generateTabs(out, tabs) << "<place-bound>\n";2567 generateTabs(out, tabs) << "<place-bound>\n";
2568 for(auto& p : _places)2568 for(auto& p : _places)
@@ -2570,33 +2570,33 @@
2570 generateTabs(out, tabs) << "</place-bound>\n";2570 generateTabs(out, tabs) << "</place-bound>\n";
2571 }2571 }
25722572
2573 void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 2573 void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
2574 out << "<place-bound>\n";2574 out << "<place-bound>\n";
2575 for(auto& p : _places)2575 for(auto& p : _places)
2576 out << "<place>" << p._name << "</place>\n";2576 out << "<place>" << p._name << "</place>\n";
2577 out << "</place-bound>\n"; 2577 out << "</place-bound>\n";
2578 }2578 }
2579 2579
2580 /******************** Query Simplification ********************/ 2580 /******************** Query Simplification ********************/
2581 2581
2582 Member LiteralExpr::constraint(SimplificationContext& context) const {2582 Member LiteralExpr::constraint(SimplificationContext& context) const {
2583 return Member(_value);2583 return Member(_value);
2584 }2584 }
2585 2585
2586 Member memberForPlace(size_t p, SimplificationContext& context) 2586 Member memberForPlace(size_t p, SimplificationContext& context)
2587 {2587 {
2588 std::vector<int> row(context.net()->numberOfTransitions(), 0);2588 std::vector<int> row(context.net()->numberOfTransitions(), 0);
2589 row.shrink_to_fit();2589 row.shrink_to_fit();
2590 for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) {2590 for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) {
2591 row[t] = context.net()->outArc(t, p) - context.net()->inArc(p, t);2591 row[t] = context.net()->outArc(t, p) - context.net()->inArc(p, t);
2592 }2592 }
2593 return Member(std::move(row), context.marking()[p]); 2593 return Member(std::move(row), context.marking()[p]);
2594 }2594 }
2595 2595
2596 Member UnfoldedIdentifierExpr::constraint(SimplificationContext& context) const {2596 Member UnfoldedIdentifierExpr::constraint(SimplificationContext& context) const {
2597 return memberForPlace(_offsetInMarking, context);2597 return memberForPlace(_offsetInMarking, context);
2598 }2598 }
2599 2599
2600 Member CommutativeExpr::commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const2600 Member CommutativeExpr::commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const
2601 {2601 {
2602 Member res;2602 Member res;
@@ -2606,7 +2606,7 @@
2606 first = false;2606 first = false;
2607 res = Member(_constant);2607 res = Member(_constant);
2608 }2608 }
2609 2609
2610 for(auto& i : _ids)2610 for(auto& i : _ids)
2611 {2611 {
2612 if(first) res = memberForPlace(i.first, context);2612 if(first) res = memberForPlace(i.first, context);
@@ -2620,28 +2620,28 @@
2620 else op(res, e->constraint(context));2620 else op(res, e->constraint(context));
2621 first = false;2621 first = false;
2622 }2622 }
2623 return res; 2623 return res;
2624 }2624 }
2625 2625
2626 Member PlusExpr::constraint(SimplificationContext& context) const {2626 Member PlusExpr::constraint(SimplificationContext& context) const {
2627 return commutativeCons(0, context, [](auto& a , auto b){ a += b;});2627 return commutativeCons(0, context, [](auto& a , auto b){ a += b;});
2628 }2628 }
2629 2629
2630 Member SubtractExpr::constraint(SimplificationContext& context) const {2630 Member SubtractExpr::constraint(SimplificationContext& context) const {
2631 Member res = _exprs[0]->constraint(context);2631 Member res = _exprs[0]->constraint(context);
2632 for(size_t i = 1; i < _exprs.size(); ++i) res -= _exprs[i]->constraint(context);2632 for(size_t i = 1; i < _exprs.size(); ++i) res -= _exprs[i]->constraint(context);
2633 return res;2633 return res;
2634 }2634 }
2635 2635
2636 Member MultiplyExpr::constraint(SimplificationContext& context) const {2636 Member MultiplyExpr::constraint(SimplificationContext& context) const {
2637 return commutativeCons(1, context, [](auto& a , auto b){ a *= b;});2637 return commutativeCons(1, context, [](auto& a , auto b){ a *= b;});
2638 }2638 }
2639 2639
2640 Member MinusExpr::constraint(SimplificationContext& context) const {2640 Member MinusExpr::constraint(SimplificationContext& context) const {
2641 Member neg(-1);2641 Member neg(-1);
2642 return _expr->constraint(context) *= neg;2642 return _expr->constraint(context) *= neg;
2643 }2643 }
2644 2644
2645 Retval simplifyEX(Retval& r, SimplificationContext& context) {2645 Retval simplifyEX(Retval& r, SimplificationContext& context) {
2646 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {2646 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {
2647 return Retval(std::make_shared<NotCondition>(2647 return Retval(std::make_shared<NotCondition>(
@@ -2652,7 +2652,7 @@
2652 return Retval(std::make_shared<EXCondition>(r.formula));2652 return Retval(std::make_shared<EXCondition>(r.formula));
2653 }2653 }
2654 }2654 }
2655 2655
2656 Retval simplifyAX(Retval& r, SimplificationContext& context) {2656 Retval simplifyAX(Retval& r, SimplificationContext& context) {
2657 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){2657 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
2658 return Retval(BooleanCondition::TRUE_CONSTANT);2658 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2672,7 +2672,7 @@
2672 return Retval(std::make_shared<EFCondition>(r.formula));2672 return Retval(std::make_shared<EFCondition>(r.formula));
2673 }2673 }
2674 }2674 }
2675 2675
2676 Retval simplifyAF(Retval& r, SimplificationContext& context){2676 Retval simplifyAF(Retval& r, SimplificationContext& context){
2677 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){2677 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
2678 return Retval(BooleanCondition::TRUE_CONSTANT);2678 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2682,7 +2682,7 @@
2682 return Retval(std::make_shared<AFCondition>(r.formula));2682 return Retval(std::make_shared<AFCondition>(r.formula));
2683 }2683 }
2684 }2684 }
2685 2685
2686 Retval simplifyEG(Retval& r, SimplificationContext& context){2686 Retval simplifyEG(Retval& r, SimplificationContext& context){
2687 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){2687 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
2688 return Retval(BooleanCondition::TRUE_CONSTANT);2688 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2692,7 +2692,7 @@
2692 return Retval(std::make_shared<EGCondition>(r.formula));2692 return Retval(std::make_shared<EGCondition>(r.formula));
2693 }2693 }
2694 }2694 }
2695 2695
2696 Retval simplifyAG(Retval& r, SimplificationContext& context){2696 Retval simplifyAG(Retval& r, SimplificationContext& context){
2697 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){2697 if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
2698 return Retval(BooleanCondition::TRUE_CONSTANT);2698 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2720,32 +2720,32 @@
2720 Retval r = _cond->simplify(context);2720 Retval r = _cond->simplify(context);
2721 return context.negated() ? simplifyAX(r, context) : simplifyEX(r, context);2721 return context.negated() ? simplifyAX(r, context) : simplifyEX(r, context);
2722 }2722 }
2723 2723
2724 Retval AXCondition::simplify(SimplificationContext& context) const {2724 Retval AXCondition::simplify(SimplificationContext& context) const {
2725 Retval r = _cond->simplify(context);2725 Retval r = _cond->simplify(context);
2726 return context.negated() ? simplifyEX(r, context) : simplifyAX(r, context);2726 return context.negated() ? simplifyEX(r, context) : simplifyAX(r, context);
2727 } 2727 }
2728 2728
2729 Retval EFCondition::simplify(SimplificationContext& context) const {2729 Retval EFCondition::simplify(SimplificationContext& context) const {
2730 Retval r = _cond->simplify(context);2730 Retval r = _cond->simplify(context);
2731 return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context); 2731 return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context);
2732 }2732 }
2733 2733
2734 Retval AFCondition::simplify(SimplificationContext& context) const {2734 Retval AFCondition::simplify(SimplificationContext& context) const {
2735 Retval r = _cond->simplify(context);2735 Retval r = _cond->simplify(context);
2736 return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context); 2736 return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context);
2737 }2737 }
2738 2738
2739 Retval EGCondition::simplify(SimplificationContext& context) const {2739 Retval EGCondition::simplify(SimplificationContext& context) const {
2740 Retval r = _cond->simplify(context);2740 Retval r = _cond->simplify(context);
2741 return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context); 2741 return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context);
2742 }2742 }
2743 2743
2744 Retval AGCondition::simplify(SimplificationContext& context) const {2744 Retval AGCondition::simplify(SimplificationContext& context) const {
2745 Retval r = _cond->simplify(context);2745 Retval r = _cond->simplify(context);
2746 return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context); 2746 return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context);
2747 }2747 }
2748 2748
2749 Retval EUCondition::simplify(SimplificationContext& context) const {2749 Retval EUCondition::simplify(SimplificationContext& context) const {
2750 // cannot push negation any further2750 // cannot push negation any further
2751 bool neg = context.negated();2751 bool neg = context.negated();
@@ -2754,20 +2754,20 @@
2754 if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))2754 if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))
2755 {2755 {
2756 context.setNegate(neg);2756 context.setNegate(neg);
2757 return neg ? 2757 return neg ?
2758 Retval(BooleanCondition::FALSE_CONSTANT) :2758 Retval(BooleanCondition::FALSE_CONSTANT) :
2759 Retval(BooleanCondition::TRUE_CONSTANT);2759 Retval(BooleanCondition::TRUE_CONSTANT);
2760 }2760 }
2761 else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))2761 else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))
2762 {2762 {
2763 context.setNegate(neg);2763 context.setNegate(neg);
2764 return neg ? 2764 return neg ?
2765 Retval(BooleanCondition::TRUE_CONSTANT) :2765 Retval(BooleanCondition::TRUE_CONSTANT) :
2766 Retval(BooleanCondition::FALSE_CONSTANT); 2766 Retval(BooleanCondition::FALSE_CONSTANT);
2767 }2767 }
2768 Retval r1 = _cond1->simplify(context);2768 Retval r1 = _cond1->simplify(context);
2769 context.setNegate(neg);2769 context.setNegate(neg);
2770 2770
2771 if(context.negated()){2771 if(context.negated()){
2772 if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){2772 if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
2773 return Retval(std::make_shared<NotCondition>(2773 return Retval(std::make_shared<NotCondition>(
@@ -2788,7 +2788,7 @@
2788 }2788 }
2789 }2789 }
2790 }2790 }
2791 2791
2792 Retval AUCondition::simplify(SimplificationContext& context) const {2792 Retval AUCondition::simplify(SimplificationContext& context) const {
2793 // cannot push negation any further2793 // cannot push negation any further
2794 bool neg = context.negated();2794 bool neg = context.negated();
@@ -2797,20 +2797,20 @@
2797 if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))2797 if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))
2798 {2798 {
2799 context.setNegate(neg);2799 context.setNegate(neg);
2800 return neg ? 2800 return neg ?
2801 Retval(BooleanCondition::FALSE_CONSTANT) :2801 Retval(BooleanCondition::FALSE_CONSTANT) :
2802 Retval(BooleanCondition::TRUE_CONSTANT);2802 Retval(BooleanCondition::TRUE_CONSTANT);
2803 }2803 }
2804 else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))2804 else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))
2805 {2805 {
2806 context.setNegate(neg);2806 context.setNegate(neg);
2807 return neg ? 2807 return neg ?
2808 Retval(BooleanCondition::TRUE_CONSTANT) :2808 Retval(BooleanCondition::TRUE_CONSTANT) :
2809 Retval(BooleanCondition::FALSE_CONSTANT);2809 Retval(BooleanCondition::FALSE_CONSTANT);
2810 }2810 }
2811 Retval r1 = _cond1->simplify(context);2811 Retval r1 = _cond1->simplify(context);
2812 context.setNegate(neg);2812 context.setNegate(neg);
2813 2813
2814 if(context.negated()){2814 if(context.negated()){
2815 if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){2815 if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
2816 return Retval(std::make_shared<NotCondition>(2816 return Retval(std::make_shared<NotCondition>(
@@ -2919,7 +2919,7 @@
2919 }2919 }
2920 return lps[0];2920 return lps[0];
2921 }2921 }
2922 2922
2923 Retval LogicalCondition::simplifyAnd(SimplificationContext& context) const {2923 Retval LogicalCondition::simplifyAnd(SimplificationContext& context) const {
29242924
2925 std::vector<Condition_ptr> conditions;2925 std::vector<Condition_ptr> conditions;
@@ -2936,12 +2936,12 @@
2936 {2936 {
2937 continue;2937 continue;
2938 }2938 }
2939 2939
2940 conditions.push_back(r.formula);2940 conditions.push_back(r.formula);
2941 lpsv.emplace_back(r.lps);2941 lpsv.emplace_back(r.lps);
2942 neglps.emplace_back(r.neglps);2942 neglps.emplace_back(r.neglps);
2943 }2943 }
2944 2944
2945 if(conditions.size() == 0)2945 if(conditions.size() == 0)
2946 {2946 {
2947 return Retval(BooleanCondition::TRUE_CONSTANT);2947 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2953,24 +2953,24 @@
2953 if(!context.timeout() && !lps->satisfiable(context))2953 if(!context.timeout() && !lps->satisfiable(context))
2954 {2954 {
2955 return Retval(BooleanCondition::FALSE_CONSTANT);2955 return Retval(BooleanCondition::FALSE_CONSTANT);
2956 } 2956 }
2957 }2957 }
2958 catch(std::bad_alloc& e)2958 catch(std::bad_alloc& e)
2959 {2959 {
2960 // we are out of memory, deal with it.2960 // we are out of memory, deal with it.
2961 std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;2961 std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
2962 }2962 }
2963 2963
2964 // Lets try to see if the r1 AND r2 can ever be false at the same time2964 // Lets try to see if the r1 AND r2 can ever be false at the same time
2965 // If not, then we know that r1 || r2 must be true.2965 // If not, then we know that r1 || r2 must be true.
2966 // we check this by checking if !r1 && !r2 is unsat2966 // we check this by checking if !r1 && !r2 is unsat
2967 2967
2968 return Retval(2968 return Retval(
2969 makeAnd(conditions), 2969 makeAnd(conditions),
2970 std::move(lps),2970 std::move(lps),
2971 std::make_shared<UnionCollection>(std::move(neglps)));2971 std::make_shared<UnionCollection>(std::move(neglps)));
2972 }2972 }
2973 2973
2974 Retval LogicalCondition::simplifyOr(SimplificationContext& context) const {2974 Retval LogicalCondition::simplifyOr(SimplificationContext& context) const {
29752975
2976 std::vector<Condition_ptr> conditions;2976 std::vector<Condition_ptr> conditions;
@@ -2993,7 +2993,7 @@
2993 lps.push_back(r.lps);2993 lps.push_back(r.lps);
2994 neglpsv.emplace_back(r.neglps);2994 neglpsv.emplace_back(r.neglps);
2995 }2995 }
2996 2996
2997 AbstractProgramCollection_ptr neglps = mergeLps(std::move(neglpsv));2997 AbstractProgramCollection_ptr neglps = mergeLps(std::move(neglpsv));
29982998
2999 if(conditions.size() == 0)2999 if(conditions.size() == 0)
@@ -3005,7 +3005,7 @@
3005 if(!context.timeout() && !neglps->satisfiable(context))3005 if(!context.timeout() && !neglps->satisfiable(context))
3006 {3006 {
3007 return Retval(BooleanCondition::TRUE_CONSTANT);3007 return Retval(BooleanCondition::TRUE_CONSTANT);
3008 } 3008 }
3009 }3009 }
3010 catch(std::bad_alloc& e)3010 catch(std::bad_alloc& e)
3011 {3011 {
@@ -3016,20 +3016,20 @@
3016 // Lets try to see if the r1 AND r2 can ever be false at the same time3016 // Lets try to see if the r1 AND r2 can ever be false at the same time
3017 // If not, then we know that r1 || r2 must be true.3017 // If not, then we know that r1 || r2 must be true.
3018 // we check this by checking if !r1 && !r2 is unsat3018 // we check this by checking if !r1 && !r2 is unsat
3019 3019
3020 return Retval(3020 return Retval(
3021 makeOr(conditions), 3021 makeOr(conditions),
3022 std::make_shared<UnionCollection>(std::move(lps)), 3022 std::make_shared<UnionCollection>(std::move(lps)),
3023 std::move(neglps)); 3023 std::move(neglps));
3024 }3024 }
3025 3025
3026 Retval AndCondition::simplify(SimplificationContext& context) const {3026 Retval AndCondition::simplify(SimplificationContext& context) const {
3027 if(context.timeout())3027 if(context.timeout())
3028 {3028 {
3029 if(context.negated()) 3029 if(context.negated())
3030 return Retval(std::make_shared<NotCondition>(3030 return Retval(std::make_shared<NotCondition>(
3031 makeAnd(_conds)));3031 makeAnd(_conds)));
3032 else 3032 else
3033 return Retval(3033 return Retval(
3034 makeAnd(_conds));3034 makeAnd(_conds));
3035 }3035 }
@@ -3038,16 +3038,16 @@
3038 return simplifyOr(context);3038 return simplifyOr(context);
3039 else3039 else
3040 return simplifyAnd(context);3040 return simplifyAnd(context);
3041 3041
3042 }3042 }
3043 3043
3044 Retval OrCondition::simplify(SimplificationContext& context) const { 3044 Retval OrCondition::simplify(SimplificationContext& context) const {
3045 if(context.timeout())3045 if(context.timeout())
3046 {3046 {
3047 if(context.negated()) 3047 if(context.negated())
3048 return Retval(std::make_shared<NotCondition>(3048 return Retval(std::make_shared<NotCondition>(
3049 makeOr(_conds)));3049 makeOr(_conds)));
3050 else 3050 else
3051 return Retval(makeOr(_conds));3051 return Retval(makeOr(_conds));
3052 }3052 }
3053 if(context.negated())3053 if(context.negated())
@@ -3055,7 +3055,7 @@
3055 else3055 else
3056 return simplifyOr(context);3056 return simplifyOr(context);
3057 }3057 }
3058 3058
3059 Retval CompareConjunction::simplify(SimplificationContext& context) const {3059 Retval CompareConjunction::simplify(SimplificationContext& context) const {
3060 if(context.timeout())3060 if(context.timeout())
3061 {3061 {
@@ -3064,7 +3064,7 @@
3064 std::vector<AbstractProgramCollection_ptr> neglps, lpsv;3064 std::vector<AbstractProgramCollection_ptr> neglps, lpsv;
3065 auto neg = context.negated() != _negated;3065 auto neg = context.negated() != _negated;
3066 std::vector<cons_t> nconstraints;3066 std::vector<cons_t> nconstraints;
3067 for(auto& c : _constraints) 3067 for(auto& c : _constraints)
3068 {3068 {
3069 nconstraints.push_back(c);3069 nconstraints.push_back(c);
3070 if(c._lower != 0 /*&& !context.timeout()*/ )3070 if(c._lower != 0 /*&& !context.timeout()*/ )
@@ -3088,7 +3088,7 @@
3088 neglps.push_back(nlp);3088 neglps.push_back(nlp);
3089 }3089 }
3090 }3090 }
3091 3091
3092 if(c._upper != std::numeric_limits<uint32_t>::max() /*&& !context.timeout()*/)3092 if(c._upper != std::numeric_limits<uint32_t>::max() /*&& !context.timeout()*/)
3093 {3093 {
3094 auto m1 = memberForPlace(c._place, context);3094 auto m1 = memberForPlace(c._place, context);
@@ -3110,26 +3110,26 @@
3110 neglps.push_back(nlp);3110 neglps.push_back(nlp);
3111 }3111 }
3112 }3112 }
3113 3113
3114 assert(nconstraints.size() > 0);3114 assert(nconstraints.size() > 0);
3115 if(nconstraints.back()._lower == 0 && nconstraints.back()._upper == std::numeric_limits<uint32_t>::max())3115 if(nconstraints.back()._lower == 0 && nconstraints.back()._upper == std::numeric_limits<uint32_t>::max())
3116 nconstraints.pop_back();3116 nconstraints.pop_back();
31173117
3118 assert(nconstraints.size() <= neglps.size()*2);3118 assert(nconstraints.size() <= neglps.size()*2);
3119 }3119 }
3120 3120
3121 auto lps = mergeLps(std::move(lpsv));3121 auto lps = mergeLps(std::move(lpsv));
3122 3122
3123 if(lps == nullptr && !context.timeout()) 3123 if(lps == nullptr && !context.timeout())
3124 {3124 {
3125 return Retval(BooleanCondition::getShared(!neg));3125 return Retval(BooleanCondition::getShared(!neg));
3126 }3126 }
3127 3127
3128 try {