Merge lp:~tapaal-ltl/verifypn/mcc2021 into lp:verifypn
- mcc2021
- Merge into new-trunk
Proposed by
Jiri Srba
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 258 |
Merged at revision: | 231 |
Proposed branch: | lp:~tapaal-ltl/verifypn/mcc2021 |
Merge into: | lp:verifypn |
Diff against target: |
17037 lines (+10331/-2420) 115 files modified
CMakeLists.txt (+23/-9) include/CTL/Algorithm/CertainZeroFPA.h (+1/-2) include/CTL/DependencyGraph/Configuration.h (+12/-15) include/CTL/DependencyGraph/Edge.h (+11/-5) include/CTL/PetriNets/PetriConfig.h (+0/-2) include/LTL/Algorithm/ModelChecker.h (+72/-0) include/LTL/Algorithm/NestedDepthFirstSearch.h (+91/-0) include/LTL/Algorithm/ProductPrinter.h (+31/-0) include/LTL/Algorithm/RandomNDFS.h (+59/-0) include/LTL/Algorithm/TarjanModelChecker.h (+140/-0) include/LTL/AlgorithmTypes.h (+40/-0) include/LTL/BuchiSuccessorGenerator.h (+95/-0) include/LTL/LTL.h (+34/-0) include/LTL/LTLToBuchi.h (+131/-0) include/LTL/LTLValidator.h (+201/-0) include/LTL/ProductSuccessorGenerator.h (+146/-0) include/LTL/Simplification/SpotToPQL.h (+42/-0) include/LTL/Structures/BuchiAutomaton.h (+31/-0) include/LTL/Structures/ProductState.h (+81/-0) include/LTL/Structures/ProductStateFactory.h (+46/-0) include/PetriEngine/Colored/ArcIntervals.h (+108/-0) include/PetriEngine/Colored/BindingGenerator.h (+71/-0) include/PetriEngine/Colored/ColoredNetStructures.h (+22/-12) include/PetriEngine/Colored/ColoredPetriNetBuilder.h (+64/-43) include/PetriEngine/Colored/Colors.h (+127/-21) include/PetriEngine/Colored/Expressions.h (+777/-66) include/PetriEngine/Colored/GuardRestrictor.h (+83/-0) include/PetriEngine/Colored/IntervalGenerator.h (+197/-0) include/PetriEngine/Colored/Intervals.h (+630/-0) include/PetriEngine/PQL/CTLVisitor.h (+197/-0) include/PetriEngine/PQL/Contexts.h (+6/-6) include/PetriEngine/PQL/Expressions.h (+304/-187) include/PetriEngine/PQL/PQL.h (+70/-71) include/PetriEngine/PQL/QueryPrinter.h (+127/-0) include/PetriEngine/PQL/Visitor.h (+82/-6) include/PetriEngine/PetriNet.h (+1/-0) include/PetriEngine/Reachability/ReachabilityResult.h (+4/-2) include/PetriEngine/Reachability/ReachabilitySearch.h (+12/-2) include/PetriEngine/Reducer.h (+8/-3) include/PetriEngine/ReducingSuccessorGenerator.h (+25/-54) include/PetriEngine/Simplification/Member.h (+1/-1) include/PetriEngine/Structures/Queue.h (+2/-0) include/PetriEngine/Structures/State.h (+40/-7) include/PetriEngine/Structures/StateSet.h (+85/-14) include/PetriEngine/Structures/binarywrapper.h (+2/-2) include/PetriEngine/Structures/light_deque.h (+4/-5) include/PetriEngine/Stubborn/InterestingTransitionVisitor.h (+175/-0) include/PetriEngine/Stubborn/ReachabilityStubbornSet.h (+40/-0) include/PetriEngine/Stubborn/StubbornSet.h (+146/-0) include/PetriEngine/SuccessorGenerator.h (+10/-1) include/PetriEngine/TAR/ContainsVisitor.h (+0/-10) include/PetriEngine/TAR/PlaceUseVisitor.h (+0/-2) include/PetriEngine/TAR/RangeContext.h (+0/-2) include/PetriEngine/TAR/RangeEvalContext.h (+0/-2) include/PetriEngine/TAR/Solver.h (+1/-0) include/PetriEngine/TAR/range.h (+19/-1) include/PetriEngine/options.h (+82/-44) include/PetriParse/PNMLParser.h (+6/-1) include/PetriParse/QueryParser.h (+2/-3) include/PetriParse/QueryXMLParser.h (+1/-1) src/CMakeLists.txt (+13/-4) src/CTL/Algorithm/CertainZeroFPA.cpp (+81/-51) src/CTL/Algorithm/LocalFPA.cpp (+1/-11) src/CTL/DependencyGraph/Configuration.cpp (+21/-2) src/CTL/PetriNets/OnTheFlyDG.cpp (+20/-19) src/CTL/SearchStrategy/HeuristicSearch.cpp (+1/-1) src/LTL/Algorithm/CMakeLists.txt (+8/-0) src/LTL/Algorithm/LTLToBuchi.cpp (+162/-0) src/LTL/Algorithm/ModelChecker.cpp (+71/-0) src/LTL/Algorithm/NestedDepthFirstSearch.cpp (+185/-0) src/LTL/Algorithm/ProductPrinter.cpp (+71/-0) src/LTL/Algorithm/ProductSuccessorGenerator.cpp (+153/-0) src/LTL/Algorithm/RandomNDFS.cpp (+107/-0) src/LTL/Algorithm/TarjanModelChecker.cpp (+216/-0) src/LTL/CMakeLists.txt (+14/-0) src/LTL/Simplification/CMakeLists.txt (+8/-0) src/LTL/Simplification/SpotToPQL.cpp (+160/-0) src/LTL/_LTL.cpp (+52/-0) src/PetriEngine/CMakeLists.txt (+2/-1) src/PetriEngine/Colored/BindingGenerator.cpp (+161/-0) src/PetriEngine/Colored/CMakeLists.txt (+3/-1) src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp (+305/-138) src/PetriEngine/Colored/Colors.cpp (+59/-9) src/PetriEngine/Colored/GuardRestrictor.cpp (+382/-0) src/PetriEngine/Colored/Multiset.cpp (+22/-14) src/PetriEngine/PQL/CMakeLists.txt (+2/-2) src/PetriEngine/PQL/CTLVisitor.cpp (+492/-0) src/PetriEngine/PQL/Expressions.cpp (+461/-778) src/PetriEngine/PQL/PQL.cpp (+6/-0) src/PetriEngine/PQL/PQLQueryParser.y (+2/-2) src/PetriEngine/PQL/QueryPrinter.cpp (+292/-0) src/PetriEngine/PetriNet.cpp (+5/-7) src/PetriEngine/PetriNetBuilder.cpp (+12/-14) src/PetriEngine/Reachability/ResultPrinter.cpp (+1/-1) src/PetriEngine/Reducer.cpp (+168/-124) src/PetriEngine/ReducingSuccessorGenerator.cpp (+31/-302) src/PetriEngine/Structures/AlignedEncoder.cpp (+1/-1) src/PetriEngine/Structures/Queue.cpp (+16/-2) src/PetriEngine/Stubborn/CMakeLists.txt (+3/-0) src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp (+326/-0) src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp (+41/-0) src/PetriEngine/Stubborn/StubbornSet.cpp (+302/-0) src/PetriEngine/SuccessorGenerator.cpp (+27/-0) src/PetriEngine/TAR/PlaceUseVisitor.cpp (+0/-12) src/PetriEngine/TAR/RangeContext.cpp (+0/-10) src/PetriEngine/TAR/RangeEvalContext.cpp (+0/-10) src/PetriEngine/TAR/Solver.cpp (+1/-1) src/PetriParse/PNMLParser.cpp (+221/-60) src/PetriParse/QueryBinaryParser.cpp (+24/-6) src/PetriParse/QueryXMLParser.cpp (+73/-133) src/VerifyPN.cpp (+447/-102) test_models/LTL/Bounded/model.pnml (+133/-0) test_models/LTL/Bounded/query.xml (+36/-0) test_models/LTL/generator.pnml (+60/-0) test_models/LTL/generator.xml (+52/-0) |
To merge this branch: | bzr merge lp:~tapaal-ltl/verifypn/mcc2021 |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
VerifyPN Maintainers | Pending | ||
Review via email: mp+400587@code.launchpad.net |
Commit message
Numerous efficiency improvements, new LTL engine and improved CPN unfolding via color fixed-point computation.
Consistency verified against the current trunk version on MCC 2020 models and queries.
Description of the change
To post a comment you must log in.
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'CMakeLists.txt' |
2 | --- CMakeLists.txt 2020-10-31 18:57:21 +0000 |
3 | +++ CMakeLists.txt 2021-04-02 18:07:40 +0000 |
4 | @@ -15,7 +15,7 @@ |
5 | set(CMAKE_POSITION_INDEPENDENT_CODE ON) |
6 | |
7 | |
8 | -set(VERIFYPN_VERSION 3.1.1) |
9 | +set(VERIFYPN_VERSION 4.0.0) |
10 | add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\") |
11 | |
12 | project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C) |
13 | @@ -32,11 +32,7 @@ |
14 | endif(VERIFYPN_MC_Simplification) |
15 | if (NOT APPLE) |
16 | set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static") |
17 | - else(NOT APPLE) |
18 | - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static-libgcc -static-libstdc++") |
19 | endif(NOT APPLE) |
20 | -else(VERIFYPN_Static) |
21 | - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static-libgcc -static-libstdc++") |
22 | endif (VERIFYPN_Static) |
23 | |
24 | if (VERIFYPN_MC_Simplification) |
25 | @@ -47,14 +43,15 @@ |
26 | set(ARCH_TYPE "linux64") |
27 | elseif(APPLE) |
28 | set(ARCH_TYPE "osx64") |
29 | - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mmacosx-version-min=10.8 -m64 ") |
30 | - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -mmacosx-version-min=10.8 -m64 ") |
31 | + set(CMAKE_OSX_DEPLOYMENT_TARGET 10.8) |
32 | + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -m64 ") |
33 | + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -m64 ") |
34 | else() |
35 | set(ARCH_TYPE "win64") |
36 | endif () |
37 | |
38 | -set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O3 -DNDEBUG") |
39 | - |
40 | +set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -s -Wall -pedantic-errors -O3 -DNDEBUG") |
41 | +set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer") |
42 | set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O3 -DNDEBUG") |
43 | if (VERIFYPN_Static AND NOT APPLE) |
44 | set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -static") |
45 | @@ -81,6 +78,23 @@ |
46 | CONFIGURE_COMMAND mkdir -p ${CMAKE_BINARY_DIR}/external/include |
47 | INSTALL_COMMAND cd ../rapidxml-ext && ${CMAKE_COMMAND} -E copy rapidxml.hpp rapidxml_iterators.hpp rapidxml_print.hpp rapidxml_utils.hpp ${EXTERNAL_INSTALL_LOCATION}/include |
48 | ) |
49 | + if (UNIX AND NOT APPLE) |
50 | + ExternalProject_add(spot-ext |
51 | + URL http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz |
52 | + URL_HASH SHA512=69ec8a3ce84b2c069bf40b8d2127e5085724c8e4ba88ffdefc3e2225f6334955959afd17bcfcde29fd6826d78d49a7f1303bd07ba756a8695473ff6cc5ade3a2 |
53 | + BUILD_COMMAND make |
54 | + CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} <SOURCE_DIR>/configure --prefix ${EXTERNAL_INSTALL_LOCATION} --disable-python --disable-devel --disable-debug --disable-shared --enable-static CFLAGS=-flto CXXFLAGS=-flto LDFLAGS=-fuse-linker-plugin |
55 | + INSTALL_COMMAND make install |
56 | + ) |
57 | + else () |
58 | + ExternalProject_add(spot-ext |
59 | + URL http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz |
60 | + URL_HASH SHA512=69ec8a3ce84b2c069bf40b8d2127e5085724c8e4ba88ffdefc3e2225f6334955959afd17bcfcde29fd6826d78d49a7f1303bd07ba756a8695473ff6cc5ade3a2 |
61 | + BUILD_COMMAND make |
62 | + CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} <SOURCE_DIR>/configure --prefix ${EXTERNAL_INSTALL_LOCATION} --disable-python --disable-devel --disable-debug --disable-shared --enable-static CFLAGS=${CMAKE_CXX_FLAGS} LDFLAGS=${CMAKE_LINKER_FLAGS} |
63 | + INSTALL_COMMAND make install |
64 | + ) |
65 | + endif () |
66 | |
67 | if (WIN32) #If windows 32 or 64 |
68 | set(GLPK_CFLAGS "-D __WOE__ -O3" ) |
69 | |
70 | === modified file 'Scripts/MCC20/competition-scripts/tapaal.sh' (properties changed: -x to +x) |
71 | === modified file 'include/CTL/Algorithm/CertainZeroFPA.h' |
72 | --- include/CTL/Algorithm/CertainZeroFPA.h 2020-03-02 21:03:24 +0000 |
73 | +++ include/CTL/Algorithm/CertainZeroFPA.h 2021-04-02 18:07:40 +0000 |
74 | @@ -27,9 +27,8 @@ |
75 | |
76 | void checkEdge(DependencyGraph::Edge* e, bool only_assign = false); |
77 | void finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a); |
78 | + void finalAssign(DependencyGraph::Edge *e, DependencyGraph::Assignment a); |
79 | void explore(DependencyGraph::Configuration *c); |
80 | - void addDependency(DependencyGraph::Edge *e, |
81 | - DependencyGraph::Configuration *target); |
82 | |
83 | }; |
84 | } |
85 | |
86 | === modified file 'include/CTL/DependencyGraph/Configuration.h' |
87 | --- include/CTL/DependencyGraph/Configuration.h 2020-03-10 13:29:26 +0000 |
88 | +++ include/CTL/DependencyGraph/Configuration.h 2021-04-02 18:07:40 +0000 |
89 | @@ -7,32 +7,29 @@ |
90 | #include <cstdio> |
91 | #include <iostream> |
92 | #include <vector> |
93 | +#include <forward_list> |
94 | |
95 | namespace DependencyGraph { |
96 | |
97 | class Edge; |
98 | |
99 | -enum Assignment { |
100 | - ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2 |
101 | -}; |
102 | - |
103 | class Configuration |
104 | { |
105 | +public: |
106 | + std::forward_list<Edge*> dependency_set; |
107 | + uint32_t nsuccs = 0; |
108 | +private: |
109 | uint32_t distance = 0; |
110 | -public: |
111 | - |
112 | - uint32_t getDistance() const { return distance; } |
113 | void setDistance(uint32_t value) { distance = value; } |
114 | - |
115 | +public: |
116 | + int8_t assignment = UNKNOWN; |
117 | Configuration() {} |
118 | - virtual ~Configuration(); |
119 | - |
120 | + uint32_t getDistance() const { return distance; } |
121 | bool isDone() const { return assignment == ONE || assignment == CZERO; } |
122 | - |
123 | - uint32_t owner = 0; |
124 | - uint32_t nsuccs = 0; |
125 | - std::vector<Edge*> dependency_set; |
126 | - Assignment assignment = UNKNOWN; |
127 | + void addDependency(Edge* e); |
128 | + void setOwner(uint32_t) { } |
129 | + uint32_t getOwner() { return 0; } |
130 | + |
131 | }; |
132 | |
133 | |
134 | |
135 | === modified file 'include/CTL/DependencyGraph/Edge.h' |
136 | --- include/CTL/DependencyGraph/Edge.h 2020-03-02 21:03:24 +0000 |
137 | +++ include/CTL/DependencyGraph/Edge.h 2021-04-02 18:07:40 +0000 |
138 | @@ -6,13 +6,17 @@ |
139 | #include <string> |
140 | #include <algorithm> |
141 | #include <cassert> |
142 | +#include <forward_list> |
143 | |
144 | namespace DependencyGraph { |
145 | |
146 | class Configuration; |
147 | +enum Assignment { |
148 | + ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2 |
149 | +}; |
150 | |
151 | class Edge { |
152 | - typedef std::vector<Configuration*> container; |
153 | + typedef std::forward_list<Configuration*> container; |
154 | public: |
155 | Edge(){} |
156 | Edge(Configuration &t_source) : source(&t_source) {} |
157 | @@ -20,17 +24,19 @@ |
158 | void addTarget(Configuration* conf) |
159 | { |
160 | assert(conf); |
161 | - targets.push_back(conf); |
162 | + targets.push_front(conf); |
163 | + //++children; |
164 | } |
165 | |
166 | + container targets; |
167 | Configuration* source; |
168 | - container targets; |
169 | uint8_t status = 0; |
170 | bool processed = false; |
171 | bool is_negated = false; |
172 | + bool handled = false; |
173 | int32_t refcnt = 0; |
174 | - bool handled = false; |
175 | - uint32_t weight = 0; |
176 | + /*size_t children; |
177 | + Assignment assignment;*/ |
178 | }; |
179 | } |
180 | #endif // EDGE_H |
181 | |
182 | === modified file 'include/CTL/PetriNets/PetriConfig.h' |
183 | --- include/CTL/PetriNets/PetriConfig.h 2020-03-02 21:03:24 +0000 |
184 | +++ include/CTL/PetriNets/PetriConfig.h 2021-04-02 18:07:40 +0000 |
185 | @@ -20,8 +20,6 @@ |
186 | DependencyGraph::Configuration(), marking(t_marking), query(t_query) { |
187 | } |
188 | |
189 | - virtual ~PetriConfig(){}; |
190 | - |
191 | size_t marking; |
192 | Condition *query; |
193 | |
194 | |
195 | === added directory 'include/LTL' |
196 | === added directory 'include/LTL/Algorithm' |
197 | === added file 'include/LTL/Algorithm/ModelChecker.h' |
198 | --- include/LTL/Algorithm/ModelChecker.h 1970-01-01 00:00:00 +0000 |
199 | +++ include/LTL/Algorithm/ModelChecker.h 2021-04-02 18:07:40 +0000 |
200 | @@ -0,0 +1,72 @@ |
201 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
202 | + * Simon M. Virenfeldt <simon@simwir.dk> |
203 | + * |
204 | + * This program is free software: you can redistribute it and/or modify |
205 | + * it under the terms of the GNU General Public License as published by |
206 | + * the Free Software Foundation, either version 3 of the License, or |
207 | + * (at your option) any later version. |
208 | + * |
209 | + * This program is distributed in the hope that it will be useful, |
210 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
211 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
212 | + * GNU General Public License for more details. |
213 | + * |
214 | + * You should have received a copy of the GNU General Public License |
215 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
216 | + */ |
217 | + |
218 | +#ifndef VERIFYPN_MODELCHECKER_H |
219 | +#define VERIFYPN_MODELCHECKER_H |
220 | + |
221 | +#include "PetriEngine/PQL/PQL.h" |
222 | +#include "LTL/ProductSuccessorGenerator.h" |
223 | +#include "LTL/Algorithm/ProductPrinter.h" |
224 | +#include "PetriEngine/options.h" |
225 | + |
226 | +namespace LTL { |
227 | + |
228 | + class ModelChecker { |
229 | + public: |
230 | + ModelChecker(const PetriEngine::PetriNet &net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak, |
231 | + TraceLevel level = TraceLevel::Transitions); |
232 | + |
233 | + virtual bool isSatisfied() = 0; |
234 | + |
235 | + virtual ~ModelChecker() = default; |
236 | + |
237 | + virtual void printStats(std::ostream &os) = 0; |
238 | + |
239 | + [[nodiscard]] bool isweak() const { return is_weak; } |
240 | + |
241 | + protected: |
242 | + struct stats_t { |
243 | + size_t explored = 0, expanded = 0; |
244 | + }; |
245 | + |
246 | + stats_t stats; |
247 | + virtual void _printStats(std::ostream &os, const PetriEngine::Structures::StateSetInterface &stateSet) { |
248 | + std::cout << "STATS:\n" |
249 | + << "\tdiscovered states: " << stateSet.discovered() << std::endl |
250 | + << "\texplored states: " << stats.explored << std::endl |
251 | + << "\texpanded states: " << stats.expanded << std::endl |
252 | + << "\tmax tokens: " << stateSet.maxTokens() << std::endl; |
253 | + } |
254 | + |
255 | + std::unique_ptr<ProductSuccessorGenerator> successorGenerator; |
256 | + const PetriEngine::PetriNet &net; |
257 | + PetriEngine::PQL::Condition_ptr formula; |
258 | + TraceLevel traceLevel; |
259 | + |
260 | + size_t _discovered = 0; |
261 | + const bool shortcircuitweak; |
262 | + bool weakskip = false; |
263 | + bool is_weak = false; |
264 | + int maxTransName; |
265 | + |
266 | + std::ostream &printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os); |
267 | + |
268 | + void printLoop(std::ostream &os); |
269 | + }; |
270 | +} |
271 | + |
272 | +#endif //VERIFYPN_MODELCHECKER_H |
273 | |
274 | === added file 'include/LTL/Algorithm/NestedDepthFirstSearch.h' |
275 | --- include/LTL/Algorithm/NestedDepthFirstSearch.h 1970-01-01 00:00:00 +0000 |
276 | +++ include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-04-02 18:07:40 +0000 |
277 | @@ -0,0 +1,91 @@ |
278 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
279 | + * Simon M. Virenfeldt <simon@simwir.dk> |
280 | + * |
281 | + * This program is free software: you can redistribute it and/or modify |
282 | + * it under the terms of the GNU General Public License as published by |
283 | + * the Free Software Foundation, either version 3 of the License, or |
284 | + * (at your option) any later version. |
285 | + * |
286 | + * This program is distributed in the hope that it will be useful, |
287 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
288 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
289 | + * GNU General Public License for more details. |
290 | + * |
291 | + * You should have received a copy of the GNU General Public License |
292 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
293 | + */ |
294 | + |
295 | +#ifndef VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H |
296 | +#define VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H |
297 | + |
298 | +#include "ModelChecker.h" |
299 | +#include "PetriEngine/Structures/StateSet.h" |
300 | +#include "PetriEngine/Structures/State.h" |
301 | +#include "PetriEngine/Structures/Queue.h" |
302 | +#include "LTL/Structures/ProductStateFactory.h" |
303 | + |
304 | +#include <ptrie/ptrie_stable.h> |
305 | +#include <unordered_set> |
306 | + |
307 | +using namespace PetriEngine; |
308 | + |
309 | +namespace LTL { |
310 | + /** |
311 | + * Implement the nested DFS algorithm for LTL model checking. Roughly based on versions given in |
312 | + * <p> |
313 | + * Jaco Geldenhuys & Antti Valmari,<br> |
314 | + * More efficient on-the-fly LTL verification with Tarjan's algorithm,<br> |
315 | + * https://doi.org/10.1016/j.tcs.2005.07.004 |
316 | + * </p> |
317 | + * and |
318 | + * <p> |
319 | + * Gerard J. Holzmann, Doron Peled, and Mihalis Yannakakis<br> |
320 | + * On Nested Depth First Search<br> |
321 | + * https://spinroot.com/gerard/pdf/inprint/spin96.pdf |
322 | + * </p> |
323 | + * For most use cases, Tarjan's algorithm (see LTL::TarjanModelChecker) is faster. |
324 | + * @tparam W type used for state storage. Use <code>PetriEngine::Structures::TracableStateSet</code> if you want traces, |
325 | + * <code>PetriEngine::Structures::StateSet</code> if you don't care (as it is faster). |
326 | + */ |
327 | + template <typename W> |
328 | + class NestedDepthFirstSearch : public ModelChecker { |
329 | + public: |
330 | + NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak, TraceLevel level = TraceLevel::Full) |
331 | + : ModelChecker(net, ptr, shortcircuitweak, level), factory{net, successorGenerator->initial_buchi_state()}, |
332 | + states(net, 0, (int)net.numberOfPlaces() + 1) {} |
333 | + |
334 | + bool isSatisfied() override; |
335 | + |
336 | + void printStats(std::ostream &os) override; |
337 | + |
338 | + private: |
339 | + using State = LTL::Structures::ProductState; |
340 | + |
341 | + Structures::ProductStateFactory factory; |
342 | + W states; //StateSet |
343 | + std::set<size_t> mark1; |
344 | + std::set<size_t> mark2; |
345 | + |
346 | + struct StackEntry { |
347 | + size_t id; |
348 | + successor_info sucinfo; |
349 | + }; |
350 | + |
351 | + State *seed; |
352 | + bool violation = false; |
353 | + |
354 | + //Used for printing the trace |
355 | + std::stack<std::pair<size_t, size_t>> nested_transitions; |
356 | + |
357 | + void dfs(); |
358 | + |
359 | + void ndfs(State &state); |
360 | + void printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os = std::cout); |
361 | + |
362 | + static constexpr bool SaveTrace = std::is_same_v<W, PetriEngine::Structures::TracableStateSet>; |
363 | + }; |
364 | + extern template class NestedDepthFirstSearch<PetriEngine::Structures::StateSet>; |
365 | + extern template class NestedDepthFirstSearch<PetriEngine::Structures::TracableStateSet>; |
366 | +} |
367 | + |
368 | +#endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H |
369 | |
370 | === added file 'include/LTL/Algorithm/ProductPrinter.h' |
371 | --- include/LTL/Algorithm/ProductPrinter.h 1970-01-01 00:00:00 +0000 |
372 | +++ include/LTL/Algorithm/ProductPrinter.h 2021-04-02 18:07:40 +0000 |
373 | @@ -0,0 +1,31 @@ |
374 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
375 | + * Simon M. Virenfeldt <simon@simwir.dk> |
376 | + * |
377 | + * This program is free software: you can redistribute it and/or modify |
378 | + * it under the terms of the GNU General Public License as published by |
379 | + * the Free Software Foundation, either version 3 of the License, or |
380 | + * (at your option) any later version. |
381 | + * |
382 | + * This program is distributed in the hope that it will be useful, |
383 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
384 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
385 | + * GNU General Public License for more details. |
386 | + * |
387 | + * You should have received a copy of the GNU General Public License |
388 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
389 | + */ |
390 | + |
391 | +#ifndef VERIFYPN_PRODUCTPRINTER_H |
392 | +#define VERIFYPN_PRODUCTPRINTER_H |
393 | + |
394 | +#include "LTL/Structures/ProductStateFactory.h" |
395 | +#include "LTL/ProductSuccessorGenerator.h" |
396 | +#include "PetriEngine/Structures/StateSet.h" |
397 | +#include "PetriEngine/Structures/Queue.h" |
398 | +#include "PetriEngine/PQL/Contexts.h" |
399 | + |
400 | +namespace LTL::ProductPrinter { |
401 | + void printProduct(ProductSuccessorGenerator &successorGenerator, std::ostream &os, const PetriEngine::PetriNet &net, |
402 | + PetriEngine::PQL::Condition_ptr formula); |
403 | +} |
404 | +#endif //VERIFYPN_PRODUCTPRINTER_H |
405 | |
406 | === added file 'include/LTL/Algorithm/RandomNDFS.h' |
407 | --- include/LTL/Algorithm/RandomNDFS.h 1970-01-01 00:00:00 +0000 |
408 | +++ include/LTL/Algorithm/RandomNDFS.h 2021-04-02 18:07:40 +0000 |
409 | @@ -0,0 +1,59 @@ |
410 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
411 | + * Simon M. Virenfeldt <simon@simwir.dk> |
412 | + * |
413 | + * This program is free software: you can redistribute it and/or modify |
414 | + * it under the terms of the GNU General Public License as published by |
415 | + * the Free Software Foundation, either version 3 of the License, or |
416 | + * (at your option) any later version. |
417 | + * |
418 | + * This program is distributed in the hope that it will be useful, |
419 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
420 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
421 | + * GNU General Public License for more details. |
422 | + * |
423 | + * You should have received a copy of the GNU General Public License |
424 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
425 | + */ |
426 | + |
427 | +#ifndef VERIFYPN_RANDOMNDFS_H |
428 | +#define VERIFYPN_RANDOMNDFS_H |
429 | + |
430 | +#include "ModelChecker.h" |
431 | +#include "PetriEngine/Structures/StateSet.h" |
432 | +#include "PetriEngine/Structures/State.h" |
433 | +#include "PetriEngine/Structures/Queue.h" |
434 | +#include "LTL/Structures/ProductStateFactory.h" |
435 | + |
436 | +#include <ptrie/ptrie_stable.h> |
437 | + |
438 | +using namespace PetriEngine; |
439 | + |
440 | +namespace LTL { |
441 | + class RandomNDFS : public ModelChecker { |
442 | + public: |
443 | + RandomNDFS(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr) |
444 | + : ModelChecker(net, ptr, false), factory{net, successorGenerator->initial_buchi_state()}, |
445 | + mark1(net, 0, (int) net.numberOfPlaces() + 1), mark2(net, 0, (int) net.numberOfPlaces() + 1) {} |
446 | + |
447 | + bool isSatisfied() override; |
448 | + |
449 | + void printStats(std::ostream &os) override; |
450 | + |
451 | + private: |
452 | + using State = LTL::Structures::ProductState; |
453 | + |
454 | + Structures::ProductStateFactory factory; |
455 | + PetriEngine::Structures::StateSet mark1; |
456 | + PetriEngine::Structures::StateSet mark2; |
457 | + |
458 | + |
459 | + State *seed; |
460 | + bool violation = false; |
461 | + |
462 | + void dfs(); |
463 | + |
464 | + void ndfs(State &state); |
465 | + }; |
466 | +} |
467 | + |
468 | +#endif //VERIFYPN_RANDOMNDFS_H |
469 | |
470 | === added file 'include/LTL/Algorithm/TarjanModelChecker.h' |
471 | --- include/LTL/Algorithm/TarjanModelChecker.h 1970-01-01 00:00:00 +0000 |
472 | +++ include/LTL/Algorithm/TarjanModelChecker.h 2021-04-02 18:07:40 +0000 |
473 | @@ -0,0 +1,140 @@ |
474 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
475 | + * Simon M. Virenfeldt <simon@simwir.dk> |
476 | + * |
477 | + * This program is free software: you can redistribute it and/or modify |
478 | + * it under the terms of the GNU General Public License as published by |
479 | + * the Free Software Foundation, either version 3 of the License, or |
480 | + * (at your option) any later version. |
481 | + * |
482 | + * This program is distributed in the hope that it will be useful, |
483 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
484 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
485 | + * GNU General Public License for more details. |
486 | + * |
487 | + * You should have received a copy of the GNU General Public License |
488 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
489 | + */ |
490 | + |
491 | +#ifndef VERIFYPN_TARJANMODELCHECKER_H |
492 | +#define VERIFYPN_TARJANMODELCHECKER_H |
493 | + |
494 | + |
495 | +#include "LTL/Algorithm/ModelChecker.h" |
496 | +#include "LTL/Structures/ProductStateFactory.h" |
497 | +#include "PetriEngine/Structures/StateSet.h" |
498 | + |
499 | +#include <stack> |
500 | +#include <unordered_set> |
501 | + |
502 | +namespace LTL { |
503 | + |
504 | + /** |
505 | + * Implements on-the-fly version of Tarjan's algorithm suitable for LTL model checking. |
506 | + * The idea is to detect some reachable strongly connected component containing an accepting state, |
507 | + * which constitutes a counter-example. |
508 | + * For more details see |
509 | + * <p> |
510 | + * Jaco Geldenhuys & Antti Valmari, |
511 | + * More efficient on-the-fly LTL verification with Tarjan's algorithm, |
512 | + * https://doi.org/10.1016/j.tcs.2005.07.004 |
513 | + * </p> |
514 | + * @tparam SaveTrace whether to save and print counter-examples when possible. |
515 | + */ |
516 | + template<bool SaveTrace> |
517 | + class TarjanModelChecker : public ModelChecker { |
518 | + public: |
519 | + TarjanModelChecker(const PetriEngine::PetriNet &net, const PetriEngine::PQL::Condition_ptr &cond, const bool shortcircuitweak, |
520 | + TraceLevel level = TraceLevel::Full) |
521 | + : ModelChecker(net, cond, shortcircuitweak, level), factory(net, successorGenerator->initial_buchi_state()), |
522 | + seen(net, 0, (int) net.numberOfPlaces() + 1) |
523 | + { |
524 | + chash.fill(std::numeric_limits<idx_t>::max()); |
525 | + } |
526 | + |
527 | + bool isSatisfied() override; |
528 | + |
529 | + void printStats(std::ostream &os) override |
530 | + { |
531 | + _printStats(os, seen); |
532 | + } |
533 | + |
534 | + private: |
535 | + using State = LTL::Structures::ProductState; |
536 | + using idx_t = size_t; |
537 | + // 64 MB hash table |
538 | + static constexpr idx_t HashSz = 16777216; |
539 | + |
540 | + LTL::Structures::ProductStateFactory factory; |
541 | + |
542 | + using StateSet = std::conditional_t<SaveTrace, PetriEngine::Structures::TracableStateSet, PetriEngine::Structures::StateSet>; |
543 | + |
544 | + StateSet seen; |
545 | + std::unordered_set<idx_t> store; |
546 | + |
547 | + // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack |
548 | + // corresponding to state. Collisions are resolved using linked list via CEntry::next. |
549 | + std::array<idx_t, HashSz> chash; |
550 | + static_assert(sizeof(chash) == (1U << 27U)); |
551 | + |
552 | + static inline idx_t hash(idx_t id) |
553 | + { |
554 | + return id % HashSz; |
555 | + } |
556 | + |
557 | + struct PlainCEntry { |
558 | + idx_t lowlink; |
559 | + idx_t stateid; |
560 | + idx_t next = std::numeric_limits<idx_t>::max(); |
561 | + |
562 | + PlainCEntry(idx_t lowlink, idx_t stateid, idx_t next) : lowlink(lowlink), stateid(stateid), next(next) {} |
563 | + }; |
564 | + |
565 | + struct TracableCEntry : PlainCEntry { |
566 | + idx_t lowsource = std::numeric_limits<idx_t>::max(); |
567 | + idx_t sourcetrans; |
568 | + |
569 | + TracableCEntry(idx_t lowlink, idx_t stateid, idx_t next) : PlainCEntry(lowlink, stateid, next) {} |
570 | + }; |
571 | + |
572 | + using CEntry = std::conditional_t<SaveTrace, |
573 | + TracableCEntry, |
574 | + PlainCEntry>; |
575 | + |
576 | + |
577 | + struct DEntry { |
578 | + idx_t pos; // position in cstack. |
579 | + successor_info sucinfo; |
580 | + }; |
581 | + |
582 | + // master list of state information. |
583 | + std::vector<CEntry> cstack; |
584 | + // depth-first search stack, contains current search path. |
585 | + std::stack<DEntry> dstack; |
586 | + // cstack positions of accepting states in current search path, for quick access. |
587 | + std::stack<idx_t> astack; |
588 | + bool violation = false; |
589 | + size_t loopstate = std::numeric_limits<size_t>::max(); |
590 | + size_t looptrans = std::numeric_limits<size_t>::max(); |
591 | + |
592 | + void push(State &state, size_t stateid); |
593 | + |
594 | + void pop(); |
595 | + |
596 | + void update(idx_t to); |
597 | + |
598 | + bool nexttrans(State &state, State &parent, DEntry &delem); |
599 | + |
600 | + void popCStack(); |
601 | + |
602 | + void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout); |
603 | + |
604 | + }; |
605 | + |
606 | + extern template |
607 | + class TarjanModelChecker<true>; |
608 | + |
609 | + extern template |
610 | + class TarjanModelChecker<false>; |
611 | +} |
612 | + |
613 | +#endif //VERIFYPN_TARJANMODELCHECKER_H |
614 | |
615 | === added file 'include/LTL/AlgorithmTypes.h' |
616 | --- include/LTL/AlgorithmTypes.h 1970-01-01 00:00:00 +0000 |
617 | +++ include/LTL/AlgorithmTypes.h 2021-04-02 18:07:40 +0000 |
618 | @@ -0,0 +1,40 @@ |
619 | +/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
620 | + * Simon M. Virenfeldt <simon@simwir.dk> |
621 | + * |
622 | + * This program is free software: you can redistribute it and/or modify |
623 | + * it under the terms of the GNU General Public License as published by |
624 | + * the Free Software Foundation, either version 3 of the License, or |
625 | + * (at your option) any later version. |
626 | + * |
627 | + * This program is distributed in the hope that it will be useful, |
628 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
629 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
630 | + * GNU General Public License for more details. |
631 | + * |
632 | + * You should have received a copy of the GNU General Public License |
633 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
634 | + */ |
635 | + |
636 | +#ifndef VERIFYPN_ALGORITHMTYPES_H |
637 | +#define VERIFYPN_ALGORITHMTYPES_H |
638 | + |
639 | +namespace LTL { |
640 | + enum class Algorithm { |
641 | + NDFS, Tarjan, None=-1 |
642 | + }; |
643 | + inline auto to_string(Algorithm alg) { |
644 | + switch (alg) { |
645 | + case Algorithm::NDFS: |
646 | + return "NDFS"; |
647 | + case Algorithm::Tarjan: |
648 | + return "TARJAN"; |
649 | + case Algorithm::None: |
650 | + default: |
651 | + std::cerr << "to_string: Invalid LTL Algorithm " << static_cast<int>(alg) << '\n'; |
652 | + assert(false); |
653 | + return "None"; |
654 | + } |
655 | + } |
656 | +} |
657 | + |
658 | +#endif //VERIFYPN_ALGORITHMTYPES_H |
659 | |
660 | === added file 'include/LTL/BuchiSuccessorGenerator.h' |
661 | --- include/LTL/BuchiSuccessorGenerator.h 1970-01-01 00:00:00 +0000 |
662 | +++ include/LTL/BuchiSuccessorGenerator.h 2021-04-02 18:07:40 +0000 |
663 | @@ -0,0 +1,95 @@ |
664 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
665 | + * Simon M. Virenfeldt <simon@simwir.dk> |
666 | + * |
667 | + * This program is free software: you can redistribute it and/or modify |
668 | + * it under the terms of the GNU General Public License as published by |
669 | + * the Free Software Foundation, either version 3 of the License, or |
670 | + * (at your option) any later version. |
671 | + * |
672 | + * This program is distributed in the hope that it will be useful, |
673 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
674 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
675 | + * GNU General Public License for more details. |
676 | + * |
677 | + * You should have received a copy of the GNU General Public License |
678 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
679 | + */ |
680 | + |
681 | +#ifndef VERIFYPN_BUCHISUCCESSORGENERATOR_H |
682 | +#define VERIFYPN_BUCHISUCCESSORGENERATOR_H |
683 | + |
684 | +#include "PetriEngine/SuccessorGenerator.h" |
685 | +#include "LTL/Structures/BuchiAutomaton.h" |
686 | + |
687 | +#include <spot/twa/twagraph.hh> |
688 | +#include <utility> |
689 | +#include <memory> |
690 | + |
691 | +namespace LTL { |
692 | + class BuchiSuccessorGenerator { |
693 | + public: |
694 | + explicit BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton) |
695 | + : aut(std::move(automaton)) |
696 | + { |
697 | + deleter = SuccIterDeleter{&aut}; |
698 | + } |
699 | + |
700 | + void prepare(size_t state) |
701 | + { |
702 | + auto curstate = aut.buchi->state_from_number(state); |
703 | + succ = _succ_iter{aut.buchi->succ_iter(curstate), SuccIterDeleter{&aut}}; |
704 | + succ->first(); |
705 | + } |
706 | + |
707 | + bool next(size_t &state, bdd &cond) |
708 | + { |
709 | + if (!succ->done()) { |
710 | + auto dst = succ->dst(); |
711 | + state = aut.buchi->state_number(dst); |
712 | + cond = succ->cond(); |
713 | + succ->next(); |
714 | + dst->destroy(); |
715 | + return true; |
716 | + } |
717 | + return false; |
718 | + } |
719 | + |
720 | + [[nodiscard]] bool is_accepting(size_t state) const |
721 | + { |
722 | + return aut.buchi->state_is_accepting(state); |
723 | + } |
724 | + |
725 | + [[nodiscard]] size_t initial_state_number() const |
726 | + { |
727 | + return aut.buchi->get_init_state_number(); |
728 | + } |
729 | + |
730 | + [[nodiscard]] PetriEngine::PQL::Condition_ptr getExpression(size_t i) const |
731 | + { |
732 | + return aut.ap_info.at(i).expression; |
733 | + } |
734 | + |
735 | + [[nodiscard]] bool is_weak() const |
736 | + { |
737 | + return (bool) aut.buchi->prop_weak(); |
738 | + } |
739 | + |
740 | + private: |
741 | + Structures::BuchiAutomaton aut; |
742 | + |
743 | + struct SuccIterDeleter { |
744 | + Structures::BuchiAutomaton *aut; |
745 | + |
746 | + void operator()(spot::twa_succ_iterator *iter) const |
747 | + { |
748 | + aut->buchi->release_iter(iter); |
749 | + } |
750 | + }; |
751 | + |
752 | + SuccIterDeleter deleter{}; |
753 | + |
754 | + using _succ_iter = std::unique_ptr<spot::twa_succ_iterator, SuccIterDeleter>; |
755 | + _succ_iter succ = nullptr; |
756 | + }; |
757 | +} |
758 | +#endif //VERIFYPN_BUCHISUCCESSORGENERATOR_H |
759 | |
760 | === added file 'include/LTL/LTL.h' |
761 | --- include/LTL/LTL.h 1970-01-01 00:00:00 +0000 |
762 | +++ include/LTL/LTL.h 2021-04-02 18:07:40 +0000 |
763 | @@ -0,0 +1,34 @@ |
764 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
765 | + * Simon M. Virenfeldt <simon@simwir.dk> |
766 | + * |
767 | + * This program is free software: you can redistribute it and/or modify |
768 | + * it under the terms of the GNU General Public License as published by |
769 | + * the Free Software Foundation, either version 3 of the License, or |
770 | + * (at your option) any later version. |
771 | + * |
772 | + * This program is distributed in the hope that it will be useful, |
773 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
774 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
775 | + * GNU General Public License for more details. |
776 | + * |
777 | + * You should have received a copy of the GNU General Public License |
778 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
779 | + */ |
780 | + |
781 | +#ifndef VERIFYPN_LTLALGORITHM_H |
782 | +#define VERIFYPN_LTLALGORITHM_H |
783 | + |
784 | +#include "LTL/LTLValidator.h" |
785 | +#include "LTL/Algorithm/TarjanModelChecker.h" |
786 | +#include "LTL/Algorithm/NestedDepthFirstSearch.h" |
787 | +#include "LTL/Algorithm/RandomNDFS.h" |
788 | +#include "LTL/Simplification/SpotToPQL.h" |
789 | +#include "LTL/LTLToBuchi.h" |
790 | + |
791 | +namespace LTL { |
792 | + |
793 | + |
794 | + std::pair<Condition_ptr, bool> to_ltl(const Condition_ptr &formula); |
795 | +} |
796 | + |
797 | +#endif |
798 | \ No newline at end of file |
799 | |
800 | === added file 'include/LTL/LTLToBuchi.h' |
801 | --- include/LTL/LTLToBuchi.h 1970-01-01 00:00:00 +0000 |
802 | +++ include/LTL/LTLToBuchi.h 2021-04-02 18:07:40 +0000 |
803 | @@ -0,0 +1,131 @@ |
804 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
805 | + * Simon M. Virenfeldt <simon@simwir.dk> |
806 | + * |
807 | + * This program is free software: you can redistribute it and/or modify |
808 | + * it under the terms of the GNU General Public License as published by |
809 | + * the Free Software Foundation, either version 3 of the License, or |
810 | + * (at your option) any later version. |
811 | + * |
812 | + * This program is distributed in the hope that it will be useful, |
813 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
814 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
815 | + * GNU General Public License for more details. |
816 | + * |
817 | + * You should have received a copy of the GNU General Public License |
818 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
819 | + */ |
820 | + |
821 | +#ifndef VERIFYPN_LTLTOBUCHI_H |
822 | +#define VERIFYPN_LTLTOBUCHI_H |
823 | + |
824 | +#include "PetriParse/QueryParser.h" |
825 | +#include "PetriEngine/PQL/QueryPrinter.h" |
826 | + |
827 | +#include <iostream> |
828 | +#include <string> |
829 | + |
830 | +#include <spot/tl/formula.hh> |
831 | + |
832 | +namespace LTL { |
833 | + struct AtomicProposition { |
834 | + PetriEngine::PQL::Condition_ptr expression; |
835 | + std::string text; |
836 | + }; |
837 | + |
838 | + using APInfo = std::vector<AtomicProposition>; |
839 | + std::string toSpotFormat(const QueryItem &query); |
840 | + void toSpotFormat(const QueryItem &query, std::ostream &os); |
841 | + std::pair<spot::formula, APInfo> to_spot_formula(const PetriEngine::PQL::Condition_ptr& query); |
842 | + |
843 | + class BuchiSuccessorGenerator; |
844 | + BuchiSuccessorGenerator makeBuchiAutomaton(const PetriEngine::PQL::Condition_ptr &query); |
845 | + |
846 | + |
847 | + class FormulaToSpotSyntax : public PetriEngine::PQL::QueryPrinter { |
848 | + protected: |
849 | + void _accept(const PetriEngine::PQL::ACondition *condition) override; |
850 | + |
851 | + void _accept(const PetriEngine::PQL::ECondition *condition) override; |
852 | + |
853 | + void _accept(const PetriEngine::PQL::NotCondition *element) override; |
854 | + |
855 | + void _accept(const PetriEngine::PQL::AndCondition *element) override; |
856 | + |
857 | + void _accept(const PetriEngine::PQL::OrCondition *element) override; |
858 | + |
859 | + void _accept(const PetriEngine::PQL::LessThanCondition *element) override; |
860 | + |
861 | + void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override; |
862 | + |
863 | + void _accept(const PetriEngine::PQL::EqualCondition *element) override; |
864 | + |
865 | + void _accept(const PetriEngine::PQL::NotEqualCondition *element) override; |
866 | + |
867 | + void _accept(const PetriEngine::PQL::UnfoldedFireableCondition *element) override; |
868 | + |
869 | + void _accept(const PetriEngine::PQL::FireableCondition *element) override; |
870 | + |
871 | + void _accept(const PetriEngine::PQL::BooleanCondition *element) override; |
872 | + |
873 | + void _accept(const PetriEngine::PQL::LiteralExpr *element) override; |
874 | + |
875 | + void _accept(const PetriEngine::PQL::PlusExpr *element) override; |
876 | + |
877 | + void _accept(const PetriEngine::PQL::MultiplyExpr *element) override; |
878 | + |
879 | + void _accept(const PetriEngine::PQL::MinusExpr *element) override; |
880 | + |
881 | + void _accept(const PetriEngine::PQL::SubtractExpr *element) override; |
882 | + |
883 | + void _accept(const PetriEngine::PQL::IdentifierExpr *element) override; |
884 | + |
885 | + void _accept(const PetriEngine::PQL::CompareConjunction *element) override; |
886 | + |
887 | + public: |
888 | + |
889 | + explicit FormulaToSpotSyntax(std::ostream &os = std::cout) |
890 | + : PetriEngine::PQL::QueryPrinter(os), compress(true) {} |
891 | + |
892 | + auto begin() const { |
893 | + return std::begin(ap_info); |
894 | + } |
895 | + |
896 | + auto end() const { |
897 | + return std::end(ap_info); |
898 | + } |
899 | + |
900 | + const APInfo &apInfo() const { |
901 | + return ap_info; |
902 | + } |
903 | + |
904 | + private: |
905 | + APInfo ap_info; |
906 | + bool is_quoted = false; |
907 | + bool compress; |
908 | + |
909 | + void make_atomic_prop(const PetriEngine::PQL::Condition_constptr &element) |
910 | + { |
911 | + auto cond = |
912 | + const_cast<PetriEngine::PQL::Condition *>(element.get())->shared_from_this(); |
913 | + std::stringstream ss; |
914 | + ss << "\""; |
915 | + if (compress) { |
916 | + // FIXME Very naive; this completely removes APs being in multiple places in the query, |
917 | + // leading to some query not being answered as is. The net gain is large in the firebaility category, |
918 | + // but ideally it would be possible to make a smarter approach that looks at previously stored APs |
919 | + // and efficiently checks for repeat APs such that we can reuse APs. |
920 | + ss << ap_info.size(); |
921 | + } |
922 | + else { |
923 | + PetriEngine::PQL::QueryPrinter _printer{ss}; |
924 | + cond->visit(_printer); |
925 | + } |
926 | + ss << "\""; |
927 | + os << ss.str(); |
928 | + ap_info.push_back(AtomicProposition{cond, ss.str().substr(1, ss.str().size() - 2)}); |
929 | + } |
930 | + }; |
931 | + |
932 | +} |
933 | + |
934 | +#endif //VERIFYPN_LTLTOBUCHI_H |
935 | |
936 | === added file 'include/LTL/LTLValidator.h' |
937 | --- include/LTL/LTLValidator.h 1970-01-01 00:00:00 +0000 |
938 | +++ include/LTL/LTLValidator.h 2021-04-02 18:07:40 +0000 |
939 | @@ -0,0 +1,201 @@ |
940 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
941 | + * Simon M. Virenfeldt <simon@simwir.dk> |
942 | + * |
943 | + * This program is free software: you can redistribute it and/or modify |
944 | + * it under the terms of the GNU General Public License as published by |
945 | + * the Free Software Foundation, either version 3 of the License, or |
946 | + * (at your option) any later version. |
947 | + * |
948 | + * This program is distributed in the hope that it will be useful, |
949 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
950 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
951 | + * GNU General Public License for more details. |
952 | + * |
953 | + * You should have received a copy of the GNU General Public License |
954 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
955 | + */ |
956 | + |
957 | +#ifndef VERIFYPN_LTLVALIDATOR_H |
958 | +#define VERIFYPN_LTLVALIDATOR_H |
959 | + |
960 | +#include "PetriEngine/PQL/Visitor.h" |
961 | + |
962 | +namespace LTL { |
963 | + using namespace PetriEngine::PQL; |
964 | + class LTLValidator : public PetriEngine::PQL::Visitor { |
965 | + public: |
966 | + bool bad() const { return _bad; } |
967 | + |
968 | + operator bool() const { return !bad(); } |
969 | + |
970 | + bool isLTL(const Condition_ptr& condition) { |
971 | + std::shared_ptr<SimpleQuantifierCondition> quantifierCondition; |
972 | + if ((quantifierCondition = std::dynamic_pointer_cast<ACondition>(condition)) != nullptr || |
973 | + (quantifierCondition = std::dynamic_pointer_cast<ECondition>(condition)) != nullptr ){ |
974 | + (*quantifierCondition)[0]->visit(*this); |
975 | + } else { |
976 | + condition->visit(*this); |
977 | + } |
978 | + return !bad(); |
979 | + } |
980 | + |
981 | + protected: |
982 | + |
983 | + void _visitNary(const LogicalCondition *condition) { |
984 | + for (const auto &cond : *condition) { |
985 | + cond->visit(*this); |
986 | + } |
987 | + }; |
988 | + |
989 | + void _accept(const PetriEngine::PQL::EFCondition *condition) override { |
990 | + setBad(); |
991 | + std::cerr << "found EFCondition" << std::endl; |
992 | + } |
993 | + |
994 | + void _accept(const PetriEngine::PQL::EGCondition *condition) override { |
995 | + setBad(); |
996 | + std::cerr << "found EGCondition" << std::endl; |
997 | + } |
998 | + |
999 | + void _accept(const PetriEngine::PQL::AGCondition *condition) override { |
1000 | + setBad(); |
1001 | + std::cerr << "found AGCondition" << std::endl; |
1002 | + } |
1003 | + |
1004 | + void _accept(const PetriEngine::PQL::AFCondition *condition) override { |
1005 | + setBad(); |
1006 | + std::cerr << "found AFCondition" << std::endl; |
1007 | + } |
1008 | + |
1009 | + void _accept(const PetriEngine::PQL::EXCondition *condition) override { |
1010 | + setBad(); |
1011 | + std::cerr << "found EXCondition" << std::endl; |
1012 | + } |
1013 | + |
1014 | + void _accept(const PetriEngine::PQL::AXCondition *condition) override { |
1015 | + setBad(); |
1016 | + std::cerr << "found AXCondition" << std::endl; |
1017 | + } |
1018 | + |
1019 | + void _accept(const PetriEngine::PQL::EUCondition *condition) override { |
1020 | + setBad(); |
1021 | + std::cerr << "found EUCondition" << std::endl; |
1022 | + } |
1023 | + |
1024 | + void _accept(const PetriEngine::PQL::AUCondition *condition) override { |
1025 | + setBad(); |
1026 | + std::cerr << "found AUCondition" << std::endl; |
1027 | + } |
1028 | + |
1029 | + void _accept(const PetriEngine::PQL::ACondition *condition) override { |
1030 | + setBad(); |
1031 | + } |
1032 | + |
1033 | + void _accept(const PetriEngine::PQL::ECondition *condition) override { |
1034 | + setBad(); |
1035 | + } |
1036 | + |
1037 | + void _accept(const PetriEngine::PQL::NotCondition *element) override { |
1038 | + (*element)[0]->visit(*this); |
1039 | + } |
1040 | + |
1041 | + void _accept(const PetriEngine::PQL::AndCondition *element) override { |
1042 | + _visitNary(element); |
1043 | + } |
1044 | + |
1045 | + void _accept(const PetriEngine::PQL::OrCondition *element) override { |
1046 | + _visitNary(element); |
1047 | + } |
1048 | + |
1049 | + void _accept(const PetriEngine::PQL::LessThanCondition *element) override { |
1050 | + (*element)[0]->visit(*this); |
1051 | + (*element)[1]->visit(*this); |
1052 | + } |
1053 | + |
1054 | + void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override { |
1055 | + (*element)[0]->visit(*this); |
1056 | + (*element)[1]->visit(*this); |
1057 | + } |
1058 | + |
1059 | + void _accept(const PetriEngine::PQL::EqualCondition *element) override { |
1060 | + (*element)[0]->visit(*this); |
1061 | + (*element)[1]->visit(*this); |
1062 | + } |
1063 | + |
1064 | + void _accept(const PetriEngine::PQL::NotEqualCondition *element) override { |
1065 | + (*element)[0]->visit(*this); |
1066 | + (*element)[1]->visit(*this); |
1067 | + } |
1068 | + |
1069 | + void _accept(const PetriEngine::PQL::DeadlockCondition *element) override { |
1070 | + |
1071 | + } |
1072 | + |
1073 | + void _accept(const PetriEngine::PQL::CompareConjunction *element) override { |
1074 | + |
1075 | + } |
1076 | + |
1077 | + void _accept(const PetriEngine::PQL::UnfoldedUpperBoundsCondition *element) override { |
1078 | + |
1079 | + } |
1080 | + |
1081 | + void _accept(const PetriEngine::PQL::GCondition *condition) override { |
1082 | + (*condition)[0]->visit(*this); |
1083 | + } |
1084 | + |
1085 | + void _accept(const PetriEngine::PQL::FCondition *condition) override { |
1086 | + (*condition)[0]->visit(*this); |
1087 | + } |
1088 | + |
1089 | + void _accept(const PetriEngine::PQL::XCondition *condition) override { |
1090 | + (*condition)[0]->visit(*this); |
1091 | + } |
1092 | + |
1093 | + void _accept(const PetriEngine::PQL::UntilCondition *condition) override { |
1094 | + (*condition)[0]->visit(*this); |
1095 | + } |
1096 | + |
1097 | + void _accept(const PetriEngine::PQL::UnfoldedFireableCondition *element) override { |
1098 | + } |
1099 | + |
1100 | + void _accept(const PetriEngine::PQL::FireableCondition *element) override { |
1101 | + } |
1102 | + |
1103 | + void _accept(const PetriEngine::PQL::UpperBoundsCondition *element) override { |
1104 | + } |
1105 | + |
1106 | + void _accept(const PetriEngine::PQL::LivenessCondition *element) override { |
1107 | + } |
1108 | + |
1109 | + void _accept(const PetriEngine::PQL::KSafeCondition *element) override { |
1110 | + } |
1111 | + |
1112 | + void _accept(const PetriEngine::PQL::QuasiLivenessCondition *element) override { |
1113 | + } |
1114 | + |
1115 | + void _accept(const PetriEngine::PQL::StableMarkingCondition *element) override { |
1116 | + } |
1117 | + |
1118 | + void _accept(const PetriEngine::PQL::BooleanCondition *element) override {} |
1119 | + |
1120 | + void _accept(const PetriEngine::PQL::UnfoldedIdentifierExpr *element) override {} |
1121 | + |
1122 | + void _accept(const PetriEngine::PQL::LiteralExpr *element) override {} |
1123 | + |
1124 | + void _accept(const PetriEngine::PQL::PlusExpr *element) override {} |
1125 | + |
1126 | + void _accept(const PetriEngine::PQL::MultiplyExpr *element) override {} |
1127 | + |
1128 | + void _accept(const PetriEngine::PQL::MinusExpr *element) override {} |
1129 | + |
1130 | + void _accept(const PetriEngine::PQL::SubtractExpr *element) override {} |
1131 | + |
1132 | + void _accept(const PetriEngine::PQL::IdentifierExpr *element) override {} |
1133 | + |
1134 | + private: |
1135 | + bool _bad = false; |
1136 | + |
1137 | + void setBad() { _bad = true; } |
1138 | + }; |
1139 | +} |
1140 | +#endif //VERIFYPN_LTLVALIDATOR_H |
1141 | |
1142 | === added file 'include/LTL/ProductSuccessorGenerator.h' |
1143 | --- include/LTL/ProductSuccessorGenerator.h 1970-01-01 00:00:00 +0000 |
1144 | +++ include/LTL/ProductSuccessorGenerator.h 2021-04-02 18:07:40 +0000 |
1145 | @@ -0,0 +1,146 @@ |
1146 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
1147 | + * Simon M. Virenfeldt <simon@simwir.dk> |
1148 | + * |
1149 | + * This program is free software: you can redistribute it and/or modify |
1150 | + * it under the terms of the GNU General Public License as published by |
1151 | + * the Free Software Foundation, either version 3 of the License, or |
1152 | + * (at your option) any later version. |
1153 | + * |
1154 | + * This program is distributed in the hope that it will be useful, |
1155 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1156 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1157 | + * GNU General Public License for more details. |
1158 | + * |
1159 | + * You should have received a copy of the GNU General Public License |
1160 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1161 | + */ |
1162 | + |
1163 | +#ifndef VERIFYPN_PRODUCTSUCCESSORGENERATOR_H |
1164 | +#define VERIFYPN_PRODUCTSUCCESSORGENERATOR_H |
1165 | + |
1166 | +#include "PetriEngine/SuccessorGenerator.h" |
1167 | +#include "PetriEngine/PQL/PQL.h" |
1168 | +#include "LTL/Structures/ProductState.h" |
1169 | +#include "LTL/BuchiSuccessorGenerator.h" |
1170 | +#include "LTL/LTLToBuchi.h" |
1171 | + |
1172 | + |
1173 | +namespace LTL { |
1174 | + /** |
1175 | + * type holding sufficient information to resume successor generation for a state from a given point. |
1176 | + */ |
1177 | + struct successor_info { |
1178 | + uint32_t pcounter; |
1179 | + uint32_t tcounter; |
1180 | + size_t buchi_state; |
1181 | + size_t last_state; |
1182 | + |
1183 | + friend bool operator==(const successor_info &lhs, const successor_info &rhs) { |
1184 | + return lhs.pcounter == rhs.pcounter && |
1185 | + lhs.tcounter == rhs.tcounter && |
1186 | + lhs.buchi_state == rhs.buchi_state && |
1187 | + lhs.last_state == rhs.last_state; |
1188 | + } |
1189 | + |
1190 | + friend bool operator!=(const successor_info &lhs, const successor_info &rhs) { |
1191 | + return !(rhs == lhs); |
1192 | + } |
1193 | + |
1194 | + inline bool has_pcounter() const { |
1195 | + return pcounter != NoPCounter; |
1196 | + } |
1197 | + |
1198 | + inline bool has_tcounter() const { |
1199 | + return tcounter != NoTCounter; |
1200 | + } |
1201 | + |
1202 | + inline bool has_buchistate() const { |
1203 | + return buchi_state != NoBuchiState; |
1204 | + } |
1205 | + |
1206 | + inline bool has_prev_state() const { |
1207 | + return last_state != NoLastState; |
1208 | + } |
1209 | + |
1210 | + static constexpr auto NoPCounter = 0; |
1211 | + static constexpr auto NoTCounter = std::numeric_limits<uint32_t>::max(); |
1212 | + static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max(); |
1213 | + static constexpr auto NoLastState = std::numeric_limits<size_t>::max(); |
1214 | + }; |
1215 | + |
1216 | + constexpr successor_info initial_suc_info{ |
1217 | + successor_info::NoPCounter, |
1218 | + successor_info::NoTCounter, |
1219 | + successor_info::NoBuchiState, |
1220 | + successor_info::NoLastState |
1221 | + }; |
1222 | + |
1223 | + class ProductSuccessorGenerator : public PetriEngine::SuccessorGenerator { |
1224 | + public: |
1225 | + |
1226 | + ProductSuccessorGenerator(const PetriEngine::PetriNet &net, |
1227 | + const PetriEngine::PQL::Condition_ptr &cond) |
1228 | + : PetriEngine::SuccessorGenerator(net), buchi(makeBuchiAutomaton(cond)) {} |
1229 | + |
1230 | + [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); }; |
1231 | + |
1232 | + void prepare(const LTL::Structures::ProductState *state); |
1233 | + |
1234 | + bool next(LTL::Structures::ProductState &state); |
1235 | + |
1236 | + bool isAccepting(const LTL::Structures::ProductState &state); |
1237 | + |
1238 | + void makeInitialState(std::vector<LTL::Structures::ProductState> &states) { |
1239 | + auto buf = new PetriEngine::MarkVal[_net.numberOfPlaces() + 1]; |
1240 | + std::copy(_net.initial(), _net.initial() + _net.numberOfPlaces(), buf); |
1241 | + buf[_net.numberOfPlaces()] = 0; |
1242 | + LTL::Structures::ProductState state; |
1243 | + state.setMarking(buf, _net.numberOfPlaces()); |
1244 | + state.setBuchiState(initial_buchi_state()); |
1245 | + buchi.prepare(state.getBuchiState()); |
1246 | + while (next_buchi_succ(state)) { |
1247 | + states.emplace_back(); |
1248 | + states.back().setMarking(new PetriEngine::MarkVal[_net.numberOfPlaces() + 1], _net.numberOfPlaces()); |
1249 | + std::copy(state.marking(), state.marking() + _net.numberOfPlaces(), states.back().marking()); |
1250 | + states.back().setBuchiState(state.getBuchiState()); |
1251 | + } |
1252 | + } |
1253 | + |
1254 | + [[nodiscard]] bool isInitialState(const LTL::Structures::ProductState &state) const { |
1255 | + return state.markingEqual(_net.initial()); |
1256 | + } |
1257 | + |
1258 | + /** |
1259 | + * prepare a state for successor generation, starting from specific point in iteration |
1260 | + * @param state the source state to generate successors from |
1261 | + * @param sucinfo the point in the iteration to start from, as returned by `next`. |
1262 | + */ |
1263 | + void prepare(const LTL::Structures::ProductState *state, const successor_info &sucinfo); |
1264 | + |
1265 | + /** |
1266 | + * compute the next successor from the last state that was sent to `prepare`. |
1267 | + * @param[out] state the state to write |
1268 | + * @param[out] sucinfo checkpoint information from which iteration can later be resumed. |
1269 | + * @return `true` if a successor was successfully generated, `false` otherwise. |
1270 | + * @warning do not use the same State for both prepare and next, this will cause wildly incorrect behaviour! |
1271 | + */ |
1272 | + bool next(Structures::ProductState &state, successor_info &sucinfo); |
1273 | + |
1274 | + [[nodiscard]] bool is_weak() const { |
1275 | + return buchi.is_weak(); |
1276 | + } |
1277 | + |
1278 | + private: |
1279 | + BuchiSuccessorGenerator buchi; |
1280 | + bdd cond; |
1281 | + size_t buchi_parent; |
1282 | + bool fresh_marking = true; |
1283 | + |
1284 | + bool guard_valid(const PetriEngine::Structures::State &state, bdd bdd); |
1285 | + |
1286 | + bool next_buchi_succ(LTL::Structures::ProductState &state); |
1287 | + }; |
1288 | + |
1289 | +} |
1290 | + |
1291 | +#endif //VERIFYPN_PRODUCTSUCCESSORGENERATOR_H |
1292 | |
1293 | === added directory 'include/LTL/Simplification' |
1294 | === added file 'include/LTL/Simplification/SpotToPQL.h' |
1295 | --- include/LTL/Simplification/SpotToPQL.h 1970-01-01 00:00:00 +0000 |
1296 | +++ include/LTL/Simplification/SpotToPQL.h 2021-04-02 18:07:40 +0000 |
1297 | @@ -0,0 +1,42 @@ |
1298 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
1299 | + * Simon M. Virenfeldt <simon@simwir.dk> |
1300 | + * |
1301 | + * This program is free software: you can redistribute it and/or modify |
1302 | + * it under the terms of the GNU General Public License as published by |
1303 | + * the Free Software Foundation, either version 3 of the License, or |
1304 | + * (at your option) any later version. |
1305 | + * |
1306 | + * This program is distributed in the hope that it will be useful, |
1307 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1308 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1309 | + * GNU General Public License for more details. |
1310 | + * |
1311 | + * You should have received a copy of the GNU General Public License |
1312 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1313 | + */ |
1314 | + |
1315 | +#ifndef VERIFYPN_SPOTTOPQL_H |
1316 | +#define VERIFYPN_SPOTTOPQL_H |
1317 | + |
1318 | +#include "PetriEngine/PQL/Expressions.h" |
1319 | +#include "LTL/LTLToBuchi.h" |
1320 | +#include <spot/tl/formula.hh> |
1321 | + |
1322 | +namespace LTL { |
1323 | + /** |
1324 | + * Transform a Spot formula back into the PQL expression tree form. |
1325 | + * @param formula The formula to translate to PQL |
1326 | + * @param apinfo List of atomic propositions in the formula. This should have been created by {@link LTL::to_spot_formula}. |
1327 | + * @return A PQL formula equivalent to the passed spot formula. |
1328 | + */ |
1329 | + PetriEngine::PQL::Condition_ptr toPQL(const spot::formula &formula, const APInfo &apinfo); |
1330 | + |
1331 | + /** |
1332 | + * Simplify an LTL formula using Spot's formula simplifier. Throws if formula is not valid LTL. |
1333 | + * @param formula The formula to simplify. |
1334 | + * @return the simplified formula. |
1335 | + */ |
1336 | + PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula); |
1337 | +} |
1338 | + |
1339 | +#endif // VERIFYPN_SPOTTOPQL_H |
1340 | |
1341 | === added directory 'include/LTL/Structures' |
1342 | === added file 'include/LTL/Structures/BuchiAutomaton.h' |
1343 | --- include/LTL/Structures/BuchiAutomaton.h 1970-01-01 00:00:00 +0000 |
1344 | +++ include/LTL/Structures/BuchiAutomaton.h 2021-04-02 18:07:40 +0000 |
1345 | @@ -0,0 +1,31 @@ |
1346 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
1347 | + * Simon M. Virenfeldt <simon@simwir.dk> |
1348 | + * |
1349 | + * This program is free software: you can redistribute it and/or modify |
1350 | + * it under the terms of the GNU General Public License as published by |
1351 | + * the Free Software Foundation, either version 3 of the License, or |
1352 | + * (at your option) any later version. |
1353 | + * |
1354 | + * This program is distributed in the hope that it will be useful, |
1355 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1356 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1357 | + * GNU General Public License for more details. |
1358 | + * |
1359 | + * You should have received a copy of the GNU General Public License |
1360 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1361 | + */ |
1362 | + |
1363 | +#ifndef VERIFYPN_BUCHIAUTOMATON_H |
1364 | +#define VERIFYPN_BUCHIAUTOMATON_H |
1365 | + |
1366 | +#include "LTL/LTLToBuchi.h" |
1367 | +#include <spot/twa/twagraph.hh> |
1368 | + |
1369 | +namespace LTL::Structures { |
1370 | + struct BuchiAutomaton { |
1371 | + spot::twa_graph_ptr buchi; |
1372 | + const std::unordered_map<int, AtomicProposition> ap_info; |
1373 | + }; |
1374 | +} |
1375 | + |
1376 | +#endif //VERIFYPN_BUCHIAUTOMATON_H |
1377 | |
1378 | === added file 'include/LTL/Structures/ProductState.h' |
1379 | --- include/LTL/Structures/ProductState.h 1970-01-01 00:00:00 +0000 |
1380 | +++ include/LTL/Structures/ProductState.h 2021-04-02 18:07:40 +0000 |
1381 | @@ -0,0 +1,81 @@ |
1382 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
1383 | + * Simon M. Virenfeldt <simon@simwir.dk> |
1384 | + * |
1385 | + * This program is free software: you can redistribute it and/or modify |
1386 | + * it under the terms of the GNU General Public License as published by |
1387 | + * the Free Software Foundation, either version 3 of the License, or |
1388 | + * (at your option) any later version. |
1389 | + * |
1390 | + * This program is distributed in the hope that it will be useful, |
1391 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1392 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1393 | + * GNU General Public License for more details. |
1394 | + * |
1395 | + * You should have received a copy of the GNU General Public License |
1396 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1397 | + */ |
1398 | + |
1399 | +#ifndef VERIFYPN_PRODUCTSTATE_H |
1400 | +#define VERIFYPN_PRODUCTSTATE_H |
1401 | + |
1402 | +#include "PetriEngine/Structures/State.h" |
1403 | + |
1404 | +namespace LTL { |
1405 | + class ProductSuccessorGenerator; |
1406 | +} |
1407 | +namespace LTL::Structures { |
1408 | + /** |
1409 | + * State on the form (M, q) for marking M and NBA state q. |
1410 | + * Represented as array of size nplaces + 1, where the last element is the number |
1411 | + * of NBA state q, and the first nplaces elements are the actual marking. |
1412 | + */ |
1413 | + class ProductState : public PetriEngine::Structures::State { |
1414 | + public: |
1415 | + ProductState() : PetriEngine::Structures::State() {} |
1416 | + |
1417 | + void setMarking(PetriEngine::MarkVal* marking, size_t nplaces) |
1418 | + { |
1419 | + State::setMarking(marking); |
1420 | + // because zero-indexing |
1421 | + buchi_state_idx = nplaces; |
1422 | + } |
1423 | + |
1424 | + //TODO override equality operators to handle both marking and NBA state |
1425 | + size_t getBuchiState() const { |
1426 | + return marking()[buchi_state_idx]; |
1427 | + } |
1428 | + |
1429 | + void setBuchiState(size_t state) { |
1430 | + marking()[buchi_state_idx] = state; |
1431 | + } |
1432 | + |
1433 | + [[nodiscard]] bool markingEqual(const PetriEngine::MarkVal *rhs) const { |
1434 | + for (size_t i = 0; i < buchi_state_idx; ++i) { |
1435 | + if (marking()[i] != rhs[i]) { |
1436 | + return false; |
1437 | + } |
1438 | + } |
1439 | + return true; |
1440 | + } |
1441 | + |
1442 | + bool operator==(const ProductState &rhs) const { |
1443 | + for (size_t i = 0; i <= buchi_state_idx; ++i) { |
1444 | + if (marking()[i] != rhs.marking()[i]) { |
1445 | + return false; |
1446 | + } |
1447 | + } |
1448 | + return true; |
1449 | + } |
1450 | + |
1451 | + size_t size() const { return buchi_state_idx + 1; } |
1452 | + |
1453 | + bool operator!=(const ProductState &rhs) const { |
1454 | + return !(rhs == *this); |
1455 | + } |
1456 | + private: |
1457 | + friend class LTL::ProductSuccessorGenerator; |
1458 | + size_t buchi_state_idx; |
1459 | + }; |
1460 | +} |
1461 | + |
1462 | +#endif //VERIFYPN_PRODUCTSTATE_H |
1463 | |
1464 | === added file 'include/LTL/Structures/ProductStateFactory.h' |
1465 | --- include/LTL/Structures/ProductStateFactory.h 1970-01-01 00:00:00 +0000 |
1466 | +++ include/LTL/Structures/ProductStateFactory.h 2021-04-02 18:07:40 +0000 |
1467 | @@ -0,0 +1,46 @@ |
1468 | +/* Copyright (C) 2020 Nikolaj J. Ulrik <nikolaj@njulrik.dk>, |
1469 | + * Simon M. Virenfeldt <simon@simwir.dk> |
1470 | + * |
1471 | + * This program is free software: you can redistribute it and/or modify |
1472 | + * it under the terms of the GNU General Public License as published by |
1473 | + * the Free Software Foundation, either version 3 of the License, or |
1474 | + * (at your option) any later version. |
1475 | + * |
1476 | + * This program is distributed in the hope that it will be useful, |
1477 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1478 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1479 | + * GNU General Public License for more details. |
1480 | + * |
1481 | + * You should have received a copy of the GNU General Public License |
1482 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1483 | + */ |
1484 | + |
1485 | +#ifndef VERIFYPN_PRODUCTSTATEFACTORY_H |
1486 | +#define VERIFYPN_PRODUCTSTATEFACTORY_H |
1487 | + |
1488 | +#include "LTL/Structures/ProductState.h" |
1489 | + |
1490 | +#include <memory> |
1491 | + |
1492 | +namespace LTL::Structures{ |
1493 | + class ProductStateFactory { |
1494 | + public: |
1495 | + ProductStateFactory(const PetriEngine::PetriNet &net, size_t initial_buchi_state) |
1496 | + : net(net), buchi_init(initial_buchi_state) {} |
1497 | + |
1498 | + ProductState newState() { |
1499 | + auto buf = new PetriEngine::MarkVal[net.numberOfPlaces()+1]; |
1500 | + std::copy(net.initial(), net.initial() + net.numberOfPlaces(), buf); |
1501 | + buf[net.numberOfPlaces()] = 0; |
1502 | + ProductState state; |
1503 | + state.setMarking(buf, net.numberOfPlaces()); |
1504 | + state.setBuchiState(buchi_init); |
1505 | + return state; |
1506 | + } |
1507 | + |
1508 | + private: |
1509 | + const PetriEngine::PetriNet &net; |
1510 | + const size_t buchi_init; |
1511 | + }; |
1512 | +} |
1513 | +#endif //VERIFYPN_PRODUCTSTATEFACTORY_H |
1514 | |
1515 | === added file 'include/PetriEngine/Colored/ArcIntervals.h' |
1516 | --- include/PetriEngine/Colored/ArcIntervals.h 1970-01-01 00:00:00 +0000 |
1517 | +++ include/PetriEngine/Colored/ArcIntervals.h 2021-04-02 18:07:40 +0000 |
1518 | @@ -0,0 +1,108 @@ |
1519 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
1520 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
1521 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
1522 | + * |
1523 | + * This program is free software: you can redistribute it and/or modify |
1524 | + * it under the terms of the GNU General Public License as published by |
1525 | + * the Free Software Foundation, either version 3 of the License, or |
1526 | + * (at your option) any later version. |
1527 | + * |
1528 | + * This program is distributed in the hope that it will be useful, |
1529 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1530 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1531 | + * GNU General Public License for more details. |
1532 | + * |
1533 | + * You should have received a copy of the GNU General Public License |
1534 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1535 | + */ |
1536 | + |
1537 | +#ifndef ARCINTERVALS_H |
1538 | +#define ARCINTERVALS_H |
1539 | + |
1540 | +#include "Colors.h" |
1541 | + |
1542 | +namespace PetriEngine { |
1543 | + namespace Colored { |
1544 | + |
1545 | + struct ArcIntervals { |
1546 | + std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> _varIndexModMap; |
1547 | + std::vector<Colored::intervalTuple_t> _intervalTupleVec; |
1548 | + Colored::ColorFixpoint * _source; |
1549 | + |
1550 | + ~ArcIntervals() {_varIndexModMap.clear();} |
1551 | + ArcIntervals() { |
1552 | + } |
1553 | + |
1554 | + ArcIntervals(Colored::ColorFixpoint * source) : _source(source){ |
1555 | + } |
1556 | + |
1557 | + ArcIntervals(Colored::ColorFixpoint * source, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varIndexModMap) : _varIndexModMap(varIndexModMap), _source(source) { |
1558 | + }; |
1559 | + |
1560 | + ArcIntervals(Colored::ColorFixpoint * source, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varIndexModMap, std::vector<Colored::intervalTuple_t> ranges) : _varIndexModMap(varIndexModMap), _intervalTupleVec(ranges), _source(source) { |
1561 | + }; |
1562 | + |
1563 | + size_t size() { |
1564 | + return _intervalTupleVec.size(); |
1565 | + } |
1566 | + |
1567 | + Colored::intervalTuple_t& operator[] (size_t index) { |
1568 | + return _intervalTupleVec[index]; |
1569 | + } |
1570 | + |
1571 | + Colored::intervalTuple_t& operator[] (int index) { |
1572 | + return _intervalTupleVec[index]; |
1573 | + } |
1574 | + |
1575 | + Colored::intervalTuple_t& operator[] (uint32_t index) { |
1576 | + assert(index < _intervalTupleVec.size()); |
1577 | + return _intervalTupleVec[index]; |
1578 | + } |
1579 | + |
1580 | + Colored::intervalTuple_t& back(){ |
1581 | + return _intervalTupleVec.back(); |
1582 | + } |
1583 | + |
1584 | + bool hasValidIntervals(){ |
1585 | + for(auto intervalTuple : _intervalTupleVec){ |
1586 | + if (intervalTuple.hasValidIntervals()){ |
1587 | + return true; |
1588 | + } |
1589 | + } |
1590 | + return false; |
1591 | + } |
1592 | + |
1593 | + bool containsVariable(Colored::Variable * var){ |
1594 | + for (auto varModPair : _varIndexModMap){ |
1595 | + if(varModPair.first == var){ |
1596 | + return true; |
1597 | + } |
1598 | + } |
1599 | + return false; |
1600 | + } |
1601 | + |
1602 | + std::set<const Colored::Variable *> getVariables(){ |
1603 | + std::set<const Colored::Variable *> res; |
1604 | + for (auto varModPair : _varIndexModMap){ |
1605 | + res.insert(varModPair.first); |
1606 | + } |
1607 | + return res; |
1608 | + } |
1609 | + |
1610 | + void print() { |
1611 | + std::cout << "[ "; |
1612 | + for(auto varModifierPair : _varIndexModMap){ |
1613 | + std::cout << "(" << varModifierPair.first->name << ", " << varModifierPair.first->colorType->productSize() << ") "; |
1614 | + } |
1615 | + std::cout << "]" << std::endl; |
1616 | + for(auto intervalTuple: _intervalTupleVec){ |
1617 | + std::cout << "--------------------------------------------------------------------" << std::endl; |
1618 | + intervalTuple.print(); |
1619 | + std::cout << "--------------------------------------------------------------------" << std::endl; |
1620 | + } |
1621 | + } |
1622 | + }; |
1623 | + } |
1624 | +} |
1625 | + |
1626 | +#endif /* INTERVALGENERATOR_H */ |
1627 | \ No newline at end of file |
1628 | |
1629 | === added file 'include/PetriEngine/Colored/BindingGenerator.h' |
1630 | --- include/PetriEngine/Colored/BindingGenerator.h 1970-01-01 00:00:00 +0000 |
1631 | +++ include/PetriEngine/Colored/BindingGenerator.h 2021-04-02 18:07:40 +0000 |
1632 | @@ -0,0 +1,71 @@ |
1633 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
1634 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
1635 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
1636 | + * Andreas H. Klostergaard |
1637 | + * |
1638 | + * This program is free software: you can redistribute it and/or modify |
1639 | + * it under the terms of the GNU General Public License as published by |
1640 | + * the Free Software Foundation, either version 3 of the License, or |
1641 | + * (at your option) any later version. |
1642 | + * |
1643 | + * This program is distributed in the hope that it will be useful, |
1644 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1645 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1646 | + * GNU General Public License for more details. |
1647 | + * |
1648 | + * You should have received a copy of the GNU General Public License |
1649 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1650 | + */ |
1651 | + |
1652 | +#include <vector> |
1653 | +#include <unordered_map> |
1654 | + |
1655 | +#include "ColoredNetStructures.h" |
1656 | + |
1657 | +namespace PetriEngine { |
1658 | + |
1659 | + typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap; |
1660 | + |
1661 | + class FixpointBindingGenerator { |
1662 | + public: |
1663 | + class Iterator { |
1664 | + private: |
1665 | + FixpointBindingGenerator* _generator; |
1666 | + |
1667 | + public: |
1668 | + Iterator(FixpointBindingGenerator* generator); |
1669 | + |
1670 | + bool operator==(Iterator& other); |
1671 | + bool operator!=(Iterator& other); |
1672 | + Iterator& operator++(); |
1673 | + const Colored::ExpressionContext::BindingMap operator++(int); |
1674 | + Colored::ExpressionContext::BindingMap& operator*(); |
1675 | + }; |
1676 | + private: |
1677 | + Colored::GuardExpression_ptr _expr; |
1678 | + Colored::ExpressionContext::BindingMap _bindings; |
1679 | + ColorTypeMap& _colorTypes; |
1680 | + Colored::Transition &_transition; |
1681 | + bool _isDone; |
1682 | + bool _noValidBindings; |
1683 | + uint32_t _nextIndex = 0; |
1684 | + |
1685 | + bool eval(); |
1686 | + |
1687 | + public: |
1688 | + FixpointBindingGenerator(Colored::Transition& transition, |
1689 | + ColorTypeMap& colorTypes); |
1690 | + |
1691 | + FixpointBindingGenerator(const FixpointBindingGenerator& ) = default; |
1692 | + |
1693 | + FixpointBindingGenerator operator= (const FixpointBindingGenerator& b) { |
1694 | + return FixpointBindingGenerator(b); |
1695 | + } |
1696 | + |
1697 | + Colored::ExpressionContext::BindingMap& nextBinding(); |
1698 | + Colored::ExpressionContext::BindingMap& currentBinding(); |
1699 | + bool isInitial() const; |
1700 | + Iterator begin(); |
1701 | + Iterator end(); |
1702 | + }; |
1703 | +} |
1704 | \ No newline at end of file |
1705 | |
1706 | === modified file 'include/PetriEngine/Colored/ColoredNetStructures.h' |
1707 | --- include/PetriEngine/Colored/ColoredNetStructures.h 2020-03-02 21:03:24 +0000 |
1708 | +++ include/PetriEngine/Colored/ColoredNetStructures.h 2021-04-02 18:07:40 +0000 |
1709 | @@ -1,14 +1,20 @@ |
1710 | -/* |
1711 | - * To change this license header, choose License Headers in Project Properties. |
1712 | - * To change this template file, choose Tools | Templates |
1713 | - * and open the template in the editor. |
1714 | - */ |
1715 | - |
1716 | -/* |
1717 | - * File: ColoredNetStructures.h |
1718 | - * Author: Klostergaard |
1719 | - * |
1720 | - * Created on 17. februar 2018, 17:07 |
1721 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
1722 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
1723 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
1724 | + * Andreas H. Klostergaard |
1725 | + * |
1726 | + * This program is free software: you can redistribute it and/or modify |
1727 | + * it under the terms of the GNU General Public License as published by |
1728 | + * the Free Software Foundation, either version 3 of the License, or |
1729 | + * (at your option) any later version. |
1730 | + * |
1731 | + * This program is distributed in the hope that it will be useful, |
1732 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1733 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1734 | + * GNU General Public License for more details. |
1735 | + * |
1736 | + * You should have received a copy of the GNU General Public License |
1737 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1738 | */ |
1739 | |
1740 | #ifndef COLOREDNETSTRUCTURES_H |
1741 | @@ -16,6 +22,7 @@ |
1742 | |
1743 | #include <vector> |
1744 | #include <set> |
1745 | +#include <assert.h> |
1746 | #include "Colors.h" |
1747 | #include "Expressions.h" |
1748 | #include "Multiset.h" |
1749 | @@ -33,7 +40,10 @@ |
1750 | struct Transition { |
1751 | std::string name; |
1752 | GuardExpression_ptr guard; |
1753 | - std::vector<Arc> arcs; |
1754 | + std::vector<Arc> input_arcs; |
1755 | + std::vector<Arc> output_arcs; |
1756 | + std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> variableMaps; |
1757 | + bool considered; |
1758 | }; |
1759 | |
1760 | struct Place { |
1761 | |
1762 | === modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h' |
1763 | --- include/PetriEngine/Colored/ColoredPetriNetBuilder.h 2020-03-02 21:03:24 +0000 |
1764 | +++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h 2021-04-02 18:07:40 +0000 |
1765 | @@ -1,8 +1,20 @@ |
1766 | -/* |
1767 | - * File: ColoredPetriNetBuilder.h |
1768 | - * Author: Klostergaard |
1769 | - * |
1770 | - * Created on 17. februar 2018, 16:25 |
1771 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
1772 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
1773 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
1774 | + * Andreas H. Klostergaard |
1775 | + * |
1776 | + * This program is free software: you can redistribute it and/or modify |
1777 | + * it under the terms of the GNU General Public License as published by |
1778 | + * the Free Software Foundation, either version 3 of the License, or |
1779 | + * (at your option) any later version. |
1780 | + * |
1781 | + * This program is distributed in the hope that it will be useful, |
1782 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1783 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1784 | + * GNU General Public License for more details. |
1785 | + * |
1786 | + * You should have received a copy of the GNU General Public License |
1787 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1788 | */ |
1789 | |
1790 | #ifndef COLOREDPETRINETBUILDER_H |
1791 | @@ -11,14 +23,16 @@ |
1792 | #include <vector> |
1793 | #include <unordered_map> |
1794 | |
1795 | -#include "ColoredNetStructures.h" |
1796 | #include "../AbstractPetriNetBuilder.h" |
1797 | #include "../PetriNetBuilder.h" |
1798 | +#include "BindingGenerator.h" |
1799 | +#include "IntervalGenerator.h" |
1800 | +#include "ArcIntervals.h" |
1801 | |
1802 | namespace PetriEngine { |
1803 | + |
1804 | class ColoredPetriNetBuilder : public AbstractPetriNetBuilder { |
1805 | public: |
1806 | - typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap; |
1807 | typedef std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>> PTPlaceMap; |
1808 | typedef std::unordered_map<std::string, std::vector<std::string>> PTTransitionMap; |
1809 | |
1810 | @@ -66,10 +80,18 @@ |
1811 | return _time; |
1812 | } |
1813 | |
1814 | + double getFixpointTime() const { |
1815 | + return _fixPointCreationTime; |
1816 | + } |
1817 | + |
1818 | uint32_t getPlaceCount() const { |
1819 | return _places.size(); |
1820 | } |
1821 | |
1822 | + uint32_t getMaxIntervals() const { |
1823 | + return _maxIntervals; |
1824 | + } |
1825 | + |
1826 | uint32_t getTransitionCount() const { |
1827 | return _transitions.size(); |
1828 | } |
1829 | @@ -77,7 +99,8 @@ |
1830 | uint32_t getArcCount() const { |
1831 | uint32_t sum = 0; |
1832 | for (auto& t : _transitions) { |
1833 | - sum += t.arcs.size(); |
1834 | + sum += t.input_arcs.size(); |
1835 | + sum += t.output_arcs.size(); |
1836 | } |
1837 | return sum; |
1838 | } |
1839 | @@ -109,71 +132,69 @@ |
1840 | |
1841 | PetriNetBuilder& unfold(); |
1842 | PetriNetBuilder& stripColors(); |
1843 | + void computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout); |
1844 | + |
1845 | private: |
1846 | std::unordered_map<std::string,uint32_t> _placenames; |
1847 | std::unordered_map<std::string,uint32_t> _transitionnames; |
1848 | + std::unordered_map<uint32_t, std::unordered_map<uint32_t, Colored::ArcIntervals>> _arcIntervals; |
1849 | + std::unordered_map<uint32_t,std::vector<uint32_t>> _placePostTransitionMap; |
1850 | + std::unordered_map<uint32_t,FixpointBindingGenerator> _bindings; |
1851 | PTPlaceMap _ptplacenames; |
1852 | PTTransitionMap _pttransitionnames; |
1853 | uint32_t _nptplaces = 0; |
1854 | uint32_t _npttransitions = 0; |
1855 | uint32_t _nptarcs = 0; |
1856 | + uint32_t _maxIntervals = 0; |
1857 | + PetriEngine::IntervalGenerator intervalGenerator; |
1858 | |
1859 | std::vector<Colored::Place> _places; |
1860 | std::vector<Colored::Transition> _transitions; |
1861 | std::vector<Colored::Arc> _arcs; |
1862 | + std::vector<Colored::ColorFixpoint> _placeColorFixpoints; |
1863 | ColorTypeMap _colors; |
1864 | PetriNetBuilder _ptBuilder; |
1865 | bool _unfolded = false; |
1866 | bool _stripped = false; |
1867 | |
1868 | + std::vector<uint32_t> _placeFixpointQueue; |
1869 | + |
1870 | double _time; |
1871 | + double _fixPointCreationTime; |
1872 | + |
1873 | + double _timer; |
1874 | |
1875 | std::string arcToString(Colored::Arc& arc) const ; |
1876 | + |
1877 | + void printPlaceTable(); |
1878 | + |
1879 | + std::unordered_map<uint32_t, Colored::ArcIntervals> setupTransitionVars(Colored::Transition transition); |
1880 | |
1881 | void addArc(const std::string& place, |
1882 | const std::string& transition, |
1883 | const Colored::ArcExpression_ptr& expr, |
1884 | bool input); |
1885 | + |
1886 | + |
1887 | + void getArcIntervals(Colored::Transition& transition, bool &transitionActivated, uint32_t max_intervals, uint32_t transitionId); |
1888 | + void processInputArcs(Colored::Transition& transition, uint32_t currentPlaceId, uint32_t transitionId, bool &transitionActivated, uint32_t max_intervals); |
1889 | + void processOutputArcs(Colored::Transition& transition); |
1890 | |
1891 | - void unfoldPlace(Colored::Place& place); |
1892 | + void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color); |
1893 | void unfoldTransition(Colored::Transition& transition); |
1894 | - void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name); |
1895 | + void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap); |
1896 | + |
1897 | + void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name, bool input); |
1898 | }; |
1899 | |
1900 | - class BindingGenerator { |
1901 | - public: |
1902 | - class Iterator { |
1903 | - private: |
1904 | - BindingGenerator* _generator; |
1905 | - |
1906 | - public: |
1907 | - Iterator(BindingGenerator* generator); |
1908 | - |
1909 | - bool operator==(Iterator& other); |
1910 | - bool operator!=(Iterator& other); |
1911 | - Iterator& operator++(); |
1912 | - const Colored::ExpressionContext::BindingMap operator++(int); |
1913 | - Colored::ExpressionContext::BindingMap& operator*(); |
1914 | - }; |
1915 | - private: |
1916 | - Colored::GuardExpression_ptr _expr; |
1917 | - Colored::ExpressionContext::BindingMap _bindings; |
1918 | - ColoredPetriNetBuilder::ColorTypeMap& _colorTypes; |
1919 | - |
1920 | - bool eval(); |
1921 | - |
1922 | - public: |
1923 | - BindingGenerator(Colored::Transition& transition, |
1924 | - const std::vector<Colored::Arc>& arcs, |
1925 | - ColoredPetriNetBuilder::ColorTypeMap& colorTypes); |
1926 | + //Used for checking if a variable is inside either a succ or pred expression |
1927 | + enum ExpressionType { |
1928 | + None, |
1929 | + Pred, |
1930 | + Succ |
1931 | + }; |
1932 | + |
1933 | |
1934 | - Colored::ExpressionContext::BindingMap& nextBinding(); |
1935 | - Colored::ExpressionContext::BindingMap& currentBinding(); |
1936 | - bool isInitial() const; |
1937 | - Iterator begin(); |
1938 | - Iterator end(); |
1939 | - }; |
1940 | } |
1941 | |
1942 | #endif /* COLOREDPETRINETBUILDER_H */ |
1943 | - |
1944 | |
1945 | === modified file 'include/PetriEngine/Colored/Colors.h' |
1946 | --- include/PetriEngine/Colored/Colors.h 2020-03-02 22:05:53 +0000 |
1947 | +++ include/PetriEngine/Colored/Colors.h 2021-04-02 18:07:40 +0000 |
1948 | @@ -1,14 +1,20 @@ |
1949 | -/* |
1950 | - * To change this license header, choose License Headers in Project Properties. |
1951 | - * To change this template file, choose Tools | Templates |
1952 | - * and open the template in the editor. |
1953 | - */ |
1954 | - |
1955 | -/* |
1956 | - * File: Colors.h |
1957 | - * Author: andreas |
1958 | - * |
1959 | - * Created on February 19, 2018, 8:22 PM |
1960 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
1961 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
1962 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
1963 | + * Andreas H. Klostergaard |
1964 | + * |
1965 | + * This program is free software: you can redistribute it and/or modify |
1966 | + * it under the terms of the GNU General Public License as published by |
1967 | + * the Free Software Foundation, either version 3 of the License, or |
1968 | + * (at your option) any later version. |
1969 | + * |
1970 | + * This program is distributed in the hope that it will be useful, |
1971 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
1972 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
1973 | + * GNU General Public License for more details. |
1974 | + * |
1975 | + * You should have received a copy of the GNU General Public License |
1976 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
1977 | */ |
1978 | |
1979 | #ifndef COLORS_H |
1980 | @@ -21,6 +27,10 @@ |
1981 | #include <utility> |
1982 | #include <vector> |
1983 | #include <unordered_map> |
1984 | +#include <iostream> |
1985 | +#include <cassert> |
1986 | + |
1987 | +#include "Intervals.h" |
1988 | |
1989 | namespace PetriEngine { |
1990 | namespace Colored { |
1991 | @@ -44,7 +54,15 @@ |
1992 | bool isTuple() const { |
1993 | return _tuple.size() > 1; |
1994 | } |
1995 | + |
1996 | + void getColorConstraints(Colored::interval_t *constraintsVector, uint32_t *index) const; |
1997 | |
1998 | + std::vector<const Color*> getTupleColors() const { |
1999 | + return _tuple; |
2000 | + } |
2001 | + |
2002 | + void getTupleId(std::vector<uint32_t> *idVector) const; |
2003 | + |
2004 | const std::string& getColorName() const { |
2005 | if (this->isTuple()) { |
2006 | throw "Cannot get color from a tuple color."; |
2007 | @@ -90,9 +108,11 @@ |
2008 | DotConstant(); |
2009 | |
2010 | public: |
2011 | - static const Color* dotConstant() { |
2012 | + static const Color* dotConstant(ColorType *ct) { |
2013 | static DotConstant _instance; |
2014 | - |
2015 | + if(ct != nullptr){ |
2016 | + _instance._colorType = ct; |
2017 | + } |
2018 | return &_instance; |
2019 | } |
2020 | |
2021 | @@ -160,12 +180,33 @@ |
2022 | virtual void addColor(const char* colorName); |
2023 | virtual void addColor(std::vector<const Color*>& colors); |
2024 | virtual void addDot() { |
2025 | - _colors.push_back(*DotConstant::dotConstant()); |
2026 | + _colors.push_back(*DotConstant::dotConstant(this)); |
2027 | } |
2028 | |
2029 | virtual size_t size() const { |
2030 | return _colors.size(); |
2031 | } |
2032 | + |
2033 | + virtual size_t productSize() { |
2034 | + return 1; |
2035 | + } |
2036 | + |
2037 | + virtual std::vector<size_t> getConstituentsSizes(){ |
2038 | + std::vector<size_t> result; |
2039 | + result.push_back(_colors.size()); |
2040 | + |
2041 | + return result; |
2042 | + } |
2043 | + |
2044 | + virtual Colored::interval_t getFullInterval(){ |
2045 | + Colored::interval_t interval; |
2046 | + interval.addRange(Reachability::range_t(0, size()-1)); |
2047 | + return interval; |
2048 | + } |
2049 | + |
2050 | + virtual void getColortypes(std::vector<ColorType *> &colorTypes){ |
2051 | + colorTypes.push_back(this); |
2052 | + } |
2053 | |
2054 | virtual const Color& operator[] (size_t index) { |
2055 | return _colors[index]; |
2056 | @@ -176,6 +217,7 @@ |
2057 | } |
2058 | |
2059 | virtual const Color& operator[] (uint32_t index) { |
2060 | + assert(index < _colors.size()); |
2061 | return _colors[index]; |
2062 | } |
2063 | |
2064 | @@ -184,6 +226,11 @@ |
2065 | virtual const Color* operator[] (const std::string& index) { |
2066 | return (*this)[index.c_str()]; |
2067 | } |
2068 | + |
2069 | + virtual const Color* getColor(std::vector<uint32_t> ids){ |
2070 | + assert(ids.size() == 1); |
2071 | + return &_colors[ids[0]]; |
2072 | + } |
2073 | |
2074 | bool operator== (const ColorType& other) const { |
2075 | return _id == other._id; |
2076 | @@ -233,6 +280,36 @@ |
2077 | return product; |
2078 | } |
2079 | |
2080 | + virtual size_t productSize() { |
2081 | + size_t size = 0; |
2082 | + for (auto ct : constituents){ |
2083 | + size += ct->productSize(); |
2084 | + } |
2085 | + return size; |
2086 | + } |
2087 | + |
2088 | + std::vector<size_t> getConstituentsSizes() override{ |
2089 | + std::vector<size_t> result; |
2090 | + for (auto ct : constituents) { |
2091 | + result.push_back(ct->size()); |
2092 | + } |
2093 | + return result; |
2094 | + } |
2095 | + |
2096 | + Colored::interval_t getFullInterval() override{ |
2097 | + Colored::interval_t interval; |
2098 | + for(auto ct : constituents) { |
2099 | + interval.addRange(Reachability::range_t(0, ct->size()-1)); |
2100 | + } |
2101 | + return interval; |
2102 | + } |
2103 | + |
2104 | + void getColortypes(std::vector<ColorType *> &colorTypes) override{ |
2105 | + for(auto ct : constituents){ |
2106 | + ct->getColortypes(colorTypes); |
2107 | + } |
2108 | + } |
2109 | + |
2110 | bool containsTypes(const std::vector<const ColorType*>& types) const { |
2111 | if (constituents.size() != types.size()) return false; |
2112 | |
2113 | @@ -245,6 +322,19 @@ |
2114 | return true; |
2115 | } |
2116 | |
2117 | + const ColorType* getNestedColorType(size_t index) { |
2118 | + return constituents[index]; |
2119 | + } |
2120 | + |
2121 | + const Color* getColor(std::vector<uint32_t> ids){ |
2122 | + assert(ids.size() == constituents.size()); |
2123 | + std::vector<const Color *> colors; |
2124 | + for(uint32_t i = 0; i < ids.size(); i++){ |
2125 | + colors.push_back(&constituents[i]->operator[](i)); |
2126 | + } |
2127 | + return getColor(colors); |
2128 | + } |
2129 | + |
2130 | const Color* getColor(const std::vector<const Color*>& colors); |
2131 | |
2132 | const Color& operator[](size_t index) override; |
2133 | @@ -263,13 +353,29 @@ |
2134 | std::string name; |
2135 | ColorType* colorType; |
2136 | }; |
2137 | - |
2138 | - struct Binding { |
2139 | - Variable* var; |
2140 | - const Color* color; |
2141 | - |
2142 | - bool operator==(Binding& other) { |
2143 | - return var->name.compare(other.var->name); |
2144 | + |
2145 | + struct ColorFixpoint { |
2146 | + Colored::intervalTuple_t constraints; |
2147 | + bool inQueue; |
2148 | + uint32_t productSize; |
2149 | + |
2150 | + bool constainsColor(std::pair<const PetriEngine::Colored::Color *const, std::vector<uint32_t>> constPair) { |
2151 | + std::unordered_map<uint32_t, bool> contained; |
2152 | + for(auto interval : constraints._intervals) { |
2153 | + for(uint32_t id : constPair.second){ |
2154 | + |
2155 | + if(contained[id] != true){ |
2156 | + contained[id] = interval[id].contains(constPair.first->getId()); |
2157 | + } |
2158 | + } |
2159 | + } |
2160 | + |
2161 | + for(auto pair : contained){ |
2162 | + if (!pair.second){ |
2163 | + return false; |
2164 | + } |
2165 | + } |
2166 | + return true; |
2167 | } |
2168 | }; |
2169 | } |
2170 | |
2171 | === modified file 'include/PetriEngine/Colored/Expressions.h' |
2172 | --- include/PetriEngine/Colored/Expressions.h 2020-03-02 21:03:24 +0000 |
2173 | +++ include/PetriEngine/Colored/Expressions.h 2021-04-02 18:07:40 +0000 |
2174 | @@ -1,14 +1,20 @@ |
2175 | -/* |
2176 | - * To change this license header, choose License Headers in Project Properties. |
2177 | - * To change this template file, choose Tools | Templates |
2178 | - * and open the template in the editor. |
2179 | - */ |
2180 | - |
2181 | -/* |
2182 | - * File: Expressions.h |
2183 | - * Author: andreas |
2184 | - * |
2185 | - * Created on February 19, 2018, 7:00 PM |
2186 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
2187 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
2188 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
2189 | + * Andreas H. Klostergaard |
2190 | + * |
2191 | + * This program is free software: you can redistribute it and/or modify |
2192 | + * it under the terms of the GNU General Public License as published by |
2193 | + * the Free Software Foundation, either version 3 of the License, or |
2194 | + * (at your option) any later version. |
2195 | + * |
2196 | + * This program is distributed in the hope that it will be useful, |
2197 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
2198 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
2199 | + * GNU General Public License for more details. |
2200 | + * |
2201 | + * You should have received a copy of the GNU General Public License |
2202 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
2203 | */ |
2204 | |
2205 | #ifndef COLORED_EXPRESSIONS_H |
2206 | @@ -25,6 +31,8 @@ |
2207 | |
2208 | #include "Colors.h" |
2209 | #include "Multiset.h" |
2210 | +#include "ArcIntervals.h" |
2211 | +#include "GuardRestrictor.h" |
2212 | #include "../errorcodes.h" |
2213 | |
2214 | namespace PetriEngine { |
2215 | @@ -32,14 +40,14 @@ |
2216 | |
2217 | namespace Colored { |
2218 | struct ExpressionContext { |
2219 | - typedef std::unordered_map<std::string, const Color*> BindingMap; |
2220 | + typedef std::unordered_map<const Colored::Variable *, const PetriEngine::Colored::Color *> BindingMap; |
2221 | |
2222 | BindingMap& binding; |
2223 | std::unordered_map<std::string, ColorType*>& colorTypes; |
2224 | |
2225 | const Color* findColor(const std::string& color) const { |
2226 | if (color.compare("dot") == 0) |
2227 | - return DotConstant::dotConstant(); |
2228 | + return DotConstant::dotConstant(nullptr); |
2229 | for (auto& elem : colorTypes) { |
2230 | auto col = (*elem.second)[color]; |
2231 | if (col) |
2232 | @@ -74,8 +82,29 @@ |
2233 | class Expression { |
2234 | public: |
2235 | Expression() {} |
2236 | - |
2237 | - virtual void getVariables(std::set<Variable*>& variables) const { |
2238 | + |
2239 | + virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const {} |
2240 | + |
2241 | + virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap) const { |
2242 | + uint32_t index = 0; |
2243 | + getVariables(variables, varPositions, varModifierMap, &index); |
2244 | + } |
2245 | + |
2246 | + virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions) const { |
2247 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap; |
2248 | + uint32_t index = 0; |
2249 | + getVariables(variables, varPositions, varModifierMap, &index); |
2250 | + } |
2251 | + |
2252 | + virtual bool isTuple() const { |
2253 | + return false; |
2254 | + } |
2255 | + |
2256 | + virtual void getVariables(std::set<const Colored::Variable*>& variables) const { |
2257 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositions; |
2258 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap; |
2259 | + |
2260 | + getVariables(variables, varPositions, varModifierMap); |
2261 | } |
2262 | |
2263 | virtual void expressionType() { |
2264 | @@ -93,12 +122,55 @@ |
2265 | virtual ~ColorExpression() {} |
2266 | |
2267 | virtual const Color* eval(ExpressionContext& context) const = 0; |
2268 | + |
2269 | + virtual void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const = 0; |
2270 | + |
2271 | + virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const = 0; |
2272 | + |
2273 | + virtual ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const = 0; |
2274 | + |
2275 | + virtual Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const { |
2276 | + return Colored::intervalTuple_t(); |
2277 | + } |
2278 | + |
2279 | }; |
2280 | |
2281 | class DotConstantExpression : public ColorExpression { |
2282 | public: |
2283 | const Color* eval(ExpressionContext& context) const override { |
2284 | - return DotConstant::dotConstant(); |
2285 | + return DotConstant::dotConstant(nullptr); |
2286 | + } |
2287 | + |
2288 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
2289 | + if (arcIntervals._intervalTupleVec.empty()) { |
2290 | + //We can add all place tokens when considering the dot constant as, that must be present |
2291 | + arcIntervals._intervalTupleVec.push_back(cfp.constraints); |
2292 | + } |
2293 | + return !cfp.constraints._intervals.empty(); |
2294 | + } |
2295 | + |
2296 | + Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override { |
2297 | + Colored::interval_t interval; |
2298 | + Colored::intervalTuple_t tupleInterval; |
2299 | + const Color *dotColor = DotConstant::dotConstant(nullptr); |
2300 | + |
2301 | + colortypes->push_back(dotColor->getColorType()); |
2302 | + |
2303 | + interval.addRange(dotColor->getId(), dotColor->getId()); |
2304 | + tupleInterval.addInterval(interval); |
2305 | + return tupleInterval; |
2306 | + } |
2307 | + |
2308 | + void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override { |
2309 | + const Color *dotColor = DotConstant::dotConstant(nullptr); |
2310 | + constantMap[index] = dotColor; |
2311 | + } |
2312 | + ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{ |
2313 | + return DotConstant::dotConstant(nullptr)->getColorType(); |
2314 | + } |
2315 | + |
2316 | + std::string toString() const override { |
2317 | + return "dot"; |
2318 | } |
2319 | }; |
2320 | |
2321 | @@ -110,17 +182,74 @@ |
2322 | |
2323 | public: |
2324 | const Color* eval(ExpressionContext& context) const override { |
2325 | - return context.binding[_variable->name]; |
2326 | + return context.binding[_variable]; |
2327 | } |
2328 | |
2329 | - void getVariables(std::set<Variable*>& variables) const override { |
2330 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2331 | variables.insert(_variable); |
2332 | + varPositions[*index] = _variable; |
2333 | + if(varModifierMap.count(_variable) == 0){ |
2334 | + std::vector<std::unordered_map<uint32_t, int32_t>> newVec; |
2335 | + |
2336 | + for(auto pair : varModifierMap){ |
2337 | + for(uint32_t i = 0; i < pair.second.size()-1; i++){ |
2338 | + std::unordered_map<uint32_t, int32_t> emptyMap; |
2339 | + newVec.push_back(emptyMap); |
2340 | + } |
2341 | + break; |
2342 | + } |
2343 | + std::unordered_map<uint32_t, int32_t> newMap; |
2344 | + newMap[*index] = 0; |
2345 | + newVec.push_back(newMap); |
2346 | + varModifierMap[_variable] = newVec; |
2347 | + } else { |
2348 | + varModifierMap[_variable].back()[*index] = 0; |
2349 | + } |
2350 | + } |
2351 | + |
2352 | + Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override { |
2353 | + Colored::intervalTuple_t varInterval; |
2354 | + |
2355 | + // If we see a new variable on an out arc, it gets its full interval |
2356 | + if (varMap.count(_variable) == 0){ |
2357 | + Colored::intervalTuple_t intervalTuple; |
2358 | + intervalTuple.addInterval(_variable->colorType->getFullInterval()); |
2359 | + varMap[_variable] = intervalTuple; |
2360 | + } |
2361 | + |
2362 | + for(auto interval : varMap[_variable]._intervals){ |
2363 | + varInterval.addInterval(interval); |
2364 | + } |
2365 | + |
2366 | + std::vector<ColorType*> varColorTypes; |
2367 | + _variable->colorType->getColortypes(varColorTypes); |
2368 | + |
2369 | + for(auto ct : varColorTypes){ |
2370 | + colortypes->push_back(ct); |
2371 | + } |
2372 | + |
2373 | + return varInterval; |
2374 | + } |
2375 | + |
2376 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
2377 | + if (arcIntervals._intervalTupleVec.empty()){ |
2378 | + //As variables does not restrict the values before the guard we include all tokens |
2379 | + arcIntervals._intervalTupleVec.push_back(cfp.constraints); |
2380 | + } |
2381 | + return !cfp.constraints._intervals.empty(); |
2382 | + } |
2383 | + |
2384 | + void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override { |
2385 | } |
2386 | |
2387 | std::string toString() const override { |
2388 | return _variable->name; |
2389 | } |
2390 | |
2391 | + ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{ |
2392 | + return _variable->colorType; |
2393 | + } |
2394 | + |
2395 | VariableExpression(Variable* variable) |
2396 | : _variable(variable) {} |
2397 | }; |
2398 | @@ -134,10 +263,63 @@ |
2399 | return _userOperator; |
2400 | } |
2401 | |
2402 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
2403 | + uint32_t colorId = _userOperator->getId() + modifier; |
2404 | + while(colorId < 0){ |
2405 | + colorId += _userOperator->getColorType()->size(); |
2406 | + } |
2407 | + colorId = colorId % _userOperator->getColorType()->size(); |
2408 | + |
2409 | + if(arcIntervals._intervalTupleVec.empty()){ |
2410 | + Colored::intervalTuple_t newIntervalTuple; |
2411 | + bool colorInFixpoint = false; |
2412 | + for (auto interval : cfp.constraints._intervals){ |
2413 | + if(interval[*index].contains(colorId)){ |
2414 | + newIntervalTuple.addInterval(interval); |
2415 | + colorInFixpoint = true; |
2416 | + } |
2417 | + } |
2418 | + arcIntervals._intervalTupleVec.push_back(newIntervalTuple); |
2419 | + return colorInFixpoint; |
2420 | + } else { |
2421 | + std::vector<uint32_t> intervalsToRemove; |
2422 | + for(auto& intervalTuple : arcIntervals._intervalTupleVec){ |
2423 | + for (uint32_t i = 0; i < intervalTuple._intervals.size(); i++){ |
2424 | + if(!intervalTuple[i][*index].contains(colorId)){ |
2425 | + intervalsToRemove.push_back(i); |
2426 | + } |
2427 | + } |
2428 | + |
2429 | + for (auto i = intervalsToRemove.rbegin(); i != intervalsToRemove.rend(); ++i) { |
2430 | + intervalTuple.removeInterval(*i); |
2431 | + } |
2432 | + } |
2433 | + return !arcIntervals._intervalTupleVec[0]._intervals.empty(); |
2434 | + } |
2435 | + } |
2436 | + |
2437 | std::string toString() const override { |
2438 | return _userOperator->toString(); |
2439 | } |
2440 | |
2441 | + void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override { |
2442 | + constantMap[index] = _userOperator; |
2443 | + } |
2444 | + ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{ |
2445 | + return _userOperator->getColorType(); |
2446 | + } |
2447 | + |
2448 | + Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override { |
2449 | + Colored::interval_t interval; |
2450 | + Colored::intervalTuple_t tupleInterval; |
2451 | + |
2452 | + colortypes->push_back(_userOperator->getColorType()); |
2453 | + |
2454 | + interval.addRange(_userOperator->getId(), _userOperator->getId()); |
2455 | + tupleInterval.addInterval(interval); |
2456 | + return tupleInterval; |
2457 | + } |
2458 | + |
2459 | UserOperatorExpression(const Color* userOperator) |
2460 | : _userOperator(userOperator) {} |
2461 | }; |
2462 | @@ -185,14 +367,47 @@ |
2463 | return &++(*_color->eval(context)); |
2464 | } |
2465 | |
2466 | - void getVariables(std::set<Variable*>& variables) const override { |
2467 | - _color->getVariables(variables); |
2468 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2469 | + //save index before evaluating nested expression to decrease all the correct modifiers |
2470 | + uint32_t indexBefore = *index; |
2471 | + _color->getVariables(variables, varPositions, varModifierMap, index); |
2472 | + for(auto& varModifierPair : varModifierMap){ |
2473 | + for(auto& idModPair : varModifierPair.second.back()){ |
2474 | + if(idModPair.first <= *index && idModPair.first >= indexBefore){ |
2475 | + idModPair.second--; |
2476 | + } |
2477 | + } |
2478 | + } |
2479 | + } |
2480 | + |
2481 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
2482 | + return _color->getArcIntervals(arcIntervals, cfp, index, modifier+1); |
2483 | + } |
2484 | + |
2485 | + Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override { |
2486 | + //store the number of colortyps already in colortypes vector and use that as offset when indexing it |
2487 | + auto colortypesBefore = colortypes->size(); |
2488 | + |
2489 | + auto nestedInterval = _color->getOutputIntervals(varMap, colortypes); |
2490 | + Colored::GuardRestrictor guardRestrictor = Colored::GuardRestrictor(); |
2491 | + return guardRestrictor.shiftIntervals(colortypes, &nestedInterval, 1, colortypesBefore); |
2492 | + } |
2493 | + |
2494 | + void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override { |
2495 | + _color->getConstants(constantMap, index); |
2496 | + for(auto& constIndexPair : constantMap){ |
2497 | + constIndexPair.second = &constIndexPair.second->operator++(); |
2498 | + } |
2499 | } |
2500 | |
2501 | std::string toString() const override { |
2502 | return _color->toString() + "++"; |
2503 | } |
2504 | |
2505 | + ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{ |
2506 | + return _color->getColorType(colorTypes); |
2507 | + } |
2508 | + |
2509 | SuccessorExpression(ColorExpression_ptr&& color) |
2510 | : _color(std::move(color)) {} |
2511 | }; |
2512 | @@ -206,14 +421,47 @@ |
2513 | return &--(*_color->eval(context)); |
2514 | } |
2515 | |
2516 | - void getVariables(std::set<Variable*>& variables) const override { |
2517 | - _color->getVariables(variables); |
2518 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2519 | + //save index before evaluating nested expression to decrease all the correct modifiers |
2520 | + uint32_t indexBefore = *index; |
2521 | + _color->getVariables(variables, varPositions, varModifierMap, index); |
2522 | + for(auto& varModifierPair : varModifierMap){ |
2523 | + for(auto& idModPair : varModifierPair.second.back()){ |
2524 | + if(idModPair.first <= *index && idModPair.first >= indexBefore){ |
2525 | + idModPair.second++; |
2526 | + } |
2527 | + } |
2528 | + } |
2529 | + } |
2530 | + |
2531 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
2532 | + return _color->getArcIntervals(arcIntervals, cfp, index, modifier-1); |
2533 | + } |
2534 | + |
2535 | + Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override { |
2536 | + //store the number of colortyps already in colortypes vector and use that as offset when indexing it |
2537 | + auto colortypesBefore = colortypes->size(); |
2538 | + |
2539 | + auto nestedInterval = _color->getOutputIntervals(varMap, colortypes); |
2540 | + Colored::GuardRestrictor guardRestrictor; |
2541 | + return guardRestrictor.shiftIntervals(colortypes, &nestedInterval, -1, colortypesBefore); |
2542 | + } |
2543 | + |
2544 | + void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override { |
2545 | + _color->getConstants(constantMap, index); |
2546 | + for(auto& constIndexPair : constantMap){ |
2547 | + constIndexPair.second = &constIndexPair.second->operator--(); |
2548 | + } |
2549 | } |
2550 | |
2551 | std::string toString() const override { |
2552 | return _color->toString() + "--"; |
2553 | } |
2554 | |
2555 | + ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{ |
2556 | + return _color->getColorType(colorTypes); |
2557 | + } |
2558 | + |
2559 | PredecessorExpression(ColorExpression_ptr&& color) |
2560 | : _color(std::move(color)) {} |
2561 | }; |
2562 | @@ -221,6 +469,7 @@ |
2563 | class TupleExpression : public ColorExpression { |
2564 | private: |
2565 | std::vector<ColorExpression_ptr> _colors; |
2566 | + ColorType* _colorType; |
2567 | |
2568 | public: |
2569 | const Color* eval(ExpressionContext& context) const override { |
2570 | @@ -236,10 +485,77 @@ |
2571 | assert(col != nullptr); |
2572 | return col; |
2573 | } |
2574 | + |
2575 | + bool isTuple() const override { |
2576 | + return true; |
2577 | + } |
2578 | + |
2579 | + Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override { |
2580 | + Colored::intervalTuple_t intervals; |
2581 | + Colored::intervalTuple_t intervalHolder; |
2582 | + |
2583 | + for(auto colorExp : _colors) { |
2584 | + Colored::intervalTuple_t intervalHolder; |
2585 | + auto nested_intervals = colorExp->getOutputIntervals(varMap, colortypes); |
2586 | + |
2587 | + if(intervals._intervals.empty()){ |
2588 | + intervals = nested_intervals; |
2589 | + } else { |
2590 | + for(auto nested_interval : nested_intervals._intervals){ |
2591 | + Colored::intervalTuple_t newIntervals; |
2592 | + for(auto interval : intervals._intervals){ |
2593 | + for(auto nestedRange : nested_interval._ranges) { |
2594 | + interval.addRange(nestedRange); |
2595 | + } |
2596 | + newIntervals.addInterval(interval); |
2597 | + } |
2598 | + for(auto newInterval : newIntervals._intervals){ |
2599 | + intervalHolder.addInterval(newInterval); |
2600 | + } |
2601 | + } |
2602 | + intervals = intervalHolder; |
2603 | + } |
2604 | + } |
2605 | + return intervals; |
2606 | + } |
2607 | + |
2608 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
2609 | + for (auto expr : _colors) { |
2610 | + bool res = expr->getArcIntervals(arcIntervals, cfp, index, modifier); |
2611 | + if(!res){ |
2612 | + return false; |
2613 | + } |
2614 | + (*index)++; |
2615 | + } |
2616 | + return true; |
2617 | + } |
2618 | |
2619 | - void getVariables(std::set<Variable*>& variables) const override { |
2620 | - for (auto elem : _colors) { |
2621 | - elem->getVariables(variables); |
2622 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2623 | + for (auto elem : _colors) { |
2624 | + elem->getVariables(variables, varPositions, varModifierMap, index); |
2625 | + (*index)++; |
2626 | + } |
2627 | + } |
2628 | + |
2629 | + ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{ |
2630 | + std::vector<const ColorType*> types; |
2631 | + for (auto color : _colors) { |
2632 | + types.push_back(color->getColorType(colorTypes)); |
2633 | + } |
2634 | + for (auto& elem : colorTypes) { |
2635 | + auto* pt = dynamic_cast<ProductType*>(elem.second); |
2636 | + if (pt && pt->containsTypes(types)) { |
2637 | + return pt; |
2638 | + } |
2639 | + } |
2640 | + std::cout << "COULD NOT FIND PRODUCT TYPE" << std::endl; |
2641 | + return nullptr; |
2642 | + } |
2643 | + |
2644 | + void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override { |
2645 | + for (auto elem : _colors) { |
2646 | + elem->getConstants(constantMap, index); |
2647 | + index++; |
2648 | } |
2649 | } |
2650 | |
2651 | @@ -252,6 +568,10 @@ |
2652 | return res; |
2653 | } |
2654 | |
2655 | + void setColorType(ColorType* ct){ |
2656 | + _colorType = ct; |
2657 | + } |
2658 | + |
2659 | TupleExpression(std::vector<ColorExpression_ptr>&& colors) |
2660 | : _colors(std::move(colors)) {} |
2661 | }; |
2662 | @@ -262,6 +582,8 @@ |
2663 | virtual ~GuardExpression() {} |
2664 | |
2665 | virtual bool eval(ExpressionContext& context) const = 0; |
2666 | + |
2667 | + virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const = 0; |
2668 | }; |
2669 | |
2670 | typedef std::shared_ptr<GuardExpression> GuardExpression_ptr; |
2671 | @@ -275,11 +597,40 @@ |
2672 | bool eval(ExpressionContext& context) const override { |
2673 | return _left->eval(context) < _right->eval(context); |
2674 | } |
2675 | + |
2676 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2677 | + _left->getVariables(variables, varPositions, varModifierMap); |
2678 | + _right->getVariables(variables, varPositions, varModifierMap); |
2679 | + } |
2680 | + |
2681 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2682 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL; |
2683 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR; |
2684 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL; |
2685 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR; |
2686 | + std::unordered_map<uint32_t, const Color*> constantMapL; |
2687 | + std::unordered_map<uint32_t, const Color*> constantMapR; |
2688 | + std::set<const Variable *> leftVars; |
2689 | + std::set<const Variable *> rightVars; |
2690 | + uint32_t index = 0; |
2691 | + _left->getVariables(leftVars, varPositionsL, varModifierMapL); |
2692 | + _right->getVariables(rightVars, varPositionsR, varModifierMapR); |
2693 | + _left->getConstants(constantMapL, index); |
2694 | + index = 0; |
2695 | + _right->getConstants(constantMapR, index); |
2696 | + |
2697 | + if(leftVars.empty() && rightVars.empty()){ |
2698 | + return; |
2699 | + } |
2700 | + Colored::GuardRestrictor guardRestrictor; |
2701 | + guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, true, true); |
2702 | + } |
2703 | |
2704 | - void getVariables(std::set<Variable*>& variables) const override { |
2705 | - _left->getVariables(variables); |
2706 | - _right->getVariables(variables); |
2707 | + std::string toString() const override { |
2708 | + std::string res = _left->toString() + " < " + _right->toString(); |
2709 | + return res; |
2710 | } |
2711 | + |
2712 | |
2713 | LessThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right) |
2714 | : _left(std::move(left)), _right(std::move(right)) {} |
2715 | @@ -295,9 +646,38 @@ |
2716 | return _left->eval(context) > _right->eval(context); |
2717 | } |
2718 | |
2719 | - void getVariables(std::set<Variable*>& variables) const override { |
2720 | - _left->getVariables(variables); |
2721 | - _right->getVariables(variables); |
2722 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2723 | + _left->getVariables(variables, varPositions, varModifierMap); |
2724 | + _right->getVariables(variables, varPositions, varModifierMap); |
2725 | + } |
2726 | + |
2727 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2728 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL; |
2729 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR; |
2730 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL; |
2731 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR; |
2732 | + std::unordered_map<uint32_t, const Color*> constantMapL; |
2733 | + std::unordered_map<uint32_t, const Color*> constantMapR; |
2734 | + std::set<const Colored::Variable *> leftVars; |
2735 | + std::set<const Colored::Variable *> rightVars; |
2736 | + uint32_t index = 0; |
2737 | + _left->getVariables(leftVars, varPositionsL, varModifierMapL); |
2738 | + _right->getVariables(rightVars, varPositionsR, varModifierMapR); |
2739 | + _left->getConstants(constantMapL, index); |
2740 | + index = 0; |
2741 | + _right->getConstants(constantMapR, index); |
2742 | + |
2743 | + if(leftVars.empty() && rightVars.empty()){ |
2744 | + return; |
2745 | + } |
2746 | + |
2747 | + Colored::GuardRestrictor guardRestrictor; |
2748 | + guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, false, true); |
2749 | + } |
2750 | + |
2751 | + std::string toString() const override { |
2752 | + std::string res = _left->toString() + " > " + _right->toString(); |
2753 | + return res; |
2754 | } |
2755 | |
2756 | GreaterThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right) |
2757 | @@ -314,10 +694,40 @@ |
2758 | return _left->eval(context) <= _right->eval(context); |
2759 | } |
2760 | |
2761 | - void getVariables(std::set<Variable*>& variables) const override { |
2762 | - _left->getVariables(variables); |
2763 | - _right->getVariables(variables); |
2764 | - } |
2765 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2766 | + _left->getVariables(variables, varPositions, varModifierMap); |
2767 | + _right->getVariables(variables, varPositions, varModifierMap); |
2768 | + } |
2769 | + |
2770 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2771 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL; |
2772 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR; |
2773 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL; |
2774 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR; |
2775 | + std::unordered_map<uint32_t, const Color*> constantMapL; |
2776 | + std::unordered_map<uint32_t, const Color*> constantMapR; |
2777 | + std::set<const Colored::Variable *> leftVars; |
2778 | + std::set<const Colored::Variable *> rightVars; |
2779 | + uint32_t index = 0; |
2780 | + _left->getVariables(leftVars, varPositionsL, varModifierMapL); |
2781 | + _right->getVariables(rightVars, varPositionsR, varModifierMapR); |
2782 | + _left->getConstants(constantMapL, index); |
2783 | + index = 0; |
2784 | + _right->getConstants(constantMapR, index); |
2785 | + |
2786 | + if(leftVars.empty() && rightVars.empty()){ |
2787 | + return; |
2788 | + } |
2789 | + |
2790 | + Colored::GuardRestrictor guardRestrictor; |
2791 | + guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, true, false); |
2792 | + } |
2793 | + |
2794 | + std::string toString() const override { |
2795 | + std::string res = _left->toString() + " <= " + _right->toString(); |
2796 | + return res; |
2797 | + } |
2798 | + |
2799 | |
2800 | LessThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right) |
2801 | : _left(std::move(left)), _right(std::move(right)) {} |
2802 | @@ -333,11 +743,40 @@ |
2803 | return _left->eval(context) >= _right->eval(context); |
2804 | } |
2805 | |
2806 | - void getVariables(std::set<Variable*>& variables) const override { |
2807 | - _left->getVariables(variables); |
2808 | - _right->getVariables(variables); |
2809 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2810 | + _left->getVariables(variables, varPositions, varModifierMap); |
2811 | + _right->getVariables(variables, varPositions, varModifierMap); |
2812 | + } |
2813 | + |
2814 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2815 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL; |
2816 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR; |
2817 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL; |
2818 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR; |
2819 | + std::unordered_map<uint32_t, const Color*> constantMapL; |
2820 | + std::unordered_map<uint32_t, const Color*> constantMapR; |
2821 | + std::set<const Colored::Variable *> leftVars; |
2822 | + std::set<const Colored::Variable *> rightVars; |
2823 | + uint32_t index = 0; |
2824 | + _left->getVariables(leftVars, varPositionsL, varModifierMapL); |
2825 | + _right->getVariables(rightVars, varPositionsR, varModifierMapR); |
2826 | + _left->getConstants(constantMapL, index); |
2827 | + index = 0; |
2828 | + _right->getConstants(constantMapR, index); |
2829 | + |
2830 | + if(leftVars.empty() && rightVars.empty()){ |
2831 | + return; |
2832 | + } |
2833 | + |
2834 | + Colored::GuardRestrictor guardRestrictor; |
2835 | + guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, false, false); |
2836 | } |
2837 | |
2838 | + std::string toString() const override { |
2839 | + std::string res = _left->toString() + " >= " + _right->toString(); |
2840 | + return res; |
2841 | + } |
2842 | + |
2843 | GreaterThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right) |
2844 | : _left(std::move(left)), _right(std::move(right)) {} |
2845 | }; |
2846 | @@ -352,11 +791,41 @@ |
2847 | return _left->eval(context) == _right->eval(context); |
2848 | } |
2849 | |
2850 | - void getVariables(std::set<Variable*>& variables) const override { |
2851 | - _left->getVariables(variables); |
2852 | - _right->getVariables(variables); |
2853 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2854 | + _left->getVariables(variables, varPositions, varModifierMap); |
2855 | + _right->getVariables(variables, varPositions, varModifierMap); |
2856 | } |
2857 | |
2858 | + |
2859 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2860 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL; |
2861 | + std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR; |
2862 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL; |
2863 | + std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR; |
2864 | + std::unordered_map<uint32_t, const Color*> constantMapL; |
2865 | + std::unordered_map<uint32_t, const Color*> constantMapR; |
2866 | + std::set<const Colored::Variable *> leftVars; |
2867 | + std::set<const Colored::Variable *> rightVars; |
2868 | + uint32_t index = 0; |
2869 | + _left->getVariables(leftVars, varPositionsL, varModifierMapL); |
2870 | + _right->getVariables(rightVars, varPositionsR, varModifierMapR); |
2871 | + _left->getConstants(constantMapL, index); |
2872 | + index = 0; |
2873 | + _right->getConstants(constantMapR, index); |
2874 | + |
2875 | + if(leftVars.empty() && rightVars.empty()){ |
2876 | + return; |
2877 | + } |
2878 | + |
2879 | + Colored::GuardRestrictor guardRestrictor; |
2880 | + guardRestrictor.restrictEquality(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR); |
2881 | + } |
2882 | + |
2883 | + std::string toString() const override { |
2884 | + std::string res = _left->toString() + " == " + _right->toString(); |
2885 | + return res; |
2886 | + } |
2887 | + |
2888 | EqualityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right) |
2889 | : _left(std::move(left)), _right(std::move(right)) {} |
2890 | }; |
2891 | @@ -371,9 +840,18 @@ |
2892 | return _left->eval(context) != _right->eval(context); |
2893 | } |
2894 | |
2895 | - void getVariables(std::set<Variable*>& variables) const override { |
2896 | - _left->getVariables(variables); |
2897 | - _right->getVariables(variables); |
2898 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2899 | + _left->getVariables(variables, varPositions, varModifierMap); |
2900 | + _right->getVariables(variables, varPositions, varModifierMap); |
2901 | + } |
2902 | + |
2903 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2904 | + |
2905 | + } |
2906 | + |
2907 | + std::string toString() const override { |
2908 | + std::string res = _left->toString() + " != " + _right->toString(); |
2909 | + return res; |
2910 | } |
2911 | |
2912 | InequalityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right) |
2913 | @@ -389,8 +867,28 @@ |
2914 | return !_expr->eval(context); |
2915 | } |
2916 | |
2917 | - void getVariables(std::set<Variable*>& variables) const override { |
2918 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2919 | + _expr->getVariables(variables, varPositions, varModifierMap, index); |
2920 | + } |
2921 | + |
2922 | + std::string toString() const override { |
2923 | + std::string res = "!" + _expr->toString(); |
2924 | + return res; |
2925 | + } |
2926 | + |
2927 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2928 | + std::set<const Colored::Variable *> variables; |
2929 | _expr->getVariables(variables); |
2930 | + //TODO: invert the var intervals here instead of using the full intervals |
2931 | + |
2932 | + for(auto var : variables){ |
2933 | + auto fullInterval = var->colorType->getFullInterval(); |
2934 | + Colored::intervalTuple_t fullTuple; |
2935 | + fullTuple.addInterval(fullInterval); |
2936 | + for(auto& varMap : variableMap){ |
2937 | + varMap[var] = fullTuple; |
2938 | + } |
2939 | + } |
2940 | } |
2941 | |
2942 | NotExpression(GuardExpression_ptr&& expr) : _expr(std::move(expr)) {} |
2943 | @@ -406,11 +904,21 @@ |
2944 | return _left->eval(context) && _right->eval(context); |
2945 | } |
2946 | |
2947 | - void getVariables(std::set<Variable*>& variables) const override { |
2948 | - _left->getVariables(variables); |
2949 | - _right->getVariables(variables); |
2950 | - } |
2951 | - |
2952 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2953 | + _left->getVariables(variables, varPositions, varModifierMap); |
2954 | + _right->getVariables(variables, varPositions, varModifierMap); |
2955 | + } |
2956 | + |
2957 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override { |
2958 | + _left->restrictVars(variableMap); |
2959 | + _right->restrictVars(variableMap); |
2960 | + } |
2961 | + |
2962 | + std::string toString() const override { |
2963 | + std::string res = _left->toString() + " && " + _right->toString(); |
2964 | + return res; |
2965 | + } |
2966 | + |
2967 | AndExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right) |
2968 | : _left(left), _right(right) {} |
2969 | }; |
2970 | @@ -425,11 +933,30 @@ |
2971 | return _left->eval(context) || _right->eval(context); |
2972 | } |
2973 | |
2974 | - void getVariables(std::set<Variable*>& variables) const override { |
2975 | - _left->getVariables(variables); |
2976 | - _right->getVariables(variables); |
2977 | - } |
2978 | - |
2979 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
2980 | + _left->getVariables(variables, varPositions, varModifierMap); |
2981 | + _right->getVariables(variables, varPositions, varModifierMap); |
2982 | + } |
2983 | + |
2984 | + void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override{ |
2985 | + auto varMapCopy = variableMap; |
2986 | + _left->restrictVars(variableMap); |
2987 | + _right->restrictVars(varMapCopy); |
2988 | + |
2989 | + for(size_t i = 0; i < variableMap.size(); i++){ |
2990 | + for(auto& varPair : varMapCopy[i]){ |
2991 | + for(auto& interval : varPair.second._intervals){ |
2992 | + variableMap[i][varPair.first].addInterval(std::move(interval)); |
2993 | + } |
2994 | + } |
2995 | + } |
2996 | + } |
2997 | + |
2998 | + std::string toString() const override { |
2999 | + std::string res = _left->toString() + " || " + _right->toString(); |
3000 | + return res; |
3001 | + } |
3002 | + |
3003 | OrExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right) |
3004 | : _left(std::move(left)), _right(std::move(right)) {} |
3005 | }; |
3006 | @@ -444,8 +971,21 @@ |
3007 | virtual void expressionType() override { |
3008 | std::cout << "ArcExpression" << std::endl; |
3009 | } |
3010 | + virtual void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const = 0; |
3011 | + |
3012 | + virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const = 0; |
3013 | |
3014 | virtual uint32_t weight() const = 0; |
3015 | + |
3016 | + virtual Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec) const { |
3017 | + std::vector<const Colored::ColorType *> colortypes; |
3018 | + |
3019 | + return getOutputIntervals(varMapVec, &colortypes); |
3020 | + } |
3021 | + |
3022 | + virtual Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const { |
3023 | + return Colored::intervalTuple_t(); |
3024 | + } |
3025 | }; |
3026 | |
3027 | typedef std::shared_ptr<ArcExpression> ArcExpression_ptr; |
3028 | @@ -465,6 +1005,45 @@ |
3029 | return colors; |
3030 | } |
3031 | |
3032 | + void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const { |
3033 | + for (size_t i = 0; i < _sort->size(); i++) { |
3034 | + constantMap[index].push_back(&(*_sort)[i]); |
3035 | + } |
3036 | + } |
3037 | + |
3038 | + Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const { |
3039 | + Colored::intervalTuple_t newIntervalTuple; |
3040 | + newIntervalTuple.addInterval(_sort->getFullInterval()); |
3041 | + return newIntervalTuple; |
3042 | + } |
3043 | + |
3044 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const { |
3045 | + |
3046 | + if(arcIntervals._intervalTupleVec.empty()){ |
3047 | + bool colorsInFixpoint = false; |
3048 | + Colored::intervalTuple_t newIntervalTuple; |
3049 | + cfp.constraints.simplify(); |
3050 | + if(cfp.constraints.getContainedColors() == _sort->size()){ |
3051 | + colorsInFixpoint = true; |
3052 | + for(auto interval : cfp.constraints._intervals){ |
3053 | + newIntervalTuple.addInterval(interval); |
3054 | + } |
3055 | + } |
3056 | + arcIntervals._intervalTupleVec.push_back(newIntervalTuple); |
3057 | + return colorsInFixpoint; |
3058 | + } else { |
3059 | + std::vector<Colored::intervalTuple_t> newIntervalTupleVec; |
3060 | + for(uint32_t i = 0; i < arcIntervals._intervalTupleVec.size(); i++){ |
3061 | + auto& intervalTuple = arcIntervals._intervalTupleVec[i]; |
3062 | + if(intervalTuple.getContainedColors() == _sort->size()){ |
3063 | + newIntervalTupleVec.push_back(intervalTuple); |
3064 | + } |
3065 | + } |
3066 | + arcIntervals._intervalTupleVec = std::move(newIntervalTupleVec); |
3067 | + return !arcIntervals._intervalTupleVec.empty(); |
3068 | + } |
3069 | + } |
3070 | + |
3071 | size_t size() const { |
3072 | return _sort->size(); |
3073 | } |
3074 | @@ -503,12 +1082,64 @@ |
3075 | } |
3076 | return Multiset(col); |
3077 | } |
3078 | - |
3079 | - void getVariables(std::set<Variable*>& variables) const override { |
3080 | + |
3081 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
3082 | if (_all != nullptr) |
3083 | return; |
3084 | for (auto elem : _color) { |
3085 | - elem->getVariables(variables); |
3086 | + //TODO: can there be more than one element in a number of expression? |
3087 | + elem->getVariables(variables, varPositions, varModifierMap, index); |
3088 | + //(*index)++; |
3089 | + } |
3090 | + } |
3091 | + |
3092 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
3093 | + if (_all != nullptr) { |
3094 | + return _all->getArcIntervals(arcIntervals, cfp, index, modifier); |
3095 | + } |
3096 | + uint32_t i = 0; |
3097 | + for (auto elem : _color) { |
3098 | + (*index) += i; |
3099 | + if(!elem->getArcIntervals(arcIntervals, cfp, index, modifier)){ |
3100 | + return false; |
3101 | + } |
3102 | + i++; |
3103 | + } |
3104 | + return true; |
3105 | + } |
3106 | + |
3107 | + Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override { |
3108 | + Colored::intervalTuple_t intervals; |
3109 | + if (_all == nullptr) { |
3110 | + for (auto elem : _color) { |
3111 | + for(auto& varMap : varMapVec){ |
3112 | + auto nestedIntervals = elem->getOutputIntervals(varMap, colortypes); |
3113 | + |
3114 | + if (intervals._intervals.empty()) { |
3115 | + intervals = nestedIntervals; |
3116 | + } else { |
3117 | + for(auto interval : nestedIntervals._intervals) { |
3118 | + intervals.addInterval(interval); |
3119 | + } |
3120 | + } |
3121 | + } |
3122 | + } |
3123 | + } else { |
3124 | + return _all->getOutputIntervals(varMapVec, colortypes); |
3125 | + } |
3126 | + return intervals; |
3127 | + } |
3128 | + |
3129 | + void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override { |
3130 | + if (_all != nullptr) |
3131 | + _all->getConstants(constantMap, index); |
3132 | + else for (auto elem : _color) { |
3133 | + std::unordered_map<uint32_t, const Color*> elemMap; |
3134 | + elem->getConstants(elemMap, index); |
3135 | + for(auto pair : elemMap){ |
3136 | + constantMap[pair.first].push_back(pair.second); |
3137 | + } |
3138 | + index++;//not sure if index should be increased here, but no number expression have multiple elements |
3139 | } |
3140 | } |
3141 | |
3142 | @@ -563,9 +1194,57 @@ |
3143 | return ms; |
3144 | } |
3145 | |
3146 | - void getVariables(std::set<Variable*>& variables) const override { |
3147 | - for (auto elem : _constituents) { |
3148 | - elem->getVariables(variables); |
3149 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
3150 | + for (auto elem : _constituents) { |
3151 | + for(auto& pair : varModifierMap){ |
3152 | + std::unordered_map<uint32_t, int32_t> newMap; |
3153 | + pair.second.push_back(newMap); |
3154 | + } |
3155 | + elem->getVariables(variables, varPositions, varModifierMap); |
3156 | + } |
3157 | + } |
3158 | + |
3159 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
3160 | + for (auto elem : _constituents) { |
3161 | + uint32_t newIndex = 0; |
3162 | + Colored::ArcIntervals newArcIntervals; |
3163 | + std::vector<uint32_t> intervalsForRemoval; |
3164 | + std::vector<Colored::interval_t> newIntervals; |
3165 | + if(!elem->getArcIntervals(newArcIntervals, cfp, &newIndex, modifier)){ |
3166 | + return false; |
3167 | + } |
3168 | + |
3169 | + if(newArcIntervals._intervalTupleVec.empty()){ |
3170 | + return false; |
3171 | + } |
3172 | + |
3173 | + arcIntervals._intervalTupleVec.insert(arcIntervals._intervalTupleVec.end(), newArcIntervals._intervalTupleVec.begin(), newArcIntervals._intervalTupleVec.end()); |
3174 | + } |
3175 | + return true; |
3176 | + } |
3177 | + |
3178 | + Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override { |
3179 | + Colored::intervalTuple_t intervals; |
3180 | + |
3181 | + for (auto elem : _constituents) { |
3182 | + auto nestedIntervals = elem->getOutputIntervals(varMapVec, colortypes); |
3183 | + |
3184 | + if (intervals._intervals.empty()) { |
3185 | + intervals = nestedIntervals; |
3186 | + } else { |
3187 | + for(auto interval : nestedIntervals._intervals) { |
3188 | + intervals.addInterval(interval); |
3189 | + } |
3190 | + } |
3191 | + } |
3192 | + return intervals; |
3193 | + } |
3194 | + |
3195 | + void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override { |
3196 | + uint32_t indexCopy = index; |
3197 | + for (auto elem : _constituents) { |
3198 | + uint32_t localIndex = indexCopy; |
3199 | + elem->getConstants(constantMap, localIndex); |
3200 | } |
3201 | } |
3202 | |
3203 | @@ -599,9 +1278,29 @@ |
3204 | return _left->eval(context) - _right->eval(context); |
3205 | } |
3206 | |
3207 | - void getVariables(std::set<Variable*>& variables) const override { |
3208 | - _left->getVariables(variables); |
3209 | - _right->getVariables(variables); |
3210 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
3211 | + _left->getVariables(variables, varPositions, varModifierMap); |
3212 | + //We ignore the restrictions imposed by the subtraction for now |
3213 | + //_right->getVariables(variables, varPositions, varModifierMap); |
3214 | + } |
3215 | + |
3216 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
3217 | + return _left->getArcIntervals(arcIntervals, cfp, index, modifier); |
3218 | + //We ignore the restrictions imposed by the subtraction for now |
3219 | + //_right->getArcIntervals(arcIntervals, cfp, &rightIndex); |
3220 | + } |
3221 | + |
3222 | + Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override { |
3223 | + //We could maybe reduce the intervals slightly by checking if the upper or lower bound is being subtracted |
3224 | + auto leftIntervals = _left->getOutputIntervals(varMapVec, colortypes); |
3225 | + |
3226 | + return leftIntervals; |
3227 | + } |
3228 | + |
3229 | + void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override { |
3230 | + uint32_t rIndex = index; |
3231 | + _left->getConstants(constantMap, index); |
3232 | + _right->getConstants(constantMap, rIndex); |
3233 | } |
3234 | |
3235 | uint32_t weight() const override { |
3236 | @@ -636,8 +1335,20 @@ |
3237 | return _expr->eval(context) * _scalar; |
3238 | } |
3239 | |
3240 | - void getVariables(std::set<Variable*>& variables) const override { |
3241 | - _expr->getVariables(variables); |
3242 | + void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override { |
3243 | + _expr->getVariables(variables, varPositions,varModifierMap); |
3244 | + } |
3245 | + |
3246 | + bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override { |
3247 | + return _expr ->getArcIntervals(arcIntervals, cfp, index, modifier); |
3248 | + } |
3249 | + |
3250 | + Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override { |
3251 | + return _expr->getOutputIntervals(varMapVec, colortypes); |
3252 | + } |
3253 | + |
3254 | + void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override { |
3255 | + _expr->getConstants(constantMap, index); |
3256 | } |
3257 | |
3258 | uint32_t weight() const override { |
3259 | |
3260 | === added file 'include/PetriEngine/Colored/GuardRestrictor.h' |
3261 | --- include/PetriEngine/Colored/GuardRestrictor.h 1970-01-01 00:00:00 +0000 |
3262 | +++ include/PetriEngine/Colored/GuardRestrictor.h 2021-04-02 18:07:40 +0000 |
3263 | @@ -0,0 +1,83 @@ |
3264 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
3265 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
3266 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
3267 | + * |
3268 | + * This program is free software: you can redistribute it and/or modify |
3269 | + * it under the terms of the GNU General Public License as published by |
3270 | + * the Free Software Foundation, either version 3 of the License, or |
3271 | + * (at your option) any later version. |
3272 | + * |
3273 | + * This program is distributed in the hope that it will be useful, |
3274 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
3275 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
3276 | + * GNU General Public License for more details. |
3277 | + * |
3278 | + * You should have received a copy of the GNU General Public License |
3279 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
3280 | + */ |
3281 | + |
3282 | +#ifndef GuardRestrictions_H |
3283 | +#define GuardRestrictions_H |
3284 | + |
3285 | +#include "Colors.h" |
3286 | +#include "Multiset.h" |
3287 | +#include <unordered_map> |
3288 | +#include <set> |
3289 | +#include <stdlib.h> |
3290 | + |
3291 | +namespace PetriEngine { |
3292 | + namespace Colored { |
3293 | + |
3294 | + class GuardRestrictor { |
3295 | + public: |
3296 | + |
3297 | + GuardRestrictor(); |
3298 | + |
3299 | + void restrictDiagonal(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap, |
3300 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL, |
3301 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR, |
3302 | + std::unordered_map<uint32_t, const Variable *> *varPositionsL, |
3303 | + std::unordered_map<uint32_t, const Variable *> *varPositionsR, |
3304 | + std::unordered_map<uint32_t, const Color*> *constantMapL, |
3305 | + std::unordered_map<uint32_t, const Color*> *constantMapR, |
3306 | + bool lessthan, bool strict); |
3307 | + |
3308 | + void restrictEquality(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap, |
3309 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL, |
3310 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR, |
3311 | + std::unordered_map<uint32_t, const Variable *> *varPositionsL, |
3312 | + std::unordered_map<uint32_t, const Variable *> *varPositionsR, |
3313 | + std::unordered_map<uint32_t, const Color*> *constantMapL, |
3314 | + std::unordered_map<uint32_t, const Color*> *constantMapR); |
3315 | + |
3316 | + intervalTuple_t shiftIntervals(std::vector<const ColorType *> *colortypes, |
3317 | + intervalTuple_t *intervals, |
3318 | + int32_t modifier, |
3319 | + uint32_t ctSizeBefore) const; |
3320 | + |
3321 | + private: |
3322 | + int32_t getVarModifier(std::unordered_map<uint32_t, int32_t> *modPairMap, uint32_t index); |
3323 | + interval_t getIntervalFromIds(std::vector<uint32_t> *idVec, uint32_t ctSize, int32_t modifier); |
3324 | + intervalTuple_t getIntervalOverlap(std::vector<interval_t> *intervals1, std::vector<interval_t> *intervals2); |
3325 | + |
3326 | + void expandIdVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap, |
3327 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap, |
3328 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap, |
3329 | + std::unordered_map<uint32_t, const Variable *> *varPositions, |
3330 | + std::unordered_map<uint32_t, const Color*> *constantMap, |
3331 | + const Variable *otherVar, |
3332 | + std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index); |
3333 | + |
3334 | + void expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap, |
3335 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap, |
3336 | + std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap, |
3337 | + std::unordered_map<uint32_t, const Variable *> *varPositions, |
3338 | + std::unordered_map<uint32_t, const Color*> *constantMap, |
3339 | + const Variable *otherVar, |
3340 | + std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index); |
3341 | + }; |
3342 | + } |
3343 | +} |
3344 | + |
3345 | + |
3346 | +#endif /* GuardRestrictions_H */ |
3347 | \ No newline at end of file |
3348 | |
3349 | === added file 'include/PetriEngine/Colored/IntervalGenerator.h' |
3350 | --- include/PetriEngine/Colored/IntervalGenerator.h 1970-01-01 00:00:00 +0000 |
3351 | +++ include/PetriEngine/Colored/IntervalGenerator.h 2021-04-02 18:07:40 +0000 |
3352 | @@ -0,0 +1,197 @@ |
3353 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
3354 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
3355 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
3356 | + * |
3357 | + * This program is free software: you can redistribute it and/or modify |
3358 | + * it under the terms of the GNU General Public License as published by |
3359 | + * the Free Software Foundation, either version 3 of the License, or |
3360 | + * (at your option) any later version. |
3361 | + * |
3362 | + * This program is distributed in the hope that it will be useful, |
3363 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
3364 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
3365 | + * GNU General Public License for more details. |
3366 | + * |
3367 | + * You should have received a copy of the GNU General Public License |
3368 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
3369 | + */ |
3370 | +#ifndef INTERVALGENERATOR_H |
3371 | +#define INTERVALGENERATOR_H |
3372 | + |
3373 | +#include "ColoredNetStructures.h" |
3374 | + |
3375 | +namespace PetriEngine { |
3376 | + struct IntervalGenerator { |
3377 | + std::vector<Colored::interval_t> getIntervalsFromInterval(Colored::interval_t *interval, uint32_t varPosition, int32_t varModifier, std::vector<Colored::ColorType*> *varColorTypes){ |
3378 | + std::vector<Colored::interval_t> varIntervals; |
3379 | + Colored::interval_t firstVarInterval; |
3380 | + varIntervals.push_back(firstVarInterval); |
3381 | + for(uint32_t i = varPosition; i < varPosition + varColorTypes->size(); i++){ |
3382 | + auto ctSize = varColorTypes->operator[](i - varPosition)->size(); |
3383 | + int32_t lower_val = ctSize + (interval->operator[](i)._lower + varModifier); |
3384 | + int32_t upper_val = ctSize + (interval->operator[](i)._upper + varModifier); |
3385 | + uint32_t lower = lower_val % ctSize; |
3386 | + uint32_t upper = upper_val % ctSize; |
3387 | + |
3388 | + if(lower > upper ){ |
3389 | + if(lower == upper+1){ |
3390 | + for (auto& varInterval : varIntervals){ |
3391 | + varInterval.addRange(0, ctSize -1); |
3392 | + } |
3393 | + } else { |
3394 | + std::vector<Colored::interval_t> newIntervals; |
3395 | + for (auto& varInterval : varIntervals){ |
3396 | + Colored::interval_t newVarInterval = varInterval; |
3397 | + varInterval.addRange(0, upper); |
3398 | + newVarInterval.addRange(lower, ctSize -1); |
3399 | + newIntervals.push_back(newVarInterval); |
3400 | + } |
3401 | + varIntervals.insert(varIntervals.end(), newIntervals.begin(), newIntervals.end()); |
3402 | + } |
3403 | + } else { |
3404 | + for (auto& varInterval : varIntervals){ |
3405 | + varInterval.addRange(lower, upper); |
3406 | + } |
3407 | + } |
3408 | + } |
3409 | + return varIntervals; |
3410 | + } |
3411 | + |
3412 | + void getArcVarIntervals(Colored::intervalTuple_t& varIntervals, std::unordered_map<uint32_t, int32_t> *modIndexMap, Colored::interval_t *interval, std::vector<Colored::ColorType*> *varColorTypes){ |
3413 | + for(auto& posModPair : *modIndexMap){ |
3414 | + auto intervals = getIntervalsFromInterval(interval, posModPair.first, posModPair.second, varColorTypes); |
3415 | + |
3416 | + if(varIntervals._intervals.empty()){ |
3417 | + for(auto& interval : intervals){ |
3418 | + varIntervals.addInterval(std::move(interval)); |
3419 | + } |
3420 | + } else { |
3421 | + Colored::intervalTuple_t newVarIntervals; |
3422 | + for(uint32_t i = 0; i < varIntervals.size(); i++){ |
3423 | + auto varInterval = &varIntervals[i]; |
3424 | + for(auto& interval : intervals){ |
3425 | + auto overlap = varInterval->getOverlap(std::move(interval)); |
3426 | + if(overlap.isSound()){ |
3427 | + newVarIntervals.addInterval(std::move(overlap)); |
3428 | + //break; |
3429 | + } |
3430 | + } |
3431 | + } |
3432 | + varIntervals = std::move(newVarIntervals); |
3433 | + } |
3434 | + } |
3435 | + } |
3436 | + |
3437 | + void populateLocalMap(Colored::ArcIntervals *arcIntervals, |
3438 | + std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t> &varMap, |
3439 | + std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> &localVarMap, |
3440 | + Colored::interval_t* interval, bool& allVarsAssigned, uint32_t tuplePos){ |
3441 | + for(auto& pair : arcIntervals->_varIndexModMap){ |
3442 | + Colored::intervalTuple_t varIntervals; |
3443 | + std::vector<Colored::ColorType*> varColorTypes; |
3444 | + pair.first->colorType->getColortypes(varColorTypes); |
3445 | + |
3446 | + getArcVarIntervals(varIntervals, &pair.second[tuplePos], interval, &varColorTypes); |
3447 | + |
3448 | + if (arcIntervals->_intervalTupleVec.size() > 1 && pair.second[tuplePos].empty()) { |
3449 | + //The variable is not on this side of the add expression, so we add a full interval to compare against for the other side |
3450 | + varIntervals.addInterval(pair.first->colorType->getFullInterval()); |
3451 | + } |
3452 | + |
3453 | + if(varMap.count(pair.first) == 0){ |
3454 | + localVarMap[pair.first] = std::move(varIntervals); |
3455 | + } else { |
3456 | + for(auto& varInterval : varIntervals._intervals){ |
3457 | + for(auto& interval : varMap[pair.first]._intervals){ |
3458 | + auto overlapInterval = varInterval.getOverlap(interval); |
3459 | + |
3460 | + if(overlapInterval.isSound()){ |
3461 | + localVarMap[pair.first].addInterval(overlapInterval); |
3462 | + } |
3463 | + } |
3464 | + } |
3465 | + } |
3466 | + |
3467 | + if(localVarMap[pair.first]._intervals.empty()){ |
3468 | + allVarsAssigned = false; |
3469 | + } |
3470 | + } |
3471 | + } |
3472 | + |
3473 | + void fillVarMaps(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>> &variableMaps, |
3474 | + Colored::ArcIntervals *arcIntervals, |
3475 | + uint32_t *intervalTupleSize, |
3476 | + uint32_t *tuplePos) |
3477 | + { |
3478 | + for(uint32_t i = 0; i < *intervalTupleSize; i++){ |
3479 | + std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> localVarMap; |
3480 | + bool validInterval = true; |
3481 | + auto interval = &arcIntervals->_intervalTupleVec[*tuplePos]._intervals[i]; |
3482 | + |
3483 | + for(auto pair : arcIntervals->_varIndexModMap){ |
3484 | + Colored::intervalTuple_t varIntervals; |
3485 | + std::vector<Colored::ColorType*> varColorTypes; |
3486 | + pair.first->colorType->getColortypes(varColorTypes); |
3487 | + getArcVarIntervals(varIntervals, &pair.second[*tuplePos], interval, &varColorTypes); |
3488 | + |
3489 | + if(arcIntervals->_intervalTupleVec.size() > 1 && pair.second[*tuplePos].empty()){ |
3490 | + //The variable is not on this side of the add expression, so we add a full interval to compare against for the other side |
3491 | + varIntervals.addInterval(pair.first->colorType->getFullInterval()); |
3492 | + } else if(varIntervals.size() < 1){ |
3493 | + //If any varinterval ends up empty then we were unable to use this arc interval |
3494 | + validInterval = false; |
3495 | + break; |
3496 | + } |
3497 | + localVarMap[pair.first] = varIntervals; |
3498 | + } |
3499 | + |
3500 | + if(validInterval){ |
3501 | + variableMaps.push_back(localVarMap); |
3502 | + } |
3503 | + } |
3504 | + } |
3505 | + |
3506 | + bool getVarIntervals(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMaps, std::unordered_map<uint32_t, Colored::ArcIntervals> placeArcIntervals){ |
3507 | + for(auto& placeArcInterval : placeArcIntervals){ |
3508 | + for(uint32_t j = 0; j < placeArcInterval.second._intervalTupleVec.size(); j++){ |
3509 | + uint32_t intervalTupleSize = placeArcInterval.second._intervalTupleVec[j].size(); |
3510 | + //If we have not found intervals for any place yet, we fill the intervals from this place |
3511 | + //Else we restrict the intervals we already found to only keep those that can also be matched in this place |
3512 | + if(variableMaps.empty()){ |
3513 | + fillVarMaps(variableMaps, &placeArcInterval.second, &intervalTupleSize, &j); |
3514 | + } else { |
3515 | + std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> newVarMapVec; |
3516 | + |
3517 | + for(auto& varMap : variableMaps){ |
3518 | + for(uint32_t i = 0; i < intervalTupleSize; i++){ |
3519 | + std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> localVarMap; |
3520 | + bool allVarsAssigned = true; |
3521 | + auto interval = &placeArcInterval.second._intervalTupleVec[j]._intervals[i]; |
3522 | + |
3523 | + populateLocalMap(&placeArcInterval.second, varMap, localVarMap, interval, allVarsAssigned, j); |
3524 | + |
3525 | + for(auto& varTuplePair : varMap){ |
3526 | + if(localVarMap.count(varTuplePair.first) == 0){ |
3527 | + localVarMap[varTuplePair.first] = std::move(varTuplePair.second); |
3528 | + } |
3529 | + } |
3530 | + |
3531 | + if(allVarsAssigned){ |
3532 | + newVarMapVec.push_back(std::move(localVarMap)); |
3533 | + } |
3534 | + } |
3535 | + } |
3536 | + variableMaps = std::move(newVarMapVec); |
3537 | + } |
3538 | + //If we did not find any intervals for an arc, then the transition cannot be activated |
3539 | + if(variableMaps.empty()){ |
3540 | + return false; |
3541 | + } |
3542 | + } |
3543 | + } |
3544 | + return true; |
3545 | + } |
3546 | + }; |
3547 | +} |
3548 | + |
3549 | +#endif /* INTERVALGENERATOR_H */ |
3550 | \ No newline at end of file |
3551 | |
3552 | === added file 'include/PetriEngine/Colored/Intervals.h' |
3553 | --- include/PetriEngine/Colored/Intervals.h 1970-01-01 00:00:00 +0000 |
3554 | +++ include/PetriEngine/Colored/Intervals.h 2021-04-02 18:07:40 +0000 |
3555 | @@ -0,0 +1,630 @@ |
3556 | +/* Copyright (C) 2020 Alexander Bilgram <alexander@bilgram.dk>, |
3557 | + * Peter Haar Taankvist <ptaankvist@gmail.com>, |
3558 | + * Thomas Pedersen <thomas.pedersen@stofanet.dk> |
3559 | + * |
3560 | + * This program is free software: you can redistribute it and/or modify |
3561 | + * it under the terms of the GNU General Public License as published by |
3562 | + * the Free Software Foundation, either version 3 of the License, or |
3563 | + * (at your option) any later version. |
3564 | + * |
3565 | + * This program is distributed in the hope that it will be useful, |
3566 | + * but WITHOUT ANY WARRANTY; without even the implied warranty of |
3567 | + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
3568 | + * GNU General Public License for more details. |
3569 | + * |
3570 | + * You should have received a copy of the GNU General Public License |
3571 | + * along with this program. If not, see <http://www.gnu.org/licenses/>. |
3572 | + */ |
3573 | + |
3574 | +#ifndef INTERVALS_H |
3575 | +#define INTERVALS_H |
3576 | + |
3577 | +#include "../TAR/range.h" |
3578 | +#include <set> |
3579 | +#include <unordered_map> |
3580 | +#include <chrono> |
3581 | + |
3582 | + |
3583 | +namespace PetriEngine { |
3584 | + namespace Colored { |
3585 | + |
3586 | + struct interval_t { |
3587 | + std::vector<Reachability::range_t> _ranges; |
3588 | + |
3589 | + interval_t() { |
3590 | + } |
3591 | + |
3592 | + ~interval_t(){} |
3593 | + |
3594 | + interval_t(std::vector<Reachability::range_t> ranges) : _ranges(ranges) { |
3595 | + } |
3596 | + |
3597 | + size_t size(){ |
3598 | + return _ranges.size(); |
3599 | + } |
3600 | + |
3601 | + uint32_t intervalCombinations(){ |
3602 | + uint32_t product = 1; |
3603 | + for(auto range : _ranges){ |
3604 | + product *= range.size(); |
3605 | + } |
3606 | + if(_ranges.empty()){ |
3607 | + return 0; |
3608 | + } |
3609 | + return product; |
3610 | + } |
3611 | + |
3612 | + bool isSound(){ |
3613 | + for(auto range: _ranges) { |
3614 | + if(!range.isSound()){ |
3615 | + return false; |
3616 | + } |
3617 | + } |
3618 | + return true; |
3619 | + } |
3620 | + |
3621 | + void addRange(Reachability::range_t newRange) { |
3622 | + _ranges.push_back(newRange); |
3623 | + } |
3624 | + |
3625 | + void addRange(Reachability::range_t newRange, uint32_t index){ |
3626 | + _ranges.insert(_ranges.begin() + index, newRange); |
3627 | + } |
3628 | + |
3629 | + void addRange(uint32_t l, uint32_t u) { |
3630 | + _ranges.push_back(Reachability::range_t(l, u)); |
3631 | + } |
3632 | + |
3633 | + void addRange(uint32_t lower, uint32_t upper, uint32_t index){ |
3634 | + _ranges.insert(_ranges.begin() + index, Reachability::range_t(lower, upper)); |
3635 | + } |
3636 | + |
3637 | + Reachability::range_t& operator[] (size_t index) { |
3638 | + return _ranges[index]; |
3639 | + } |
3640 | + |
3641 | + Reachability::range_t& operator[] (int index) { |
3642 | + return _ranges[index]; |
3643 | + } |
3644 | + |
3645 | + Reachability::range_t& operator[] (uint32_t index) { |
3646 | + assert(index < _ranges.size()); |
3647 | + return _ranges[index]; |
3648 | + } |
3649 | + |
3650 | + Reachability::range_t& getFirst() { |
3651 | + return _ranges[0]; |
3652 | + } |
3653 | + |
3654 | + Reachability::range_t& getLast() { |
3655 | + return _ranges.back(); |
3656 | + } |
3657 | + |
3658 | + std::vector<uint32_t> getLowerIds(){ |
3659 | + std::vector<uint32_t> ids; |
3660 | + for(auto range : _ranges){ |
3661 | + ids.push_back(range._lower); |
3662 | + } |
3663 | + return ids; |
3664 | + } |
3665 | + |
3666 | + std::vector<uint32_t> getUpperIds(){ |
3667 | + std::vector<uint32_t> ids; |
3668 | + for(auto range : _ranges){ |
3669 | + ids.push_back(range._upper); |
3670 | + } |
3671 | + return ids; |
3672 | + } |
3673 | + |
3674 | + bool equals(interval_t other){ |
3675 | + if(other.size() != size()){ |
3676 | + return false; |
3677 | + } |
3678 | + for(uint32_t i = 0; i < size(); i++){ |
3679 | + auto comparisonRes = _ranges[i].compare(other[i]); |
3680 | + if(!comparisonRes.first || !comparisonRes.second){ |
3681 | + return false; |
3682 | + } |
3683 | + } |
3684 | + return true; |
3685 | + } |
3686 | + |
3687 | + uint32_t getContainedColors(){ |
3688 | + uint32_t colors = 1; |
3689 | + for(auto range: _ranges) { |
3690 | + colors *= 1+ range._upper - range._lower; |
3691 | + } |
3692 | + return colors; |
3693 | + } |
3694 | + |
3695 | + bool contains(interval_t other){ |
3696 | + if(other.size() != size()){ |
3697 | + return false; |
3698 | + } |
3699 | + for(uint32_t i = 0; i < size(); i++){ |
3700 | + if(!_ranges[i].compare(other[i]).first){ |
3701 | + return false; |
3702 | + } |
3703 | + } |
3704 | + return true; |
3705 | + } |
3706 | + |
3707 | + void constrain(interval_t other){ |
3708 | + for(uint32_t i = 0; i < _ranges.size(); i++){ |
3709 | + _ranges[i] &= other._ranges[i]; |
3710 | + } |
3711 | + } |
3712 | + |
3713 | + interval_t getOverlap(interval_t other){ |
3714 | + interval_t overlapInterval; |
3715 | + if(size() != other.size()){ |
3716 | + return overlapInterval; |
3717 | + } |
3718 | + |
3719 | + for(uint32_t i = 0; i < size(); i++){ |
3720 | + auto rangeCopy = _ranges[i]; |
3721 | + overlapInterval.addRange(rangeCopy &= other[i]); |
3722 | + } |
3723 | + |
3724 | + return overlapInterval; |
3725 | + } |
3726 | + |
3727 | + void print() { |
3728 | + for(auto range : _ranges){ |
3729 | + std::cout << " " << range._lower << "-" << range._upper << " "; |
3730 | + } |
3731 | + } |
3732 | + }; |
3733 | + |
3734 | + struct closestIntervals { |
3735 | + uint32_t intervalId1; |
3736 | + uint32_t intervalId2; |
3737 | + uint32_t distance; |
3738 | + }; |
3739 | + |
3740 | + struct intervalTuple_t { |
3741 | + std::vector<interval_t> _intervals; |
3742 | + double totalinputtime = 0; |
3743 | + |
3744 | + ~intervalTuple_t() { |
3745 | + } |
3746 | + |
3747 | + intervalTuple_t() { |
3748 | + } |
3749 | + |
3750 | + intervalTuple_t(std::vector<interval_t> ranges) : _intervals(ranges) { |
3751 | + }; |
3752 | + |
3753 | + interval_t& getFirst(){ |
3754 | + return _intervals[0]; |
3755 | + } |
3756 | + |
3757 | + interval_t& back() { |
3758 | + return _intervals.back(); |
3759 | + } |
3760 | + |
3761 | + size_t size() { |
3762 | + return _intervals.size(); |
3763 | + } |
3764 | + |
3765 | + size_t tupleSize() { |
3766 | + return _intervals[0].size(); |
3767 | + } |
3768 | + |
3769 | + uint32_t getContainedColors(){ |
3770 | + uint32_t colors = 0; |
3771 | + for (auto interval : _intervals) { |
3772 | + colors += interval.getContainedColors(); |
3773 | + } |
3774 | + return colors; |
3775 | + } |
3776 | + |
3777 | + std::pair<uint32_t,uint32_t> shiftInterval(uint32_t lower, uint32_t upper, uint32_t ctSize, int32_t modifier){ |
3778 | + int32_t lower_val = ctSize + (lower + modifier); |
3779 | + int32_t upper_val = ctSize + (upper + modifier); |
3780 | + return std::make_pair(lower_val % ctSize, upper_val % ctSize); |
3781 | + } |
3782 | + |
3783 | + uint32_t intervalCombinations(){ |
3784 | + uint32_t res = 0; |
3785 | + for(auto interval : _intervals){ |
3786 | + res += interval.intervalCombinations(); |
3787 | + } |
3788 | + return res; |
3789 | + } |
3790 | + |
3791 | + bool hasValidIntervals(){ |
3792 | + for(auto interval : _intervals) { |
3793 | + if(interval.isSound()){ |
3794 | + return true; |
3795 | + } |
3796 | + } |
3797 | + return false; |
3798 | + } |
3799 | + |
3800 | + interval_t& operator[] (size_t index) { |
3801 | + return _intervals[index]; |
3802 | + } |
3803 | + |
3804 | + interval_t& operator[] (int index) { |
3805 | + return _intervals[index]; |
3806 | + } |
3807 | + |
3808 | + interval_t& operator[] (uint32_t index) { |
3809 | + assert(index < _intervals.size()); |
3810 | + return _intervals[index]; |
3811 | + } |
3812 | + |
3813 | + interval_t isRangeEnd(std::vector<uint32_t> ids) { |
3814 | + for (uint32_t j = 0; j < _intervals.size(); j++) { |
3815 | + bool rangeEnd = true; |
3816 | + for (uint32_t i = 0; i < _intervals[j].size(); i++) { |
3817 | + auto range = _intervals[j][i]; |
3818 | + if (range._upper != ids[i]) { |
3819 | + rangeEnd = false; |
3820 | + break; |
3821 | + } |
3822 | + } |
3823 | + if(rangeEnd) { |
3824 | + if(j+1 != _intervals.size()) { |
3825 | + return _intervals[j+1]; |
3826 | + } else { |
3827 | + return getFirst(); |
3828 | + } |
3829 | + } |
3830 | + } |
3831 | + return interval_t(); |
3832 | + } |
3833 | + |
3834 | + std::vector<Colored::interval_t> shrinkIntervals(uint32_t newSize){ |
3835 | + std::vector<Colored::interval_t> resizedIntervals; |
3836 | + for(auto interval : _intervals){ |
3837 | + Colored::interval_t resizedInterval; |
3838 | + for(uint32_t i = 0; i < newSize; i++){ |
3839 | + resizedInterval.addRange(interval[i]); |
3840 | + } |
3841 | + resizedIntervals.push_back(resizedInterval); |
3842 | + } |
3843 | + return resizedIntervals; |
3844 | + } |
3845 | + |
3846 | + void addInterval(interval_t interval) { |
3847 | + uint32_t vecIndex = 0; |
3848 | + |
3849 | + if(!_intervals.empty()) { |
3850 | + assert(_intervals[0].size() == interval.size()); |
3851 | + } else { |
3852 | + _intervals.push_back(interval); |
3853 | + return; |
3854 | + } |
3855 | + |
3856 | + for (auto& localInterval : _intervals) { |
3857 | + bool overlap = true; |
3858 | + enum FoundPlace {undecided, greater, lower}; |
3859 | + FoundPlace foundPlace = undecided; |
3860 | + |
3861 | + for(uint32_t k = 0; k < interval.size(); k++){ |
3862 | + if(interval[k]._lower > localInterval[k]._upper || localInterval[k]._lower > interval[k]._upper){ |
3863 | + overlap = false; |
3864 | + } |
3865 | + if(interval[k]._lower < localInterval[k]._lower){ |
3866 | + if(foundPlace == undecided){ |
3867 | + foundPlace = lower; |
3868 | + } |
3869 | + } else if (interval[k]._lower > localInterval[k]._lower){ |
3870 | + if(foundPlace == undecided){ |
3871 | + foundPlace = greater; |
3872 | + } |
3873 | + } |
3874 | + if(!overlap && foundPlace != undecided){ |
3875 | + break; |
3876 | + } |
3877 | + } |
3878 | + |
3879 | + if(overlap) { |
3880 | + for(uint32_t k = 0; k < interval.size(); k++){ |
3881 | + localInterval[k] |= interval[k]; |
3882 | + } |
3883 | + return; |
3884 | + } else if(foundPlace == lower){ |
3885 | + break; |
3886 | + } |
3887 | + vecIndex++; |
3888 | + } |
3889 | + |
3890 | + _intervals.insert(_intervals.begin() + vecIndex, interval); |
3891 | + } |
3892 | + |
3893 | + void constrainLower(std::vector<uint32_t> values, bool strict) { |
3894 | + for(uint32_t i = 0; i < _intervals.size(); i++) { |
3895 | + for(uint32_t j = 0; j < values.size(); j++){ |
3896 | + if(strict && _intervals[i][j]._lower <= values[j]){ |
3897 | + _intervals[i][j]._lower = values[j]+1; |
3898 | + } |
3899 | + else if(!strict && _intervals[i][j]._lower < values[j]){ |
3900 | + _intervals[i][j]._lower = values[j]; |
3901 | + } |
3902 | + } |
3903 | + } |
3904 | + simplify(); |
3905 | + } |
3906 | + |
3907 | + void constrainUpper(std::vector<uint32_t> values, bool strict) { |
3908 | + for(uint32_t i = 0; i < _intervals.size(); i++) { |
3909 | + for(uint32_t j = 0; j < values.size(); j++){ |
3910 | + if(strict && _intervals[i][j]._upper >= values[j]){ |
3911 | + _intervals[i][j]._upper = values[j]-1; |
3912 | + } |
3913 | + else if(!strict && _intervals[i][j]._upper > values[j]){ |
3914 | + _intervals[i][j]._upper = values[j]; |
3915 | + } |
3916 | + } |
3917 | + } |
3918 | + simplify(); |
3919 | + } |
3920 | + |
3921 | + void expandLower(std::vector<uint32_t> values) { |
3922 | + for(uint32_t i = 0; i < values.size(); i++) { |
3923 | + _intervals[0][i]._lower = std::min(values[i],_intervals[0][i]._lower); |
3924 | + } |
3925 | + } |
3926 | + |
3927 | + void expandUpper(std::vector<uint32_t> values) { |
3928 | + for(uint32_t i = 0; i < values.size(); i++) { |
3929 | + _intervals[0][i]._upper = std::max(values[i],_intervals[0][i]._upper); |
3930 | + } |
3931 | + } |
3932 | + |
3933 | + void print() { |
3934 | + for (auto interval : _intervals){ |
3935 | + std::cout << "["; |
3936 | + interval.print(); |
3937 | + std::cout << "]" << std::endl; |
3938 | + } |
3939 | + } |
3940 | + |
3941 | + std::vector<uint32_t> getLowerIds(){ |
3942 | + std::vector<uint32_t> ids; |
3943 | + for(auto interval : _intervals){ |
3944 | + if(ids.empty()){ |
3945 | + ids = interval.getLowerIds(); |
3946 | + } else { |
3947 | + for(uint32_t i = 0; i < ids.size(); i++){ |
3948 | + ids[i] = std::min(ids[i], interval[i]._lower); |
3949 | + } |
3950 | + } |
3951 | + } |
3952 | + return ids; |
3953 | + } |
3954 | + |
3955 | + std::vector<uint32_t> getLowerIds(int32_t modifier, std::vector<size_t> sizes){ |
3956 | + std::vector<uint32_t> ids; |
3957 | + for(uint32_t j = 0; j < size(); j++){ |
3958 | + auto interval = &_intervals[j]; |
3959 | + if(ids.empty()){ |
3960 | + for(uint32_t i = 0; i < ids.size(); i++){ |
3961 | + auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier); |
3962 | + if(shiftedInterval.first > shiftedInterval.second){ |
3963 | + ids.push_back(0); |
3964 | + } else { |
3965 | + ids.push_back(shiftedInterval.first); |
3966 | + } |
3967 | + } |
3968 | + } else { |
3969 | + for(uint32_t i = 0; i < ids.size(); i++){ |
3970 | + if(ids[i] == 0){ |
3971 | + continue; |
3972 | + } |
3973 | + auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier); |
3974 | + if(shiftedInterval.first > shiftedInterval.second){ |
3975 | + ids[i] = 0; |
3976 | + } else { |
3977 | + ids[i] = std::max(ids[i], shiftedInterval.first); |
3978 | + } |
3979 | + } |
3980 | + } |
3981 | + } |
3982 | + return ids; |
3983 | + } |
3984 | + |
3985 | + std::vector<uint32_t> getUpperIds(){ |
3986 | + std::vector<uint32_t> ids; |
3987 | + for(auto interval : _intervals){ |
3988 | + if(ids.empty()){ |
3989 | + ids = interval.getUpperIds(); |
3990 | + } else { |
3991 | + for(uint32_t i = 0; i < ids.size(); i++){ |
3992 | + ids[i] = std::max(ids[i], interval[i]._upper); |
3993 | + } |
3994 | + } |
3995 | + } |
3996 | + return ids; |
3997 | + } |
3998 | + |
3999 | + std::vector<uint32_t> getUpperIds(int32_t modifier, std::vector<size_t> sizes){ |
4000 | + std::vector<uint32_t> ids; |
4001 | + for(uint32_t j = 0; j < size(); j++){ |
4002 | + auto interval = &_intervals[j]; |
4003 | + if(ids.empty()){ |
4004 | + for(uint32_t i = 0; i < ids.size(); i++){ |
4005 | + auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier); |
4006 | + |
4007 | + if(shiftedInterval.first > shiftedInterval.second){ |
4008 | + ids.push_back(sizes[i]-1); |
4009 | + } else { |
4010 | + ids.push_back(shiftedInterval.second); |
4011 | + } |
4012 | + } |
4013 | + } else { |
4014 | + for(uint32_t i = 0; i < ids.size(); i++){ |
4015 | + if(ids[i] == sizes[i]-1){ |
4016 | + continue; |
4017 | + } |
4018 | + auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier); |
4019 | + |
4020 | + if(shiftedInterval.first > shiftedInterval.second){ |
4021 | + ids[i] = sizes[i]-1; |
4022 | + } else { |
4023 | + ids[i] = std::max(ids[i], shiftedInterval.second); |
4024 | + } |
4025 | + } |
4026 | + } |
4027 | + } |
4028 | + return ids; |
4029 | + } |
4030 | + |
4031 | + void applyModifier(int32_t modifier, std::vector<size_t> sizes){ |
4032 | + std::vector<interval_t> collectedIntervals; |
4033 | + for(auto& interval : _intervals){ |
4034 | + std::vector<interval_t> newIntervals; |
4035 | + newIntervals.push_back(std::move(interval)); |
4036 | + for(uint32_t i = 0; i < interval.size(); i++){ |
4037 | + std::vector<interval_t> tempIntervals; |
4038 | + for(auto& interval1 : newIntervals){ |
4039 | + auto shiftedInterval = shiftInterval(interval1[i]._lower, interval1[i]._upper, sizes[i], modifier); |
4040 | + |
4041 | + if(shiftedInterval.first > shiftedInterval.second){ |
4042 | + auto newInterval = interval1; |
4043 | + |
4044 | + interval1[i]._lower = 0; |
4045 | + interval1[i]._upper = shiftedInterval.second; |
4046 | + |
4047 | + newInterval[i]._lower = shiftedInterval.first; |
4048 | + newInterval[i]._upper = sizes[i]-1; |
4049 | + tempIntervals.push_back(std::move(newInterval)); |
4050 | + }else { |
4051 | + interval1[i]._lower = shiftedInterval.first; |
4052 | + interval1[i]._upper = shiftedInterval.second; |
4053 | + } |
4054 | + } |
4055 | + newIntervals.insert(newIntervals.end(), tempIntervals.begin(), tempIntervals.end()); |
4056 | + } |
4057 | + collectedIntervals.insert(collectedIntervals.end(), newIntervals.begin(), newIntervals.end()); |
4058 | + } |
4059 | + |
4060 | + _intervals = std::move(collectedIntervals); |
4061 | + } |
4062 | + |
4063 | + bool contains(interval_t interval){ |
4064 | + for(auto localInterval : _intervals){ |
4065 | + if(localInterval.contains(interval)){ |
4066 | + return true; |
4067 | + } |
4068 | + } |
4069 | + return false; |
4070 | + } |
4071 | + |
4072 | + void removeInterval(interval_t interval) { |
4073 | + for (uint32_t i = 0; i < _intervals.size(); i++) { |
4074 | + if(interval.equals(_intervals[i])){ |
4075 | + removeInterval(i); |
4076 | + return; |
4077 | + } |
4078 | + } |
4079 | + } |
4080 | + |
4081 | + void removeInterval(uint32_t index) { |
4082 | + _intervals.erase(_intervals.begin() + index); |
4083 | + } |
4084 | + |
4085 | + |
4086 | + |
4087 | + void restrict(uint32_t k){ |
4088 | + simplify(); |
4089 | + if(k == 0){ |
4090 | + return; |
4091 | + } |
4092 | + |
4093 | + while (size() > k){ |
4094 | + closestIntervals closestInterval = getClosestIntervals(); |
4095 | + auto interval = &_intervals[closestInterval.intervalId1]; |
4096 | + auto otherInterval = &_intervals[closestInterval.intervalId2]; |
4097 | + |
4098 | + for(uint32_t l = 0; l < interval->size(); l++) { |
4099 | + interval->operator[](l) |= otherInterval->operator[](l); |
4100 | + } |
4101 | + |
4102 | + _intervals.erase(_intervals.begin() + closestInterval.intervalId2); |
4103 | + |
4104 | + } |
4105 | + } |
4106 | + |
4107 | + closestIntervals getClosestIntervals(){ |
4108 | + closestIntervals currentBest = {0,0, UINT32_MAX}; |
4109 | + for (uint32_t i = 0; i < size()-1; i++) { |
4110 | + auto interval = &_intervals[i]; |
4111 | + for(uint32_t j = i+1; j < size(); j++){ |
4112 | + auto otherInterval = &_intervals[j]; |
4113 | + uint32_t dist = 0; |
4114 | + |
4115 | + for(uint32_t k = 0; k < interval->size(); k++) { |
4116 | + int32_t val1 = otherInterval->operator[](k)._lower - interval->operator[](k)._upper; |
4117 | + int32_t val2 = interval->operator[](k)._lower - otherInterval->operator[](k)._upper; |
4118 | + dist += std::max(0, std::max(val1, val2)); |
4119 | + if(dist >= currentBest.distance){ |
4120 | + break; |
4121 | + } |
4122 | + } |
4123 | + |
4124 | + if(dist < currentBest.distance){ |
4125 | + currentBest.distance = dist; |
4126 | + currentBest.intervalId1 = i; |
4127 | + currentBest.intervalId2 = j; |
4128 | + |
4129 | + //if the distance is 1 we cannot find any intervals that are closer so we stop searching |
4130 | + if(currentBest.distance == 1){ |
4131 | + return currentBest; |
4132 | + } |
4133 | + } |
4134 | + } |
4135 | + } |
4136 | + return currentBest; |
4137 | + } |
4138 | + |
4139 | + void simplify() { |
4140 | + std::set<uint32_t> rangesToRemove; |
4141 | + if(_intervals.empty()){ |
4142 | + return; |
4143 | + } |
4144 | + |
4145 | + for (uint32_t i = 0; i < _intervals.size(); i++) { |
4146 | + auto interval = &_intervals[i]; |
4147 | + if(!interval->isSound()){ |
4148 | + rangesToRemove.insert(i); |
4149 | + continue; |
4150 | + } |
4151 | + for(uint32_t j = i+1; j < _intervals.size(); j++){ |
4152 | + auto otherInterval = &_intervals[j]; |
4153 | + |
4154 | + if(!otherInterval->isSound()){ |
4155 | + continue; |
4156 | + } |
4157 | + bool overlap = true; |
4158 | + |
4159 | + if(overlap){ |
4160 | + for(uint32_t k = 0; k < interval->size(); k++) { |
4161 | + if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper || otherInterval->operator[](k)._lower > interval->operator[](k)._upper) { |
4162 | + overlap = false; |
4163 | + break; |
4164 | + } |
4165 | + } |
4166 | + } |
4167 | + |
4168 | + if(overlap) { |
4169 | + for(uint32_t l = 0; l < interval->size(); l++) { |
4170 | + interval->operator[](l) |= otherInterval->operator[](l); |
4171 | + } |
4172 | + rangesToRemove.insert(j); |
4173 | + } |
4174 | + } |
4175 | + } |
4176 | + for (auto i = rangesToRemove.rbegin(); i != rangesToRemove.rend(); ++i) { |
4177 | + _intervals.erase(_intervals.begin() + *i); |
4178 | + } |
4179 | + } |
4180 | + }; |
4181 | + } |
4182 | +} |
4183 | + |
4184 | + |
4185 | +#endif /* INTERVALS_H */ |
4186 | \ No newline at end of file |
4187 | |
4188 | === added file 'include/PetriEngine/PQL/CTLVisitor.h' |
4189 | --- include/PetriEngine/PQL/CTLVisitor.h 1970-01-01 00:00:00 +0000 |
4190 | +++ include/PetriEngine/PQL/CTLVisitor.h 2021-04-02 18:07:40 +0000 |
4191 | @@ -0,0 +1,197 @@ |
4192 | +#ifndef VERIFYPN_CTLVISITOR_H |
4193 | +#define VERIFYPN_CTLVISITOR_H |
4194 | + |
4195 | +#include "Visitor.h" |
4196 | + |
4197 | +namespace PetriEngine::PQL { |
4198 | + |
4199 | + enum CTLSyntaxType {BOOLEAN, PATH, ERROR = -1}; |
4200 | + |
4201 | + class IsCTLVisitor : public Visitor { |
4202 | + public: |
4203 | + bool isCTL = true; |
4204 | + |
4205 | + protected: |
4206 | + void _accept(const NotCondition *element) override; |
4207 | + |
4208 | + void _accept(const AndCondition *element) override; |
4209 | + |
4210 | + void _accept(const OrCondition *element) override; |
4211 | + |
4212 | + void _accept(const LessThanCondition *element) override; |
4213 | + |
4214 | + void _accept(const LessThanOrEqualCondition *element) override; |
4215 | + |
4216 | + void _accept(const EqualCondition *element) override; |
4217 | + |
4218 | + void _accept(const NotEqualCondition *element) override; |
4219 | + |
4220 | + void _accept(const DeadlockCondition *element) override; |
4221 | + |
4222 | + void _accept(const CompareConjunction *element) override; |
4223 | + |
4224 | + void _accept(const UnfoldedUpperBoundsCondition *element) override; |
4225 | + |
4226 | + void _accept(const EFCondition *condition) override; |
4227 | + |
4228 | + void _accept(const EGCondition *condition) override; |
4229 | + |
4230 | + void _accept(const AGCondition *condition) override; |
4231 | + |
4232 | + void _accept(const AFCondition *condition) override; |
4233 | + |
4234 | + void _accept(const EXCondition *condition) override; |
4235 | + |
4236 | + void _accept(const AXCondition *condition) override; |
4237 | + |
4238 | + void _accept(const EUCondition *condition) override; |
4239 | + |
4240 | + void _accept(const AUCondition *condition) override; |
4241 | + |
4242 | + void _accept(const ACondition *condition) override; |
4243 | + |
4244 | + void _accept(const ECondition *condition) override; |
4245 | + |
4246 | + void _accept(const GCondition *condition) override; |
4247 | + |
4248 | + void _accept(const FCondition *condition) override; |
4249 | + |
4250 | + void _accept(const XCondition *condition) override; |
4251 | + |
4252 | + void _accept(const UntilCondition *condition) override; |
4253 | + |
4254 | + void _accept(const UnfoldedFireableCondition *element) override; |
4255 | + |
4256 | + void _accept(const FireableCondition *element) override; |
4257 | + |
4258 | + void _accept(const UpperBoundsCondition *element) override; |
4259 | + |
4260 | + void _accept(const LivenessCondition *element) override; |
4261 | + |
4262 | + void _accept(const KSafeCondition *element) override; |
4263 | + |
4264 | + void _accept(const QuasiLivenessCondition *element) override; |
4265 | + |
4266 | + void _accept(const StableMarkingCondition *element) override; |
4267 | + |
4268 | + void _accept(const BooleanCondition *element) override; |
4269 | + |
4270 | + void _accept(const UnfoldedIdentifierExpr *element) override; |
4271 | + |
4272 | + void _accept(const LiteralExpr *element) override; |
4273 | + |
4274 | + void _accept(const PlusExpr *element) override; |
4275 | + |
4276 | + void _accept(const MultiplyExpr *element) override; |
4277 | + |
4278 | + void _accept(const MinusExpr *element) override; |
4279 | + |
4280 | + void _accept(const SubtractExpr *element) override; |
4281 | + |
4282 | + void _accept(const IdentifierExpr *element) override; |
4283 | + |
4284 | + private: |
4285 | + CTLSyntaxType _cur_type; |
4286 | + |
4287 | + void _accept(const LogicalCondition *element); |
4288 | + |
4289 | + void _accept(const CompareCondition *element); |
4290 | + }; |
4291 | + |
4292 | + class AsCTL : public Visitor { |
4293 | + public: |
4294 | + Condition_ptr _ctl_query = nullptr; |
4295 | + Expr_ptr _expression = nullptr; |
4296 | + |
4297 | + protected: |
4298 | + void _accept(const NotCondition *element) override; |
4299 | + |
4300 | + void _accept(const AndCondition *element) override; |
4301 | + |
4302 | + void _accept(const OrCondition *element) override; |
4303 | + |
4304 | + void _accept(const LessThanCondition *element) override; |
4305 | + |
4306 | + void _accept(const LessThanOrEqualCondition *element) override; |
4307 | + |
4308 | + void _accept(const EqualCondition *element) override; |
4309 | + |
4310 | + void _accept(const NotEqualCondition *element) override; |
4311 | + |
4312 | + void _accept(const DeadlockCondition *element) override; |
4313 | + |
4314 | + void _accept(const CompareConjunction *element) override; |
4315 | + |
4316 | + void _accept(const UnfoldedUpperBoundsCondition *element) override; |
4317 | + |
4318 | + void _accept(const EFCondition *condition) override; |
4319 | + |
4320 | + void _accept(const EGCondition *condition) override; |
4321 | + |
4322 | + void _accept(const AGCondition *condition) override; |
4323 | + |
4324 | + void _accept(const AFCondition *condition) override; |
4325 | + |
4326 | + void _accept(const EXCondition *condition) override; |
4327 | + |
4328 | + void _accept(const AXCondition *condition) override; |
4329 | + |
4330 | + void _accept(const EUCondition *condition) override; |
4331 | + |
4332 | + void _accept(const AUCondition *condition) override; |
4333 | + |
4334 | + void _accept(const ACondition *condition) override; |
4335 | + |
4336 | + void _accept(const ECondition *condition) override; |
4337 | + |
4338 | + void _accept(const GCondition *condition) override; |
4339 | + |
4340 | + void _accept(const FCondition *condition) override; |
4341 | + |
4342 | + void _accept(const XCondition *condition) override; |
4343 | + |
4344 | + void _accept(const UntilCondition *condition) override; |
4345 | + |
4346 | + void _accept(const UnfoldedFireableCondition *element) override; |
4347 | + |
4348 | + void _accept(const FireableCondition *element) override; |
4349 | + |
4350 | + void _accept(const UpperBoundsCondition *element) override; |
4351 | + |
4352 | + void _accept(const LivenessCondition *element) override; |
4353 | + |
4354 | + void _accept(const KSafeCondition *element) override; |
4355 | + |
4356 | + void _accept(const QuasiLivenessCondition *element) override; |
4357 | + |
4358 | + void _accept(const StableMarkingCondition *element) override; |
4359 | + |
4360 | + void _accept(const BooleanCondition *element) override; |
4361 | + |
4362 | + void _accept(const UnfoldedIdentifierExpr *element) override; |
4363 | + |
4364 | + void _accept(const LiteralExpr *element) override; |
4365 | + |
4366 | + void _accept(const PlusExpr *element) override; |
4367 | + |
4368 | + void _accept(const MultiplyExpr *element) override; |
4369 | + |
4370 | + void _accept(const MinusExpr *element) override; |
4371 | + |
4372 | + void _accept(const SubtractExpr *element) override; |
4373 | + |
4374 | + void _accept(const IdentifierExpr *element) override; |
4375 | + |
4376 | + private: |
4377 | + template<typename T> |
4378 | + void _acceptNary(const T *element); |
4379 | + |
4380 | + template<typename T> |
4381 | + Expr_ptr copy_narry_expr(const T* el); |
4382 | + |
4383 | + template<typename T> |
4384 | + std::shared_ptr<T> copy_compare_condition(const T *element); |
4385 | + }; |
4386 | +} |
4387 | + |
4388 | +#endif //VERIFYPN_CTLVISITOR_H |
4389 | |
4390 | === modified file 'include/PetriEngine/PQL/Contexts.h' |
4391 | --- include/PetriEngine/PQL/Contexts.h 2020-04-27 14:47:10 +0000 |
4392 | +++ include/PetriEngine/PQL/Contexts.h 2021-04-02 18:07:40 +0000 |
4393 | @@ -38,8 +38,8 @@ |
4394 | /** Context provided for context analysis */ |
4395 | class AnalysisContext { |
4396 | protected: |
4397 | - const unordered_map<std::string, uint32_t>& _placeNames; |
4398 | - const unordered_map<std::string, uint32_t>& _transitionNames; |
4399 | + const std::unordered_map<std::string, uint32_t>& _placeNames; |
4400 | + const std::unordered_map<std::string, uint32_t>& _transitionNames; |
4401 | const PetriNet* _net; |
4402 | std::vector<ExprError> _errors; |
4403 | public: |
4404 | @@ -176,7 +176,7 @@ |
4405 | |
4406 | SimplificationContext(const MarkVal* marking, |
4407 | const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, |
4408 | - LPCache* cache) |
4409 | + Simplification::LPCache* cache) |
4410 | : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) { |
4411 | _negated = false; |
4412 | _marking = marking; |
4413 | @@ -222,8 +222,8 @@ |
4414 | } |
4415 | |
4416 | uint32_t getLpTimeout() const; |
4417 | - |
4418 | - LPCache* cache() const |
4419 | + |
4420 | + Simplification::LPCache* cache() const |
4421 | { |
4422 | return _cache; |
4423 | } |
4424 | @@ -237,7 +237,7 @@ |
4425 | const PetriNet* _net; |
4426 | uint32_t _queryTimeout, _lpTimeout; |
4427 | std::chrono::high_resolution_clock::time_point _start; |
4428 | - LPCache* _cache; |
4429 | + Simplification::LPCache* _cache; |
4430 | mutable glp_prob* _base_lp = nullptr; |
4431 | |
4432 | glp_prob* buildBase() const; |
4433 | |
4434 | === modified file 'include/PetriEngine/PQL/Expressions.h' |
4435 | --- include/PetriEngine/PQL/Expressions.h 2020-06-02 16:20:24 +0000 |
4436 | +++ include/PetriEngine/PQL/Expressions.h 2021-04-02 18:07:40 +0000 |
4437 | @@ -34,7 +34,7 @@ |
4438 | |
4439 | namespace PetriEngine { |
4440 | namespace PQL { |
4441 | - |
4442 | + |
4443 | std::string generateTabs(uint32_t tabs); |
4444 | class CompareCondition; |
4445 | class NotCondition; |
4446 | @@ -55,19 +55,22 @@ |
4447 | for(auto& e : _exprs) sum += e->formulaSize(); |
4448 | return sum + 1; |
4449 | } |
4450 | - void toString(std::ostream&) const override; |
4451 | bool placeFree() const override; |
4452 | auto& expressions() const { return _exprs; } |
4453 | + size_t operands() const { return _exprs.size(); } |
4454 | + const Expr_ptr &operator[](size_t i) const { |
4455 | + return _exprs[i]; |
4456 | + } |
4457 | protected: |
4458 | virtual int apply(int v1, int v2) const = 0; |
4459 | virtual std::string op() const = 0; |
4460 | std::vector<Expr_ptr> _exprs; |
4461 | virtual int32_t preOp(const EvaluationContext& context) const; |
4462 | }; |
4463 | - |
4464 | + |
4465 | class PlusExpr; |
4466 | class MultiplyExpr; |
4467 | - |
4468 | + |
4469 | class CommutativeExpr : public NaryExpr |
4470 | { |
4471 | public: |
4472 | @@ -80,7 +83,6 @@ |
4473 | for(auto& e : _exprs) sum += e->formulaSize(); |
4474 | return sum + 1; |
4475 | } |
4476 | - void toString(std::ostream&) const override; |
4477 | bool placeFree() const override; |
4478 | auto constant() const { return _constant; } |
4479 | auto& places() const { return _ids; } |
4480 | @@ -98,13 +100,12 @@ |
4481 | public: |
4482 | |
4483 | PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk = false); |
4484 | - |
4485 | + |
4486 | Expr::Types type() const override; |
4487 | Member constraint(SimplificationContext& context) const override; |
4488 | void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override; |
4489 | bool tk = false; |
4490 | - void incr(ReducingSuccessorGenerator& generator) const override; |
4491 | - void decr(ReducingSuccessorGenerator& generator) const override; |
4492 | + |
4493 | void visit(Visitor& visitor) const override; |
4494 | protected: |
4495 | int apply(int v1, int v2) const override; |
4496 | @@ -122,8 +123,7 @@ |
4497 | Expr::Types type() const override; |
4498 | Member constraint(SimplificationContext& context) const override; |
4499 | void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override; |
4500 | - void incr(ReducingSuccessorGenerator& generator) const override; |
4501 | - void decr(ReducingSuccessorGenerator& generator) const override; |
4502 | + |
4503 | void toBinary(std::ostream&) const override; |
4504 | void visit(Visitor& visitor) const override; |
4505 | protected: |
4506 | @@ -140,8 +140,7 @@ |
4507 | Expr::Types type() const override; |
4508 | Member constraint(SimplificationContext& context) const override; |
4509 | void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override; |
4510 | - void incr(ReducingSuccessorGenerator& generator) const override; |
4511 | - void decr(ReducingSuccessorGenerator& generator) const override; |
4512 | + |
4513 | void visit(Visitor& visitor) const override; |
4514 | protected: |
4515 | int apply(int v1, int v2) const override; |
4516 | @@ -158,13 +157,11 @@ |
4517 | } |
4518 | void analyze(AnalysisContext& context) override; |
4519 | int evaluate(const EvaluationContext& context) override; |
4520 | - void toString(std::ostream&) const override; |
4521 | Expr::Types type() const override; |
4522 | Member constraint(SimplificationContext& context) const override; |
4523 | void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override; |
4524 | void toBinary(std::ostream&) const override; |
4525 | - void incr(ReducingSuccessorGenerator& generator) const override; |
4526 | - void decr(ReducingSuccessorGenerator& generator) const override; |
4527 | + |
4528 | void visit(Visitor& visitor) const override; |
4529 | int formulaSize() const override{ |
4530 | return _expr->formulaSize() + 1; |
4531 | @@ -181,14 +178,13 @@ |
4532 | |
4533 | LiteralExpr(int value) : _value(value) { |
4534 | } |
4535 | + LiteralExpr(const LiteralExpr&) = default; |
4536 | void analyze(AnalysisContext& context) override; |
4537 | int evaluate(const EvaluationContext& context) override; |
4538 | - void toString(std::ostream&) const override; |
4539 | Expr::Types type() const override; |
4540 | void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override; |
4541 | void toBinary(std::ostream&) const override; |
4542 | - void incr(ReducingSuccessorGenerator& generator) const override; |
4543 | - void decr(ReducingSuccessorGenerator& generator) const override; |
4544 | + |
4545 | void visit(Visitor& visitor) const override; |
4546 | int formulaSize() const override{ |
4547 | return 1; |
4548 | @@ -206,29 +202,18 @@ |
4549 | class IdentifierExpr : public Expr { |
4550 | public: |
4551 | IdentifierExpr(const std::string& name) : _name(name) {} |
4552 | + IdentifierExpr(const IdentifierExpr&) = default; |
4553 | void analyze(AnalysisContext& context) override; |
4554 | int evaluate(const EvaluationContext& context) override { |
4555 | return _compiled->evaluate(context); |
4556 | } |
4557 | - void toString(std::ostream& os) const override { |
4558 | - if(_compiled) |
4559 | - _compiled->toString(os); |
4560 | - else |
4561 | - os << _name; |
4562 | - } |
4563 | - Expr::Types type() const override { |
4564 | + [[nodiscard]] Expr::Types type() const override { |
4565 | if(_compiled) return _compiled->type(); |
4566 | return Expr::IdentifierExpr; |
4567 | } |
4568 | void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override { |
4569 | _compiled->toXML(os, tabs, tokencount); |
4570 | } |
4571 | - void incr(ReducingSuccessorGenerator& generator) const override { |
4572 | - _compiled->incr(generator); |
4573 | - } |
4574 | - void decr(ReducingSuccessorGenerator& generator) const override { |
4575 | - _compiled->decr(generator); |
4576 | - } |
4577 | int formulaSize() const override { |
4578 | if(_compiled) return _compiled->formulaSize(); |
4579 | return 1; |
4580 | @@ -241,11 +226,20 @@ |
4581 | Member constraint(SimplificationContext& context) const override { |
4582 | return _compiled->constraint(context); |
4583 | } |
4584 | - |
4585 | + |
4586 | void toBinary(std::ostream& s) const override { |
4587 | _compiled->toBinary(s); |
4588 | } |
4589 | - void visit(Visitor& visitor) const override; |
4590 | + void visit(Visitor& visitor) const override; |
4591 | + |
4592 | + [[nodiscard]] const std::string &name() const { |
4593 | + return _name; |
4594 | + } |
4595 | + |
4596 | + [[nodiscard]] const Expr_ptr &compiled() const { |
4597 | + return _compiled; |
4598 | + } |
4599 | + |
4600 | private: |
4601 | std::string _name; |
4602 | Expr_ptr _compiled; |
4603 | @@ -257,18 +251,17 @@ |
4604 | UnfoldedIdentifierExpr(const std::string& name, int offest) |
4605 | : _offsetInMarking(offest), _name(name) { |
4606 | } |
4607 | - |
4608 | + |
4609 | UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) { |
4610 | } |
4611 | |
4612 | + UnfoldedIdentifierExpr(const UnfoldedIdentifierExpr&) = default; |
4613 | + |
4614 | void analyze(AnalysisContext& context) override; |
4615 | int evaluate(const EvaluationContext& context) override; |
4616 | - void toString(std::ostream&) const override; |
4617 | Expr::Types type() const override; |
4618 | void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override; |
4619 | void toBinary(std::ostream&) const override; |
4620 | - void incr(ReducingSuccessorGenerator& generator) const override; |
4621 | - void decr(ReducingSuccessorGenerator& generator) const override; |
4622 | int formulaSize() const override{ |
4623 | return 1; |
4624 | } |
4625 | @@ -276,7 +269,7 @@ |
4626 | int offset() const { |
4627 | return _offsetInMarking; |
4628 | } |
4629 | - const std::string& name() |
4630 | + const std::string& name() const |
4631 | { |
4632 | return _name; |
4633 | } |
4634 | @@ -311,18 +304,14 @@ |
4635 | |
4636 | void toXML(std::ostream& out, uint32_t tabs) const override |
4637 | { _compiled->toXML(out, tabs); } |
4638 | - void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override |
4639 | - { _compiled->findInteresting(generator, negated);} |
4640 | + |
4641 | + |
4642 | Quantifier getQuantifier() const override |
4643 | { return _compiled->getQuantifier(); } |
4644 | Path getPath() const override { return _compiled->getPath(); } |
4645 | CTLType getQueryType() const override { return _compiled->getQueryType(); } |
4646 | bool containsNext() const override { return _compiled->containsNext(); } |
4647 | bool nestedDeadlock() const override { return _compiled->nestedDeadlock(); } |
4648 | -#ifdef VERIFYPN_TAR |
4649 | - virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const |
4650 | - { return _compiled->encodeSat(net, context, uses, incremented); } |
4651 | -#endif |
4652 | int formulaSize() const override{ |
4653 | return _compiled->formulaSize(); |
4654 | } |
4655 | @@ -344,14 +333,13 @@ |
4656 | if (_compiled) _compiled->analyze(context); |
4657 | else _analyze(context); |
4658 | } |
4659 | - void toString(std::ostream &out) const { |
4660 | - if (_compiled) _compiled->toString(out); |
4661 | - else _toString(out); |
4662 | + public: |
4663 | + const Condition_ptr &getCompiled() const { |
4664 | + return _compiled; |
4665 | } |
4666 | |
4667 | protected: |
4668 | virtual void _analyze(AnalysisContext& context) = 0; |
4669 | - virtual void _toString(std::ostream& out) const = 0; |
4670 | virtual Condition_ptr clone() = 0; |
4671 | Condition_ptr _compiled = nullptr; |
4672 | }; |
4673 | @@ -373,7 +361,6 @@ |
4674 | Result evalAndSet(const EvaluationContext& context) override; |
4675 | void visit(Visitor&) const override; |
4676 | uint32_t distance(DistanceContext& context) const override; |
4677 | - void toString(std::ostream&) const override; |
4678 | void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override; |
4679 | Retval simplify(SimplificationContext& context) const override; |
4680 | bool isReachability(uint32_t depth) const override; |
4681 | @@ -381,7 +368,7 @@ |
4682 | Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4683 | void toXML(std::ostream&, uint32_t tabs) const override; |
4684 | void toBinary(std::ostream&) const override; |
4685 | - void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override; |
4686 | + |
4687 | Quantifier getQuantifier() const override { return Quantifier::NEG; } |
4688 | Path getPath() const override { return Path::pError; } |
4689 | CTLType getQueryType() const override { return CTLType::LOPERATOR; } |
4690 | @@ -393,18 +380,18 @@ |
4691 | Condition_ptr _cond; |
4692 | bool _temporal = false; |
4693 | }; |
4694 | - |
4695 | - |
4696 | - /******************** TEMPORAL OPERATORS ********************/ |
4697 | - |
4698 | + |
4699 | + |
4700 | + /******************** TEMPORAL OPERATORS ********************/ |
4701 | + |
4702 | class QuantifierCondition : public Condition |
4703 | { |
4704 | public: |
4705 | - virtual bool isTemporal() const override { return true;} |
4706 | + bool isTemporal() const override { return true;} |
4707 | CTLType getQueryType() const override { return CTLType::PATHQEURY; } |
4708 | virtual const Condition_ptr& operator[] (size_t i) const = 0; |
4709 | }; |
4710 | - |
4711 | + |
4712 | class SimpleQuantifierCondition : public QuantifierCondition { |
4713 | public: |
4714 | SimpleQuantifierCondition(const Condition_ptr cond) { |
4715 | @@ -414,24 +401,174 @@ |
4716 | int formulaSize() const override{ |
4717 | return _cond->formulaSize() + 1; |
4718 | } |
4719 | - |
4720 | + |
4721 | void analyze(AnalysisContext& context) override; |
4722 | Result evaluate(const EvaluationContext& context) override; |
4723 | Result evalAndSet(const EvaluationContext& context) override; |
4724 | - void toString(std::ostream&) const override; |
4725 | void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override; |
4726 | void toBinary(std::ostream& out) const override; |
4727 | - void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override; |
4728 | + |
4729 | virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;} |
4730 | - virtual bool containsNext() const override { return _cond->containsNext(); } |
4731 | + bool containsNext() const override { return _cond->containsNext(); } |
4732 | bool nestedDeadlock() const override { return _cond->nestedDeadlock(); } |
4733 | private: |
4734 | virtual std::string op() const = 0; |
4735 | - |
4736 | + |
4737 | protected: |
4738 | Condition_ptr _cond; |
4739 | }; |
4740 | - |
4741 | + |
4742 | + class ECondition : public SimpleQuantifierCondition { |
4743 | + public: |
4744 | + using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4745 | + |
4746 | + Result evaluate(const EvaluationContext& context) override; |
4747 | + |
4748 | + Retval simplify(SimplificationContext& context) const override; |
4749 | + |
4750 | + bool isReachability(uint32_t depth) const override; |
4751 | + Condition_ptr prepareForReachability(bool negated) const override; |
4752 | + Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4753 | + void toXML(std::ostream&, uint32_t tabs) const override; |
4754 | + Quantifier getQuantifier() const override { return Quantifier::E; } |
4755 | + Path getPath() const override { return Path::pError; } |
4756 | + uint32_t distance(DistanceContext& context) const override { |
4757 | + // TODO implement |
4758 | + assert(false); std::cerr << "TODO implement" << std::endl; exit(0); |
4759 | + } |
4760 | + bool isLoopSensitive() const override { |
4761 | + // Other LTL Loop sensitivity depend on the outermost quantifier being an A, |
4762 | + // so if it is an E we disable loop sensitive reductions. |
4763 | + return true; |
4764 | + } |
4765 | + void visit(Visitor&) const override; |
4766 | + private: |
4767 | + std::string op() const override; |
4768 | + }; |
4769 | + |
4770 | + class ACondition : public SimpleQuantifierCondition { |
4771 | + public: |
4772 | + using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4773 | + |
4774 | + Result evaluate(const EvaluationContext& context) override; |
4775 | + |
4776 | + Retval simplify(SimplificationContext& context) const override; |
4777 | + bool isReachability(uint32_t depth) const override; |
4778 | + Condition_ptr prepareForReachability(bool negated) const override; |
4779 | + Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4780 | + void toXML(std::ostream&, uint32_t tabs) const override; |
4781 | + Quantifier getQuantifier() const override { return Quantifier::A; } |
4782 | + Path getPath() const override { return Path::pError; } |
4783 | + uint32_t distance(DistanceContext& context) const override { |
4784 | + uint32_t retval = _cond->distance(context); |
4785 | + return retval; |
4786 | + } |
4787 | + void visit(Visitor&) const override; |
4788 | + |
4789 | + private: |
4790 | + std::string op() const override; |
4791 | + }; |
4792 | + |
4793 | + class GCondition : public SimpleQuantifierCondition { |
4794 | + public: |
4795 | + using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4796 | + |
4797 | + Result evaluate(const EvaluationContext &context) override; |
4798 | + |
4799 | + bool isReachability(uint32_t depth) const override { |
4800 | + // This could potentially be a reachability formula if the parent is an A. |
4801 | + // This case is however already handled by ACondition. |
4802 | + return false; |
4803 | + } |
4804 | + |
4805 | + Condition_ptr prepareForReachability(bool negated) const override { |
4806 | + // TODO implement |
4807 | + assert(false); |
4808 | + std::cerr << "TODO implement" << std::endl; |
4809 | + exit(0); |
4810 | + } |
4811 | + |
4812 | + Condition_ptr |
4813 | + pushNegation(negstat_t &, const EvaluationContext &context, bool nested, bool negated, bool initrw) override; |
4814 | + |
4815 | + Retval simplify(SimplificationContext &context) const override; |
4816 | + |
4817 | + void toXML(std::ostream &, uint32_t tabs) const override; |
4818 | + |
4819 | + Quantifier getQuantifier() const override { return Quantifier::EMPTY; } |
4820 | + |
4821 | + Path getPath() const override { return Path::G; } |
4822 | + |
4823 | + uint32_t distance(DistanceContext &context) const override { |
4824 | + context.negate(); |
4825 | + uint32_t retval = _cond->distance(context); |
4826 | + context.negate(); |
4827 | + return retval; |
4828 | + } |
4829 | + |
4830 | + bool isLoopSensitive() const override { return true; } |
4831 | + |
4832 | + void visit(Visitor &) const override; |
4833 | + |
4834 | + private: |
4835 | + std::string op() const override; |
4836 | + }; |
4837 | + |
4838 | + class FCondition : public SimpleQuantifierCondition { |
4839 | + public: |
4840 | + using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4841 | + |
4842 | + Result evaluate(const EvaluationContext& context) override; |
4843 | + |
4844 | + Retval simplify(SimplificationContext& context) const override; |
4845 | + bool isReachability(uint32_t depth) const override { |
4846 | + // This could potentially be a reachability formula if the parent is an E. |
4847 | + // This case is however already handled by ECondition. |
4848 | + return false; |
4849 | + } |
4850 | + Condition_ptr prepareForReachability(bool negated) const override { |
4851 | + // TODO implement |
4852 | + assert(false); std::cerr << "TODO implement" << std::endl; exit(0); |
4853 | + } |
4854 | + Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4855 | + void toXML(std::ostream&, uint32_t tabs) const override; |
4856 | + Quantifier getQuantifier() const override { return Quantifier::EMPTY; } |
4857 | + Path getPath() const override { return Path::F; } |
4858 | + uint32_t distance(DistanceContext& context) const override { |
4859 | + return _cond->distance(context); |
4860 | + } |
4861 | + bool isLoopSensitive() const override { return true; } |
4862 | + void visit(Visitor&) const override; |
4863 | + private: |
4864 | + std::string op() const override; |
4865 | + }; |
4866 | + |
4867 | + class XCondition : public SimpleQuantifierCondition { |
4868 | + public: |
4869 | + using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4870 | + |
4871 | + bool isReachability(uint32_t depth) const override { |
4872 | + return false; |
4873 | + } |
4874 | + Condition_ptr prepareForReachability(bool negated) const override { |
4875 | + // TODO implement |
4876 | + assert(false); std::cerr << "TODO implement" << std::endl; exit(0); |
4877 | + } |
4878 | + Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4879 | + Retval simplify(SimplificationContext& context) const override; |
4880 | + void toXML(std::ostream&, uint32_t tabs) const override; |
4881 | + Quantifier getQuantifier() const override { return Quantifier::EMPTY; } |
4882 | + Path getPath() const override { return Path::X; } |
4883 | + uint32_t distance(DistanceContext& context) const override { |
4884 | + return _cond->distance(context); |
4885 | + } |
4886 | + bool containsNext() const override { return true; } |
4887 | + bool isLoopSensitive() const override { return true; } |
4888 | + void visit(Visitor&) const override; |
4889 | + private: |
4890 | + std::string op() const override; |
4891 | + }; |
4892 | + |
4893 | class EXCondition : public SimpleQuantifierCondition { |
4894 | public: |
4895 | using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4896 | @@ -443,24 +580,24 @@ |
4897 | Quantifier getQuantifier() const override { return Quantifier::E; } |
4898 | Path getPath() const override { return Path::X; } |
4899 | uint32_t distance(DistanceContext& context) const override; |
4900 | - bool containsNext() const override { return true; } |
4901 | + bool containsNext() const override { return true; } |
4902 | virtual bool isLoopSensitive() const override { return true; } |
4903 | void visit(Visitor&) const override; |
4904 | private: |
4905 | std::string op() const override; |
4906 | }; |
4907 | - |
4908 | + |
4909 | class EGCondition : public SimpleQuantifierCondition { |
4910 | public: |
4911 | using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4912 | - |
4913 | + |
4914 | Retval simplify(SimplificationContext& context) const override; |
4915 | bool isReachability(uint32_t depth) const override; |
4916 | Condition_ptr prepareForReachability(bool negated) const override; |
4917 | Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4918 | void toXML(std::ostream&, uint32_t tabs) const override; |
4919 | Quantifier getQuantifier() const override { return Quantifier::E; } |
4920 | - Path getPath() const override { return Path::G; } |
4921 | + Path getPath() const override { return Path::G; } |
4922 | uint32_t distance(DistanceContext& context) const override; |
4923 | Result evaluate(const EvaluationContext& context) override; |
4924 | Result evalAndSet(const EvaluationContext& context) override; |
4925 | @@ -469,18 +606,18 @@ |
4926 | private: |
4927 | std::string op() const override; |
4928 | }; |
4929 | - |
4930 | + |
4931 | class EFCondition : public SimpleQuantifierCondition { |
4932 | public: |
4933 | using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4934 | - |
4935 | + |
4936 | Retval simplify(SimplificationContext& context) const override; |
4937 | bool isReachability(uint32_t depth) const override; |
4938 | Condition_ptr prepareForReachability(bool negated) const override; |
4939 | Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4940 | void toXML(std::ostream&, uint32_t tabs) const override; |
4941 | Quantifier getQuantifier() const override { return Quantifier::E; } |
4942 | - Path getPath() const override { return Path::F; } |
4943 | + Path getPath() const override { return Path::F; } |
4944 | uint32_t distance(DistanceContext& context) const override; |
4945 | Result evaluate(const EvaluationContext& context) override; |
4946 | Result evalAndSet(const EvaluationContext& context) override; |
4947 | @@ -506,7 +643,7 @@ |
4948 | private: |
4949 | std::string op() const override; |
4950 | }; |
4951 | - |
4952 | + |
4953 | class AGCondition : public SimpleQuantifierCondition { |
4954 | public: |
4955 | using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4956 | @@ -516,7 +653,7 @@ |
4957 | Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4958 | void toXML(std::ostream&, uint32_t tabs) const override; |
4959 | Quantifier getQuantifier() const override { return Quantifier::A; } |
4960 | - Path getPath() const override { return Path::G; } |
4961 | + Path getPath() const override { return Path::G; } |
4962 | uint32_t distance(DistanceContext& context) const override; |
4963 | Result evaluate(const EvaluationContext& context) override; |
4964 | Result evalAndSet(const EvaluationContext& context) override; |
4965 | @@ -524,7 +661,7 @@ |
4966 | private: |
4967 | std::string op() const override; |
4968 | }; |
4969 | - |
4970 | + |
4971 | class AFCondition : public SimpleQuantifierCondition { |
4972 | public: |
4973 | using SimpleQuantifierCondition::SimpleQuantifierCondition; |
4974 | @@ -534,7 +671,7 @@ |
4975 | Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override; |
4976 | void toXML(std::ostream&, uint32_t tabs) const override; |
4977 | Quantifier getQuantifier() const override { return Quantifier::A; } |
4978 | - Path getPath() const override { return Path::F; } |
4979 | + Path getPath() const override { return Path::F; } |
4980 | uint32_t distance(DistanceContext& context) const override; |
4981 | Result evaluate(const EvaluationContext& context) override; |
4982 | Result evalAndSet(const EvaluationContext& context) override; |
4983 | @@ -542,8 +679,8 @@ |
4984 | virtual bool isLoopSensitive() const override { return true; } |
4985 | private: |
4986 | std::string op() const override; |
4987 | - }; |
4988 | - |
4989 | + }; |
4990 | + |
4991 | class UntilCondition : public QuantifierCondition { |
4992 | public: |
4993 | UntilCondition(const Condition_ptr cond1, const Condition_ptr cond2) { |
4994 | @@ -554,50 +691,59 @@ |
4995 | int formulaSize() const override{ |
4996 | return _cond1->formulaSize() + _cond2->formulaSize() + 1; |
4997 | } |
4998 | - |
4999 | + |
5000 | void analyze(AnalysisContext& context) override; |
The diff has been truncated for viewing.