Merge lp:~verifypn-maintainers/verifypn/interval_tar into lp:verifypn

Proposed by Peter Gjøl Jensen on 2020-07-01
Status: Merged
Approved by: Jiri Srba on 2020-09-11
Approved revision: 364
Merged at revision: 225
Proposed branch: lp:~verifypn-maintainers/verifypn/interval_tar
Merge into: lp:verifypn
Diff against target: 165007 lines (+159658/-95)
930 files modified
.bzrignore (+6/-4)
CMakeLists.txt (+99/-40)
README.md (+64/-51)
glpk-warning.patch (+10/-0)
include/CTL/Algorithm/AlgorithmTypes.h (+10/-0)
include/CTL/Algorithm/CertainZeroFPA.h (+36/-0)
include/CTL/Algorithm/FixedPointAlgorithm.h (+32/-0)
include/CTL/Algorithm/LocalFPA.h (+29/-0)
include/CTL/CTLEngine.h (+25/-0)
include/CTL/CTLResult.h (+33/-0)
include/CTL/DependencyGraph/BasicDependencyGraph.h (+23/-0)
include/CTL/DependencyGraph/Configuration.h (+40/-0)
include/CTL/DependencyGraph/Edge.h (+36/-0)
include/CTL/DependencyGraph/assignment.h (+11/-0)
include/CTL/PetriNets/OnTheFlyDG.h (+115/-0)
include/CTL/PetriNets/PetriConfig.h (+31/-0)
include/CTL/SearchStrategy/BFSSearch.h (+36/-0)
include/CTL/SearchStrategy/DFSSearch.h (+29/-0)
include/CTL/SearchStrategy/HeuristicSearch.h (+32/-0)
include/CTL/SearchStrategy/RDFSSearch.h (+34/-0)
include/CTL/SearchStrategy/SearchStrategy.h (+56/-0)
include/CTL/Stopwatch.h (+40/-0)
include/PetriEngine/AbstractPetriNetBuilder.h (+114/-0)
include/PetriEngine/Colored/ColoredNetStructures.h (+48/-0)
include/PetriEngine/Colored/ColoredPetriNetBuilder.h (+179/-0)
include/PetriEngine/Colored/Colors.h (+279/-0)
include/PetriEngine/Colored/Expressions.h (+658/-0)
include/PetriEngine/Colored/Multiset.h (+83/-0)
include/PetriEngine/NetStructures.h (+91/-0)
include/PetriEngine/PQL/Contexts.h (+250/-0)
include/PetriEngine/PQL/Expressions.h (+1221/-0)
include/PetriEngine/PQL/PQL.h (+285/-0)
include/PetriEngine/PQL/PQLParser.h (+34/-0)
include/PetriEngine/PQL/Visitor.h (+101/-0)
include/PetriEngine/PetriNet.h (+136/-0)
include/PetriEngine/PetriNetBuilder.h (+145/-0)
include/PetriEngine/Reachability/ReachabilityResult.h (+97/-0)
include/PetriEngine/Reachability/ReachabilitySearch.h (+182/-0)
include/PetriEngine/Reducer.h (+175/-0)
include/PetriEngine/ReducingSuccessorGenerator.h (+68/-0)
include/PetriEngine/STSolver.h (+55/-0)
include/PetriEngine/Simplification/LPCache.h (+54/-0)
include/PetriEngine/Simplification/LinearProgram.h (+94/-0)
include/PetriEngine/Simplification/LinearPrograms.h (+309/-0)
include/PetriEngine/Simplification/Member.h (+229/-0)
include/PetriEngine/Simplification/MurmurHash2.h (+39/-0)
include/PetriEngine/Simplification/Retval.h (+77/-0)
include/PetriEngine/Simplification/Vector.h (+130/-0)
include/PetriEngine/Structures/AlignedEncoder.h (+84/-0)
include/PetriEngine/Structures/Queue.h (+106/-0)
include/PetriEngine/Structures/State.h (+79/-0)
include/PetriEngine/Structures/StateSet.h (+258/-0)
include/PetriEngine/Structures/binarywrapper.h (+406/-0)
include/PetriEngine/Structures/light_deque.h (+78/-0)
include/PetriEngine/Structures/linked_bucket.h (+227/-0)
include/PetriEngine/SuccessorGenerator.h (+74/-0)
include/PetriEngine/TAR/AntiChain.h (+95/-0)
include/PetriEngine/TAR/ContainsVisitor.h (+230/-0)
include/PetriEngine/TAR/PlaceUseVisitor.h (+66/-0)
include/PetriEngine/TAR/RangeContext.h (+70/-0)
include/PetriEngine/TAR/RangeEvalContext.h (+66/-0)
include/PetriEngine/TAR/Solver.h (+56/-0)
include/PetriEngine/TAR/TARAutomata.h (+337/-0)
include/PetriEngine/TAR/TARReachability.h (+90/-0)
include/PetriEngine/TAR/TraceSet.h (+52/-0)
include/PetriEngine/TAR/range.h (+422/-0)
include/PetriEngine/errorcodes.h (+22/-0)
include/PetriEngine/options.h (+126/-0)
include/PetriParse/PNMLParser.h (+109/-0)
include/PetriParse/QueryBinaryParser.h (+45/-0)
include/PetriParse/QueryParser.h (+21/-0)
include/PetriParse/QueryXMLParser.h (+58/-0)
run_tests.sh (+40/-0)
src/CMakeLists.txt (+15/-0)
src/CTL/Algorithm/CMakeLists.txt (+9/-0)
src/CTL/Algorithm/CertainZeroFPA.cpp (+233/-0)
src/CTL/Algorithm/FixedPointAlgorithm.cpp (+33/-0)
src/CTL/Algorithm/LocalFPA.cpp (+123/-0)
src/CTL/CMakeLists.txt (+12/-0)
src/CTL/CTLEngine.cpp (+319/-0)
src/CTL/DependencyGraph/CMakeLists.txt (+3/-0)
src/CTL/DependencyGraph/Configuration.cpp (+5/-0)
src/CTL/PetriNets/CMakeLists.txt (+5/-0)
src/CTL/PetriNets/OnTheFlyDG.cpp (+634/-0)
src/CTL/SearchStrategy/CMakeLists.txt (+5/-0)
src/CTL/SearchStrategy/HeuristicSearch.cpp (+30/-0)
src/CTL/SearchStrategy/RDFSSearch.cpp (+38/-0)
src/CTL/SearchStrategy/SearchStrategy.cpp (+138/-0)
src/PetriEngine/CMakeLists.txt (+19/-0)
src/PetriEngine/Colored/CMakeLists.txt (+6/-0)
src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp (+302/-0)
src/PetriEngine/Colored/Colors.cpp (+218/-0)
src/PetriEngine/Colored/Multiset.cpp (+193/-0)
src/PetriEngine/PQL/CMakeLists.txt (+17/-0)
src/PetriEngine/PQL/Contexts.cpp (+141/-0)
src/PetriEngine/PQL/Expressions.cpp (+4207/-0)
src/PetriEngine/PQL/PQL.cpp (+70/-0)
src/PetriEngine/PQL/PQLQueryParser.y (+83/-0)
src/PetriEngine/PQL/PQLQueryTokens.l (+75/-0)
src/PetriEngine/PetriNet.cpp (+248/-0)
src/PetriEngine/PetriNetBuilder.cpp (+467/-0)
src/PetriEngine/Reachability/CMakeLists.txt (+7/-0)
src/PetriEngine/Reachability/ReachabilitySearch.cpp (+158/-0)
src/PetriEngine/Reachability/ResultPrinter.cpp (+239/-0)
src/PetriEngine/Reducer.cpp (+1741/-0)
src/PetriEngine/ReducingSuccessorGenerator.cpp (+318/-0)
src/PetriEngine/STSolver.cpp (+276/-0)
src/PetriEngine/Simplification/CMakeLists.txt (+5/-0)
src/PetriEngine/Simplification/LPCache.cpp (+26/-0)
src/PetriEngine/Simplification/LinearProgram.cpp (+369/-0)
src/PetriEngine/Simplification/MurmurHash2.cpp (+523/-0)
src/PetriEngine/Simplification/Vector.cpp (+40/-0)
src/PetriEngine/Structures/AlignedEncoder.cpp (+595/-0)
src/PetriEngine/Structures/CMakeLists.txt (+4/-0)
src/PetriEngine/Structures/Queue.cpp (+129/-0)
src/PetriEngine/Structures/binarywrapper.cpp (+167/-0)
src/PetriEngine/SuccessorGenerator.cpp (+114/-0)
src/PetriEngine/TAR/CMakeLists.txt (+9/-0)
src/PetriEngine/TAR/PlaceUseVisitor.cpp (+147/-0)
src/PetriEngine/TAR/RangeContext.cpp (+336/-0)
src/PetriEngine/TAR/RangeEvalContext.cpp (+268/-0)
src/PetriEngine/TAR/Solver.cpp (+616/-0)
src/PetriEngine/TAR/TARReachability.cpp (+546/-0)
src/PetriEngine/TAR/TraceSet.cpp (+397/-0)
src/PetriParse/CMakeLists.txt (+5/-0)
src/PetriParse/PNMLParser.cpp (+620/-0)
src/PetriParse/QueryBinaryParser.cpp (+289/-0)
src/PetriParse/QueryXMLParser.cpp (+600/-0)
src/VerifyPN.cpp (+1093/-0)
test_models/FMS2-untimed/model.pnml (+588/-0)
test_models/FMS2-untimed/query.xml (+2904/-0)
test_models/Kanban2-test001/model.pnml (+450/-0)
test_models/Kanban2-test001/query.xml (+436/-0)
test_models/MAPK-test001/model.pnml (+738/-0)
test_models/MAPK-test001/query.xml (+136/-0)
test_models/abp-test001/model.pnml (+424/-0)
test_models/abp-test001/query.xml (+60/-0)
test_models/abp-test002/model.pnml (+424/-0)
test_models/abp-test002/query.xml (+60/-0)
test_models/abp-test003/model.pnml (+424/-0)
test_models/abp-test003/query.xml (+60/-0)
test_models/abp-test004/model.pnml (+424/-0)
test_models/abp-test004/query.xml (+60/-0)
test_models/abp-test005/model.pnml (+174/-0)
test_models/abp-test005/query.xml (+58/-0)
test_models/abp-test006/model.pnml (+200/-0)
test_models/abp-test006/query.xml (+58/-0)
test_models/abp-test007/model.pnml (+200/-0)
test_models/abp-test007/query.xml (+58/-0)
test_models/abp-test008/model.pnml (+174/-0)
test_models/abp-test008/query.xml (+58/-0)
test_models/arithmetic-test001/model.pnml (+870/-0)
test_models/arithmetic-test001/query.xml (+136/-0)
test_models/arithmetic-test002/model.pnml (+203/-0)
test_models/arithmetic-test002/query.xml (+426/-0)
test_models/arithmetic-test003/model.pnml (+423/-0)
test_models/arithmetic-test003/query.xml (+426/-0)
test_models/arithmetic-test004/model.pnml (+24/-0)
test_models/arithmetic-test004/query.xml (+38/-0)
test_models/arithmetic-test005/model.pnml (+52/-0)
test_models/arithmetic-test005/query.xml (+52/-0)
test_models/arithmetic-test006/model.pnml (+52/-0)
test_models/arithmetic-test006/query.xml (+90/-0)
test_models/arithmetic-test007/model.pnml (+94/-0)
test_models/arithmetic-test007/query.xml (+228/-0)
test_models/combined-test001/model.pnml (+170/-0)
test_models/combined-test001/query.xml (+134/-0)
test_models/combined-test002/model.pnml (+148/-0)
test_models/combined-test002/query.xml (+76/-0)
test_models/combined-test003/model.pnml (+210/-0)
test_models/combined-test003/query.xml (+52/-0)
test_models/combined-test004/model.pnml (+209/-0)
test_models/combined-test004/query.xml (+52/-0)
test_models/combined-test005/model.pnml (+181/-0)
test_models/combined-test005/query.xml (+20/-0)
test_models/combined-test006/model.pnml (+181/-0)
test_models/combined-test006/query.xml (+20/-0)
test_models/combined-test007/model.pnml (+858/-0)
test_models/combined-test007/query.xml (+84/-0)
test_models/composition-prime-test001/model.pnml (+1424/-0)
test_models/composition-prime-test001/query.xml (+20/-0)
test_models/composition-prime-test002/model.pnml (+1424/-0)
test_models/composition-prime-test002/query.xml (+20/-0)
test_models/composition-prime-test003/model.pnml (+1424/-0)
test_models/composition-prime-test003/query.xml (+20/-0)
test_models/composition-prime-test004/model.pnml (+1424/-0)
test_models/composition-prime-test004/query.xml (+20/-0)
test_models/composition-prime-test005/model.pnml (+1424/-0)
test_models/composition-prime-test005/query.xml (+20/-0)
test_models/composition-test001/model.pnml (+137/-0)
test_models/composition-test001/query.xml (+20/-0)
test_models/composition-test002/model.pnml (+137/-0)
test_models/composition-test002/query.xml (+20/-0)
test_models/composition-test003/model.pnml (+137/-0)
test_models/composition-test003/query.xml (+20/-0)
test_models/composition-test004/model.pnml (+124/-0)
test_models/composition-test004/query.xml (+20/-0)
test_models/composition-test005/model.pnml (+229/-0)
test_models/composition-test005/query.xml (+20/-0)
test_models/composition-test006/model.pnml (+229/-0)
test_models/composition-test006/query.xml (+20/-0)
test_models/composition-test007/model.pnml (+229/-0)
test_models/composition-test007/query.xml (+20/-0)
test_models/composition-test008/model.pnml (+244/-0)
test_models/composition-test008/query.xml (+20/-0)
test_models/composition-test009/model.pnml (+397/-0)
test_models/composition-test009/query.xml (+52/-0)
test_models/composition-test010/model.pnml (+397/-0)
test_models/composition-test010/query.xml (+28/-0)
test_models/composition-test011/model.pnml (+397/-0)
test_models/composition-test011/query.xml (+28/-0)
test_models/composition-test012/model.pnml (+149/-0)
test_models/composition-test012/query.xml (+52/-0)
test_models/composition-test013/model.pnml (+149/-0)
test_models/composition-test013/query.xml (+52/-0)
test_models/composition-test014/model.pnml (+295/-0)
test_models/composition-test014/query.xml (+34/-0)
test_models/composition-test015/model.pnml (+295/-0)
test_models/composition-test015/query.xml (+34/-0)
test_models/constant-test001/model.pnml (+159/-0)
test_models/constant-test001/query.xml (+20/-0)
test_models/constant-test002/model.pnml (+159/-0)
test_models/constant-test002/query.xml (+20/-0)
test_models/continuous-test001/model.pnml (+135/-0)
test_models/continuous-test001/query.xml (+39/-0)
test_models/continuous-test002/model.pnml (+135/-0)
test_models/continuous-test002/query.xml (+36/-0)
test_models/continuous-test003/model.pnml (+144/-0)
test_models/continuous-test003/query.xml (+15/-0)
test_models/continuous-test004/model.pnml (+144/-0)
test_models/continuous-test004/query.xml (+15/-0)
test_models/continuous-test005/model.pnml (+150/-0)
test_models/continuous-test005/query.xml (+15/-0)
test_models/continuous-test006/model.pnml (+147/-0)
test_models/continuous-test006/query.xml (+20/-0)
test_models/continuous-test007/model.pnml (+147/-0)
test_models/continuous-test007/query.xml (+20/-0)
test_models/continuous-test008/model.pnml (+143/-0)
test_models/continuous-test008/query.xml (+36/-0)
test_models/continuous-test009/model.pnml (+113/-0)
test_models/continuous-test009/query.xml (+66/-0)
test_models/deadlock-test001/model.pnml (+216/-0)
test_models/deadlock-test001/query.xml (+20/-0)
test_models/deadlock-test002/model.pnml (+394/-0)
test_models/deadlock-test002/query.xml (+52/-0)
test_models/deadlock-test003/model.pnml (+306/-0)
test_models/deadlock-test003/query.xml (+66/-0)
test_models/deadlock-test004/model.pnml (+164/-0)
test_models/deadlock-test004/query.xml (+20/-0)
test_models/deadlock-test005/model.pnml (+326/-0)
test_models/deadlock-test005/query.xml (+68/-0)
test_models/deadlock-test006/model.pnml (+326/-0)
test_models/deadlock-test006/query.xml (+60/-0)
test_models/deadlock-test007/model.pnml (+322/-0)
test_models/deadlock-test007/query.xml (+28/-0)
test_models/deadlock-test008/model.pnml (+348/-0)
test_models/deadlock-test008/query.xml (+28/-0)
test_models/deadlock-test009/model.pnml (+348/-0)
test_models/deadlock-test009/query.xml (+28/-0)
test_models/deadlock-test010/model.pnml (+322/-0)
test_models/deadlock-test010/query.xml (+28/-0)
test_models/deadlock-test011/model.pnml (+424/-0)
test_models/deadlock-test011/query.xml (+15/-0)
test_models/deadlock-test012/model.pnml (+424/-0)
test_models/deadlock-test012/query.xml (+15/-0)
test_models/deadlock-test013/model.pnml (+87/-0)
test_models/deadlock-test013/query.xml (+55/-0)
test_models/deadlock-test014/model.pnml (+82/-0)
test_models/deadlock-test014/query.xml (+55/-0)
test_models/deadlock-test015/model.pnml (+211/-0)
test_models/deadlock-test015/query.xml (+17/-0)
test_models/deadlock-test016/model.pnml (+232/-0)
test_models/deadlock-test016/query.xml (+38/-0)
test_models/deadlock-test017/model.pnml (+983/-0)
test_models/deadlock-test017/query.xml (+112/-0)
test_models/deadlock-test018/model.pnml (+45/-0)
test_models/deadlock-test018/query.xml (+34/-0)
test_models/deadlock-test019/model.pnml (+93/-0)
test_models/deadlock-test019/query.xml (+25/-0)
test_models/deadlock-test020/model.pnml (+93/-0)
test_models/deadlock-test020/query.xml (+158/-0)
test_models/deadlock-test021/model.pnml (+112/-0)
test_models/deadlock-test021/query.xml (+158/-0)
test_models/discrete-test-009/model.pnml (+261/-0)
test_models/discrete-test-009/query.xml (+114/-0)
test_models/discrete-test001/model.pnml (+43/-0)
test_models/discrete-test001/query.xml (+47/-0)
test_models/discrete-test002/model.pnml (+128/-0)
test_models/discrete-test002/query.xml (+44/-0)
test_models/discrete-test003/model.pnml (+159/-0)
test_models/discrete-test003/query.xml (+36/-0)
test_models/discrete-test004/model.pnml (+186/-0)
test_models/discrete-test004/query.xml (+80/-0)
test_models/discrete-test005/model.pnml (+566/-0)
test_models/discrete-test005/query.xml (+44/-0)
test_models/discrete-test006/model.pnml (+228/-0)
test_models/discrete-test006/query.xml (+200/-0)
test_models/discrete-test007/model.pnml (+248/-0)
test_models/discrete-test007/query.xml (+108/-0)
test_models/discrete-test008/model.pnml (+147/-0)
test_models/discrete-test008/query.xml (+94/-0)
test_models/discrete-test009/model.pnml (+261/-0)
test_models/discrete-test009/query.xml (+114/-0)
test_models/discrete-test010/model.pnml (+561/-0)
test_models/discrete-test010/query.xml (+262/-0)
test_models/discrete-test011/model.pnml (+512/-0)
test_models/discrete-test011/query.xml (+144/-0)
test_models/discrete-test012/model.pnml (+334/-0)
test_models/discrete-test012/query.xml (+20/-0)
test_models/division-test001/model.pnml (+593/-0)
test_models/division-test001/query.xml (+34/-0)
test_models/division-test002/model.pnml (+593/-0)
test_models/division-test002/query.xml (+34/-0)
test_models/error-conjunction-bug-test001/model.pnml (+612/-0)
test_models/error-conjunction-bug-test001/query.xml (+36/-0)
test_models/error-conjunction-reducer-test002/model.pnml (+631/-0)
test_models/error-conjunction-reducer-test002/query.xml (+62/-0)
test_models/error-encoder-test-001/model.pnml (+87/-0)
test_models/error-encoder-test-001/query.xml (+20/-0)
test_models/exercise-test001/model.pnml (+208/-0)
test_models/exercise-test001/query.xml (+72/-0)
test_models/exercise-test002/model.pnml (+174/-0)
test_models/exercise-test002/query.xml (+36/-0)
test_models/exercise-test003/model.pnml (+148/-0)
test_models/exercise-test003/query.xml (+28/-0)
test_models/exercise-test004/model.pnml (+148/-0)
test_models/exercise-test004/query.xml (+28/-0)
test_models/exercise-test005/model.pnml (+222/-0)
test_models/exercise-test005/query.xml (+20/-0)
test_models/exercise-test006/model.pnml (+222/-0)
test_models/exercise-test006/query.xml (+20/-0)
test_models/exercise-test007/model.pnml (+191/-0)
test_models/exercise-test007/query.xml (+20/-0)
test_models/exercise-test008/model.pnml (+220/-0)
test_models/exercise-test008/query.xml (+36/-0)
test_models/exercise-test009/model.pnml (+377/-0)
test_models/exercise-test009/query.xml (+20/-0)
test_models/exercise-test010/model.pnml (+377/-0)
test_models/exercise-test010/query.xml (+20/-0)
test_models/extra-test-001-liveness/model.pnml (+121/-0)
test_models/extra-test-001-liveness/query.xml (+38/-0)
test_models/extra-test-002-search-order/model.pnml (+158/-0)
test_models/extra-test-002-search-order/query.xml (+20/-0)
test_models/extra-test-003-maintanance/model.pnml (+406/-0)
test_models/extra-test-003-maintanance/query.xml (+20/-0)
test_models/extra-test-004-burger/model.pnml (+416/-0)
test_models/extra-test-004-burger/query.xml (+20/-0)
test_models/extra-test-004-transfusion/model.pnml (+2314/-0)
test_models/extra-test-004-transfusion/query.xml (+20/-0)
test_models/extra-test-005-liveness/model.pnml (+122/-0)
test_models/extra-test-005-liveness/query.xml (+76/-0)
test_models/extra-test-006-liveness/model.pnml (+141/-0)
test_models/extra-test-006-liveness/query.xml (+63/-0)
test_models/extra-test-007-liveness/model.pnml (+228/-0)
test_models/extra-test-007-liveness/query.xml (+70/-0)
test_models/fms-test001/model.pnml (+602/-0)
test_models/fms-test001/query.xml (+104/-0)
test_models/inclusion-test001/model.pnml (+182/-0)
test_models/inclusion-test001/query.xml (+112/-0)
test_models/inclusion-test002/model.pnml (+191/-0)
test_models/inclusion-test002/query.xml (+204/-0)
test_models/inclusion-test003/model.pnml (+191/-0)
test_models/inclusion-test003/query.xml (+204/-0)
test_models/inclusion-test004/model.pnml (+192/-0)
test_models/inclusion-test004/query.xml (+120/-0)
test_models/inclusion-test005/model.pnml (+194/-0)
test_models/inclusion-test005/query.xml (+120/-0)
test_models/inclusion-test006/model.pnml (+79/-0)
test_models/inclusion-test006/query.xml (+52/-0)
test_models/inclusion-test007/model.pnml (+132/-0)
test_models/inclusion-test007/query.xml (+104/-0)
test_models/inhibitors-test001/model.pnml (+134/-0)
test_models/inhibitors-test001/query.xml (+20/-0)
test_models/inhibitors-test002/model.pnml (+134/-0)
test_models/inhibitors-test002/query.xml (+20/-0)
test_models/inhibitors-test003/model.pnml (+134/-0)
test_models/inhibitors-test003/query.xml (+20/-0)
test_models/inhibitors-test004/model.pnml (+134/-0)
test_models/inhibitors-test004/query.xml (+20/-0)
test_models/invariants-test001/model.pnml (+184/-0)
test_models/invariants-test001/query.xml (+20/-0)
test_models/invariants-test002/model.pnml (+134/-0)
test_models/invariants-test002/query.xml (+20/-0)
test_models/invariants-test003/model.pnml (+134/-0)
test_models/invariants-test003/query.xml (+20/-0)
test_models/invariants-test004/model.pnml (+127/-0)
test_models/invariants-test004/query.xml (+20/-0)
test_models/invariants-test005/model.pnml (+127/-0)
test_models/invariants-test005/query.xml (+20/-0)
test_models/invariants-test006/model.pnml (+127/-0)
test_models/invariants-test006/query.xml (+20/-0)
test_models/invariants-test007/model.pnml (+129/-0)
test_models/invariants-test007/query.xml (+20/-0)
test_models/invariants-test008/model.pnml (+129/-0)
test_models/invariants-test008/query.xml (+20/-0)
test_models/invariants-test009/model.pnml (+172/-0)
test_models/invariants-test009/query.xml (+28/-0)
test_models/invariants-test010/model.pnml (+199/-0)
test_models/invariants-test010/query.xml (+28/-0)
test_models/invariants-test011/model.pnml (+156/-0)
test_models/invariants-test011/query.xml (+47/-0)
test_models/lightcross-text001/model.pnml (+172/-0)
test_models/lightcross-text001/query.xml (+84/-0)
test_models/liveness-test001/model.pnml (+171/-0)
test_models/liveness-test001/query.xml (+60/-0)
test_models/liveness-test002/model.pnml (+191/-0)
test_models/liveness-test002/query.xml (+20/-0)
test_models/liveness-test003/model.pnml (+191/-0)
test_models/liveness-test003/query.xml (+20/-0)
test_models/orphans-test001/model.pnml (+142/-0)
test_models/orphans-test001/query.xml (+28/-0)
test_models/orphans-test002/model.pnml (+142/-0)
test_models/orphans-test002/query.xml (+28/-0)
test_models/orphans-test003/model.pnml (+232/-0)
test_models/orphans-test003/query.xml (+30/-0)
test_models/orphans-test004/model.pnml (+232/-0)
test_models/orphans-test004/query.xml (+30/-0)
test_models/other-test001/model.pnml (+335/-0)
test_models/other-test001/query.xml (+28/-0)
test_models/other-test002/model.pnml (+335/-0)
test_models/other-test002/query.xml (+28/-0)
test_models/other-test003/model.pnml (+150/-0)
test_models/other-test003/query.xml (+20/-0)
test_models/other-test004/model.pnml (+150/-0)
test_models/other-test004/query.xml (+20/-0)
test_models/other-test005/model.pnml (+207/-0)
test_models/other-test005/query.xml (+20/-0)
test_models/other-test006/model.pnml (+207/-0)
test_models/other-test006/query.xml (+20/-0)
test_models/other-test007/model.pnml (+179/-0)
test_models/other-test007/query.xml (+28/-0)
test_models/other-test008/model.pnml (+174/-0)
test_models/other-test008/query.xml (+28/-0)
test_models/other-test009/model.pnml (+272/-0)
test_models/other-test009/query.xml (+20/-0)
test_models/other-test010/model.pnml (+272/-0)
test_models/other-test010/query.xml (+20/-0)
test_models/other-test011/model.pnml (+272/-0)
test_models/other-test011/query.xml (+20/-0)
test_models/other-test012/model.pnml (+195/-0)
test_models/other-test012/query.xml (+36/-0)
test_models/other-test013/model.pnml (+235/-0)
test_models/other-test013/query.xml (+84/-0)
test_models/other-test014/model.pnml (+252/-0)
test_models/other-test014/query.xml (+84/-0)
test_models/other-test015/model.pnml (+309/-0)
test_models/other-test015/query.xml (+68/-0)
test_models/prime-test001/model.pnml (+621/-0)
test_models/prime-test001/query.xml (+34/-0)
test_models/prime-test0019/model.pnml (+359/-0)
test_models/prime-test0019/query.xml (+20/-0)
test_models/prime-test002/model.pnml (+621/-0)
test_models/prime-test002/query.xml (+34/-0)
test_models/prime-test0020/model.pnml (+359/-0)
test_models/prime-test0020/query.xml (+20/-0)
test_models/prime-test0021/model.pnml (+359/-0)
test_models/prime-test0021/query.xml (+20/-0)
test_models/prime-test0022/model.pnml (+359/-0)
test_models/prime-test0022/query.xml (+20/-0)
test_models/prime-test003/model.pnml (+621/-0)
test_models/prime-test003/query.xml (+34/-0)
test_models/prime-test004/model.pnml (+621/-0)
test_models/prime-test004/query.xml (+34/-0)
test_models/prime-test005/model.pnml (+621/-0)
test_models/prime-test005/query.xml (+34/-0)
test_models/prime-test006/model.pnml (+621/-0)
test_models/prime-test006/query.xml (+34/-0)
test_models/prime-test007/model.pnml (+621/-0)
test_models/prime-test007/query.xml (+34/-0)
test_models/prime-test008/model.pnml (+621/-0)
test_models/prime-test008/query.xml (+34/-0)
test_models/prime-test009/model.pnml (+621/-0)
test_models/prime-test009/query.xml (+34/-0)
test_models/prime-test010/model.pnml (+621/-0)
test_models/prime-test010/query.xml (+34/-0)
test_models/prime-test011/model.pnml (+621/-0)
test_models/prime-test011/query.xml (+34/-0)
test_models/prime-test012/model.pnml (+621/-0)
test_models/prime-test012/query.xml (+34/-0)
test_models/prime-test013/model.pnml (+621/-0)
test_models/prime-test013/query.xml (+34/-0)
test_models/prime-test014/model.pnml (+621/-0)
test_models/prime-test014/query.xml (+34/-0)
test_models/prime-test015/model.pnml (+621/-0)
test_models/prime-test015/query.xml (+34/-0)
test_models/prime-test016/model.pnml (+802/-0)
test_models/prime-test016/query.xml (+36/-0)
test_models/prime-test017/model.pnml (+802/-0)
test_models/prime-test017/query.xml (+36/-0)
test_models/prime-test018/model.pnml (+802/-0)
test_models/prime-test018/query.xml (+36/-0)
test_models/prime-test019/model.pnml (+359/-0)
test_models/prime-test019/query.xml (+20/-0)
test_models/prime-test020/model.pnml (+359/-0)
test_models/prime-test020/query.xml (+20/-0)
test_models/prime-test023/model.pnml (+251/-0)
test_models/prime-test023/query.xml (+32/-0)
test_models/prime-test024/model.pnml (+251/-0)
test_models/prime-test024/query.xml (+32/-0)
test_models/productline-test001/model.pnml (+245/-0)
test_models/productline-test001/query.xml (+20/-0)
test_models/productline-test002/model.pnml (+245/-0)
test_models/productline-test002/query.xml (+20/-0)
test_models/productline-test003/model.pnml (+245/-0)
test_models/productline-test003/query.xml (+20/-0)
test_models/productline-test004/model.pnml (+255/-0)
test_models/productline-test004/query.xml (+20/-0)
test_models/productline-test005/model.pnml (+255/-0)
test_models/productline-test005/query.xml (+20/-0)
test_models/query-test001/model.pnml (+167/-0)
test_models/query-test001/query.xml (+224/-0)
test_models/query-test002/model.pnml (+135/-0)
test_models/query-test002/query.xml (+306/-0)
test_models/query-test003/model.pnml (+276/-0)
test_models/query-test003/query.xml (+102/-0)
test_models/query-test004/model.pnml (+165/-0)
test_models/query-test004/query.xml (+124/-0)
test_models/query-test005/model.pnml (+105/-0)
test_models/query-test005/query.xml (+76/-0)
test_models/reduction-001/model.pnml (+203/-0)
test_models/reduction-001/query.xml (+20/-0)
test_models/reduction-002/model.pnml (+203/-0)
test_models/reduction-002/query.xml (+20/-0)
test_models/reduction-003/model.pnml (+205/-0)
test_models/reduction-003/query.xml (+20/-0)
test_models/reduction-004/model.pnml (+207/-0)
test_models/reduction-004/query.xml (+20/-0)
test_models/reduction-005/model.pnml (+207/-0)
test_models/reduction-005/query.xml (+20/-0)
test_models/reduction-006/model.pnml (+203/-0)
test_models/reduction-006/query.xml (+20/-0)
test_models/reduction-007/model.pnml (+208/-0)
test_models/reduction-007/query.xml (+20/-0)
test_models/reduction-008-house/model.pnml (+623/-0)
test_models/reduction-008-house/query.xml (+44/-0)
test_models/reduction-009/model.pnml (+260/-0)
test_models/reduction-009/query.xml (+28/-0)
test_models/reduction-010/model.pnml (+122/-0)
test_models/reduction-010/query.xml (+20/-0)
test_models/reduction-011/model.pnml (+112/-0)
test_models/reduction-011/query.xml (+20/-0)
test_models/reduction-012/model.pnml (+121/-0)
test_models/reduction-012/query.xml (+20/-0)
test_models/reduction-013/model.pnml (+113/-0)
test_models/reduction-013/query.xml (+20/-0)
test_models/reduction-014/model.pnml (+151/-0)
test_models/reduction-014/query.xml (+20/-0)
test_models/reduction-015/model.pnml (+165/-0)
test_models/reduction-015/query.xml (+20/-0)
test_models/reduction-016/model.pnml (+134/-0)
test_models/reduction-016/query.xml (+20/-0)
test_models/reduction-017/model.pnml (+95/-0)
test_models/reduction-017/query.xml (+20/-0)
test_models/reduction-018/model.pnml (+98/-0)
test_models/reduction-018/query.xml (+22/-0)
test_models/reduction-019-deadlock/model.pnml (+154/-0)
test_models/reduction-019-deadlock/query.xml (+15/-0)
test_models/reduction-020-deadlock/model.pnml (+109/-0)
test_models/reduction-020-deadlock/query.xml (+15/-0)
test_models/reduction-021-deadlock/model.pnml (+109/-0)
test_models/reduction-021-deadlock/query.xml (+15/-0)
test_models/reduction-022-deadlock/model.pnml (+78/-0)
test_models/reduction-022-deadlock/query.xml (+15/-0)
test_models/reduction-023-deadlock/model.pnml (+51/-0)
test_models/reduction-023-deadlock/query.xml (+15/-0)
test_models/reduction-024/model.pnml (+802/-0)
test_models/reduction-024/query.xml (+44/-0)
test_models/reduction-025/model.pnml (+157/-0)
test_models/reduction-025/query.xml (+44/-0)
test_models/reduction-026/model.pnml (+165/-0)
test_models/reduction-026/query.xml (+44/-0)
test_models/reduction-027/model.pnml (+165/-0)
test_models/reduction-027/query.xml (+44/-0)
test_models/reduction-028/model.pnml (+161/-0)
test_models/reduction-028/query.xml (+44/-0)
test_models/reduction-029/model.pnml (+308/-0)
test_models/reduction-029/query.xml (+31/-0)
test_models/reduction-030/model.pnml (+308/-0)
test_models/reduction-030/query.xml (+31/-0)
test_models/reduction-031/model.pnml (+310/-0)
test_models/reduction-031/query.xml (+31/-0)
test_models/reduction-032/model.pnml (+217/-0)
test_models/reduction-032/query.xml (+31/-0)
test_models/reduction-033/model.pnml (+248/-0)
test_models/reduction-033/query.xml (+31/-0)
test_models/reduction-034/model.pnml (+248/-0)
test_models/reduction-034/query.xml (+31/-0)
test_models/reduction-035/model.pnml (+164/-0)
test_models/reduction-035/query.xml (+20/-0)
test_models/reduction-036/model.pnml (+164/-0)
test_models/reduction-036/query.xml (+20/-0)
test_models/reduction-037/model.pnml (+277/-0)
test_models/reduction-037/query.xml (+31/-0)
test_models/reduction-038/model.pnml (+277/-0)
test_models/reduction-038/query.xml (+57/-0)
test_models/reduction-039/model.pnml (+265/-0)
test_models/reduction-039/query.xml (+105/-0)
test_models/reduction-040/model.pnml (+150/-0)
test_models/reduction-040/query.xml (+20/-0)
test_models/reduction-041/model.pnml (+174/-0)
test_models/reduction-041/query.xml (+20/-0)
test_models/reduction-042/model.pnml (+178/-0)
test_models/reduction-042/query.xml (+31/-0)
test_models/reduction-043/model.pnml (+191/-0)
test_models/reduction-043/query.xml (+28/-0)
test_models/reduction-044/model.pnml (+170/-0)
test_models/reduction-044/query.xml (+31/-0)
test_models/reduction-045/model.pnml (+174/-0)
test_models/reduction-045/query.xml (+31/-0)
test_models/reduction-046/model.pnml (+111/-0)
test_models/reduction-046/query.xml (+47/-0)
test_models/reduction-047/model.pnml (+130/-0)
test_models/reduction-047/query.xml (+47/-0)
test_models/reduction-048/model.pnml (+130/-0)
test_models/reduction-048/query.xml (+47/-0)
test_models/reduction-049/model.pnml (+130/-0)
test_models/reduction-049/query.xml (+31/-0)
test_models/reduction-050/model.pnml (+66/-0)
test_models/reduction-050/query.xml (+20/-0)
test_models/shortest-path-test001/model.pnml (+337/-0)
test_models/shortest-path-test001/query.xml (+20/-0)
test_models/shortest-path-test002/model.pnml (+337/-0)
test_models/shortest-path-test002/query.xml (+20/-0)
test_models/sim-test001/model.pnml (+173/-0)
test_models/sim-test001/query.xml (+44/-0)
test_models/sim-test002/model.pnml (+226/-0)
test_models/sim-test002/query.xml (+44/-0)
test_models/simple-test001/model.pnml (+96/-0)
test_models/simple-test001/query.xml (+20/-0)
test_models/simple-test002/model.pnml (+111/-0)
test_models/simple-test002/query.xml (+20/-0)
test_models/simple-test003/model.pnml (+111/-0)
test_models/simple-test003/query.xml (+20/-0)
test_models/simple-test004/model.pnml (+232/-0)
test_models/simple-test004/query.xml (+20/-0)
test_models/simple-test005/model.pnml (+232/-0)
test_models/simple-test005/query.xml (+20/-0)
test_models/simple-test006/model.pnml (+250/-0)
test_models/simple-test006/query.xml (+20/-0)
test_models/simple-test007/model.pnml (+250/-0)
test_models/simple-test007/query.xml (+20/-0)
test_models/simple-test008/model.pnml (+151/-0)
test_models/simple-test008/query.xml (+20/-0)
test_models/simple-test009/model.pnml (+151/-0)
test_models/simple-test009/query.xml (+28/-0)
test_models/simple-test010/model.pnml (+151/-0)
test_models/simple-test010/query.xml (+28/-0)
test_models/simple-test011/model.pnml (+148/-0)
test_models/simple-test011/query.xml (+20/-0)
test_models/simple-test012/model.pnml (+148/-0)
test_models/simple-test012/query.xml (+20/-0)
test_models/simple-test013/model.pnml (+189/-0)
test_models/simple-test013/query.xml (+28/-0)
test_models/simple-test014/model.pnml (+189/-0)
test_models/simple-test014/query.xml (+28/-0)
test_models/simple-test015/model.pnml (+189/-0)
test_models/simple-test015/query.xml (+28/-0)
test_models/simple-test016/model.pnml (+151/-0)
test_models/simple-test016/query.xml (+20/-0)
test_models/simple-test017/model.pnml (+221/-0)
test_models/simple-test017/query.xml (+28/-0)
test_models/simple-test018/model.pnml (+94/-0)
test_models/simple-test018/query.xml (+36/-0)
test_models/simple-test019/model.pnml (+94/-0)
test_models/simple-test019/query.xml (+52/-0)
test_models/simple-test020/model.pnml (+134/-0)
test_models/simple-test020/query.xml (+44/-0)
test_models/subsetsum-test001/model.pnml (+202/-0)
test_models/subsetsum-test001/query.xml (+20/-0)
test_models/subsetsum-test002/model.pnml (+202/-0)
test_models/subsetsum-test002/query.xml (+20/-0)
test_models/subsetsum-test003/model.pnml (+260/-0)
test_models/subsetsum-test003/query.xml (+20/-0)
test_models/subsetsum-test004/model.pnml (+260/-0)
test_models/subsetsum-test004/query.xml (+20/-0)
test_models/subsetsum-test005/model.pnml (+247/-0)
test_models/subsetsum-test005/query.xml (+20/-0)
test_models/task-graph-test001/model.pnml (+470/-0)
test_models/task-graph-test001/query.xml (+124/-0)
test_models/trace-test001/model.pnml (+147/-0)
test_models/trace-test001/query.xml (+44/-0)
test_models/trace-test002/model.pnml (+136/-0)
test_models/trace-test002/query.xml (+44/-0)
test_models/trace-test003/model.pnml (+91/-0)
test_models/trace-test003/query.xml (+31/-0)
test_models/trace-test004/model.pnml (+118/-0)
test_models/trace-test004/query.xml (+20/-0)
test_models/trace-test005/model.pnml (+2634/-0)
test_models/trace-test005/query.xml (+20/-0)
test_models/trace-test006/model.pnml (+110/-0)
test_models/trace-test006/query.xml (+17/-0)
test_models/trace-test007/model.pnml (+110/-0)
test_models/trace-test007/query.xml (+17/-0)
test_models/trace-test008/model.pnml (+110/-0)
test_models/trace-test008/query.xml (+17/-0)
test_models/trace-test009/model.pnml (+110/-0)
test_models/trace-test009/query.xml (+17/-0)
test_models/train-simple-test001/model.pnml (+224/-0)
test_models/train-simple-test001/query.xml (+36/-0)
test_models/train-simple-test002/model.pnml (+224/-0)
test_models/train-simple-test002/query.xml (+36/-0)
test_models/train-simple-test003/model.pnml (+224/-0)
test_models/train-simple-test003/query.xml (+36/-0)
test_models/train-simple-test004/model.pnml (+224/-0)
test_models/train-simple-test004/query.xml (+36/-0)
test_models/train-simple-test005/model.pnml (+224/-0)
test_models/train-simple-test005/query.xml (+36/-0)
test_models/transInv-test001/model.pnml (+135/-0)
test_models/transInv-test001/query.xml (+20/-0)
test_models/transInv-test002/model.pnml (+135/-0)
test_models/transInv-test002/query.xml (+20/-0)
test_models/transInv-test003/model.pnml (+125/-0)
test_models/transInv-test003/query.xml (+20/-0)
test_models/transInv-test004/model.pnml (+135/-0)
test_models/transInv-test004/query.xml (+20/-0)
test_models/transInv-test005/model.pnml (+135/-0)
test_models/transInv-test005/query.xml (+20/-0)
test_models/transport-test001/model.pnml (+211/-0)
test_models/transport-test001/query.xml (+20/-0)
test_models/transport-test002/model.pnml (+211/-0)
test_models/transport-test002/query.xml (+20/-0)
test_models/transport-test003/model.pnml (+222/-0)
test_models/transport-test003/query.xml (+20/-0)
test_models/transport-test004/model.pnml (+222/-0)
test_models/transport-test004/query.xml (+20/-0)
test_models/transport-test005/model.pnml (+222/-0)
test_models/transport-test005/query.xml (+20/-0)
test_models/transport-test006/model.pnml (+220/-0)
test_models/transport-test006/query.xml (+20/-0)
test_models/transport-test007/model.pnml (+220/-0)
test_models/transport-test007/query.xml (+20/-0)
test_models/transport-test008/model.pnml (+220/-0)
test_models/transport-test008/query.xml (+20/-0)
test_models/transport-test009/model.pnml (+134/-0)
test_models/transport-test009/query.xml (+20/-0)
test_models/transport-test010/model.pnml (+134/-0)
test_models/transport-test010/query.xml (+20/-0)
test_models/transport-test011/model.pnml (+188/-0)
test_models/transport-test011/query.xml (+34/-0)
test_models/transport-test012/model.pnml (+188/-0)
test_models/transport-test012/query.xml (+34/-0)
test_models/transport-test013/model.pnml (+168/-0)
test_models/transport-test013/query.xml (+34/-0)
test_models/transport-test014/model.pnml (+168/-0)
test_models/transport-test014/query.xml (+34/-0)
test_models/transport-test015/model.pnml (+180/-0)
test_models/transport-test015/query.xml (+20/-0)
test_models/transport-test016/model.pnml (+180/-0)
test_models/transport-test016/query.xml (+20/-0)
test_models/transport-test017/model.pnml (+316/-0)
test_models/transport-test017/query.xml (+36/-0)
test_models/transport-test018/model.pnml (+234/-0)
test_models/transport-test018/query.xml (+36/-0)
test_models/transport-test019/model.pnml (+159/-0)
test_models/transport-test019/query.xml (+80/-0)
test_models/transport-test020/model.pnml (+66/-0)
test_models/transport-test020/query.xml (+36/-0)
test_models/transport-test021/model.pnml (+135/-0)
test_models/transport-test021/query.xml (+73/-0)
test_models/transport-test022/model.pnml (+136/-0)
test_models/transport-test022/query.xml (+55/-0)
test_models/transport-test023/model.pnml (+162/-0)
test_models/transport-test023/query.xml (+39/-0)
test_models/tricky-test001/model.pnml (+215/-0)
test_models/tricky-test001/query.xml (+28/-0)
test_models/tricky-test002/model.pnml (+215/-0)
test_models/tricky-test002/query.xml (+28/-0)
test_models/tricky-test003/model.pnml (+188/-0)
test_models/tricky-test003/query.xml (+34/-0)
test_models/tricky-test004/model.pnml (+125/-0)
test_models/tricky-test004/query.xml (+52/-0)
test_models/untimed-reductions-A-test001/model.pnml (+132/-0)
test_models/untimed-reductions-A-test001/query.xml (+36/-0)
test_models/untimed-reductions-A-test002/model.pnml (+144/-0)
test_models/untimed-reductions-A-test002/query.xml (+44/-0)
test_models/untimed-reductions-A-test003/model.pnml (+149/-0)
test_models/untimed-reductions-A-test003/query.xml (+44/-0)
test_models/untimed-reductions-A-test004/model.pnml (+146/-0)
test_models/untimed-reductions-A-test004/query.xml (+36/-0)
test_models/untimed-reductions-B-test001/model.pnml (+182/-0)
test_models/untimed-reductions-B-test001/query.xml (+44/-0)
test_models/untimed-reductions-B-test002/model.pnml (+177/-0)
test_models/untimed-reductions-B-test002/query.xml (+36/-0)
test_models/untimed-reductions-B-test003/model.pnml (+187/-0)
test_models/untimed-reductions-B-test003/query.xml (+36/-0)
test_models/untimed-reductions-B-test004/model.pnml (+182/-0)
test_models/untimed-reductions-B-test004/query.xml (+36/-0)
test_models/untimed-reductions-B-test005/model.pnml (+163/-0)
test_models/untimed-reductions-B-test005/query.xml (+36/-0)
test_models/untimed-reductions-C-test001/model.pnml (+150/-0)
test_models/untimed-reductions-C-test001/query.xml (+36/-0)
test_models/untimed-reductions-C-test002/model.pnml (+150/-0)
test_models/untimed-reductions-C-test002/query.xml (+36/-0)
test_models/untimed-reductions-C-test003/model.pnml (+150/-0)
test_models/untimed-reductions-C-test003/query.xml (+36/-0)
test_models/untimed-reductions-C-test004/model.pnml (+150/-0)
test_models/untimed-reductions-C-test004/query.xml (+56/-0)
test_models/untimed-reductions-D-test001/model.pnml (+209/-0)
test_models/untimed-reductions-D-test001/query.xml (+36/-0)
test_models/untimed-reductions-D-test002/model.pnml (+224/-0)
test_models/untimed-reductions-D-test002/query.xml (+36/-0)
test_models/untimed-reductions-E-test001/model.pnml (+109/-0)
test_models/untimed-reductions-E-test001/query.xml (+20/-0)
test_models/untimed-reductions-jacob-A-test001/model.pnml (+181/-0)
test_models/untimed-reductions-jacob-A-test001/query.xml (+119/-0)
test_models/untimed-reductions-jacob-B-test001/model.pnml (+259/-0)
test_models/untimed-reductions-jacob-B-test001/query.xml (+76/-0)
test_models/untimed-reductions-jacob-C-test001/model.pnml (+181/-0)
test_models/untimed-reductions-jacob-C-test001/query.xml (+124/-0)
test_models/untimed-reductions-jacob-D1-test001/model.pnml (+228/-0)
test_models/untimed-reductions-jacob-D1-test001/query.xml (+129/-0)
test_models/untimed-reductions-jacob-D2-test001/model.pnml (+150/-0)
test_models/untimed-reductions-jacob-D2-test001/query.xml (+15/-0)
test_models/untimed-reductions-jacob-E-test001/model.pnml (+173/-0)
test_models/untimed-reductions-jacob-E-test001/query.xml (+76/-0)
test_models/untimed-reductions-mads-test001/model.pnml (+140/-0)
test_models/untimed-reductions-mads-test001/query.xml (+47/-0)
test_models/untimed-reductions-mads-test002/model.pnml (+160/-0)
test_models/untimed-reductions-mads-test002/query.xml (+39/-0)
test_models/untimed-reductions-mads-test003/model.pnml (+140/-0)
test_models/untimed-reductions-mads-test003/query.xml (+39/-0)
test_models/untimed-reductions-mads-test004/model.pnml (+156/-0)
test_models/untimed-reductions-mads-test004/query.xml (+44/-0)
test_models/untimed-reductions-mads-test005/model.pnml (+124/-0)
test_models/untimed-reductions-mads-test005/query.xml (+50/-0)
test_models/untimed-reductions-mads-test006/model.pnml (+104/-0)
test_models/untimed-reductions-mads-test006/query.xml (+55/-0)
test_models/untimed-reductions-mads-test007/model.pnml (+152/-0)
test_models/untimed-reductions-mads-test007/query.xml (+15/-0)
test_models/untimed-reductions-mads-test008/model.pnml (+72/-0)
test_models/untimed-reductions-mads-test008/query.xml (+66/-0)
test_models/untimed-reductions-mads-test009/model.pnml (+637/-0)
test_models/untimed-reductions-mads-test009/query.xml (+50/-0)
test_models/untimed-test001/model.pnml (+140/-0)
test_models/untimed-test001/query.xml (+84/-0)
test_models/untimed-test002/model.pnml (+128/-0)
test_models/untimed-test002/query.xml (+20/-0)
test_models/untimed-test003/model.pnml (+128/-0)
test_models/untimed-test003/query.xml (+20/-0)
test_models/untimed-test004/model.pnml (+1021/-0)
test_models/untimed-test004/query.xml (+327/-0)
test_models/untimed-test005/model.pnml (+1035/-0)
test_models/untimed-test005/query.xml (+121/-0)
test_models/untimed-test006-philosophers/model.pnml (+856/-0)
test_models/untimed-test006-philosophers/query.xml (+63/-0)
test_models/untimed-test007-swimming-pool/model.pnml (+233/-0)
test_models/untimed-test007-swimming-pool/query.xml (+55/-0)
test_models/untimed-test008/model.pnml (+87/-0)
test_models/untimed-test008/query.xml (+20/-0)
test_models/untimed-test009/model.pnml (+129/-0)
test_models/untimed-test009/query.xml (+28/-0)
test_models/untimed-test010/model.pnml (+94/-0)
test_models/untimed-test010/query.xml (+36/-0)
test_models/untimed-test011/model.pnml (+134/-0)
test_models/untimed-test011/query.xml (+84/-0)
test_models/urgency-test001/model.pnml (+78/-0)
test_models/urgency-test001/query.xml (+76/-0)
test_models/urgency-test002/model.pnml (+82/-0)
test_models/urgency-test002/query.xml (+76/-0)
test_models/urgency-test003/model.pnml (+105/-0)
test_models/urgency-test003/query.xml (+44/-0)
test_models/urgency-test004/model.pnml (+266/-0)
test_models/urgency-test004/query.xml (+68/-0)
test_models/urgency-test005/model.pnml (+274/-0)
test_models/urgency-test005/query.xml (+52/-0)
test_models/urgency-test006/model.pnml (+301/-0)
test_models/urgency-test006/query.xml (+124/-0)
test_models/urgency-test007/model.pnml (+192/-0)
test_models/urgency-test007/query.xml (+108/-0)
test_models/urgency-test008/model.pnml (+193/-0)
test_models/urgency-test008/query.xml (+108/-0)
test_models/urgency-test009/model.pnml (+209/-0)
test_models/urgency-test009/query.xml (+108/-0)
test_models/urgency-test010/model.pnml (+514/-0)
test_models/urgency-test010/query.xml (+36/-0)
test_models/urgency-test011/model.pnml (+514/-0)
test_models/urgency-test011/query.xml (+36/-0)
test_models/urgency-test012/model.pnml (+269/-0)
test_models/urgency-test012/query.xml (+120/-0)
test_models/urgency-test013/model.pnml (+269/-0)
test_models/urgency-test013/query.xml (+120/-0)
test_models/urgency-test014/model.pnml (+243/-0)
test_models/urgency-test014/query.xml (+60/-0)
test_models/urgency-test015/model.pnml (+543/-0)
test_models/urgency-test015/query.xml (+52/-0)
test_models/urgency-test016/model.pnml (+258/-0)
test_models/urgency-test016/query.xml (+60/-0)
test_models/urgency-test017/model.pnml (+265/-0)
test_models/urgency-test017/query.xml (+36/-0)
test_models/weighted-test001/model.pnml (+268/-0)
test_models/weighted-test001/query.xml (+68/-0)
test_models/weighted-test002/model.pnml (+295/-0)
test_models/weighted-test002/query.xml (+20/-0)
test_models/weighted-test003/model.pnml (+312/-0)
test_models/weighted-test003/query.xml (+50/-0)
test_models/weighted-test004/model.pnml (+294/-0)
test_models/weighted-test004/query.xml (+178/-0)
test_models/workflow-test001/model.pnml (+162/-0)
test_models/workflow-test001/query.xml (+20/-0)
test_models/workflow-test002/model.pnml (+162/-0)
test_models/workflow-test002/query.xml (+20/-0)
test_models/workflow-test003/model.pnml (+162/-0)
test_models/workflow-test003/query.xml (+20/-0)
test_models/workflow-test004/model.pnml (+167/-0)
test_models/workflow-test004/query.xml (+20/-0)
test_models/workflow-test005/model.pnml (+172/-0)
test_models/workflow-test005/query.xml (+20/-0)
test_models/workflow-test006/model.pnml (+172/-0)
test_models/workflow-test006/query.xml (+20/-0)
test_models/workflow-test007/model.pnml (+237/-0)
test_models/workflow-test007/query.xml (+20/-0)
test_models/workflow-test008/model.pnml (+237/-0)
test_models/workflow-test008/query.xml (+20/-0)
test_models/workflow-test009/model.pnml (+237/-0)
test_models/workflow-test009/query.xml (+20/-0)
test_models/workflow-test010/model.pnml (+1304/-0)
test_models/workflow-test010/query.xml (+156/-0)
test_models/workflow-test011/model.pnml (+428/-0)
test_models/workflow-test011/query.xml (+68/-0)
test_models/workflow-test012/model.pnml (+599/-0)
test_models/workflow-test012/query.xml (+76/-0)
test_models/workflow-test013/model.pnml (+351/-0)
test_models/workflow-test013/query.xml (+116/-0)
test_models/workflow-test014/model.pnml (+351/-0)
test_models/workflow-test014/query.xml (+116/-0)
test_models/workflow-test015/model.pnml (+378/-0)
test_models/workflow-test015/query.xml (+116/-0)
test_models/workflow-test016/model.pnml (+583/-0)
test_models/workflow-test016/query.xml (+87/-0)
toolchain-x86_64-w64-mingw32.cmake (+17/-0)
To merge this branch: bzr merge lp:~verifypn-maintainers/verifypn/interval_tar
Reviewer Review Type Date Requested Status
Jiri Srba 2020-07-01 Approve on 2020-09-11
Review via email: mp+386674@code.launchpad.net

Commit message

 - Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Passes MCC'19 models, needs manual validation.

To post a comment you must log in.
353. By Peter G. Jensen <email address hidden> on 2020-07-02

Merged in trunk

354. By Peter G. Jensen <email address hidden> on 2020-07-03

added simple test-script and test models

355. By Peter G. Jensen <email address hidden> on 2020-07-03

inhibitor arcs are not yet handled by TAR solver, so return error if used with TAR

356. By Peter G. Jensen <email address hidden> on 2020-07-06

fixed handling of inhibitor

357. By Peter G. Jensen <email address hidden> on 2020-07-06

removing unused glpk import from STSolver

358. By Peter G. Jensen <email address hidden> on 2020-07-06

another missing inhib check

359. By <email address hidden> on 2020-07-08

allowed compilation for Mac

360. By <email address hidden> on 2020-07-08

updated readme as TAR is now possible for all platforms

361. By Kenneth Yrke Jørgensen on 2020-07-09

Updated argeument for cross compile glpk for windows

362. By Kenneth Yrke Jørgensen on 2020-08-18

Updated readme with info for cross-compile

363. By Kenneth Yrke Jørgensen on 2020-09-11

Updated readme

364. By <email address hidden> on 2020-09-11

updated README with compilation instructions for mac

Jiri Srba (srba) wrote :

It now compiles for all three platforms!

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file '.bzrignore'
2--- .bzrignore 2018-03-06 02:18:12 +0000
3+++ .bzrignore 2020-09-11 14:21:20 +0000
4@@ -2,10 +2,12 @@
5 *.creator
6 *.files
7 *.includes
8-verifypn-experimental-linux64
9 *.user
10-verifypn-linux64
11-verifypn-osx64
12 nbproject/
13 cmake-build-*
14-.idea/
15\ No newline at end of file
16+.idea/
17+src/PetriEngine/PQL/PQLQueryParser.parser.cpp
18+src/PetriEngine/PQL/PQLQueryParser.parser.hpp
19+src/PetriEngine/PQL/PQLQueryTokens.lexer.cpp
20+build/
21+
22
23=== modified file 'CMakeLists.txt'
24--- CMakeLists.txt 2018-06-12 16:18:51 +0000
25+++ CMakeLists.txt 2020-09-11 14:21:20 +0000
26@@ -1,46 +1,105 @@
27-cmake_minimum_required(VERSION 2.8.4)
28-project(verifypn)
29+cmake_minimum_required(VERSION 3.9)
30+cmake_policy(SET CMP0048 NEW)
31+cmake_policy(SET CMP0069 NEW)
32+
33+set(CMAKE_CXX_STANDARD 17)
34+if (NOT CMAKE_BUILD_TYPE)
35+ set(CMAKE_BUILD_TYPE Release)
36+endif (NOT CMAKE_BUILD_TYPE)
37+
38+if (CMAKE_BUILD_TYPE MATCHES Release)
39+ if (NOT APPLE)
40+ set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
41+ endif ()
42+endif ()
43+set(CMAKE_POSITION_INDEPENDENT_CODE ON)
44+
45+
46+set(VERIFYPN_VERSION 3.0.1)
47+add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")
48+
49+project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)
50+
51+option(VERIFYPN_Static "Link libraries statically" ON)
52+option(VERIFYPN_MC_Simplification "Enables multicore simplification, incompatible with static linking" OFF)
53+option(VERIFYPN_GetDependencies "Fetch external dependencies from web." ON)
54+
55+
56+if (VERIFYPN_Static)
57+ set(BUILD_SHARED_LIBS OFF)
58+ if (VERIFYPN_MC_Simplification)
59+ message( FATAL_ERROR "Multicore Simplification is not compatible with static linking" )
60+ endif(VERIFYPN_MC_Simplification)
61+ if (NOT APPLE)
62+ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static")
63+ endif(NOT APPLE)
64+else(VERIFYPN_Static)
65+ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static-libgcc -static-libstdc++")
66+endif (VERIFYPN_Static)
67+
68+if (VERIFYPN_MC_Simplification)
69+ add_compile_definitions(VERIFYPN_MC_Simplification)
70+endif(VERIFYPN_MC_Simplification)
71
72 if (UNIX AND NOT APPLE)
73- if (CMAKE_SIZEOF_VOID_P EQUAL 8) # is system 64-bit?
74- set(ARCH_TYPE "linux64")
75- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC -flto -march=x86-64 -std=c++14 -m64 -I.")
76- set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -flto=4 -march=x86-64 -std=c++14 -m64 -static -static-libgcc -static-libstdc++")
77- else()
78- set(ARCH_TYPE "linux32")
79- endif ()
80+ set(ARCH_TYPE "linux64")
81 elseif(APPLE)
82- if (CMAKE_SIZEOF_VOID_P EQUAL 8) # is system 64-bit?
83- set(ARCH_TYPE "osx64")
84- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mmacosx-version-min=10.7 -std=c++14 -m64 -I. -stdlib=libc++")
85- set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -dynamic -mmacosx-version-min=10.7 -std=c++14 -m64 -stdlib=libc++ -lc++")
86- else()
87- set(ARCH_TYPE "osx32")
88- endif ()
89+ set(ARCH_TYPE "osx64")
90+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mmacosx-version-min=10.8 -m64 ")
91+ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -mmacosx-version-min=10.8 -m64 ")
92 else()
93- if (CMAKE_CL_64)
94- set(ARCH_TYPE "win64")
95- else()
96- set(ARCH_TYPE "win32")
97- endif()
98+ set(ARCH_TYPE "win64")
99 endif ()
100
101-set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O2 -DNDEBUG")
102-set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -g")
103-
104-set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O2 -DNDEBUG")
105-set(CMAKE_EXE_LINKER_FLAGS_DEBUG "${CMAKE_EXE_LINKER_FLAGS_DEBUG} -g")
106-
107-include_directories(PUBLIC .)
108-
109-file(GLOB verifypn_SRC
110- "*.h"
111- "*.cpp"
112- "**/*.cpp"
113- "**/*.h"
114- "**/**/*.cpp"
115- "**/**/*.h"
116-)
117-
118-add_executable(verifypn ${verifypn_SRC})
119-target_link_libraries(verifypn ${CMAKE_SOURCE_DIR}/lpsolve/liblpsolve55-${ARCH_TYPE}.a)
120+set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O3 -DNDEBUG")
121+
122+set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O3 -DNDEBUG")
123+if (VERIFYPN_Static AND NOT APPLE)
124+ set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -static")
125+endif()
126+
127+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
128+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
129+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
130+
131+if (VERIFYPN_GetDependencies)
132+ # setup for external imports
133+ include(ExternalProject)
134+ set(EXTERNAL_INSTALL_LOCATION ${CMAKE_BINARY_DIR}/external)
135+
136+ ExternalProject_add(ptrie-ext
137+ GIT_REPOSITORY https://github.com/petergjoel/ptrie
138+ GIT_TAG 230b3640bfbe2ed5befdafbaf17bd3804231b50f
139+ CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION} -DPTRIE_BuildTest=OFF -DCMAKE_BUILD_TYPE=Release
140+ )
141+ ExternalProject_add(rapidxml-ext
142+ URL https://downloads.sourceforge.net/project/rapidxml/rapidxml/rapidxml%201.13/rapidxml-1.13.zip
143+ URL_HASH SHA512=6c10583e6631ccdb0217d0a5381172cb4c1046226de6ef1acf398d85e81d145228e14c3016aefcd7b70a1db8631505b048d8b4f5d4b0dbf1811d2482eefdd265
144+ BUILD_COMMAND ""
145+ CONFIGURE_COMMAND mkdir -p ${CMAKE_BINARY_DIR}/external/include
146+ INSTALL_COMMAND cd ../rapidxml-ext && ${CMAKE_COMMAND} -E copy rapidxml.hpp rapidxml_iterators.hpp rapidxml_print.hpp rapidxml_utils.hpp ${EXTERNAL_INSTALL_LOCATION}/include
147+ )
148+
149+ if (WIN32) #If windows 32 or 64
150+ set(GLPK_CFLAGS "-D __WOE__ -O3" )
151+ else(WIN32)
152+ set(GLPK_CFLAGS "-O3" )
153+ endif(WIN32)
154+ ExternalProject_add(glpk-ext
155+ URL https://ftp.gnu.org/gnu/glpk/glpk-4.65.tar.gz
156+ URL_HASH SHA512=997e8e599ff1718a08c66b86eadd0e01f4644899f1e95920f8ae91d66b4d8361021766b346845f4dcbcfe667b41ab72ea3d377017a0ebf85d7ece091cfd81375
157+ CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} <SOURCE_DIR>/configure --enable-shared=no --prefix=${EXTERNAL_INSTALL_LOCATION} CFLAGS=${GLPK_CFLAGS}
158+ BUILD_COMMAND make
159+ INSTALL_COMMAND make install
160+ PATCH_COMMAND patch -p1 < ${PROJECT_SOURCE_DIR}/glpk-warning.patch
161+ )
162+
163+ link_directories(${EXTERNAL_INSTALL_LOCATION}/lib)
164+ link_directories(${EXTERNAL_INSTALL_LOCATION}/lib64)
165+
166+ # we can now include external libraries
167+ include_directories(${EXTERNAL_INSTALL_LOCATION}/include)
168+endif (VERIFYPN_GetDependencies)
169+include_directories(include)
170+
171+add_subdirectory(${CMAKE_SOURCE_DIR}/src/)
172
173=== removed directory 'CTL'
174=== removed directory 'CTL/Algorithm'
175=== removed file 'CTL/Algorithm/AlgorithmTypes.h'
176=== removed file 'CTL/Algorithm/CertainZeroFPA.cpp'
177=== removed file 'CTL/Algorithm/CertainZeroFPA.h'
178=== removed file 'CTL/Algorithm/FixedPointAlgorithm.cpp'
179=== removed file 'CTL/Algorithm/FixedPointAlgorithm.h'
180=== removed file 'CTL/Algorithm/LocalFPA.cpp'
181=== removed file 'CTL/Algorithm/LocalFPA.h'
182=== removed file 'CTL/CTLEngine.cpp'
183=== removed file 'CTL/CTLEngine.h'
184=== removed file 'CTL/CTLResult.h'
185=== removed directory 'CTL/DependencyGraph'
186=== removed file 'CTL/DependencyGraph/BasicDependencyGraph.h'
187=== removed file 'CTL/DependencyGraph/Configuration.cpp'
188=== removed file 'CTL/DependencyGraph/Configuration.h'
189=== removed file 'CTL/DependencyGraph/Edge.h'
190=== removed file 'CTL/DependencyGraph/assignment.h'
191=== removed directory 'CTL/PetriNets'
192=== removed file 'CTL/PetriNets/OnTheFlyDG.cpp'
193=== removed file 'CTL/PetriNets/OnTheFlyDG.h'
194=== removed file 'CTL/PetriNets/PetriConfig.h'
195=== removed directory 'CTL/SearchStrategy'
196=== removed file 'CTL/SearchStrategy/BFSSearch.h'
197=== removed file 'CTL/SearchStrategy/DFSSearch.h'
198=== removed file 'CTL/SearchStrategy/HeuristicSearch.cpp'
199=== removed file 'CTL/SearchStrategy/HeuristicSearch.h'
200=== removed file 'CTL/SearchStrategy/RDFSSearch.cpp'
201=== removed file 'CTL/SearchStrategy/RDFSSearch.h'
202=== removed file 'CTL/SearchStrategy/SearchStrategy.cpp'
203=== removed file 'CTL/SearchStrategy/SearchStrategy.h'
204=== removed file 'CTL/Stopwatch.h'
205=== removed directory 'PetriEngine'
206=== removed file 'PetriEngine/AbstractPetriNetBuilder.h'
207=== removed directory 'PetriEngine/Colored'
208=== removed file 'PetriEngine/Colored/ColoredNetStructures.h'
209=== removed file 'PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
210=== removed file 'PetriEngine/Colored/ColoredPetriNetBuilder.h'
211=== removed file 'PetriEngine/Colored/Colors.cpp'
212=== removed file 'PetriEngine/Colored/Colors.h'
213=== removed file 'PetriEngine/Colored/Expressions.h'
214=== removed file 'PetriEngine/Colored/Multiset.cpp'
215=== removed file 'PetriEngine/Colored/Multiset.h'
216=== removed file 'PetriEngine/NetStructures.h'
217=== removed directory 'PetriEngine/PQL'
218=== removed file 'PetriEngine/PQL/Contexts.h'
219=== removed file 'PetriEngine/PQL/Expressions.cpp'
220=== removed file 'PetriEngine/PQL/Expressions.h'
221=== removed file 'PetriEngine/PQL/PQL.cpp'
222=== removed file 'PetriEngine/PQL/PQL.h'
223=== removed file 'PetriEngine/PQL/PQLParser.h'
224=== removed file 'PetriEngine/PQL/PQLQueryParser.parser.cpp'
225=== removed file 'PetriEngine/PQL/PQLQueryParser.parser.hpp'
226=== removed file 'PetriEngine/PQL/PQLQueryParser.y'
227=== removed file 'PetriEngine/PQL/PQLQueryTokens.l'
228=== removed file 'PetriEngine/PQL/PQLQueryTokens.lexer.cpp'
229=== removed file 'PetriEngine/PetriNet.cpp'
230=== removed file 'PetriEngine/PetriNet.h'
231=== removed file 'PetriEngine/PetriNetBuilder.cpp'
232=== removed file 'PetriEngine/PetriNetBuilder.h'
233=== removed directory 'PetriEngine/Reachability'
234=== removed file 'PetriEngine/Reachability/ReachabilityResult.h'
235=== removed file 'PetriEngine/Reachability/ReachabilitySearch.cpp'
236=== removed file 'PetriEngine/Reachability/ReachabilitySearch.h'
237=== removed file 'PetriEngine/Reachability/ResultPrinter.cpp'
238=== removed file 'PetriEngine/Reachability/TARReachability.cpp'
239=== removed file 'PetriEngine/Reachability/TARReachability.h'
240=== removed file 'PetriEngine/Reducer.cpp'
241=== removed file 'PetriEngine/Reducer.h'
242=== removed file 'PetriEngine/ReducingSuccessorGenerator.cpp'
243=== removed file 'PetriEngine/ReducingSuccessorGenerator.h'
244=== removed file 'PetriEngine/STSolver.cpp'
245=== removed file 'PetriEngine/STSolver.h'
246=== removed directory 'PetriEngine/Simplification'
247=== removed file 'PetriEngine/Simplification/LPCache.cpp'
248=== removed file 'PetriEngine/Simplification/LPCache.h'
249=== removed file 'PetriEngine/Simplification/LinearProgram.cpp'
250=== removed file 'PetriEngine/Simplification/LinearProgram.h'
251=== removed file 'PetriEngine/Simplification/LinearPrograms.h'
252=== removed file 'PetriEngine/Simplification/Member.h'
253=== removed file 'PetriEngine/Simplification/MurmurHash2.cpp'
254=== removed file 'PetriEngine/Simplification/MurmurHash2.h'
255=== removed file 'PetriEngine/Simplification/Retval.h'
256=== removed file 'PetriEngine/Simplification/Vector.cpp'
257=== removed file 'PetriEngine/Simplification/Vector.h'
258=== removed directory 'PetriEngine/Structures'
259=== removed file 'PetriEngine/Structures/AlignedEncoder.cpp'
260=== removed file 'PetriEngine/Structures/AlignedEncoder.h'
261=== removed file 'PetriEngine/Structures/BitField.h'
262=== removed file 'PetriEngine/Structures/Queue.cpp'
263=== removed file 'PetriEngine/Structures/Queue.h'
264=== removed file 'PetriEngine/Structures/State.h'
265=== removed file 'PetriEngine/Structures/StateSet.h'
266=== removed file 'PetriEngine/Structures/binarywrapper.cpp'
267=== removed file 'PetriEngine/Structures/binarywrapper.h'
268=== removed file 'PetriEngine/Structures/light_deque.h'
269=== removed file 'PetriEngine/Structures/linked_bucket.h'
270=== removed file 'PetriEngine/Structures/ptrie.h'
271=== removed file 'PetriEngine/Structures/ptrie_map.h'
272=== removed file 'PetriEngine/Structures/ptrie_stable.h'
273=== removed file 'PetriEngine/SuccessorGenerator.cpp'
274=== removed file 'PetriEngine/SuccessorGenerator.h'
275=== removed directory 'PetriEngine/TAR'
276=== removed file 'PetriEngine/TAR/AntiChain.h'
277=== removed file 'PetriEngine/TAR/Renamer.h'
278=== removed file 'PetriEngine/TAR/TARAutomata.h'
279=== removed file 'PetriEngine/errorcodes.h'
280=== removed file 'PetriEngine/options.h'
281=== removed directory 'PetriParse'
282=== removed file 'PetriParse/PNMLParser.cpp'
283=== removed file 'PetriParse/PNMLParser.h'
284=== removed file 'PetriParse/QueryBinaryParser.cpp'
285=== removed file 'PetriParse/QueryBinaryParser.h'
286=== removed file 'PetriParse/QueryParser.h'
287=== removed file 'PetriParse/QueryXMLParser.cpp'
288=== removed file 'PetriParse/QueryXMLParser.h'
289=== removed directory 'PetriParse/rapidxml'
290=== removed file 'PetriParse/rapidxml/license.txt'
291=== removed file 'PetriParse/rapidxml/manual.html'
292=== removed file 'PetriParse/rapidxml/rapidxml.hpp'
293=== removed file 'PetriParse/rapidxml/rapidxml_iterators.hpp'
294=== removed file 'PetriParse/rapidxml/rapidxml_print.hpp'
295=== removed file 'PetriParse/rapidxml/rapidxml_utils.hpp'
296=== renamed file 'README.mkd' => 'README.md'
297--- README.mkd 2014-04-21 18:12:28 +0000
298+++ README.md 2020-09-11 14:21:20 +0000
299@@ -1,58 +1,71 @@
300-VerifyPN
301-========
302+# VerifyPN
303 VerifyPN is based on [PeTe](https://github.com/jopsen/PeTe) and aims to provide
304 a fast untimed engine for TAPAAL.
305
306-Building VerifyPN
307------------------
308-VerifyPN is build using a simple makefile, depending on you platform and
309-configuration of it, you might need to modify the makefile in order link
310-correctly against following dependencies:
311-
312- * GNU Bison (>= 2.4)
313- * flex (>= 2.5)
314- * lp_solve (>= 5.5)
315-
316-For simplicity, compiled output form GNU Bison, flex and binaries of lpsolve
317-are included in the source tree.
318-
319-To cross compile for Windows on linux install `g++-mingw-w64` and run
320-`make -f makefile.win32` for 32 bit version, and `make -f makefile.win64` for
321-64 bit version.
322-
323-**Warning** both `verifypn-win32` and `verifypn-win64` are accompanied by a dll
324-called `lpsolve55.dll`, however, this is **not** the same dll for both 32 and 64
325-bit versions. Unfortunately, we cannot rename the dll either, so either we need
326-to build with MSVC or accept this pain, and distribute Windows 32 and 64 bit
327-versions in different folders, and watch out of this during deployment.
328-
329-To cross compile for 32 bit linux you need to run install `gcc-multilib`,
330-`g++-multilib` and probably a few others.
331-
332-To build on OS X run `make -f makefile.osx32` or `make -f makefile.osx64`,
333-as cross compilers for OS X are not readily available (e.g. in package manager)
334-cross compilation for OS X is not supported.
335-
336-Testing
337--------
338-VerifyPN builds can be validated with `make check` (for the respective makefiles).
339-This executes a simple script that iterates over the files in the Tests/ folder,
340-the tested Petri net is <test-name>-<exit-code>-<strategy>.xml and queries for
341-this network is in <test-name>-<exit-code>-<strategy>.xml.q, here <test-name> is
342-an identifier for the test, <exit-code> is the exit code expected by VerifyPN when
343-given the Petri net and query. <strategy> is the search strategy used for the
344-verification, `All` if all strategies should be tested.
345-
346-License
347--------
348-VerifyPN is available under the terms of the GNU GPL versoin 3 or
349+## License
350+VerifyPN is available under the terms of the GNU GPL version 3 or
351 (at your option) any later version.
352 If this license doesn't suit you're welcome to contact us, and purpose an
353 alternative license.
354
355-Authors
356--------
357- * Jonas Finnemann Jensen
358- * Thomas Søndersø Nielsen
359- * Lars Kærlund Østergaard
360- * Jiri Srba
361+## Compilation
362+Requirements for compilation
363+```
364+cmake >= 3.9
365+flex >= 2.6.4
366+bison >= 3.0.5
367+gmp-static (required only for model checking competition)
368+
369+sudo apt update
370+sudo apt install build-essential cmake flex bison brz
371+
372+```
373+
374+The four distributions of VerifyPN can be compiled as follows
375+### Linux64 and OSX64
376+```
377+bzr branch lp:verifypn
378+mkdir build && cd build
379+cmake .. -DVERIFYPN_Static=ON -DVERIFYPN_MC_Simplification=OFF
380+
381+#For mac, one need to enforce that we use the GCC compiler using:
382+export CC=gcc-9
383+export CXX=g++-9
384+#and point to the correct version of flex and bison by adding
385+#-DBISON_EXECUTABLE=/usr/local/opt/bison/bin/bison -DFLEX_EXECUTABLE=/usr/local/opt/flex/bin/flex
386+#to cmake call
387+
388+```
389+
390+### Windows 64 cross-compilation with minGW
391+Install cross-compiler and libs
392+
393+```
394+sudo apt install mingw-w64-x86-64-dev mingw-w64-tools g++-mingw-w64-x86-64
395+sudo apt install wine wine-binfmt #Needed to run tests compile
396+```
397+
398+To build
399+
400+```
401+mkdir build-win && cd build-win
402+cmake .. -DVERIFYPN_Static=ON -DVERIFYPN_MC_Simplification=OFF -DCMAKE_TOOLCHAIN_FILE=../toolchain-x86_64-w64-mingw32.cmake
403+make
404+```
405+
406+### Linux64 - Model Checking Competition
407+```
408+mkdir build
409+cd build
410+cmake .. -DVERIFYPN_Static=OFF -DVERIFYPN_MC_Simplification=ON
411+make
412+```
413+
414+### Mac 64 compilation
415+```
416+mkdir build
417+cd build
418+cmake -DVERIFYPN_MC_Simplification=OFF -DBISON_EXECUTABLE=/usr/local/opt/bison/bin/bison -DFLEX_EXECUTABLE=/usr/local/opt/flex/bin/flex -DCMAKE_C_COMPILER=/usr/local/bin/gcc-9 -DCMAKE_CXX_COMPILER=/usr/local/bin/g++-9 ..
419+make
420+```
421+
422
423=== removed file 'VerifyPN.cpp'
424=== added file 'glpk-warning.patch'
425--- glpk-warning.patch 1970-01-01 00:00:00 +0000
426+++ glpk-warning.patch 2020-09-11 14:21:20 +0000
427@@ -0,0 +1,10 @@
428+--- a/src/draft/glpios03.c
429++++ b/src/draft/glpios03.c
430+@@ -925,7 +925,6 @@
431+ #if 0 /* 20/I-2018 */
432+ xprintf("WARNING: LONG-STEP DUAL SIMPLEX WILL BE USED\n");
433+ #else
434+- xprintf("Long-step dual simplex will be used\n");
435+ #endif
436+ #endif
437+ /* on entry to the B&B driver it is assumed that the active list
438
439=== added directory 'include'
440=== added directory 'include/CTL'
441=== added directory 'include/CTL/Algorithm'
442=== added file 'include/CTL/Algorithm/AlgorithmTypes.h'
443--- include/CTL/Algorithm/AlgorithmTypes.h 1970-01-01 00:00:00 +0000
444+++ include/CTL/Algorithm/AlgorithmTypes.h 2020-09-11 14:21:20 +0000
445@@ -0,0 +1,10 @@
446+#ifndef ALGORITHMTYPES_H
447+#define ALGORITHMTYPES_H
448+
449+namespace CTL {
450+
451+enum CTLAlgorithmType{
452+ Local = 0, CZero = 1
453+};
454+}
455+#endif // ALGORITHMTYPES_H
456
457=== added file 'include/CTL/Algorithm/CertainZeroFPA.h'
458--- include/CTL/Algorithm/CertainZeroFPA.h 1970-01-01 00:00:00 +0000
459+++ include/CTL/Algorithm/CertainZeroFPA.h 2020-09-11 14:21:20 +0000
460@@ -0,0 +1,36 @@
461+#ifndef CERTAINZEROFPA_H
462+#define CERTAINZEROFPA_H
463+
464+#include "FixedPointAlgorithm.h"
465+#include "CTL/DependencyGraph/Edge.h"
466+#include "CTL/DependencyGraph/Configuration.h"
467+#include "PetriEngine/Reachability/ReachabilitySearch.h"
468+#include "CTL/SearchStrategy/SearchStrategy.h"
469+
470+
471+namespace Algorithm {
472+
473+class CertainZeroFPA : public FixedPointAlgorithm
474+{
475+public:
476+ CertainZeroFPA(PetriEngine::Reachability::Strategy type) : FixedPointAlgorithm(type)
477+ {
478+ }
479+ virtual ~CertainZeroFPA()
480+ {
481+ }
482+ virtual bool search(DependencyGraph::BasicDependencyGraph &t_graph) override;
483+protected:
484+
485+ DependencyGraph::BasicDependencyGraph *graph;
486+ DependencyGraph::Configuration* vertex;
487+
488+ void checkEdge(DependencyGraph::Edge* e, bool only_assign = false);
489+ void finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a);
490+ void explore(DependencyGraph::Configuration *c);
491+ void addDependency(DependencyGraph::Edge *e,
492+ DependencyGraph::Configuration *target);
493+
494+};
495+}
496+#endif // CERTAINZEROFPA_H
497
498=== added file 'include/CTL/Algorithm/FixedPointAlgorithm.h'
499--- include/CTL/Algorithm/FixedPointAlgorithm.h 1970-01-01 00:00:00 +0000
500+++ include/CTL/Algorithm/FixedPointAlgorithm.h 2020-09-11 14:21:20 +0000
501@@ -0,0 +1,32 @@
502+#ifndef FIXEDPOINTALGORITHM_H
503+#define FIXEDPOINTALGORITHM_H
504+
505+#include "CTL/DependencyGraph/BasicDependencyGraph.h"
506+#include "CTL/SearchStrategy/SearchStrategy.h"
507+#include "PetriEngine/Reachability/ReachabilitySearch.h"
508+
509+namespace Algorithm {
510+
511+class FixedPointAlgorithm {
512+public:
513+ virtual bool search(DependencyGraph::BasicDependencyGraph &graph) =0;
514+ FixedPointAlgorithm(PetriEngine::Reachability::Strategy type);
515+ virtual ~FixedPointAlgorithm(){}
516+
517+ size_t processedEdges() const { return _processedEdges; }
518+ size_t processedNegationEdges() const { return _processedNegationEdges; }
519+ size_t exploredConfigurations() const { return _exploredConfigurations; }
520+ size_t numberOfEdges() const { return _numberOfEdges; }
521+protected:
522+ std::shared_ptr<SearchStrategy::SearchStrategy> strategy;
523+ //total number of processed edges
524+ size_t _processedEdges = 0;
525+ //total number of processed negation edges
526+ size_t _processedNegationEdges = 0;
527+ //number of explored configurations
528+ size_t _exploredConfigurations = 0;
529+ //total number of edges found when computing successors
530+ size_t _numberOfEdges = 0;
531+};
532+}
533+#endif // FIXEDPOINTALGORITHM_H
534
535=== added file 'include/CTL/Algorithm/LocalFPA.h'
536--- include/CTL/Algorithm/LocalFPA.h 1970-01-01 00:00:00 +0000
537+++ include/CTL/Algorithm/LocalFPA.h 2020-09-11 14:21:20 +0000
538@@ -0,0 +1,29 @@
539+#ifndef LOCALFPA_H
540+#define LOCALFPA_H
541+
542+#include "FixedPointAlgorithm.h"
543+#include "../DependencyGraph/Configuration.h"
544+
545+namespace Algorithm {
546+
547+class LocalFPA : public FixedPointAlgorithm
548+{
549+
550+ // FixedPointAlgorithm interface
551+public:
552+ LocalFPA(PetriEngine::Reachability::Strategy type) : FixedPointAlgorithm(type)
553+ {
554+ }
555+ virtual ~LocalFPA (){}
556+ virtual bool search(DependencyGraph::BasicDependencyGraph &graph);
557+
558+protected:
559+ DependencyGraph::BasicDependencyGraph *graph;
560+
561+ void finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a);
562+ void explore(DependencyGraph::Configuration *c);
563+ void addDependency(DependencyGraph::Edge *e,
564+ DependencyGraph::Configuration *target);
565+};
566+}
567+#endif // LOCALFPA_H
568
569=== added file 'include/CTL/CTLEngine.h'
570--- include/CTL/CTLEngine.h 1970-01-01 00:00:00 +0000
571+++ include/CTL/CTLEngine.h 2020-09-11 14:21:20 +0000
572@@ -0,0 +1,25 @@
573+#ifndef CTLENGINE_H
574+#define CTLENGINE_H
575+
576+#include "../PetriEngine/errorcodes.h"
577+#include "../PetriEngine/PetriNet.h"
578+#include "../PetriEngine/Reachability/ReachabilitySearch.h"
579+
580+#include "Algorithm/AlgorithmTypes.h"
581+#include "../PetriEngine/PQL/PQL.h"
582+
583+#include <set>
584+
585+ReturnValue CTLMain(PetriEngine::PetriNet* net,
586+ CTL::CTLAlgorithmType algorithmtype,
587+ PetriEngine::Reachability::Strategy strategytype,
588+ bool gamemode,
589+ bool printstatistics,
590+ bool mccoutput,
591+ bool partial_order,
592+ const std::vector<std::string>& querynames,
593+ const std::vector<std::shared_ptr<PetriEngine::PQL::Condition>>& reducedQueries,
594+ const std::vector<size_t>& ids,
595+ options_t& options);
596+
597+#endif // CTLENGINE_H
598
599=== added file 'include/CTL/CTLResult.h'
600--- include/CTL/CTLResult.h 1970-01-01 00:00:00 +0000
601+++ include/CTL/CTLResult.h 2020-09-11 14:21:20 +0000
602@@ -0,0 +1,33 @@
603+#ifndef CTLRESULT_H
604+#define CTLRESULT_H
605+
606+#include "../PetriEngine/errorcodes.h"
607+#include "../PetriEngine/PQL/PQL.h"
608+
609+#include <string>
610+
611+struct CTLResult {
612+ CTLResult(const PetriEngine::PQL::Condition_ptr& qry){
613+ query = qry;
614+ }
615+
616+ PetriEngine::PQL::Condition_ptr query;
617+ bool result;
618+
619+ double duration = 0;
620+ size_t numberOfMarkings = 0;
621+ size_t numberOfConfigurations = 0;
622+ size_t processedEdges = 0;
623+ size_t processedNegationEdges = 0;
624+ size_t exploredConfigurations = 0;
625+ size_t numberOfEdges = 0;
626+#ifdef VERIFYPNDIST
627+ size_t numberOfRoundsComputingDistance = 0;
628+ size_t numberOfTokensReceived = 0;
629+ size_t numberOfRequestsReceived = 0;
630+ size_t numberOfAnswersReceived = 0;
631+ size_t numberOfMessagesSend = 0;
632+#endif
633+};
634+
635+#endif // CTLRESULT_H
636
637=== added directory 'include/CTL/DependencyGraph'
638=== added file 'include/CTL/DependencyGraph/BasicDependencyGraph.h'
639--- include/CTL/DependencyGraph/BasicDependencyGraph.h 1970-01-01 00:00:00 +0000
640+++ include/CTL/DependencyGraph/BasicDependencyGraph.h 2020-09-11 14:21:20 +0000
641@@ -0,0 +1,23 @@
642+#ifndef ABSTRACTDEPENDENCYGRAPH_H
643+#define ABSTRACTDEPENDENCYGRAPH_H
644+
645+#include <cstddef>
646+#include <vector>
647+#include <cstdint>
648+
649+namespace DependencyGraph {
650+
651+class Configuration;
652+class Edge;
653+
654+class BasicDependencyGraph {
655+
656+public:
657+ virtual std::vector<Edge*> successors(Configuration *c) =0;
658+ virtual Configuration *initialConfiguration() =0;
659+ virtual void release(Edge* e) = 0;
660+ virtual void cleanUp() =0;
661+};
662+
663+}
664+#endif // ABSTRACTDEPENDENCYGRAPH_H
665
666=== added file 'include/CTL/DependencyGraph/Configuration.h'
667--- include/CTL/DependencyGraph/Configuration.h 1970-01-01 00:00:00 +0000
668+++ include/CTL/DependencyGraph/Configuration.h 2020-09-11 14:21:20 +0000
669@@ -0,0 +1,40 @@
670+#ifndef CONFIGURATION_H
671+#define CONFIGURATION_H
672+
673+#include "Edge.h"
674+
675+#include <string>
676+#include <cstdio>
677+#include <iostream>
678+#include <vector>
679+
680+namespace DependencyGraph {
681+
682+class Edge;
683+
684+enum Assignment {
685+ ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2
686+};
687+
688+class Configuration
689+{
690+ uint32_t distance = 0;
691+public:
692+
693+ uint32_t getDistance() const { return distance; }
694+ void setDistance(uint32_t value) { distance = value; }
695+
696+ Configuration() {}
697+ virtual ~Configuration();
698+
699+ bool isDone() const { return assignment == ONE || assignment == CZERO; }
700+
701+ uint32_t owner = 0;
702+ uint32_t nsuccs = 0;
703+ std::vector<Edge*> dependency_set;
704+ Assignment assignment = UNKNOWN;
705+};
706+
707+
708+}
709+#endif // CONFIGURATION_H
710
711=== added file 'include/CTL/DependencyGraph/Edge.h'
712--- include/CTL/DependencyGraph/Edge.h 1970-01-01 00:00:00 +0000
713+++ include/CTL/DependencyGraph/Edge.h 2020-09-11 14:21:20 +0000
714@@ -0,0 +1,36 @@
715+#ifndef EDGE_H
716+#define EDGE_H
717+
718+#include <cstdio>
719+#include <vector>
720+#include <string>
721+#include <algorithm>
722+#include <cassert>
723+
724+namespace DependencyGraph {
725+
726+class Configuration;
727+
728+class Edge {
729+ typedef std::vector<Configuration*> container;
730+public:
731+ Edge(){}
732+ Edge(Configuration &t_source) : source(&t_source) {}
733+
734+ void addTarget(Configuration* conf)
735+ {
736+ assert(conf);
737+ targets.push_back(conf);
738+ }
739+
740+ Configuration* source;
741+ container targets;
742+ uint8_t status = 0;
743+ bool processed = false;
744+ bool is_negated = false;
745+ int32_t refcnt = 0;
746+ bool handled = false;
747+ uint32_t weight = 0;
748+};
749+}
750+#endif // EDGE_H
751
752=== added file 'include/CTL/DependencyGraph/assignment.h'
753--- include/CTL/DependencyGraph/assignment.h 1970-01-01 00:00:00 +0000
754+++ include/CTL/DependencyGraph/assignment.h 2020-09-11 14:21:20 +0000
755@@ -0,0 +1,11 @@
756+#ifndef ASSIGNMENT_H
757+#define ASSIGNMENT_H
758+
759+namespace DependencyGraph {
760+
761+enum Assignment {
762+ ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2
763+};
764+}
765+
766+#endif // ASSIGNMENT_H
767
768=== added directory 'include/CTL/PetriNets'
769=== added file 'include/CTL/PetriNets/OnTheFlyDG.h'
770--- include/CTL/PetriNets/OnTheFlyDG.h 1970-01-01 00:00:00 +0000
771+++ include/CTL/PetriNets/OnTheFlyDG.h 2020-09-11 14:21:20 +0000
772@@ -0,0 +1,115 @@
773+#ifndef ONTHEFLYDG_H
774+#define ONTHEFLYDG_H
775+
776+#include <functional>
777+#include <stack>
778+#include <ptrie/ptrie_map.h>
779+
780+#include "CTL/DependencyGraph/BasicDependencyGraph.h"
781+#include "CTL/DependencyGraph/Configuration.h"
782+#include "CTL/DependencyGraph/Edge.h"
783+#include "PetriConfig.h"
784+#include "PetriParse/PNMLParser.h"
785+#include "PetriEngine/PQL/PQL.h"
786+#include "PetriEngine/Structures/AlignedEncoder.h"
787+#include "PetriEngine/Structures/linked_bucket.h"
788+#include "PetriEngine/ReducingSuccessorGenerator.h"
789+
790+namespace PetriNets {
791+class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
792+{
793+public:
794+ using Condition = PetriEngine::PQL::Condition;
795+ using Condition_ptr = PetriEngine::PQL::Condition_ptr;
796+ using Marking = PetriEngine::Structures::State;
797+ OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
798+
799+ virtual ~OnTheFlyDG();
800+
801+ //Dependency graph interface
802+ virtual std::vector<DependencyGraph::Edge*> successors(DependencyGraph::Configuration *c) override;
803+ virtual DependencyGraph::Configuration *initialConfiguration() override;
804+ virtual void cleanUp() override;
805+ void setQuery(const Condition_ptr& query);
806+
807+ virtual void release(DependencyGraph::Edge* e) override;
808+
809+ size_t owner(Marking& marking, Condition* cond);
810+ size_t owner(Marking& marking, const Condition_ptr& cond)
811+ {
812+ return owner(marking, cond.get());
813+ }
814+
815+
816+ //stats
817+ size_t configurationCount() const;
818+ size_t markingCount() const;
819+
820+ Condition::Result initialEval();
821+
822+protected:
823+
824+ //initialized from constructor
825+ AlignedEncoder encoder;
826+ PetriEngine::PetriNet *net = nullptr;
827+ PetriConfig* initial_config;
828+ Marking working_marking;
829+ Marking query_marking;
830+ uint32_t n_transitions = 0;
831+ uint32_t n_places = 0;
832+ size_t _markingCount = 0;
833+ size_t _configurationCount = 0;
834+ //used after query is set
835+ Condition_ptr query = nullptr;
836+
837+ Condition::Result fastEval(Condition* query, Marking* unfolded);
838+ Condition::Result fastEval(const Condition_ptr& query, Marking* unfolded)
839+ {
840+ return fastEval(query.get(), unfolded);
841+ }
842+ void nextStates(Marking& t_marking, Condition*,
843+ std::function<void ()> pre,
844+ std::function<bool (Marking&)> foreach,
845+ std::function<void ()> post);
846+ template<typename T>
847+ void dowork(T& gen, bool& first,
848+ std::function<void ()>& pre,
849+ std::function<bool (Marking&)>& foreach)
850+ {
851+ gen.prepare(&query_marking);
852+
853+ while(gen.next(working_marking)){
854+ if(first) pre();
855+ first = false;
856+ if(!foreach(working_marking))
857+ {
858+ gen.reset();
859+ break;
860+ }
861+ }
862+ }
863+ PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
864+ PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
865+ {
866+ return createConfiguration(marking, own, query.get());
867+ }
868+ size_t createMarking(Marking &marking);
869+ void markingStats(const uint32_t* marking, size_t& sum, bool& allsame, uint32_t& val, uint32_t& active, uint32_t& last);
870+
871+ DependencyGraph::Edge* newEdge(DependencyGraph::Configuration &t_source, uint32_t weight);
872+
873+ std::stack<DependencyGraph::Edge*> recycle;
874+ ptrie::map<ptrie::uchar, std::vector<PetriConfig*> > trie;
875+ linked_bucket_t<DependencyGraph::Edge,1024*10>* edge_alloc = nullptr;
876+
877+ // Problem with linked bucket and complex constructor
878+ linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>* conf_alloc = nullptr;
879+
880+ PetriEngine::ReducingSuccessorGenerator _redgen;
881+ bool _partial_order = false;
882+
883+};
884+
885+
886+}
887+#endif // ONTHEFLYDG_H
888
889=== added file 'include/CTL/PetriNets/PetriConfig.h'
890--- include/CTL/PetriNets/PetriConfig.h 1970-01-01 00:00:00 +0000
891+++ include/CTL/PetriNets/PetriConfig.h 2020-09-11 14:21:20 +0000
892@@ -0,0 +1,31 @@
893+#ifndef PETRICONFIG_H
894+#define PETRICONFIG_H
895+
896+#include "CTL/DependencyGraph/Configuration.h"
897+#include "PetriEngine/PQL/PQL.h"
898+
899+#include <sstream>
900+
901+namespace PetriNets {
902+
903+class PetriConfig : public DependencyGraph::Configuration {
904+
905+public:
906+ using Condition = PetriEngine::PQL::Condition;
907+ PetriConfig() :
908+ DependencyGraph::Configuration(), marking(0), query(NULL)
909+ {}
910+
911+ PetriConfig(size_t t_marking, Condition *t_query) :
912+ DependencyGraph::Configuration(), marking(t_marking), query(t_query) {
913+ }
914+
915+ virtual ~PetriConfig(){};
916+
917+ size_t marking;
918+ Condition *query;
919+
920+};
921+
922+}
923+#endif // PETRICONFIG_H
924
925=== added directory 'include/CTL/SearchStrategy'
926=== added file 'include/CTL/SearchStrategy/BFSSearch.h'
927--- include/CTL/SearchStrategy/BFSSearch.h 1970-01-01 00:00:00 +0000
928+++ include/CTL/SearchStrategy/BFSSearch.h 2020-09-11 14:21:20 +0000
929@@ -0,0 +1,36 @@
930+/*
931+ * File: Encoder.h
932+ * Author: Peter G. Jensen
933+ *
934+ * Created on March 7, 2018, 1:50 PM
935+ */
936+
937+#ifndef BFSSEARCH_H
938+#define BFSSEARCH_H
939+#include <queue>
940+#include "CTL/DependencyGraph/Edge.h"
941+#include "SearchStrategy.h"
942+
943+namespace SearchStrategy {
944+
945+// A custom search strategy that should ensure as little overhead as possible
946+// while running sequential computation.
947+
948+class BFSSearch : public SearchStrategy {
949+
950+protected:
951+ size_t Wsize() const { return W.size(); };
952+ void pushToW(DependencyGraph::Edge* edge) { W.push(edge); };
953+ DependencyGraph::Edge* popFromW()
954+ {
955+ auto e = W.front();
956+ W.pop();
957+ return e;
958+ };
959+ std::queue<DependencyGraph::Edge*> W;
960+};
961+
962+} // end SearchStrategy
963+
964+#endif /* BFSSEARCH_H */
965+
966
967=== added file 'include/CTL/SearchStrategy/DFSSearch.h'
968--- include/CTL/SearchStrategy/DFSSearch.h 1970-01-01 00:00:00 +0000
969+++ include/CTL/SearchStrategy/DFSSearch.h 2020-09-11 14:21:20 +0000
970@@ -0,0 +1,29 @@
971+#ifndef DFSSEARCH_H
972+#define DFSSEARCH_H
973+
974+#include <stack>
975+#include "CTL/DependencyGraph/Edge.h"
976+#include "SearchStrategy.h"
977+
978+namespace SearchStrategy {
979+
980+// A custom search strategy that should ensure as little overhead as possible
981+// while running sequential computation.
982+
983+class DFSSearch : public SearchStrategy {
984+
985+protected:
986+ size_t Wsize() const { return W.size(); };
987+ void pushToW(DependencyGraph::Edge* edge) { W.push(edge); };
988+ DependencyGraph::Edge* popFromW()
989+ {
990+ auto e = W.top();
991+ W.pop();
992+ return e;
993+ };
994+ std::stack<DependencyGraph::Edge*> W;
995+};
996+
997+} // end SearchStrategy
998+
999+#endif // DFSSEARCH_H
1000
1001=== added file 'include/CTL/SearchStrategy/HeuristicSearch.h'
1002--- include/CTL/SearchStrategy/HeuristicSearch.h 1970-01-01 00:00:00 +0000
1003+++ include/CTL/SearchStrategy/HeuristicSearch.h 2020-09-11 14:21:20 +0000
1004@@ -0,0 +1,32 @@
1005+/*
1006+ * File: Encoder.h
1007+ * Author: Peter G. Jensen
1008+ *
1009+ * Created on March 7, 2018, 1:51 PM
1010+ */
1011+
1012+#ifndef HEURISTICSEARCH_H
1013+#define HEURISTICSEARCH_H
1014+
1015+#include <vector>
1016+#include "CTL/DependencyGraph/Edge.h"
1017+#include "SearchStrategy.h"
1018+
1019+namespace SearchStrategy {
1020+
1021+// A custom search strategy that should ensure as little overhead as possible
1022+// while running sequential computation.
1023+
1024+class HeuristicSearch : public SearchStrategy {
1025+
1026+protected:
1027+ size_t Wsize() const;
1028+ void pushToW(DependencyGraph::Edge* edge);
1029+ DependencyGraph::Edge* popFromW();
1030+ std::vector<DependencyGraph::Edge*> W;
1031+};
1032+
1033+} // end SearchStrategy
1034+
1035+#endif /* HEURISTICSEARCH_H */
1036+
1037
1038=== added file 'include/CTL/SearchStrategy/RDFSSearch.h'
1039--- include/CTL/SearchStrategy/RDFSSearch.h 1970-01-01 00:00:00 +0000
1040+++ include/CTL/SearchStrategy/RDFSSearch.h 2020-09-11 14:21:20 +0000
1041@@ -0,0 +1,34 @@
1042+/*
1043+ * File: Encoder.h
1044+ * Author: Peter G. Jensen
1045+ *
1046+ * Created on March 7, 2018, 1:52 PM
1047+ */
1048+
1049+#ifndef RDFSSEARCH_H
1050+#define RDFSSEARCH_H
1051+
1052+#include <deque>
1053+#include "CTL/DependencyGraph/Edge.h"
1054+#include "SearchStrategy.h"
1055+
1056+namespace SearchStrategy {
1057+
1058+// A custom search strategy that should ensure as little overhead as possible
1059+// while running sequential computation.
1060+
1061+class RDFSSearch : public SearchStrategy {
1062+public:
1063+ void flush();
1064+protected:
1065+ size_t Wsize() const;
1066+ void pushToW(DependencyGraph::Edge* edge);
1067+ DependencyGraph::Edge* popFromW();
1068+ std::vector<DependencyGraph::Edge*> W;
1069+ size_t last_parent = 0;
1070+};
1071+
1072+} // end SearchStrategy
1073+
1074+#endif /* RDFSSEARCH_H */
1075+
1076
1077=== added file 'include/CTL/SearchStrategy/SearchStrategy.h'
1078--- include/CTL/SearchStrategy/SearchStrategy.h 1970-01-01 00:00:00 +0000
1079+++ include/CTL/SearchStrategy/SearchStrategy.h 2020-09-11 14:21:20 +0000
1080@@ -0,0 +1,56 @@
1081+#ifndef ISEARCHSTRATEGY_H
1082+#define ISEARCHSTRATEGY_H
1083+
1084+#include "CTL/DependencyGraph/Edge.h"
1085+#include <sstream>
1086+
1087+namespace SearchStrategy {
1088+
1089+struct Message {
1090+ uint32_t sender;
1091+ uint32_t distance;
1092+ enum Type {HALT = 0, REQUEST = 1, ANSWER_ONE = 2, ANSWER_ZERO = 3} type;
1093+ DependencyGraph::Configuration *configuration;
1094+
1095+ Message() {}
1096+ Message(size_t sender, uint32_t distance, Type type, DependencyGraph::Configuration *configuration) :
1097+ sender(sender), distance(distance), type(type), configuration(configuration) {}
1098+
1099+ std::string ToString() {
1100+ std::stringstream ss;
1101+ ss << "Message from " << sender << ": ";
1102+ ss << (type == HALT ? "Halt" : type == REQUEST ? "Request" : type == ANSWER_ONE ? "Answer 1" : "Answer 0");
1103+ ss << configuration << "\n";
1104+ return ss.str();
1105+ }
1106+};
1107+
1108+
1109+class SearchStrategy
1110+{
1111+public:
1112+ virtual ~SearchStrategy() {};
1113+ bool empty() const;
1114+ void pushEdge(DependencyGraph::Edge *edge);
1115+ void pushDependency(DependencyGraph::Edge* edge);
1116+ void pushNegation(DependencyGraph::Edge *edge);
1117+ DependencyGraph::Edge* popEdge(bool saturate = false);
1118+ size_t size() const;
1119+//#ifdef VERIFYPNDIST
1120+ uint32_t maxDistance() const;
1121+ bool available() const;
1122+ void releaseNegationEdges(uint32_t );
1123+ bool trivialNegation();
1124+ virtual void flush() {};
1125+//#endif
1126+protected:
1127+ virtual size_t Wsize() const = 0;
1128+ virtual void pushToW(DependencyGraph::Edge* edge) = 0;
1129+ virtual DependencyGraph::Edge* popFromW() = 0;
1130+
1131+ std::vector<DependencyGraph::Edge*> N;
1132+ std::vector<DependencyGraph::Edge*> D;
1133+};
1134+
1135+}
1136+#endif // SEARCHSTRATEGY_H
1137
1138=== added file 'include/CTL/Stopwatch.h'
1139--- include/CTL/Stopwatch.h 1970-01-01 00:00:00 +0000
1140+++ include/CTL/Stopwatch.h 2020-09-11 14:21:20 +0000
1141@@ -0,0 +1,40 @@
1142+#ifndef STOPWATCH_H
1143+#define STOPWATCH_H
1144+
1145+#include <ctime>
1146+#include <sstream>
1147+
1148+using namespace std;
1149+
1150+class stopwatch {
1151+ bool _running = false;
1152+ clock_t _start;
1153+ clock_t _stop;
1154+
1155+public:
1156+ double started() const { return _start; }
1157+ double stopped() const { return _stop; }
1158+ bool running() const { return _running; }
1159+ void start() {
1160+ _running = true;
1161+ _start = clock();
1162+ }
1163+ void stop() {
1164+ _stop = clock();
1165+ _running = false;
1166+ }
1167+ double duration() const { return ( (double(_stop - _start))*1000)/CLOCKS_PER_SEC; }
1168+
1169+ ostream &operator<<(ostream &os){
1170+ os << duration() << " ms";
1171+ return os;
1172+ }
1173+
1174+ std::string toString(){
1175+ stringstream ss;
1176+ ss << this;
1177+ return ss.str();
1178+ }
1179+};
1180+
1181+#endif // STOPWATCH_H
1182
1183=== added directory 'include/PetriEngine'
1184=== added file 'include/PetriEngine/AbstractPetriNetBuilder.h'
1185--- include/PetriEngine/AbstractPetriNetBuilder.h 1970-01-01 00:00:00 +0000
1186+++ include/PetriEngine/AbstractPetriNetBuilder.h 2020-09-11 14:21:20 +0000
1187@@ -0,0 +1,114 @@
1188+/* PeTe - Petri Engine exTremE
1189+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
1190+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
1191+ * Lars Kærlund Østergaard <larsko@gmail.com>,
1192+ * Peter Gjøl Jensen <root@petergjoel.dk>
1193+ *
1194+ * This program is free software: you can redistribute it and/or modify
1195+ * it under the terms of the GNU General Public License as published by
1196+ * the Free Software Foundation, either version 3 of the License, or
1197+ * (at your option) any later version.
1198+ *
1199+ * This program is distributed in the hope that it will be useful,
1200+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
1201+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
1202+ * GNU General Public License for more details.
1203+ *
1204+ * You should have received a copy of the GNU General Public License
1205+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
1206+ */
1207+#ifndef ABSTRACTPETRINETBUILDER_H
1208+#define ABSTRACTPETRINETBUILDER_H
1209+
1210+#include <string>
1211+
1212+#include "PQL/PQL.h"
1213+#include "Colored/Multiset.h"
1214+#include "Colored/Expressions.h"
1215+
1216+namespace PetriEngine {
1217+
1218+ /** Abstract builder for petri nets */
1219+ class AbstractPetriNetBuilder {
1220+ protected:
1221+ bool _isColored = false;
1222+
1223+ public:
1224+ /** Add a new place with a unique name */
1225+ virtual void addPlace(const std::string& name,
1226+ int tokens,
1227+ double x = 0,
1228+ double y = 0) = 0;
1229+ /** Add a new colored place with a unique name */
1230+ virtual void addPlace(const std::string& name,
1231+ Colored::ColorType* type,
1232+ Colored::Multiset&& tokens,
1233+ double x = 0,
1234+ double y = 0)
1235+ {
1236+ std::cerr << "Colored places are not supported in standard P/T nets" << std::endl;
1237+ exit(ErrorCode);
1238+ }
1239+ /** Add a new transition with a unique name */
1240+ virtual void addTransition(const std::string& name,
1241+ double x = 0,
1242+ double y = 0) = 0;
1243+ /** Add a new colored transition with a unique name */
1244+ virtual void addTransition(const std::string& name,
1245+ const Colored::GuardExpression_ptr& guard,
1246+ double x = 0,
1247+ double y = 0)
1248+ {
1249+ std::cerr << "Colored transitions are not supported in standard P/T nets" << std::endl;
1250+ exit(ErrorCode);
1251+ }
1252+ /** Add input arc with given weight */
1253+ virtual void addInputArc(const std::string& place,
1254+ const std::string& transition,
1255+ bool inhibitor,
1256+ int) = 0;
1257+ /** Add colored input arc with given arc expression */
1258+ virtual void addInputArc(const std::string& place,
1259+ const std::string& transition,
1260+ const Colored::ArcExpression_ptr& expr)
1261+ {
1262+ std::cerr << "Colored input arcs are not supported in standard P/T nets" << std::endl;
1263+ exit(ErrorCode);
1264+ }
1265+ /** Add output arc with given weight */
1266+ virtual void addOutputArc(const std::string& transition,
1267+ const std::string& place,
1268+ int weight = 1) = 0;
1269+ /** Add output arc with given arc expression */
1270+ virtual void addOutputArc(const std::string& transition,
1271+ const std::string& place,
1272+ const Colored::ArcExpression_ptr& expr)
1273+ {
1274+ std::cerr << "Colored output arcs are not supported in standard P/T nets" << std::endl;
1275+ exit(ErrorCode);
1276+ }
1277+ /** Add color types with id */
1278+ virtual void addColorType(const std::string& id,
1279+ Colored::ColorType* type)
1280+ {
1281+ std::cerr << "Color types are not supported in standard P/T nets" << std::endl;
1282+ exit(ErrorCode);
1283+ }
1284+
1285+ virtual void enableColors() {
1286+ _isColored = true;
1287+ }
1288+
1289+ virtual bool isColored() const {
1290+ return _isColored;
1291+ }
1292+
1293+ virtual void sort() = 0;
1294+
1295+ virtual ~AbstractPetriNetBuilder() {
1296+ }
1297+ };
1298+
1299+}
1300+
1301+#endif // ABSTRACTPETRINETBUILDER_H
1302
1303=== added directory 'include/PetriEngine/Colored'
1304=== added file 'include/PetriEngine/Colored/ColoredNetStructures.h'
1305--- include/PetriEngine/Colored/ColoredNetStructures.h 1970-01-01 00:00:00 +0000
1306+++ include/PetriEngine/Colored/ColoredNetStructures.h 2020-09-11 14:21:20 +0000
1307@@ -0,0 +1,48 @@
1308+/*
1309+ * To change this license header, choose License Headers in Project Properties.
1310+ * To change this template file, choose Tools | Templates
1311+ * and open the template in the editor.
1312+ */
1313+
1314+/*
1315+ * File: ColoredNetStructures.h
1316+ * Author: Klostergaard
1317+ *
1318+ * Created on 17. februar 2018, 17:07
1319+ */
1320+
1321+#ifndef COLOREDNETSTRUCTURES_H
1322+#define COLOREDNETSTRUCTURES_H
1323+
1324+#include <vector>
1325+#include <set>
1326+#include "Colors.h"
1327+#include "Expressions.h"
1328+#include "Multiset.h"
1329+
1330+namespace PetriEngine {
1331+ namespace Colored {
1332+
1333+ struct Arc {
1334+ uint32_t place;
1335+ uint32_t transition;
1336+ ArcExpression_ptr expr;
1337+ bool input;
1338+ };
1339+
1340+ struct Transition {
1341+ std::string name;
1342+ GuardExpression_ptr guard;
1343+ std::vector<Arc> arcs;
1344+ };
1345+
1346+ struct Place {
1347+ std::string name;
1348+ ColorType* type;
1349+ Multiset marking;
1350+ };
1351+ }
1352+}
1353+
1354+#endif /* COLOREDNETSTRUCTURES_H */
1355+
1356
1357=== added file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
1358--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h 1970-01-01 00:00:00 +0000
1359+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h 2020-09-11 14:21:20 +0000
1360@@ -0,0 +1,179 @@
1361+/*
1362+ * File: ColoredPetriNetBuilder.h
1363+ * Author: Klostergaard
1364+ *
1365+ * Created on 17. februar 2018, 16:25
1366+ */
1367+
1368+#ifndef COLOREDPETRINETBUILDER_H
1369+#define COLOREDPETRINETBUILDER_H
1370+
1371+#include <vector>
1372+#include <unordered_map>
1373+
1374+#include "ColoredNetStructures.h"
1375+#include "../AbstractPetriNetBuilder.h"
1376+#include "../PetriNetBuilder.h"
1377+
1378+namespace PetriEngine {
1379+ class ColoredPetriNetBuilder : public AbstractPetriNetBuilder {
1380+ public:
1381+ typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap;
1382+ typedef std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>> PTPlaceMap;
1383+ typedef std::unordered_map<std::string, std::vector<std::string>> PTTransitionMap;
1384+
1385+ public:
1386+ ColoredPetriNetBuilder();
1387+ ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig);
1388+ virtual ~ColoredPetriNetBuilder();
1389+
1390+ void addPlace(const std::string& name,
1391+ int tokens,
1392+ double x = 0,
1393+ double y = 0) override ;
1394+ void addPlace(const std::string& name,
1395+ Colored::ColorType* type,
1396+ Colored::Multiset&& tokens,
1397+ double x = 0,
1398+ double y = 0) override;
1399+ void addTransition(const std::string& name,
1400+ double x = 0,
1401+ double y = 0) override;
1402+ void addTransition(const std::string& name,
1403+ const Colored::GuardExpression_ptr& guard,
1404+ double x = 0,
1405+ double y = 0) override;
1406+ void addInputArc(const std::string& place,
1407+ const std::string& transition,
1408+ bool inhibitor,
1409+ int) override;
1410+ void addInputArc(const std::string& place,
1411+ const std::string& transition,
1412+ const Colored::ArcExpression_ptr& expr) override;
1413+ void addOutputArc(const std::string& transition,
1414+ const std::string& place,
1415+ int weight = 1) override;
1416+ void addOutputArc(const std::string& transition,
1417+ const std::string& place,
1418+ const Colored::ArcExpression_ptr& expr) override;
1419+ void addColorType(const std::string& id,
1420+ Colored::ColorType* type) override;
1421+
1422+
1423+ void sort() override;
1424+
1425+ double getUnfoldTime() const {
1426+ return _time;
1427+ }
1428+
1429+ uint32_t getPlaceCount() const {
1430+ return _places.size();
1431+ }
1432+
1433+ uint32_t getTransitionCount() const {
1434+ return _transitions.size();
1435+ }
1436+
1437+ uint32_t getArcCount() const {
1438+ uint32_t sum = 0;
1439+ for (auto& t : _transitions) {
1440+ sum += t.arcs.size();
1441+ }
1442+ return sum;
1443+ }
1444+
1445+ uint32_t getUnfoldedPlaceCount() const {
1446+ //return _nptplaces;
1447+ return _ptBuilder.numberOfPlaces();
1448+ }
1449+
1450+ uint32_t getUnfoldedTransitionCount() const {
1451+ return _ptBuilder.numberOfTransitions();
1452+ }
1453+
1454+ uint32_t getUnfoldedArcCount() const {
1455+ return _nptarcs;
1456+ }
1457+
1458+ bool isUnfolded() const {
1459+ return _unfolded;
1460+ }
1461+
1462+ const PTPlaceMap& getUnfoldedPlaceNames() const {
1463+ return _ptplacenames;
1464+ }
1465+
1466+ const PTTransitionMap& getUnfoldedTransitionNames() const {
1467+ return _pttransitionnames;
1468+ }
1469+
1470+ PetriNetBuilder& unfold();
1471+ PetriNetBuilder& stripColors();
1472+ private:
1473+ std::unordered_map<std::string,uint32_t> _placenames;
1474+ std::unordered_map<std::string,uint32_t> _transitionnames;
1475+ PTPlaceMap _ptplacenames;
1476+ PTTransitionMap _pttransitionnames;
1477+ uint32_t _nptplaces = 0;
1478+ uint32_t _npttransitions = 0;
1479+ uint32_t _nptarcs = 0;
1480+
1481+ std::vector<Colored::Place> _places;
1482+ std::vector<Colored::Transition> _transitions;
1483+ std::vector<Colored::Arc> _arcs;
1484+ ColorTypeMap _colors;
1485+ PetriNetBuilder _ptBuilder;
1486+ bool _unfolded = false;
1487+ bool _stripped = false;
1488+
1489+ double _time;
1490+
1491+ std::string arcToString(Colored::Arc& arc) const ;
1492+
1493+ void addArc(const std::string& place,
1494+ const std::string& transition,
1495+ const Colored::ArcExpression_ptr& expr,
1496+ bool input);
1497+
1498+ void unfoldPlace(Colored::Place& place);
1499+ void unfoldTransition(Colored::Transition& transition);
1500+ void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
1501+ };
1502+
1503+ class BindingGenerator {
1504+ public:
1505+ class Iterator {
1506+ private:
1507+ BindingGenerator* _generator;
1508+
1509+ public:
1510+ Iterator(BindingGenerator* generator);
1511+
1512+ bool operator==(Iterator& other);
1513+ bool operator!=(Iterator& other);
1514+ Iterator& operator++();
1515+ const Colored::ExpressionContext::BindingMap operator++(int);
1516+ Colored::ExpressionContext::BindingMap& operator*();
1517+ };
1518+ private:
1519+ Colored::GuardExpression_ptr _expr;
1520+ Colored::ExpressionContext::BindingMap _bindings;
1521+ ColoredPetriNetBuilder::ColorTypeMap& _colorTypes;
1522+
1523+ bool eval();
1524+
1525+ public:
1526+ BindingGenerator(Colored::Transition& transition,
1527+ const std::vector<Colored::Arc>& arcs,
1528+ ColoredPetriNetBuilder::ColorTypeMap& colorTypes);
1529+
1530+ Colored::ExpressionContext::BindingMap& nextBinding();
1531+ Colored::ExpressionContext::BindingMap& currentBinding();
1532+ bool isInitial() const;
1533+ Iterator begin();
1534+ Iterator end();
1535+ };
1536+}
1537+
1538+#endif /* COLOREDPETRINETBUILDER_H */
1539+
1540
1541=== added file 'include/PetriEngine/Colored/Colors.h'
1542--- include/PetriEngine/Colored/Colors.h 1970-01-01 00:00:00 +0000
1543+++ include/PetriEngine/Colored/Colors.h 2020-09-11 14:21:20 +0000
1544@@ -0,0 +1,279 @@
1545+/*
1546+ * To change this license header, choose License Headers in Project Properties.
1547+ * To change this template file, choose Tools | Templates
1548+ * and open the template in the editor.
1549+ */
1550+
1551+/*
1552+ * File: Colors.h
1553+ * Author: andreas
1554+ *
1555+ * Created on February 19, 2018, 8:22 PM
1556+ */
1557+
1558+#ifndef COLORS_H
1559+#define COLORS_H
1560+
1561+#include <stdint.h>
1562+#include <stddef.h>
1563+#include <string>
1564+#include <string.h>
1565+#include <utility>
1566+#include <vector>
1567+#include <unordered_map>
1568+
1569+namespace PetriEngine {
1570+ namespace Colored {
1571+ class ColorType;
1572+
1573+ class Color {
1574+ public:
1575+ friend std::ostream& operator<< (std::ostream& stream, const Color& color);
1576+
1577+ protected:
1578+ const std::vector<const Color*> _tuple;
1579+ ColorType* _colorType;
1580+ std::string _colorName;
1581+ uint32_t _id;
1582+
1583+ public:
1584+ Color(ColorType* colorType, uint32_t id, std::vector<const Color*>& colors);
1585+ Color(ColorType* colorType, uint32_t id, const char* color);
1586+ ~Color() {}
1587+
1588+ bool isTuple() const {
1589+ return _tuple.size() > 1;
1590+ }
1591+
1592+ const std::string& getColorName() const {
1593+ if (this->isTuple()) {
1594+ throw "Cannot get color from a tuple color.";
1595+ }
1596+ return _colorName;
1597+ }
1598+
1599+ ColorType* getColorType() const {
1600+ return _colorType;
1601+ }
1602+
1603+ uint32_t getId() const {
1604+ return _id;
1605+ }
1606+
1607+ const Color* operator[] (size_t index) const;
1608+ bool operator< (const Color& other) const;
1609+ bool operator> (const Color& other) const;
1610+ bool operator<= (const Color& other) const;
1611+ bool operator>= (const Color& other) const;
1612+
1613+ bool operator== (const Color& other) const {
1614+ return _colorType == other._colorType && _id == other._id;
1615+ }
1616+ bool operator!= (const Color& other) const {
1617+ return !((*this) == other);
1618+ }
1619+
1620+ const Color& operator++ () const;
1621+ const Color& operator-- () const;
1622+
1623+ std::string toString() const;
1624+ static std::string toString(const Color* color);
1625+ static std::string toString(const std::vector<const Color*>& colors);
1626+ };
1627+
1628+ /*
1629+ * Singleton pattern from:
1630+ * https://stackoverflow.com/questions/1008019/c-singleton-design-pattern
1631+ */
1632+ class DotConstant : public Color {
1633+ private:
1634+ DotConstant();
1635+
1636+ public:
1637+ static const Color* dotConstant() {
1638+ static DotConstant _instance;
1639+
1640+ return &_instance;
1641+ }
1642+
1643+ DotConstant(DotConstant const&) = delete;
1644+ void operator=(DotConstant const&) = delete;
1645+
1646+ bool operator== (const DotConstant& other) {
1647+ return true;
1648+ }
1649+ };
1650+
1651+ class ColorType {
1652+ public:
1653+ class iterator {
1654+ private:
1655+ ColorType& type;
1656+ size_t index;
1657+
1658+ public:
1659+ iterator(ColorType& type, size_t index) : type(type), index(index) {}
1660+
1661+ const Color& operator++() {
1662+ return type[++index];
1663+ }
1664+
1665+ const Color& operator++(int) {
1666+ return type[index++];
1667+ }
1668+
1669+ const Color& operator--() {
1670+ return type[--index];
1671+ }
1672+ const Color& operator--(int) {
1673+ return type[index--];
1674+ }
1675+
1676+ const Color& operator*() {
1677+ return type[index];
1678+ }
1679+
1680+ const Color* operator->() {
1681+ return &type[index];
1682+ }
1683+
1684+ bool operator==(iterator& other) {
1685+ return type == other.type && index == other.index;
1686+ }
1687+
1688+ bool operator!=(iterator& other) {
1689+ return !(type == other.type) || index != other.index;
1690+ }
1691+ };
1692+
1693+ private:
1694+ std::vector<Color> _colors;
1695+ uintptr_t _id;
1696+ std::string _name;
1697+
1698+ public:
1699+ ColorType(std::vector<ColorType*> elements);
1700+ ColorType(std::string name = "Undefined") : _colors(), _name(std::move(name)) {
1701+ _id = (uintptr_t)this;
1702+ }
1703+
1704+ virtual void addColor(const char* colorName);
1705+ virtual void addColor(std::vector<const Color*>& colors);
1706+ virtual void addDot() {
1707+ _colors.push_back(*DotConstant::dotConstant());
1708+ }
1709+
1710+ virtual size_t size() const {
1711+ return _colors.size();
1712+ }
1713+
1714+ virtual const Color& operator[] (size_t index) {
1715+ return _colors[index];
1716+ }
1717+
1718+ virtual const Color& operator[] (int index) {
1719+ return _colors[index];
1720+ }
1721+
1722+ virtual const Color& operator[] (uint32_t index) {
1723+ return _colors[index];
1724+ }
1725+
1726+ virtual const Color* operator[] (const char* index);
1727+
1728+ virtual const Color* operator[] (const std::string& index) {
1729+ return (*this)[index.c_str()];
1730+ }
1731+
1732+ bool operator== (const ColorType& other) const {
1733+ return _id == other._id;
1734+ }
1735+
1736+ uintptr_t getId() {
1737+ return _id;
1738+ }
1739+
1740+ const std::string& getName() const {
1741+ return _name;
1742+ }
1743+
1744+ iterator begin() {
1745+ return {*this, 0};
1746+ }
1747+
1748+ iterator end() {
1749+ return {*this, size()};
1750+ }
1751+ };
1752+
1753+ class ProductType : public ColorType {
1754+ private:
1755+ std::vector<ColorType*> constituents;
1756+ std::unordered_map<size_t,Color> cache;
1757+
1758+ public:
1759+ ProductType(const std::string& name = "Undefined") : ColorType(name) {}
1760+ ~ProductType() {
1761+ cache.clear();
1762+ }
1763+
1764+ void addType(ColorType* type) {
1765+ constituents.push_back(type);
1766+ }
1767+
1768+ void addColor(const char* colorName) override {}
1769+ void addColor(std::vector<const Color*>& colors) override {}
1770+ void addDot() override {}
1771+
1772+ size_t size() const override {
1773+ size_t product = 1;
1774+ for (auto ct : constituents) {
1775+ product *= ct->size();
1776+ }
1777+ return product;
1778+ }
1779+
1780+ bool containsTypes(const std::vector<const ColorType*>& types) const {
1781+ if (constituents.size() != types.size()) return false;
1782+
1783+ for (size_t i = 0; i < constituents.size(); ++i) {
1784+ if (!(*constituents[i] == *types[i])) {
1785+ return false;
1786+ }
1787+ }
1788+
1789+ return true;
1790+ }
1791+
1792+ const Color* getColor(const std::vector<const Color*>& colors);
1793+
1794+ const Color& operator[](size_t index) override;
1795+ const Color& operator[](int index) override {
1796+ return operator[]((size_t)index);
1797+ }
1798+ const Color& operator[](uint32_t index) override {
1799+ return operator[]((size_t)index);
1800+ }
1801+
1802+ const Color* operator[](const char* index) override;
1803+ const Color* operator[](const std::string& index) override;
1804+ };
1805+
1806+ struct Variable {
1807+ std::string name;
1808+ ColorType* colorType;
1809+ };
1810+
1811+ struct Binding {
1812+ Variable* var;
1813+ const Color* color;
1814+
1815+ bool operator==(Binding& other) {
1816+ return var->name.compare(other.var->name);
1817+ }
1818+ };
1819+ }
1820+}
1821+
1822+#endif /* COLORS_H */
1823+
1824
1825=== added file 'include/PetriEngine/Colored/Expressions.h'
1826--- include/PetriEngine/Colored/Expressions.h 1970-01-01 00:00:00 +0000
1827+++ include/PetriEngine/Colored/Expressions.h 2020-09-11 14:21:20 +0000
1828@@ -0,0 +1,658 @@
1829+/*
1830+ * To change this license header, choose License Headers in Project Properties.
1831+ * To change this template file, choose Tools | Templates
1832+ * and open the template in the editor.
1833+ */
1834+
1835+/*
1836+ * File: Expressions.h
1837+ * Author: andreas
1838+ *
1839+ * Created on February 19, 2018, 7:00 PM
1840+ */
1841+
1842+#ifndef COLORED_EXPRESSIONS_H
1843+#define COLORED_EXPRESSIONS_H
1844+
1845+#include <string>
1846+#include <unordered_map>
1847+#include <set>
1848+#include <stdlib.h>
1849+#include <iostream>
1850+#include <cassert>
1851+#include <memory>
1852+
1853+
1854+#include "Colors.h"
1855+#include "Multiset.h"
1856+#include "../errorcodes.h"
1857+
1858+namespace PetriEngine {
1859+ class ColoredPetriNetBuilder;
1860+
1861+ namespace Colored {
1862+ struct ExpressionContext {
1863+ typedef std::unordered_map<std::string, const Color*> BindingMap;
1864+
1865+ BindingMap& binding;
1866+ std::unordered_map<std::string, ColorType*>& colorTypes;
1867+
1868+ const Color* findColor(const std::string& color) const {
1869+ if (color.compare("dot") == 0)
1870+ return DotConstant::dotConstant();
1871+ for (auto& elem : colorTypes) {
1872+ auto col = (*elem.second)[color];
1873+ if (col)
1874+ return col;
1875+ }
1876+ printf("Could not find color: %s\nCANNOT_COMPUTE\n", color.c_str());
1877+ exit(ErrorCode);
1878+ }
1879+
1880+ ProductType* findProductColorType(const std::vector<const ColorType*>& types) const {
1881+ for (auto& elem : colorTypes) {
1882+ auto* pt = dynamic_cast<ProductType*>(elem.second);
1883+ if (pt && pt->containsTypes(types)) {
1884+ return pt;
1885+ }
1886+ }
1887+ return nullptr;
1888+ }
1889+ };
1890+
1891+ class WeightException : public std::exception {
1892+ private:
1893+ std::string _message;
1894+ public:
1895+ explicit WeightException(std::string message) : _message(message) {}
1896+
1897+ const char* what() const noexcept override {
1898+ return ("Undefined weight: " + _message).c_str();
1899+ }
1900+ };
1901+
1902+ class Expression {
1903+ public:
1904+ Expression() {}
1905+
1906+ virtual void getVariables(std::set<Variable*>& variables) const {
1907+ }
1908+
1909+ virtual void expressionType() {
1910+ std::cout << "Expression" << std::endl;
1911+ }
1912+
1913+ virtual std::string toString() const {
1914+ return "Unsupported";
1915+ }
1916+ };
1917+
1918+ class ColorExpression : public Expression {
1919+ public:
1920+ ColorExpression() {}
1921+ virtual ~ColorExpression() {}
1922+
1923+ virtual const Color* eval(ExpressionContext& context) const = 0;
1924+ };
1925+
1926+ class DotConstantExpression : public ColorExpression {
1927+ public:
1928+ const Color* eval(ExpressionContext& context) const override {
1929+ return DotConstant::dotConstant();
1930+ }
1931+ };
1932+
1933+ typedef std::shared_ptr<ColorExpression> ColorExpression_ptr;
1934+
1935+ class VariableExpression : public ColorExpression {
1936+ private:
1937+ Variable* _variable;
1938+
1939+ public:
1940+ const Color* eval(ExpressionContext& context) const override {
1941+ return context.binding[_variable->name];
1942+ }
1943+
1944+ void getVariables(std::set<Variable*>& variables) const override {
1945+ variables.insert(_variable);
1946+ }
1947+
1948+ std::string toString() const override {
1949+ return _variable->name;
1950+ }
1951+
1952+ VariableExpression(Variable* variable)
1953+ : _variable(variable) {}
1954+ };
1955+
1956+ class UserOperatorExpression : public ColorExpression {
1957+ private:
1958+ const Color* _userOperator;
1959+
1960+ public:
1961+ const Color* eval(ExpressionContext& context) const override {
1962+ return _userOperator;
1963+ }
1964+
1965+ std::string toString() const override {
1966+ return _userOperator->toString();
1967+ }
1968+
1969+ UserOperatorExpression(const Color* userOperator)
1970+ : _userOperator(userOperator) {}
1971+ };
1972+
1973+ class UserSortExpression : public Expression {
1974+ private:
1975+ ColorType* _userSort;
1976+
1977+ public:
1978+ ColorType* eval(ExpressionContext& context) const {
1979+ return _userSort;
1980+ }
1981+
1982+ std::string toString() const override {
1983+ return _userSort->getName();
1984+ }
1985+
1986+ UserSortExpression(ColorType* userSort)
1987+ : _userSort(userSort) {}
1988+ };
1989+
1990+ typedef std::shared_ptr<UserSortExpression> UserSortExpression_ptr;
1991+
1992+ class NumberConstantExpression : public Expression {
1993+ private:
1994+ uint32_t _number;
1995+
1996+ public:
1997+ uint32_t eval(ExpressionContext& context) const {
1998+ return _number;
1999+ }
2000+
2001+ NumberConstantExpression(uint32_t number)
2002+ : _number(number) {}
2003+ };
2004+
2005+ typedef std::shared_ptr<NumberConstantExpression> NumberConstantExpression_ptr;
2006+
2007+ class SuccessorExpression : public ColorExpression {
2008+ private:
2009+ ColorExpression_ptr _color;
2010+
2011+ public:
2012+ const Color* eval(ExpressionContext& context) const override {
2013+ return &++(*_color->eval(context));
2014+ }
2015+
2016+ void getVariables(std::set<Variable*>& variables) const override {
2017+ _color->getVariables(variables);
2018+ }
2019+
2020+ std::string toString() const override {
2021+ return _color->toString() + "++";
2022+ }
2023+
2024+ SuccessorExpression(ColorExpression_ptr&& color)
2025+ : _color(std::move(color)) {}
2026+ };
2027+
2028+ class PredecessorExpression : public ColorExpression {
2029+ private:
2030+ ColorExpression_ptr _color;
2031+
2032+ public:
2033+ const Color* eval(ExpressionContext& context) const override {
2034+ return &--(*_color->eval(context));
2035+ }
2036+
2037+ void getVariables(std::set<Variable*>& variables) const override {
2038+ _color->getVariables(variables);
2039+ }
2040+
2041+ std::string toString() const override {
2042+ return _color->toString() + "--";
2043+ }
2044+
2045+ PredecessorExpression(ColorExpression_ptr&& color)
2046+ : _color(std::move(color)) {}
2047+ };
2048+
2049+ class TupleExpression : public ColorExpression {
2050+ private:
2051+ std::vector<ColorExpression_ptr> _colors;
2052+
2053+ public:
2054+ const Color* eval(ExpressionContext& context) const override {
2055+ std::vector<const Color*> colors;
2056+ std::vector<const ColorType*> types;
2057+ for (auto color : _colors) {
2058+ colors.push_back(color->eval(context));
2059+ types.push_back(colors.back()->getColorType());
2060+ }
2061+ ProductType* pt = context.findProductColorType(types);
2062+
2063+ const Color* col = pt->getColor(colors);
2064+ assert(col != nullptr);
2065+ return col;
2066+ }
2067+
2068+ void getVariables(std::set<Variable*>& variables) const override {
2069+ for (auto elem : _colors) {
2070+ elem->getVariables(variables);
2071+ }
2072+ }
2073+
2074+ std::string toString() const override {
2075+ std::string res = "(" + _colors[0]->toString();
2076+ for (uint32_t i = 1; i < _colors.size(); ++i) {
2077+ res += "," + _colors[i]->toString();
2078+ }
2079+ res += ")";
2080+ return res;
2081+ }
2082+
2083+ TupleExpression(std::vector<ColorExpression_ptr>&& colors)
2084+ : _colors(std::move(colors)) {}
2085+ };
2086+
2087+ class GuardExpression : public Expression {
2088+ public:
2089+ GuardExpression() {}
2090+ virtual ~GuardExpression() {}
2091+
2092+ virtual bool eval(ExpressionContext& context) const = 0;
2093+ };
2094+
2095+ typedef std::shared_ptr<GuardExpression> GuardExpression_ptr;
2096+
2097+ class LessThanExpression : public GuardExpression {
2098+ private:
2099+ ColorExpression_ptr _left;
2100+ ColorExpression_ptr _right;
2101+
2102+ public:
2103+ bool eval(ExpressionContext& context) const override {
2104+ return _left->eval(context) < _right->eval(context);
2105+ }
2106+
2107+ void getVariables(std::set<Variable*>& variables) const override {
2108+ _left->getVariables(variables);
2109+ _right->getVariables(variables);
2110+ }
2111+
2112+ LessThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
2113+ : _left(std::move(left)), _right(std::move(right)) {}
2114+ };
2115+
2116+ class GreaterThanExpression : public GuardExpression {
2117+ private:
2118+ ColorExpression_ptr _left;
2119+ ColorExpression_ptr _right;
2120+
2121+ public:
2122+ bool eval(ExpressionContext& context) const override {
2123+ return _left->eval(context) > _right->eval(context);
2124+ }
2125+
2126+ void getVariables(std::set<Variable*>& variables) const override {
2127+ _left->getVariables(variables);
2128+ _right->getVariables(variables);
2129+ }
2130+
2131+ GreaterThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
2132+ : _left(std::move(left)), _right(std::move(right)) {}
2133+ };
2134+
2135+ class LessThanEqExpression : public GuardExpression {
2136+ private:
2137+ ColorExpression_ptr _left;
2138+ ColorExpression_ptr _right;
2139+
2140+ public:
2141+ bool eval(ExpressionContext& context) const override {
2142+ return _left->eval(context) <= _right->eval(context);
2143+ }
2144+
2145+ void getVariables(std::set<Variable*>& variables) const override {
2146+ _left->getVariables(variables);
2147+ _right->getVariables(variables);
2148+ }
2149+
2150+ LessThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
2151+ : _left(std::move(left)), _right(std::move(right)) {}
2152+ };
2153+
2154+ class GreaterThanEqExpression : public GuardExpression {
2155+ private:
2156+ ColorExpression_ptr _left;
2157+ ColorExpression_ptr _right;
2158+
2159+ public:
2160+ bool eval(ExpressionContext& context) const override {
2161+ return _left->eval(context) >= _right->eval(context);
2162+ }
2163+
2164+ void getVariables(std::set<Variable*>& variables) const override {
2165+ _left->getVariables(variables);
2166+ _right->getVariables(variables);
2167+ }
2168+
2169+ GreaterThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
2170+ : _left(std::move(left)), _right(std::move(right)) {}
2171+ };
2172+
2173+ class EqualityExpression : public GuardExpression {
2174+ private:
2175+ ColorExpression_ptr _left;
2176+ ColorExpression_ptr _right;
2177+
2178+ public:
2179+ bool eval(ExpressionContext& context) const override {
2180+ return _left->eval(context) == _right->eval(context);
2181+ }
2182+
2183+ void getVariables(std::set<Variable*>& variables) const override {
2184+ _left->getVariables(variables);
2185+ _right->getVariables(variables);
2186+ }
2187+
2188+ EqualityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
2189+ : _left(std::move(left)), _right(std::move(right)) {}
2190+ };
2191+
2192+ class InequalityExpression : public GuardExpression {
2193+ private:
2194+ ColorExpression_ptr _left;
2195+ ColorExpression_ptr _right;
2196+
2197+ public:
2198+ bool eval(ExpressionContext& context) const override {
2199+ return _left->eval(context) != _right->eval(context);
2200+ }
2201+
2202+ void getVariables(std::set<Variable*>& variables) const override {
2203+ _left->getVariables(variables);
2204+ _right->getVariables(variables);
2205+ }
2206+
2207+ InequalityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
2208+ : _left(std::move(left)), _right(std::move(right)) {}
2209+ };
2210+
2211+ class NotExpression : public GuardExpression {
2212+ private:
2213+ GuardExpression_ptr _expr;
2214+
2215+ public:
2216+ bool eval(ExpressionContext& context) const override {
2217+ return !_expr->eval(context);
2218+ }
2219+
2220+ void getVariables(std::set<Variable*>& variables) const override {
2221+ _expr->getVariables(variables);
2222+ }
2223+
2224+ NotExpression(GuardExpression_ptr&& expr) : _expr(std::move(expr)) {}
2225+ };
2226+
2227+ class AndExpression : public GuardExpression {
2228+ private:
2229+ GuardExpression_ptr _left;
2230+ GuardExpression_ptr _right;
2231+
2232+ public:
2233+ bool eval(ExpressionContext& context) const override {
2234+ return _left->eval(context) && _right->eval(context);
2235+ }
2236+
2237+ void getVariables(std::set<Variable*>& variables) const override {
2238+ _left->getVariables(variables);
2239+ _right->getVariables(variables);
2240+ }
2241+
2242+ AndExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
2243+ : _left(left), _right(right) {}
2244+ };
2245+
2246+ class OrExpression : public GuardExpression {
2247+ private:
2248+ GuardExpression_ptr _left;
2249+ GuardExpression_ptr _right;
2250+
2251+ public:
2252+ bool eval(ExpressionContext& context) const override {
2253+ return _left->eval(context) || _right->eval(context);
2254+ }
2255+
2256+ void getVariables(std::set<Variable*>& variables) const override {
2257+ _left->getVariables(variables);
2258+ _right->getVariables(variables);
2259+ }
2260+
2261+ OrExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
2262+ : _left(std::move(left)), _right(std::move(right)) {}
2263+ };
2264+
2265+ class ArcExpression : public Expression {
2266+ public:
2267+ ArcExpression() {}
2268+ virtual ~ArcExpression() {}
2269+
2270+ virtual Multiset eval(ExpressionContext& context) const = 0;
2271+
2272+ virtual void expressionType() override {
2273+ std::cout << "ArcExpression" << std::endl;
2274+ }
2275+
2276+ virtual uint32_t weight() const = 0;
2277+ };
2278+
2279+ typedef std::shared_ptr<ArcExpression> ArcExpression_ptr;
2280+
2281+ class AllExpression : public Expression {
2282+ private:
2283+ ColorType* _sort;
2284+
2285+ public:
2286+ virtual ~AllExpression() {};
2287+ std::vector<const Color*> eval(ExpressionContext& context) const {
2288+ std::vector<const Color*> colors;
2289+ assert(_sort != nullptr);
2290+ for (size_t i = 0; i < _sort->size(); i++) {
2291+ colors.push_back(&(*_sort)[i]);
2292+ }
2293+ return colors;
2294+ }
2295+
2296+ size_t size() const {
2297+ return _sort->size();
2298+ }
2299+
2300+ std::string toString() const override {
2301+ return _sort->getName() + ".all";
2302+ }
2303+
2304+ AllExpression(ColorType* sort) : _sort(sort)
2305+ {
2306+ assert(sort != nullptr);
2307+ }
2308+ };
2309+
2310+ typedef std::shared_ptr<AllExpression> AllExpression_ptr;
2311+
2312+ class NumberOfExpression : public ArcExpression {
2313+ private:
2314+ uint32_t _number;
2315+ std::vector<ColorExpression_ptr> _color;
2316+ AllExpression_ptr _all;
2317+
2318+ public:
2319+ Multiset eval(ExpressionContext& context) const override {
2320+ std::vector<const Color*> colors;
2321+ if (!_color.empty()) {
2322+ for (auto elem : _color) {
2323+ colors.push_back(elem->eval(context));
2324+ }
2325+ } else if (_all != nullptr) {
2326+ colors = _all->eval(context);
2327+ }
2328+ std::vector<std::pair<const Color*,uint32_t>> col;
2329+ for (auto elem : colors) {
2330+ col.push_back(std::make_pair(elem, _number));
2331+ }
2332+ return Multiset(col);
2333+ }
2334+
2335+ void getVariables(std::set<Variable*>& variables) const override {
2336+ if (_all != nullptr)
2337+ return;
2338+ for (auto elem : _color) {
2339+ elem->getVariables(variables);
2340+ }
2341+ }
2342+
2343+ uint32_t weight() const override {
2344+ if (_all == nullptr)
2345+ return _number * _color.size();
2346+ else
2347+ return _number * _all->size();
2348+ }
2349+
2350+ bool isAll() const {
2351+ return (bool)_all;
2352+ }
2353+
2354+ bool isSingleColor() const {
2355+ return !isAll() && _color.size() == 1;
2356+ }
2357+
2358+ uint32_t number() const {
2359+ return _number;
2360+ }
2361+
2362+ std::string toString() const override {
2363+ if (isAll())
2364+ return std::to_string(_number) + "'(" + _all->toString() + ")";
2365+ std::string res = std::to_string(_number) + "'(" + _color[0]->toString() + ")";
2366+ for (uint32_t i = 1; i < _color.size(); ++i) {
2367+ res += " + ";
2368+ res += std::to_string(_number) + "'(" + _color[i]->toString() + ")";
2369+ }
2370+ return res;
2371+ }
2372+
2373+ NumberOfExpression(std::vector<ColorExpression_ptr>&& color, uint32_t number = 1)
2374+ : _number(number), _color(std::move(color)), _all(nullptr) {}
2375+ NumberOfExpression(AllExpression_ptr&& all, uint32_t number = 1)
2376+ : _number(number), _color(), _all(std::move(all)) {}
2377+ };
2378+
2379+ typedef std::shared_ptr<NumberOfExpression> NumberOfExpression_ptr;
2380+
2381+ class AddExpression : public ArcExpression {
2382+ private:
2383+ std::vector<ArcExpression_ptr> _constituents;
2384+
2385+ public:
2386+ Multiset eval(ExpressionContext& context) const override {
2387+ Multiset ms;
2388+ for (auto expr : _constituents) {
2389+ ms += expr->eval(context);
2390+ }
2391+ return ms;
2392+ }
2393+
2394+ void getVariables(std::set<Variable*>& variables) const override {
2395+ for (auto elem : _constituents) {
2396+ elem->getVariables(variables);
2397+ }
2398+ }
2399+
2400+ uint32_t weight() const override {
2401+ uint32_t res = 0;
2402+ for (auto expr : _constituents) {
2403+ res += expr->weight();
2404+ }
2405+ return res;
2406+ }
2407+
2408+ std::string toString() const override {
2409+ std::string res = _constituents[0]->toString();
2410+ for (uint32_t i = 1; i < _constituents.size(); ++i) {
2411+ res += " + " + _constituents[i]->toString();
2412+ }
2413+ return res;
2414+ }
2415+
2416+ AddExpression(std::vector<ArcExpression_ptr>&& constituents)
2417+ : _constituents(std::move(constituents)) {}
2418+ };
2419+
2420+ class SubtractExpression : public ArcExpression {
2421+ private:
2422+ ArcExpression_ptr _left;
2423+ ArcExpression_ptr _right;
2424+
2425+ public:
2426+ Multiset eval(ExpressionContext& context) const override {
2427+ return _left->eval(context) - _right->eval(context);
2428+ }
2429+
2430+ void getVariables(std::set<Variable*>& variables) const override {
2431+ _left->getVariables(variables);
2432+ _right->getVariables(variables);
2433+ }
2434+
2435+ uint32_t weight() const override {
2436+ auto* left = dynamic_cast<NumberOfExpression*>(_left.get());
2437+ if (!left || !left->isAll()) {
2438+ throw WeightException("Left constituent of subtract is not an all expression!");
2439+ }
2440+ auto* right = dynamic_cast<NumberOfExpression*>(_right.get());
2441+ if (!right || !right->isSingleColor()) {
2442+ throw WeightException("Right constituent of subtract is not a single color number of expression!");
2443+ }
2444+
2445+ uint32_t val = std::min(left->number(), right->number());
2446+ return _left->weight() - val;
2447+ }
2448+
2449+ std::string toString() const override {
2450+ return _left->toString() + " - " + _right->toString();
2451+ }
2452+
2453+ SubtractExpression(ArcExpression_ptr&& left, ArcExpression_ptr&& right)
2454+ : _left(std::move(left)), _right(std::move(right)) {}
2455+ };
2456+
2457+ class ScalarProductExpression : public ArcExpression {
2458+ private:
2459+ uint32_t _scalar;
2460+ ArcExpression_ptr _expr;
2461+
2462+ public:
2463+ Multiset eval(ExpressionContext& context) const override {
2464+ return _expr->eval(context) * _scalar;
2465+ }
2466+
2467+ void getVariables(std::set<Variable*>& variables) const override {
2468+ _expr->getVariables(variables);
2469+ }
2470+
2471+ uint32_t weight() const override {
2472+ return _scalar * _expr->weight();
2473+ }
2474+
2475+ std::string toString() const override {
2476+ return std::to_string(_scalar) + " * " + _expr->toString();
2477+ }
2478+
2479+ ScalarProductExpression(ArcExpression_ptr&& expr, uint32_t scalar)
2480+ : _scalar(std::move(scalar)), _expr(expr) {}
2481+ };
2482+ }
2483+}
2484+
2485+#endif /* COLORED_EXPRESSIONS_H */
2486+
2487
2488=== added file 'include/PetriEngine/Colored/Multiset.h'
2489--- include/PetriEngine/Colored/Multiset.h 1970-01-01 00:00:00 +0000
2490+++ include/PetriEngine/Colored/Multiset.h 2020-09-11 14:21:20 +0000
2491@@ -0,0 +1,83 @@
2492+/*
2493+ * To change this license header, choose License Headers in Project Properties.
2494+ * To change this template file, choose Tools | Templates
2495+ * and open the template in the editor.
2496+ */
2497+
2498+/*
2499+ * File: Multiset.h
2500+ * Author: andreas
2501+ *
2502+ * Created on February 20, 2018, 10:37 AM
2503+ */
2504+
2505+#ifndef MULTISET_H
2506+#define MULTISET_H
2507+
2508+#include <vector>
2509+#include <utility>
2510+
2511+#include "Colors.h"
2512+
2513+
2514+namespace PetriEngine {
2515+ namespace Colored {
2516+ class Multiset {
2517+ private:
2518+ class Iterator {
2519+ private:
2520+ Multiset* ms;
2521+ size_t index;
2522+
2523+ public:
2524+ Iterator(Multiset* ms, size_t index)
2525+ : ms(ms), index(index) {}
2526+
2527+ bool operator==(Iterator& other);
2528+ bool operator!=(Iterator& other);
2529+ Iterator& operator++();
2530+ std::pair<const Color*,uint32_t&> operator++(int);
2531+ std::pair<const Color*,uint32_t&> operator*();
2532+ };
2533+
2534+ typedef std::vector<std::pair<uint32_t,uint32_t>> Internal;
2535+
2536+ public:
2537+ Multiset();
2538+ Multiset(const Multiset& orig);
2539+ Multiset(std::pair<const Color*,uint32_t> color);
2540+ Multiset(std::vector<std::pair<const Color*,uint32_t>>& colors);
2541+ virtual ~Multiset();
2542+
2543+ Multiset operator+ (const Multiset& other) const;
2544+ Multiset operator- (const Multiset& other) const;
2545+ Multiset operator* (uint32_t scalar) const;
2546+ void operator+= (const Multiset& other);
2547+ void operator-= (const Multiset& other);
2548+ void operator*= (uint32_t scalar);
2549+ uint32_t operator[] (const Color* color) const;
2550+ uint32_t& operator[] (const Color* color);
2551+
2552+ bool empty() const;
2553+ void clean();
2554+
2555+ size_t distinctSize() const {
2556+ return _set.size();
2557+ }
2558+
2559+ size_t size() const;
2560+
2561+ Iterator begin();
2562+ Iterator end();
2563+
2564+ std::string toString() const;
2565+
2566+ private:
2567+ Internal _set;
2568+ ColorType* type;
2569+ };
2570+ }
2571+}
2572+
2573+#endif /* MULTISET_H */
2574+
2575
2576=== added file 'include/PetriEngine/NetStructures.h'
2577--- include/PetriEngine/NetStructures.h 1970-01-01 00:00:00 +0000
2578+++ include/PetriEngine/NetStructures.h 2020-09-11 14:21:20 +0000
2579@@ -0,0 +1,91 @@
2580+/*
2581+ * File: NetStructures.h
2582+ * Author: Peter G. Jensen
2583+ *
2584+ * Created on 09 March 2016, 21:08
2585+ */
2586+
2587+#ifndef NETSTRUCTURES_H
2588+#define NETSTRUCTURES_H
2589+
2590+#include <limits>
2591+#include <vector>
2592+
2593+namespace PetriEngine {
2594+
2595+ struct Arc {
2596+ uint32_t place;
2597+ uint32_t weight;
2598+ bool skip = false;
2599+ bool inhib = false;
2600+
2601+ Arc() :
2602+ place(std::numeric_limits<uint32_t>::max()),
2603+ weight(std::numeric_limits<uint32_t>::max()),
2604+ skip(false),
2605+ inhib(false) {
2606+ };
2607+
2608+ bool operator < (const Arc& other) const
2609+ {
2610+ return place < other.place;
2611+ }
2612+
2613+ bool operator == (const Arc& other) const
2614+ {
2615+ return place == other.place && weight == other.weight && inhib == other.inhib;
2616+ }
2617+ };
2618+
2619+ struct Transition {
2620+ std::vector<Arc> pre;
2621+ std::vector<Arc> post;
2622+ bool skip = false;
2623+ bool inhib = false;
2624+
2625+ void addPreArc(const Arc& arc)
2626+ {
2627+ auto lb = std::lower_bound(pre.begin(), pre.end(), arc);
2628+ if(lb != pre.end() && lb->place == arc.place)
2629+ lb->weight += arc.weight;
2630+ else
2631+ lb = pre.insert(lb, arc);
2632+ assert(lb->weight > 0);
2633+ }
2634+
2635+ void addPostArc(const Arc& arc)
2636+ {
2637+ auto lb = std::lower_bound(post.begin(), post.end(), arc);
2638+ if(lb != post.end() && lb->place == arc.place)
2639+ lb->weight += arc.weight;
2640+ else
2641+ lb = post.insert(lb, arc);
2642+ assert(lb->weight > 0);
2643+
2644+ }
2645+ };
2646+
2647+ struct Place {
2648+ std::vector<uint32_t> consumers; // things consuming
2649+ std::vector<uint32_t> producers; // things producing
2650+ bool skip = false;
2651+ bool inhib = false;
2652+
2653+ // should be replaced using concepts in c++20
2654+ void addConsumer(uint32_t id)
2655+ {
2656+ auto lb = std::lower_bound(consumers.begin(), consumers.end(), id);
2657+ if(lb == consumers.end() || *lb != id)
2658+ consumers.insert(lb, id);
2659+ }
2660+
2661+ void addProducer(uint32_t id)
2662+ {
2663+ auto lb = std::lower_bound(producers.begin(), producers.end(), id);
2664+ if(lb == producers.end() || *lb != id)
2665+ producers.insert(lb, id);
2666+ }
2667+ };
2668+}
2669+#endif /* NETSTRUCTURES_H */
2670+
2671
2672=== added directory 'include/PetriEngine/PQL'
2673=== added file 'include/PetriEngine/PQL/Contexts.h'
2674--- include/PetriEngine/PQL/Contexts.h 1970-01-01 00:00:00 +0000
2675+++ include/PetriEngine/PQL/Contexts.h 2020-09-11 14:21:20 +0000
2676@@ -0,0 +1,250 @@
2677+/* PeTe - Petri Engine exTremE
2678+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
2679+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
2680+ * Lars Kærlund Østergaard <larsko@gmail.com>,
2681+ * Peter Gjøl Jensen <root@petergjoel.dk>
2682+ *
2683+ * This program is free software: you can redistribute it and/or modify
2684+ * it under the terms of the GNU General Public License as published by
2685+ * the Free Software Foundation, either version 3 of the License, or
2686+ * (at your option) any later version.
2687+ *
2688+ * This program is distributed in the hope that it will be useful,
2689+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
2690+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2691+ * GNU General Public License for more details.
2692+ *
2693+ * You should have received a copy of the GNU General Public License
2694+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
2695+ */
2696+#ifndef CONTEXTS_H
2697+#define CONTEXTS_H
2698+
2699+#include "../PetriNet.h"
2700+#include "../Simplification/LPCache.h"
2701+#include "PQL.h"
2702+#include "../NetStructures.h"
2703+
2704+#include <string>
2705+#include <vector>
2706+#include <list>
2707+#include <map>
2708+#include <chrono>
2709+#include <glpk.h>
2710+
2711+namespace PetriEngine {
2712+ namespace PQL {
2713+
2714+ /** Context provided for context analysis */
2715+ class AnalysisContext {
2716+ protected:
2717+ const unordered_map<std::string, uint32_t>& _placeNames;
2718+ const unordered_map<std::string, uint32_t>& _transitionNames;
2719+ const PetriNet* _net;
2720+ std::vector<ExprError> _errors;
2721+ public:
2722+
2723+ /** A resolution result */
2724+ struct ResolutionResult {
2725+ /** Offset in relevant vector */
2726+ int offset;
2727+ /** True, if the resolution was successful */
2728+ bool success;
2729+ };
2730+
2731+ AnalysisContext(const std::unordered_map<std::string, uint32_t>& places, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net)
2732+ : _placeNames(places), _transitionNames(tnames), _net(net) {
2733+
2734+ }
2735+
2736+ virtual void setHasDeadlock(){};
2737+
2738+ const PetriNet* net() const
2739+ {
2740+ return _net;
2741+ }
2742+
2743+ /** Resolve an identifier */
2744+ virtual ResolutionResult resolve(const std::string& identifier, bool place = true);
2745+
2746+ /** Report error */
2747+ void reportError(const ExprError& error) {
2748+ _errors.push_back(error);
2749+ }
2750+
2751+ /** Get list of errors */
2752+ const std::vector<ExprError>& errors() const {
2753+ return _errors;
2754+ }
2755+ auto& allPlaceNames() const { return _placeNames; }
2756+ auto& allTransitionNames() const { return _transitionNames; }
2757+
2758+ };
2759+
2760+ class ColoredAnalysisContext : public AnalysisContext {
2761+ protected:
2762+ const std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>>& _coloredPlaceNames;
2763+ const std::unordered_map<std::string, std::vector<std::string>>& _coloredTransitionNames;
2764+
2765+ bool _colored;
2766+
2767+ public:
2768+ ColoredAnalysisContext(const std::unordered_map<std::string, uint32_t>& places,
2769+ const std::unordered_map<std::string, uint32_t>& tnames,
2770+ const PetriNet* net,
2771+ const std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>>& cplaces,
2772+ const std::unordered_map<std::string, std::vector<std::string>>& ctnames,
2773+ bool colored)
2774+ : AnalysisContext(places, tnames, net),
2775+ _coloredPlaceNames(cplaces),
2776+ _coloredTransitionNames(ctnames),
2777+ _colored(colored)
2778+ {}
2779+
2780+ bool resolvePlace(const std::string& place, std::unordered_map<uint32_t,std::string>& out);
2781+
2782+ bool resolveTransition(const std::string& transition, std::vector<std::string>& out);
2783+
2784+ bool isColored() const {
2785+ return _colored;
2786+ }
2787+ auto& allColoredPlaceNames() const { return _coloredPlaceNames; }
2788+ auto& allColoredTransitionNames() const { return _coloredTransitionNames; }
2789+ };
2790+
2791+ /** Context provided for evalation */
2792+ class EvaluationContext {
2793+ public:
2794+
2795+ /** Create evaluation context, this doesn't take ownership */
2796+ EvaluationContext(const MarkVal* marking,
2797+ const PetriNet* net) {
2798+ _marking = marking;
2799+ _net = net;
2800+ }
2801+
2802+ EvaluationContext() {};
2803+
2804+ const MarkVal* marking() const {
2805+ return _marking;
2806+ }
2807+
2808+ void setMarking(MarkVal* marking) {
2809+ _marking = marking;
2810+ }
2811+
2812+ const PetriNet* net() const {
2813+ return _net;
2814+ }
2815+ private:
2816+ const MarkVal* _marking = nullptr;
2817+ const PetriNet* _net = nullptr;
2818+ };
2819+
2820+ /** Context for distance computation */
2821+ class DistanceContext : public EvaluationContext {
2822+ public:
2823+
2824+ DistanceContext(const PetriNet* net,
2825+ const MarkVal* marking)
2826+ : EvaluationContext(marking, net) {
2827+ _negated = false;
2828+ }
2829+
2830+
2831+ void negate() {
2832+ _negated = !_negated;
2833+ }
2834+
2835+ bool negated() const {
2836+ return _negated;
2837+ }
2838+
2839+ private:
2840+ bool _negated;
2841+ };
2842+
2843+ /** Context for condition to TAPAAL export */
2844+ class TAPAALConditionExportContext {
2845+ public:
2846+ bool failed;
2847+ std::string netName;
2848+ };
2849+
2850+ class SimplificationContext {
2851+ public:
2852+
2853+ SimplificationContext(const MarkVal* marking,
2854+ const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
2855+ LPCache* cache)
2856+ : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) {
2857+ _negated = false;
2858+ _marking = marking;
2859+ _net = net;
2860+ _base_lp = buildBase();
2861+ _start = std::chrono::high_resolution_clock::now();
2862+ _cache = cache;
2863+ }
2864+
2865+ virtual ~SimplificationContext() {
2866+ if(_base_lp != nullptr)
2867+ glp_delete_prob(_base_lp);
2868+ _base_lp = nullptr;
2869+ }
2870+
2871+
2872+ const MarkVal* marking() const {
2873+ return _marking;
2874+ }
2875+
2876+ const PetriNet* net() const {
2877+ return _net;
2878+ }
2879+
2880+ void negate() {
2881+ _negated = !_negated;
2882+ }
2883+
2884+ bool negated() const {
2885+ return _negated;
2886+ }
2887+
2888+ void setNegate(bool b){
2889+ _negated = b;
2890+ }
2891+
2892+ double getReductionTime();
2893+
2894+ bool timeout() const {
2895+ auto end = std::chrono::high_resolution_clock::now();
2896+ auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _start);
2897+ return (diff.count() >= _queryTimeout);
2898+ }
2899+
2900+ uint32_t getLpTimeout() const;
2901+
2902+ LPCache* cache() const
2903+ {
2904+ return _cache;
2905+ }
2906+
2907+
2908+ glp_prob* makeBaseLP() const;
2909+
2910+ private:
2911+ bool _negated;
2912+ const MarkVal* _marking;
2913+ const PetriNet* _net;
2914+ uint32_t _queryTimeout, _lpTimeout;
2915+ std::chrono::high_resolution_clock::time_point _start;
2916+ LPCache* _cache;
2917+ mutable glp_prob* _base_lp = nullptr;
2918+
2919+ glp_prob* buildBase() const;
2920+
2921+ };
2922+
2923+ } // PQL
2924+} // PetriEngine
2925+
2926+#endif // CONTEXTS_H
2927
2928=== added file 'include/PetriEngine/PQL/Expressions.h'
2929--- include/PetriEngine/PQL/Expressions.h 1970-01-01 00:00:00 +0000
2930+++ include/PetriEngine/PQL/Expressions.h 2020-09-11 14:21:20 +0000
2931@@ -0,0 +1,1221 @@
2932+/* PeTe - Petri Engine exTremE
2933+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
2934+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
2935+ * Lars Kærlund Østergaard <larsko@gmail.com>,
2936+ * Peter Gjøl Jensen <root@petergjoel.dk>
2937+ *
2938+ * This program is free software: you can redistribute it and/or modify
2939+ * it under the terms of the GNU General Public License as published by
2940+ * the Free Software Foundation, either version 3 of the License, or
2941+ * (at your option) any later version.
2942+ *
2943+ * This program is distributed in the hope that it will be useful,
2944+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
2945+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2946+ * GNU General Public License for more details.
2947+ *
2948+ * You should have received a copy of the GNU General Public License
2949+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
2950+ */
2951+#ifndef EXPRESSIONS_H
2952+#define EXPRESSIONS_H
2953+
2954+
2955+#include <iostream>
2956+#include <fstream>
2957+#include <algorithm>
2958+#include "PQL.h"
2959+#include "Contexts.h"
2960+#include "..//Simplification/Member.h"
2961+#include "../Simplification/LinearPrograms.h"
2962+#include "../Simplification/Retval.h"
2963+
2964+using namespace PetriEngine::Simplification;
2965+
2966+namespace PetriEngine {
2967+ namespace PQL {
2968+
2969+ std::string generateTabs(uint32_t tabs);
2970+ class CompareCondition;
2971+ class NotCondition;
2972+ /******************** EXPRESSIONS ********************/
2973+
2974+ /** Base class for all binary expressions */
2975+ class NaryExpr : public Expr {
2976+ protected:
2977+ NaryExpr() {};
2978+ public:
2979+
2980+ NaryExpr(std::vector<Expr_ptr>&& exprs) : _exprs(std::move(exprs)) {
2981+ }
2982+ virtual void analyze(AnalysisContext& context) override;
2983+ int evaluate(const EvaluationContext& context) override;
2984+ int formulaSize() const override{
2985+ size_t sum = 0;
2986+ for(auto& e : _exprs) sum += e->formulaSize();
2987+ return sum + 1;
2988+ }
2989+ void toString(std::ostream&) const override;
2990+ bool placeFree() const override;
2991+ auto& expressions() const { return _exprs; }
2992+ protected:
2993+ virtual int apply(int v1, int v2) const = 0;
2994+ virtual std::string op() const = 0;
2995+ std::vector<Expr_ptr> _exprs;
2996+ virtual int32_t preOp(const EvaluationContext& context) const;
2997+ };
2998+
2999+ class PlusExpr;
3000+ class MultiplyExpr;
3001+
3002+ class CommutativeExpr : public NaryExpr
3003+ {
3004+ public:
3005+ friend CompareCondition;
3006+ virtual void analyze(AnalysisContext& context) override;
3007+ int evaluate(const EvaluationContext& context) override;
3008+ void toBinary(std::ostream&) const override;
3009+ int formulaSize() const override{
3010+ size_t sum = _ids.size();
3011+ for(auto& e : _exprs) sum += e->formulaSize();
3012+ return sum + 1;
3013+ }
3014+ void toString(std::ostream&) const override;
3015+ bool placeFree() const override;
3016+ auto constant() const { return _constant; }
3017+ auto& places() const { return _ids; }
3018+ protected:
3019+ CommutativeExpr(int constant): _constant(constant) {};
3020+ void init(std::vector<Expr_ptr>&& exprs);
3021+ virtual int32_t preOp(const EvaluationContext& context) const override;
3022+ int32_t _constant;
3023+ std::vector<std::pair<uint32_t,std::string>> _ids;
3024+ Member commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const;
3025+ };
3026+
3027+ /** Binary plus expression */
3028+ class PlusExpr : public CommutativeExpr {
3029+ public:
3030+
3031+ PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk = false);
3032+
3033+ Expr::Types type() const override;
3034+ Member constraint(SimplificationContext& context) const override;
3035+ void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
3036+ bool tk = false;
3037+ void incr(ReducingSuccessorGenerator& generator) const override;
3038+ void decr(ReducingSuccessorGenerator& generator) const override;
3039+ void visit(Visitor& visitor) const override;
3040+ protected:
3041+ int apply(int v1, int v2) const override;
3042+ //int binaryOp() const;
3043+ std::string op() const override;
3044+ };
3045+
3046+ /** Binary minus expression */
3047+ class SubtractExpr : public NaryExpr {
3048+ public:
3049+
3050+ SubtractExpr(std::vector<Expr_ptr>&& exprs) : NaryExpr(std::move(exprs))
3051+ {
3052+ }
3053+ Expr::Types type() const override;
3054+ Member constraint(SimplificationContext& context) const override;
3055+ void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
3056+ void incr(ReducingSuccessorGenerator& generator) const override;
3057+ void decr(ReducingSuccessorGenerator& generator) const override;
3058+ void toBinary(std::ostream&) const override;
3059+ void visit(Visitor& visitor) const override;
3060+ protected:
3061+ int apply(int v1, int v2) const override;
3062+ //int binaryOp() const;
3063+ std::string op() const override;
3064+ };
3065+
3066+ /** Binary multiplication expression **/
3067+ class MultiplyExpr : public CommutativeExpr {
3068+ public:
3069+
3070+ MultiplyExpr(std::vector<Expr_ptr>&& exprs);
3071+ Expr::Types type() const override;
3072+ Member constraint(SimplificationContext& context) const override;
3073+ void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
3074+ void incr(ReducingSuccessorGenerator& generator) const override;
3075+ void decr(ReducingSuccessorGenerator& generator) const override;
3076+ void visit(Visitor& visitor) const override;
3077+ protected:
3078+ int apply(int v1, int v2) const override;
3079+ //int binaryOp() const;
3080+ std::string op() const override;
3081+ };
3082+
3083+ /** Unary minus expression*/
3084+ class MinusExpr : public Expr {
3085+ public:
3086+
3087+ MinusExpr(const Expr_ptr expr) {
3088+ _expr = expr;
3089+ }
3090+ void analyze(AnalysisContext& context) override;
3091+ int evaluate(const EvaluationContext& context) override;
3092+ void toString(std::ostream&) const override;
3093+ Expr::Types type() const override;
3094+ Member constraint(SimplificationContext& context) const override;
3095+ void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
3096+ void toBinary(std::ostream&) const override;
3097+ void incr(ReducingSuccessorGenerator& generator) const override;
3098+ void decr(ReducingSuccessorGenerator& generator) const override;
3099+ void visit(Visitor& visitor) const override;
3100+ int formulaSize() const override{
3101+ return _expr->formulaSize() + 1;
3102+ }
3103+ bool placeFree() const override;
3104+ const Expr_ptr& operator[](size_t i) const { return _expr; };
3105+ private:
3106+ Expr_ptr _expr;
3107+ };
3108+
3109+ /** Literal integer value expression */
3110+ class LiteralExpr : public Expr {
3111+ public:
3112+
3113+ LiteralExpr(int value) : _value(value) {
3114+ }
3115+ void analyze(AnalysisContext& context) override;
3116+ int evaluate(const EvaluationContext& context) override;
3117+ void toString(std::ostream&) const override;
3118+ Expr::Types type() const override;
3119+ void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
3120+ void toBinary(std::ostream&) const override;
3121+ void incr(ReducingSuccessorGenerator& generator) const override;
3122+ void decr(ReducingSuccessorGenerator& generator) const override;
3123+ void visit(Visitor& visitor) const override;
3124+ int formulaSize() const override{
3125+ return 1;
3126+ }
3127+ int value() const {
3128+ return _value;
3129+ };
3130+ Member constraint(SimplificationContext& context) const override;
3131+ bool placeFree() const override { return true; }
3132+ private:
3133+ int _value;
3134+ };
3135+
3136+
3137+ class IdentifierExpr : public Expr {
3138+ public:
3139+ IdentifierExpr(const std::string& name) : _name(name) {}
3140+ void analyze(AnalysisContext& context) override;
3141+ int evaluate(const EvaluationContext& context) override {
3142+ return _compiled->evaluate(context);
3143+ }
3144+ void toString(std::ostream& os) const override {
3145+ if(_compiled)
3146+ _compiled->toString(os);
3147+ else
3148+ os << _name;
3149+ }
3150+ Expr::Types type() const override {
3151+ if(_compiled) return _compiled->type();
3152+ return Expr::IdentifierExpr;
3153+ }
3154+ void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
3155+ _compiled->toXML(os, tabs, tokencount);
3156+ }
3157+ void incr(ReducingSuccessorGenerator& generator) const override {
3158+ _compiled->incr(generator);
3159+ }
3160+ void decr(ReducingSuccessorGenerator& generator) const override {
3161+ _compiled->decr(generator);
3162+ }
3163+ int formulaSize() const override {
3164+ if(_compiled) return _compiled->formulaSize();
3165+ return 1;
3166+ }
3167+ virtual bool placeFree() const override {
3168+ if(_compiled) return _compiled->placeFree();
3169+ return false;
3170+ }
3171+
3172+ Member constraint(SimplificationContext& context) const override {
3173+ return _compiled->constraint(context);
3174+ }
3175+
3176+ void toBinary(std::ostream& s) const override {
3177+ _compiled->toBinary(s);
3178+ }
3179+ void visit(Visitor& visitor) const override;
3180+ private:
3181+ std::string _name;
3182+ Expr_ptr _compiled;
3183+ };
3184+
3185+ /** Identifier expression */
3186+ class UnfoldedIdentifierExpr : public Expr {
3187+ public:
3188+ UnfoldedIdentifierExpr(const std::string& name, int offest)
3189+ : _offsetInMarking(offest), _name(name) {
3190+ }
3191+
3192+ UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
3193+ }
3194+
3195+ void analyze(AnalysisContext& context) override;
3196+ int evaluate(const EvaluationContext& context) override;
3197+ void toString(std::ostream&) const override;
3198+ Expr::Types type() const override;
3199+ void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
3200+ void toBinary(std::ostream&) const override;
3201+ void incr(ReducingSuccessorGenerator& generator) const override;
3202+ void decr(ReducingSuccessorGenerator& generator) const override;
3203+ int formulaSize() const override{
3204+ return 1;
3205+ }
3206+ /** Offset in marking or valuation */
3207+ int offset() const {
3208+ return _offsetInMarking;
3209+ }
3210+ const std::string& name()
3211+ {
3212+ return _name;
3213+ }
3214+ Member constraint(SimplificationContext& context) const override;
3215+ bool placeFree() const override { return false; }
3216+ void visit(Visitor& visitor) const override;
3217+ private:
3218+ /** Offset in marking, -1 if undefined, should be resolved during analysis */
3219+ int _offsetInMarking;
3220+ /** Identifier text */
3221+ std::string _name;
3222+ };
3223+
3224+ class ShallowCondition : public Condition
3225+ {
3226+ Result evaluate(const EvaluationContext& context) override
3227+ { return _compiled->evaluate(context); }
3228+ Result evalAndSet(const EvaluationContext& context) override
3229+ { return _compiled->evalAndSet(context); }
3230+ uint32_t distance(DistanceContext& context) const override
3231+ { return _compiled->distance(context); }
3232+ void toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const override
3233+ { _compiled->toTAPAALQuery(out, context); }
3234+ void toBinary(std::ostream& out) const override
3235+ { return _compiled->toBinary(out); }
3236+ Retval simplify(SimplificationContext& context) const override
3237+ { return _compiled->simplify(context); }
3238+ Condition_ptr prepareForReachability(bool negated) const override
3239+ { return _compiled->prepareForReachability(negated); }
3240+ bool isReachability(uint32_t depth) const override
3241+ { return _compiled->isReachability(depth); }
3242+
3243+ void toXML(std::ostream& out, uint32_t tabs) const override
3244+ { _compiled->toXML(out, tabs); }
3245+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override
3246+ { _compiled->findInteresting(generator, negated);}
3247+ Quantifier getQuantifier() const override
3248+ { return _compiled->getQuantifier(); }
3249+ Path getPath() const override { return _compiled->getPath(); }
3250+ CTLType getQueryType() const override { return _compiled->getQueryType(); }
3251+ bool containsNext() const override { return _compiled->containsNext(); }
3252+ bool nestedDeadlock() const override { return _compiled->nestedDeadlock(); }
3253+#ifdef VERIFYPN_TAR
3254+ virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
3255+ { return _compiled->encodeSat(net, context, uses, incremented); }
3256+#endif
3257+ int formulaSize() const override{
3258+ return _compiled->formulaSize();
3259+ }
3260+
3261+ virtual Condition_ptr pushNegation(negstat_t& neg, const EvaluationContext& context, bool nested, bool negated, bool initrw) override
3262+ {
3263+ if(_compiled)
3264+ return _compiled->pushNegation(neg, context, nested, negated, initrw);
3265+ else {
3266+ if(negated)
3267+ return std::static_pointer_cast<Condition>(std::make_shared<NotCondition>(clone()));
3268+ else
3269+ return clone();
3270+ }
3271+ }
3272+
3273+ void analyze(AnalysisContext& context) override
3274+ {
3275+ if (_compiled) _compiled->analyze(context);
3276+ else _analyze(context);
3277+ }
3278+ void toString(std::ostream &out) const {
3279+ if (_compiled) _compiled->toString(out);
3280+ else _toString(out);
3281+ }
3282+
3283+ protected:
3284+ virtual void _analyze(AnalysisContext& context) = 0;
3285+ virtual void _toString(std::ostream& out) const = 0;
3286+ virtual Condition_ptr clone() = 0;
3287+ Condition_ptr _compiled = nullptr;
3288+ };
3289+
3290+ /* Not condition */
3291+ class NotCondition : public Condition {
3292+ public:
3293+
3294+ NotCondition(const Condition_ptr cond) {
3295+ _cond = cond;
3296+ _temporal = _cond->isTemporal();
3297+ _loop_sensitive = _cond->isLoopSensitive();
3298+ }
3299+ int formulaSize() const override{
3300+ return _cond->formulaSize() + 1;
3301+ }
3302+ void analyze(AnalysisContext& context) override;
3303+ Result evaluate(const EvaluationContext& context) override;
3304+ Result evalAndSet(const EvaluationContext& context) override;
3305+ void visit(Visitor&) const override;
3306+ uint32_t distance(DistanceContext& context) const override;
3307+ void toString(std::ostream&) const override;
3308+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3309+ Retval simplify(SimplificationContext& context) const override;
3310+ bool isReachability(uint32_t depth) const override;
3311+ Condition_ptr prepareForReachability(bool negated) const override;
3312+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3313+ void toXML(std::ostream&, uint32_t tabs) const override;
3314+ void toBinary(std::ostream&) const override;
3315+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3316+ Quantifier getQuantifier() const override { return Quantifier::NEG; }
3317+ Path getPath() const override { return Path::pError; }
3318+ CTLType getQueryType() const override { return CTLType::LOPERATOR; }
3319+ const Condition_ptr& operator[](size_t i) const { return _cond; };
3320+ virtual bool isTemporal() const override { return _temporal;}
3321+ bool containsNext() const override { return _cond->containsNext(); }
3322+ bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
3323+ private:
3324+ Condition_ptr _cond;
3325+ bool _temporal = false;
3326+ };
3327+
3328+
3329+ /******************** TEMPORAL OPERATORS ********************/
3330+
3331+ class QuantifierCondition : public Condition
3332+ {
3333+ public:
3334+ virtual bool isTemporal() const override { return true;}
3335+ CTLType getQueryType() const override { return CTLType::PATHQEURY; }
3336+ virtual const Condition_ptr& operator[] (size_t i) const = 0;
3337+ };
3338+
3339+ class SimpleQuantifierCondition : public QuantifierCondition {
3340+ public:
3341+ SimpleQuantifierCondition(const Condition_ptr cond) {
3342+ _cond = cond;
3343+ _loop_sensitive = cond->isLoopSensitive();
3344+ }
3345+ int formulaSize() const override{
3346+ return _cond->formulaSize() + 1;
3347+ }
3348+
3349+ void analyze(AnalysisContext& context) override;
3350+ Result evaluate(const EvaluationContext& context) override;
3351+ Result evalAndSet(const EvaluationContext& context) override;
3352+ void toString(std::ostream&) const override;
3353+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3354+ void toBinary(std::ostream& out) const override;
3355+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3356+ virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
3357+ virtual bool containsNext() const override { return _cond->containsNext(); }
3358+ bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
3359+ private:
3360+ virtual std::string op() const = 0;
3361+
3362+ protected:
3363+ Condition_ptr _cond;
3364+ };
3365+
3366+ class EXCondition : public SimpleQuantifierCondition {
3367+ public:
3368+ using SimpleQuantifierCondition::SimpleQuantifierCondition;
3369+ Retval simplify(SimplificationContext& context) const override;
3370+ bool isReachability(uint32_t depth) const override;
3371+ Condition_ptr prepareForReachability(bool negated) const override;
3372+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3373+ void toXML(std::ostream&, uint32_t tabs) const override;
3374+ Quantifier getQuantifier() const override { return Quantifier::E; }
3375+ Path getPath() const override { return Path::X; }
3376+ uint32_t distance(DistanceContext& context) const override;
3377+ bool containsNext() const override { return true; }
3378+ virtual bool isLoopSensitive() const override { return true; }
3379+ void visit(Visitor&) const override;
3380+ private:
3381+ std::string op() const override;
3382+ };
3383+
3384+ class EGCondition : public SimpleQuantifierCondition {
3385+ public:
3386+ using SimpleQuantifierCondition::SimpleQuantifierCondition;
3387+
3388+ Retval simplify(SimplificationContext& context) const override;
3389+ bool isReachability(uint32_t depth) const override;
3390+ Condition_ptr prepareForReachability(bool negated) const override;
3391+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3392+ void toXML(std::ostream&, uint32_t tabs) const override;
3393+ Quantifier getQuantifier() const override { return Quantifier::E; }
3394+ Path getPath() const override { return Path::G; }
3395+ uint32_t distance(DistanceContext& context) const override;
3396+ Result evaluate(const EvaluationContext& context) override;
3397+ Result evalAndSet(const EvaluationContext& context) override;
3398+ virtual bool isLoopSensitive() const override { return true; }
3399+ void visit(Visitor&) const override;
3400+ private:
3401+ std::string op() const override;
3402+ };
3403+
3404+ class EFCondition : public SimpleQuantifierCondition {
3405+ public:
3406+ using SimpleQuantifierCondition::SimpleQuantifierCondition;
3407+
3408+ Retval simplify(SimplificationContext& context) const override;
3409+ bool isReachability(uint32_t depth) const override;
3410+ Condition_ptr prepareForReachability(bool negated) const override;
3411+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3412+ void toXML(std::ostream&, uint32_t tabs) const override;
3413+ Quantifier getQuantifier() const override { return Quantifier::E; }
3414+ Path getPath() const override { return Path::F; }
3415+ uint32_t distance(DistanceContext& context) const override;
3416+ Result evaluate(const EvaluationContext& context) override;
3417+ Result evalAndSet(const EvaluationContext& context) override;
3418+ void visit(Visitor&) const override;
3419+ private:
3420+ std::string op() const override;
3421+ };
3422+
3423+ class AXCondition : public SimpleQuantifierCondition {
3424+ public:
3425+ using SimpleQuantifierCondition::SimpleQuantifierCondition;
3426+ Retval simplify(SimplificationContext& context) const override;
3427+ bool isReachability(uint32_t depth) const override;
3428+ Condition_ptr prepareForReachability(bool negated) const override;
3429+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3430+ void toXML(std::ostream&, uint32_t tabs) const override;
3431+ Quantifier getQuantifier() const override { return Quantifier::A; }
3432+ Path getPath() const override { return Path::X; }
3433+ uint32_t distance(DistanceContext& context) const override;
3434+ bool containsNext() const override { return true; }
3435+ virtual bool isLoopSensitive() const override { return true; }
3436+ void visit(Visitor&) const override;
3437+ private:
3438+ std::string op() const override;
3439+ };
3440+
3441+ class AGCondition : public SimpleQuantifierCondition {
3442+ public:
3443+ using SimpleQuantifierCondition::SimpleQuantifierCondition;
3444+ Retval simplify(SimplificationContext& context) const override;
3445+ bool isReachability(uint32_t depth) const override;
3446+ Condition_ptr prepareForReachability(bool negated) const override;
3447+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3448+ void toXML(std::ostream&, uint32_t tabs) const override;
3449+ Quantifier getQuantifier() const override { return Quantifier::A; }
3450+ Path getPath() const override { return Path::G; }
3451+ uint32_t distance(DistanceContext& context) const override;
3452+ Result evaluate(const EvaluationContext& context) override;
3453+ Result evalAndSet(const EvaluationContext& context) override;
3454+ void visit(Visitor&) const override;
3455+ private:
3456+ std::string op() const override;
3457+ };
3458+
3459+ class AFCondition : public SimpleQuantifierCondition {
3460+ public:
3461+ using SimpleQuantifierCondition::SimpleQuantifierCondition;
3462+ Retval simplify(SimplificationContext& context) const override;
3463+ bool isReachability(uint32_t depth) const override;
3464+ Condition_ptr prepareForReachability(bool negated) const override;
3465+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3466+ void toXML(std::ostream&, uint32_t tabs) const override;
3467+ Quantifier getQuantifier() const override { return Quantifier::A; }
3468+ Path getPath() const override { return Path::F; }
3469+ uint32_t distance(DistanceContext& context) const override;
3470+ Result evaluate(const EvaluationContext& context) override;
3471+ Result evalAndSet(const EvaluationContext& context) override;
3472+ void visit(Visitor&) const override;
3473+ virtual bool isLoopSensitive() const override { return true; }
3474+ private:
3475+ std::string op() const override;
3476+ };
3477+
3478+ class UntilCondition : public QuantifierCondition {
3479+ public:
3480+ UntilCondition(const Condition_ptr cond1, const Condition_ptr cond2) {
3481+ _cond1 = cond1;
3482+ _cond2 = cond2;
3483+ _loop_sensitive = _cond1->isLoopSensitive() || _cond2->isLoopSensitive();
3484+ }
3485+ int formulaSize() const override{
3486+ return _cond1->formulaSize() + _cond2->formulaSize() + 1;
3487+ }
3488+
3489+ void analyze(AnalysisContext& context) override;
3490+ Result evaluate(const EvaluationContext& context) override;
3491+ void toString(std::ostream&) const override;
3492+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3493+ void toBinary(std::ostream& out) const override;
3494+ bool isReachability(uint32_t depth) const override;
3495+ Condition_ptr prepareForReachability(bool negated) const override;
3496+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3497+ Result evalAndSet(const EvaluationContext& context) override;
3498+
3499+ virtual const Condition_ptr& operator[] (size_t i) const override
3500+ { if(i == 0) return _cond1; return _cond2;}
3501+ Path getPath() const override
3502+ { return Path::U; }
3503+ bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
3504+ bool nestedDeadlock() const override { return _cond1->nestedDeadlock() || _cond2->nestedDeadlock(); }
3505+ private:
3506+ virtual std::string op() const = 0;
3507+
3508+ protected:
3509+ Condition_ptr _cond1;
3510+ Condition_ptr _cond2;
3511+ };
3512+
3513+ class EUCondition : public UntilCondition {
3514+ public:
3515+ using UntilCondition::UntilCondition;
3516+ Retval simplify(SimplificationContext& context) const override;
3517+ Quantifier getQuantifier() const override { return Quantifier::E; }
3518+ void visit(Visitor&) const override;
3519+ uint32_t distance(DistanceContext& context) const override;
3520+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3521+ void toXML(std::ostream&, uint32_t tabs) const override;
3522+
3523+ private:
3524+ std::string op() const override;
3525+ };
3526+
3527+ class AUCondition : public UntilCondition {
3528+ public:
3529+ using UntilCondition::UntilCondition;
3530+ Retval simplify(SimplificationContext& context) const override;
3531+ Quantifier getQuantifier() const override { return Quantifier::A; }
3532+ void visit(Visitor&) const override;
3533+ uint32_t distance(DistanceContext& context) const override;
3534+ void toXML(std::ostream&, uint32_t tabs) const override;
3535+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3536+ virtual bool isLoopSensitive() const override { return true; }
3537+ private:
3538+ std::string op() const override;
3539+ };
3540+
3541+ /******************** CONDITIONS ********************/
3542+
3543+ class UnfoldedFireableCondition : public ShallowCondition {
3544+ public:
3545+ UnfoldedFireableCondition(const std::string& tname) : ShallowCondition(), _name(tname) {};
3546+ Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3547+ void visit(Visitor&) const override;
3548+ protected:
3549+ void _analyze(AnalysisContext& context) override;
3550+ virtual void _toString(std::ostream& out) const;
3551+ Condition_ptr clone() { return std::make_shared<UnfoldedFireableCondition>(_name); }
3552+ private:
3553+ const std::string _name;
3554+ };
3555+
3556+ class FireableCondition : public ShallowCondition {
3557+ public:
3558+ FireableCondition(const std::string& tname) : _name(tname) {};
3559+ Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3560+ void visit(Visitor&) const override;
3561+ protected:
3562+ void _analyze(AnalysisContext& context) override;
3563+ virtual void _toString(std::ostream& out) const;
3564+ Condition_ptr clone() { return std::make_shared<FireableCondition>(_name); }
3565+ private:
3566+ const std::string _name;
3567+ };
3568+
3569+ /* Logical conditon */
3570+ class LogicalCondition : public Condition {
3571+ public:
3572+ int formulaSize() const override {
3573+ size_t i = 1;
3574+ for(auto& c : _conds) i += c->formulaSize();
3575+ return i;
3576+ }
3577+ void analyze(AnalysisContext& context) override;
3578+
3579+ uint32_t distance(DistanceContext& context) const override;
3580+ void toString(std::ostream&) const override;
3581+ void toBinary(std::ostream& out) const override;
3582+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3583+ bool isReachability(uint32_t depth) const override;
3584+ Condition_ptr prepareForReachability(bool negated) const override;
3585+ const Condition_ptr& operator[](size_t i) const
3586+ {
3587+ return _conds[i];
3588+ };
3589+ CTLType getQueryType() const override { return CTLType::LOPERATOR; }
3590+ Path getPath() const override { return Path::pError; }
3591+
3592+ bool isTemporal() const override
3593+ {
3594+ return _temporal;
3595+ }
3596+ auto begin() { return _conds.begin(); }
3597+ auto end() { return _conds.end(); }
3598+ auto begin() const { return _conds.begin(); }
3599+ auto end() const { return _conds.end(); }
3600+ bool empty() const { return _conds.size() == 0; }
3601+ bool singular() const { return _conds.size() == 1; }
3602+ size_t size() const { return _conds.size(); }
3603+ bool containsNext() const override
3604+ { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
3605+ bool nestedDeadlock() const override;
3606+
3607+ protected:
3608+ LogicalCondition() {};
3609+ Retval simplifyOr(SimplificationContext& context) const;
3610+ Retval simplifyAnd(SimplificationContext& context) const;
3611+
3612+ private:
3613+ virtual uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const = 0;
3614+ virtual std::string op() const = 0;
3615+
3616+ protected:
3617+ bool _temporal = false;
3618+ std::vector<Condition_ptr> _conds;
3619+ };
3620+
3621+ /* Conjunctive and condition */
3622+ class AndCondition : public LogicalCondition {
3623+ public:
3624+
3625+ AndCondition(std::vector<Condition_ptr>&& conds);
3626+
3627+ AndCondition(const std::vector<Condition_ptr>& conds);
3628+
3629+ AndCondition(Condition_ptr left, Condition_ptr right);
3630+
3631+ Retval simplify(SimplificationContext& context) const override;
3632+ Result evaluate(const EvaluationContext& context) override;
3633+ Result evalAndSet(const EvaluationContext& context) override;
3634+ void visit(Visitor&) const override;
3635+ void toXML(std::ostream&, uint32_t tabs) const override;
3636+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3637+ Quantifier getQuantifier() const override { return Quantifier::AND; }
3638+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3639+ private:
3640+ //int logicalOp() const;
3641+ uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
3642+ std::string op() const override;
3643+ };
3644+
3645+ /* Disjunctive or conditon */
3646+ class OrCondition : public LogicalCondition {
3647+ public:
3648+
3649+ OrCondition(std::vector<Condition_ptr>&& conds);
3650+
3651+ OrCondition(const std::vector<Condition_ptr>& conds);
3652+
3653+ OrCondition(Condition_ptr left, Condition_ptr right);
3654+
3655+ Retval simplify(SimplificationContext& context) const override;
3656+ Result evaluate(const EvaluationContext& context) override;
3657+ Result evalAndSet(const EvaluationContext& context) override;
3658+ void visit(Visitor&) const override;
3659+ void toXML(std::ostream&, uint32_t tabs) const override;
3660+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3661+ Quantifier getQuantifier() const override { return Quantifier::OR; }
3662+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3663+ private:
3664+ //int logicalOp() const;
3665+ uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
3666+ std::string op() const override;
3667+ };
3668+
3669+ class CompareConjunction : public Condition
3670+ {
3671+ public:
3672+ struct cons_t {
3673+ int32_t _place = -1;
3674+ uint32_t _upper = std::numeric_limits<uint32_t>::max();
3675+ uint32_t _lower = 0;
3676+ std::string _name;
3677+ bool operator<(const cons_t& other) const
3678+ {
3679+ return _place < other._place;
3680+ }
3681+
3682+ void invert()
3683+ {
3684+ if(_lower == 0 && _upper == std::numeric_limits<uint32_t>::max())
3685+ return;
3686+ assert(_lower == 0 || _upper == std::numeric_limits<uint32_t>::max());
3687+ if(_lower == 0)
3688+ {
3689+ _lower = _upper + 1;
3690+ _upper = std::numeric_limits<uint32_t>::max();
3691+ }
3692+ else if(_upper == std::numeric_limits<uint32_t>::max())
3693+ {
3694+ _upper = _lower - 1;
3695+ _lower = 0;
3696+ }
3697+ else
3698+ {
3699+ assert(false);
3700+ }
3701+ }
3702+
3703+ void intersect(const cons_t& other)
3704+ {
3705+ _lower = std::max(_lower, other._lower);
3706+ _upper = std::min(_upper, other._upper);
3707+ }
3708+ };
3709+
3710+ CompareConjunction(bool negated = false)
3711+ : _negated(false) {};
3712+ friend FireableCondition;
3713+ CompareConjunction(const std::vector<cons_t>&& cons, bool negated)
3714+ : _constraints(cons), _negated(negated) {};
3715+ CompareConjunction(const std::vector<Condition_ptr>&, bool negated);
3716+ CompareConjunction(const CompareConjunction& other, bool negated = false)
3717+ : _constraints(other._constraints), _negated(other._negated != negated)
3718+ {
3719+ };
3720+
3721+ void merge(const CompareConjunction& other);
3722+ void merge(const std::vector<Condition_ptr>&, bool negated);
3723+
3724+ int formulaSize() const override{
3725+ int sum = 0;
3726+ for(auto& c : _constraints)
3727+ {
3728+ assert(c._place >= 0);
3729+ if(c._lower == c._upper) ++sum;
3730+ else {
3731+ if(c._lower != 0) ++sum;
3732+ if(c._upper != std::numeric_limits<uint32_t>::max()) ++sum;
3733+ }
3734+ }
3735+ if(sum == 1) return 2;
3736+ else return (sum*2) + 1;
3737+ }
3738+ void analyze(AnalysisContext& context) override;
3739+ uint32_t distance(DistanceContext& context) const override;
3740+ void toString(std::ostream& stream) const override;
3741+ void toTAPAALQuery(std::ostream& stream,TAPAALConditionExportContext& context) const override;
3742+ void toBinary(std::ostream& out) const override;
3743+ bool isReachability(uint32_t depth) const override { return depth > 0; };
3744+ Condition_ptr prepareForReachability(bool negated) const override;
3745+ CTLType getQueryType() const override { return CTLType::LOPERATOR; }
3746+ Path getPath() const override { return Path::pError; }
3747+ virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
3748+ Retval simplify(SimplificationContext& context) const override;
3749+ Result evaluate(const EvaluationContext& context) override;
3750+ Result evalAndSet(const EvaluationContext& context) override;
3751+ void visit(Visitor&) const override;
3752+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3753+ Quantifier getQuantifier() const override { return _negated ? Quantifier::OR : Quantifier::AND; }
3754+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3755+ bool isNegated() const { return _negated; }
3756+ bool singular() const
3757+ {
3758+ return _constraints.size() == 1 &&
3759+ (_constraints[0]._lower == 0 ||
3760+ _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
3761+ };
3762+ bool containsNext() const override { return false;}
3763+ bool nestedDeadlock() const override { return false; }
3764+ const std::vector<cons_t>& constraints() const { return _constraints; }
3765+ std::vector<cons_t>::const_iterator begin() const { return _constraints.begin(); }
3766+ std::vector<cons_t>::const_iterator end() const { return _constraints.end(); }
3767+ private:
3768+ std::vector<cons_t> _constraints;
3769+ bool _negated = false;
3770+ };
3771+
3772+
3773+ /* Comparison conditon */
3774+ class CompareCondition : public Condition {
3775+ public:
3776+
3777+ CompareCondition(const Expr_ptr expr1, const Expr_ptr expr2)
3778+ : _expr1(expr1), _expr2(expr2) {}
3779+
3780+ int formulaSize() const override{
3781+ return _expr1->formulaSize() + _expr2->formulaSize() + 1;
3782+ }
3783+ void analyze(AnalysisContext& context) override;
3784+ Result evaluate(const EvaluationContext& context) override;
3785+ Result evalAndSet(const EvaluationContext& context) override;
3786+ void toString(std::ostream&) const override;
3787+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3788+ void toBinary(std::ostream& out) const override;
3789+ bool isReachability(uint32_t depth) const override;
3790+ Condition_ptr prepareForReachability(bool negated) const override;
3791+ Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
3792+ Path getPath() const override { return Path::pError; }
3793+ CTLType getQueryType() const override { return CTLType::EVAL; }
3794+ const Expr_ptr& operator[](uint32_t id) const
3795+ {
3796+ if(id == 0) return _expr1;
3797+ else return _expr2;
3798+ }
3799+ bool containsNext() const override { return false; }
3800+ bool nestedDeadlock() const override { return false; }
3801+ bool isTrivial() const;
3802+ protected:
3803+ uint32_t _distance(DistanceContext& c,
3804+ std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
3805+ {
3806+ return d(_expr1->evaluate(c), _expr2->evaluate(c), c.negated());
3807+ }
3808+ private:
3809+ virtual bool apply(int v1, int v2) const = 0;
3810+ virtual std::string op() const = 0;
3811+ /** Operator when exported to TAPAAL */
3812+ virtual std::string opTAPAAL() const = 0;
3813+ /** Swapped operator when exported to TAPAAL, e.g. operator when operands are swapped */
3814+ virtual std::string sopTAPAAL() const = 0;
3815+
3816+ protected:
3817+ Expr_ptr _expr1;
3818+ Expr_ptr _expr2;
3819+ };
3820+
3821+ /* delta */
3822+ template<typename T>
3823+ uint32_t delta(int v1, int v2, bool negated)
3824+ { return 0; }
3825+
3826+ class EqualCondition : public CompareCondition {
3827+ public:
3828+
3829+ using CompareCondition::CompareCondition;
3830+ Retval simplify(SimplificationContext& context) const override;
3831+ void toXML(std::ostream&, uint32_t tabs) const override;
3832+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3833+ uint32_t distance(DistanceContext& context) const override;
3834+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3835+ void visit(Visitor&) const override;
3836+ private:
3837+ bool apply(int v1, int v2) const override;
3838+ std::string op() const override;
3839+ std::string opTAPAAL() const override;
3840+ std::string sopTAPAAL() const override;
3841+ };
3842+
3843+ /* None equality conditon */
3844+ class NotEqualCondition : public CompareCondition {
3845+ public:
3846+
3847+ using CompareCondition::CompareCondition;
3848+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3849+ Retval simplify(SimplificationContext& context) const override;
3850+ void toXML(std::ostream&, uint32_t tabs) const override;
3851+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3852+ uint32_t distance(DistanceContext& context) const override;
3853+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3854+ void visit(Visitor&) const override;
3855+ private:
3856+ bool apply(int v1, int v2) const override;
3857+ std::string op() const override;
3858+ std::string opTAPAAL() const override;
3859+ std::string sopTAPAAL() const override;
3860+ };
3861+
3862+ /* Less-than conditon */
3863+ class LessThanCondition : public CompareCondition {
3864+ public:
3865+
3866+ using CompareCondition::CompareCondition;
3867+ Retval simplify(SimplificationContext& context) const override;
3868+ void toXML(std::ostream&, uint32_t tabs) const override;
3869+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3870+ uint32_t distance(DistanceContext& context) const override;
3871+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3872+ void visit(Visitor&) const override;
3873+ private:
3874+ bool apply(int v1, int v2) const override;
3875+ std::string op() const override;
3876+ std::string opTAPAAL() const override;
3877+ std::string sopTAPAAL() const override;
3878+ };
3879+
3880+ /* Less-than-or-equal conditon */
3881+ class LessThanOrEqualCondition : public CompareCondition {
3882+ public:
3883+
3884+ using CompareCondition::CompareCondition;
3885+ Retval simplify(SimplificationContext& context) const override;
3886+ void toXML(std::ostream&, uint32_t tabs) const override;
3887+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3888+ uint32_t distance(DistanceContext& context) const override;
3889+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3890+ void visit(Visitor&) const override;
3891+ private:
3892+ bool apply(int v1, int v2) const override;
3893+ std::string op() const override;
3894+ std::string opTAPAAL() const override;
3895+ std::string sopTAPAAL() const override;
3896+ };
3897+
3898+ /* Greater-than conditon */
3899+ class GreaterThanCondition : public CompareCondition {
3900+ public:
3901+
3902+ using CompareCondition::CompareCondition;
3903+ Retval simplify(SimplificationContext& context) const override;
3904+ void toXML(std::ostream&, uint32_t tabs) const override;
3905+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3906+ uint32_t distance(DistanceContext& context) const override;
3907+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3908+ void visit(Visitor&) const override;
3909+ private:
3910+ bool apply(int v1, int v2) const override;
3911+ std::string op() const override;
3912+ std::string opTAPAAL() const override;
3913+ std::string sopTAPAAL() const override;
3914+ };
3915+
3916+ /* Greater-than-or-equal conditon */
3917+ class GreaterThanOrEqualCondition : public CompareCondition {
3918+ public:
3919+ using CompareCondition::CompareCondition;
3920+ Retval simplify(SimplificationContext& context) const override;
3921+ void toXML(std::ostream&, uint32_t tabs) const override;
3922+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3923+ uint32_t distance(DistanceContext& context) const override;
3924+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3925+ void visit(Visitor&) const override;
3926+ private:
3927+ bool apply(int v1, int v2) const override;
3928+ std::string op() const override;
3929+ std::string opTAPAAL() const override;
3930+ std::string sopTAPAAL() const override;
3931+ };
3932+
3933+ /* Bool condition */
3934+ class BooleanCondition : public Condition {
3935+ public:
3936+
3937+ BooleanCondition(bool value) : _value(value) {
3938+ if (value) {
3939+ trivial = 1;
3940+ } else {
3941+ trivial = 2;
3942+ }
3943+ }
3944+ int formulaSize() const override{
3945+ return 0;
3946+ }
3947+ void analyze(AnalysisContext& context) override;
3948+ Result evaluate(const EvaluationContext& context) override;
3949+ Result evalAndSet(const EvaluationContext& context) override;
3950+ void visit(Visitor&) const override;
3951+ uint32_t distance(DistanceContext& context) const override;
3952+ static Condition_ptr TRUE_CONSTANT;
3953+ static Condition_ptr FALSE_CONSTANT;
3954+ void toString(std::ostream&) const override;
3955+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3956+ static Condition_ptr getShared(bool val);
3957+ Retval simplify(SimplificationContext& context) const override;
3958+ bool isReachability(uint32_t depth) const override;
3959+ Condition_ptr prepareForReachability(bool negated) const override;
3960+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3961+ void toXML(std::ostream&, uint32_t tabs) const override;
3962+ void toBinary(std::ostream&) const override;
3963+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3964+ Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
3965+ Path getPath() const override { return Path::pError; }
3966+ CTLType getQueryType() const override { return CTLType::EVAL; }
3967+ bool containsNext() const override { return false; }
3968+ bool nestedDeadlock() const override { return false; }
3969+ private:
3970+ const bool _value;
3971+ };
3972+
3973+ /* Deadlock condition */
3974+ class DeadlockCondition : public Condition {
3975+ public:
3976+
3977+ DeadlockCondition() {
3978+ _loop_sensitive = true;
3979+ }
3980+ int formulaSize() const override{
3981+ return 1;
3982+ }
3983+ void analyze(AnalysisContext& context) override;
3984+ Result evaluate(const EvaluationContext& context) override;
3985+ Result evalAndSet(const EvaluationContext& context) override;
3986+ void visit(Visitor&) const override;
3987+ uint32_t distance(DistanceContext& context) const override;
3988+ void toString(std::ostream&) const override;
3989+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
3990+ Retval simplify(SimplificationContext& context) const override;
3991+ bool isReachability(uint32_t depth) const override;
3992+ Condition_ptr prepareForReachability(bool negated) const override;
3993+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
3994+ void toXML(std::ostream&, uint32_t tabs) const override;
3995+ void toBinary(std::ostream&) const override;
3996+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
3997+ static Condition_ptr DEADLOCK;
3998+ Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
3999+ Path getPath() const override { return Path::pError; }
4000+ CTLType getQueryType() const override { return CTLType::EVAL; }
4001+ bool containsNext() const override { return false; }
4002+ bool nestedDeadlock() const override { return false; }
4003+ };
4004+
4005+ class KSafeCondition : public ShallowCondition
4006+ {
4007+ public:
4008+ KSafeCondition(const Expr_ptr& expr1) : _bound(expr1)
4009+ {}
4010+
4011+ protected:
4012+ void _analyze(AnalysisContext& context) override;
4013+ void _toString(std::ostream& out) const override;
4014+ void visit(Visitor&) const override;
4015+ Condition_ptr clone() override
4016+ {
4017+ return std::make_shared<KSafeCondition>(_bound);
4018+ }
4019+ private:
4020+ Expr_ptr _bound = nullptr;
4021+ };
4022+
4023+ class LivenessCondition : public ShallowCondition
4024+ {
4025+ public:
4026+ LivenessCondition() {}
4027+ protected:
4028+ void _analyze(AnalysisContext& context) override;
4029+ void _toString(std::ostream& out) const override;
4030+ void visit(Visitor&) const override;
4031+ Condition_ptr clone() override { return std::make_shared<LivenessCondition>(); }
4032+ };
4033+
4034+ class QuasiLivenessCondition : public ShallowCondition
4035+ {
4036+ public:
4037+ QuasiLivenessCondition() {}
4038+ protected:
4039+ void _analyze(AnalysisContext& context) override;
4040+ void _toString(std::ostream& out) const override;
4041+ void visit(Visitor&) const override;
4042+ Condition_ptr clone() override { return std::make_shared<QuasiLivenessCondition>(); }
4043+ };
4044+
4045+ class StableMarkingCondition : public ShallowCondition
4046+ {
4047+ public:
4048+ StableMarkingCondition() {}
4049+ protected:
4050+ void _analyze(AnalysisContext& context) override;
4051+ void _toString(std::ostream& out) const override;
4052+ void visit(Visitor&) const override;
4053+ Condition_ptr clone() override { return std::make_shared<StableMarkingCondition>(); }
4054+ };
4055+
4056+ class UpperBoundsCondition : public ShallowCondition
4057+ {
4058+ public:
4059+
4060+ UpperBoundsCondition(const std::vector<std::string>& places) : _places(places)
4061+ {}
4062+ protected:
4063+ void _toString(std::ostream& out) const override;
4064+ void _analyze(AnalysisContext& context) override;
4065+ void visit(Visitor&) const override;
4066+ Condition_ptr clone() override
4067+ {
4068+ return std::make_shared<UpperBoundsCondition>(_places);
4069+ }
4070+
4071+ private:
4072+ std::vector<std::string> _places;
4073+ };
4074+
4075+ class UnfoldedUpperBoundsCondition : public Condition
4076+ {
4077+ public:
4078+ struct place_t {
4079+ std::string _name;
4080+ uint32_t _place = 0;
4081+ double _max = std::numeric_limits<double>::infinity();
4082+ bool _maxed_out = false;
4083+ place_t(const std::string& name)
4084+ {
4085+ _name = name;
4086+ }
4087+ place_t(const place_t& other, double max)
4088+ {
4089+ _name = other._name;
4090+ _place = other._place;
4091+ _max = max;
4092+ }
4093+ bool operator<(const place_t& other) const{
4094+ return _place < other._place;
4095+ }
4096+ };
4097+
4098+ UnfoldedUpperBoundsCondition(const std::vector<std::string>& places)
4099+ {
4100+ for(auto& s : places) _places.push_back(s);
4101+ }
4102+ UnfoldedUpperBoundsCondition(const std::vector<place_t>& places, double max, double offset)
4103+ : _places(places), _max(max), _offset(offset) {
4104+ };
4105+ int formulaSize() const override{
4106+ return _places.size();
4107+ }
4108+ void analyze(AnalysisContext& context) override;
4109+ size_t value(const MarkVal*);
4110+ Result evaluate(const EvaluationContext& context) override;
4111+ Result evalAndSet(const EvaluationContext& context) override;
4112+ void visit(Visitor&) const override;
4113+ uint32_t distance(DistanceContext& context) const override;
4114+ void toString(std::ostream&) const override;
4115+ void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
4116+ void toBinary(std::ostream&) const override;
4117+ Retval simplify(SimplificationContext& context) const override;
4118+ bool isReachability(uint32_t depth) const override;
4119+ Condition_ptr prepareForReachability(bool negated) const override;
4120+ Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
4121+ void toXML(std::ostream&, uint32_t tabs) const override;
4122+ void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
4123+ Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
4124+ Path getPath() const override { return Path::pError; }
4125+ CTLType getQueryType() const override { return CTLType::EVAL; }
4126+ bool containsNext() const override { return false; }
4127+ bool nestedDeadlock() const override { return false; }
4128+
4129+ double bounds(bool add_offset = true) const {
4130+ return (add_offset ? _offset : 0 ) + _bound;
4131+ }
4132+
4133+ virtual void setUpperBound(size_t bound)
4134+ {
4135+ _bound = std::max(_bound, bound);
4136+ }
4137+
4138+ const std::vector<place_t>& places() const { return _places; }
4139+
4140+ private:
4141+ std::vector<place_t> _places;
4142+ size_t _bound = 0;
4143+ double _max = std::numeric_limits<double>::infinity();
4144+ double _offset = 0;
4145+ };
4146+
4147+ }
4148+}
4149+
4150+
4151+
4152+#endif // EXPRESSIONS_H
4153
4154=== added file 'include/PetriEngine/PQL/PQL.h'
4155--- include/PetriEngine/PQL/PQL.h 1970-01-01 00:00:00 +0000
4156+++ include/PetriEngine/PQL/PQL.h 2020-09-11 14:21:20 +0000
4157@@ -0,0 +1,285 @@
4158+/* PeTe - Petri Engine exTremE
4159+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
4160+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
4161+ * Lars Kærlund Østergaard <larsko@gmail.com>,
4162+ *
4163+ * This program is free software: you can redistribute it and/or modify
4164+ * it under the terms of the GNU General Public License as published by
4165+ * the Free Software Foundation, either version 3 of the License, or
4166+ * (at your option) any later version.
4167+ *
4168+ * This program is distributed in the hope that it will be useful,
4169+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
4170+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
4171+ * GNU General Public License for more details.
4172+ *
4173+ * You should have received a copy of the GNU General Public License
4174+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
4175+ */
4176+#ifndef PQL_H
4177+#define PQL_H
4178+#include <string>
4179+#include <list>
4180+#include <vector>
4181+#include <algorithm>
4182+#include <unordered_map>
4183+#include <memory>
4184+
4185+#include "../PetriNet.h"
4186+#include "../Structures/State.h"
4187+#include "../ReducingSuccessorGenerator.h"
4188+#include "../Simplification/LPCache.h"
4189+
4190+namespace PetriEngine {
4191+ class ReducingSuccessorGenerator;
4192+ namespace Simplification
4193+ {
4194+ class Member;
4195+ struct Retval;
4196+ }
4197+ namespace PQL {
4198+ class Visitor;
4199+
4200+ enum CTLType {PATHQEURY = 1, LOPERATOR = 2, EVAL = 3, TYPE_ERROR = -1};
4201+ enum Quantifier { AND = 1, OR = 2, A = 3, E = 4, NEG = 5, COMPCONJ = 6, DEADLOCK = 7, UPPERBOUNDS = 8, PN_BOOLEAN = 9, EMPTY = -1 };
4202+ enum Path { G = 1, X = 2, F = 3, U = 4, pError = -1 };
4203+
4204+
4205+ class AnalysisContext;
4206+ class EvaluationContext;
4207+ class DistanceContext;
4208+ class TAPAALConditionExportContext;
4209+ class SimplificationContext;
4210+
4211+ /** Representation of a PQL error */
4212+ class ExprError {
4213+ std::string _text;
4214+ int _length;
4215+ public:
4216+
4217+ ExprError(std::string text = "", int length = 0) {
4218+ _text = text;
4219+ _length = length;
4220+ }
4221+
4222+ /** Human readable explaination of the error */
4223+ const std::string& text() const {
4224+ return _text;
4225+ }
4226+
4227+ /** length in the source, 0 if not applicable */
4228+ int length() const {
4229+ return _length;
4230+ }
4231+
4232+ /** Convert error to string */
4233+ std::string toString() const {
4234+ return "Parsing error \"" + text() + "\"";
4235+ }
4236+
4237+ /** True, if this is a default created ExprError without any information */
4238+ bool isEmpty() const {
4239+ return _text.empty() && _length == 0;
4240+ }
4241+ };
4242+
4243+ /** Representation of an expression */
4244+ class Expr {
4245+ int _eval = 0;
4246+ public:
4247+ /** Types of expressions */
4248+ enum Types {
4249+ /** Binary addition expression */
4250+ PlusExpr,
4251+ /** Binary subtraction expression */
4252+ SubtractExpr,
4253+ /** Binary multiplication expression */
4254+ MultiplyExpr,
4255+ /** Unary minus expression */
4256+ MinusExpr,
4257+ /** Literal integer expression */
4258+ LiteralExpr,
4259+ /** Identifier expression */
4260+ IdentifierExpr
4261+ };
4262+ public:
4263+ /** Virtual destructor, an expression should know it subexpressions */
4264+ virtual ~Expr();
4265+ /** Perform context analysis */
4266+ virtual void analyze(AnalysisContext& context) = 0;
4267+ /** Evaluate the expression given marking and assignment */
4268+ virtual int evaluate(const EvaluationContext& context) = 0;
4269+ int evalAndSet(const EvaluationContext& context);
4270+ virtual void visit(Visitor& visitor) const = 0;
4271+ /** Convert expression to string */
4272+ virtual void toString(std::ostream&) const = 0;
4273+ /** Expression type */
4274+ virtual Types type() const = 0;
4275+ /** Construct left/right side of equations used in query simplification */
4276+ virtual Simplification::Member constraint(SimplificationContext& context) const = 0;
4277+ /** Output the expression as it currently is to a file in XML */
4278+ virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
4279+ virtual void toBinary(std::ostream&) const = 0;
4280+ /** Stubborn reduction: increasing and decreasing sets */
4281+ virtual void incr(ReducingSuccessorGenerator& generator) const = 0;
4282+ virtual void decr(ReducingSuccessorGenerator& generator) const = 0;
4283+ /** Count size of the entire formula in number of nodes */
4284+ virtual int formulaSize() const = 0;
4285+
4286+ virtual bool placeFree() const = 0;
4287+
4288+ void setEval(int eval) {
4289+ _eval = eval;
4290+ }
4291+
4292+ int getEval() const {
4293+ return _eval;
4294+ }
4295+ };
4296+/******************* NEGATION PUSH STATS *******************/
4297+
4298+ struct negstat_t
4299+ {
4300+ negstat_t()
4301+ {
4302+ for(size_t i = 0; i < 31; ++i) _used[i] = 0;
4303+ }
4304+ void print(std::ostream& stream)
4305+ {
4306+ for(size_t i = 0; i < 31; ++i) stream << _used[i] << ",";
4307+ }
4308+ void printRules(std::ostream& stream)
4309+ {
4310+ for(size_t i = 0; i < 31; ++i) stream << _rulename[i] << ",";
4311+ }
4312+ int _used[31];
4313+ const std::vector<const char*> _rulename = {
4314+ "EG p-> !EF !p",
4315+ "AG p-> !AF !p",
4316+ "!EX p -> AX p",
4317+ "EX false -> false",
4318+ "EX true -> !deadlock",
4319+ "!AX p -> EX p",
4320+ "AX false -> deadlock",
4321+ "AX true -> true",
4322+ "EF !deadlock -> !deadlock",
4323+ "EF EF p -> EF p",
4324+ "EF AF p -> AF p",
4325+ "EF E p U q -> EF q",
4326+ "EF A p U q -> EF q",
4327+ "EF .. or .. -> EF .. or EF ..",
4328+ "AF !deadlock -> !deadlock",
4329+ "AF AF p -> AF p",
4330+ "AF EF p -> EF p",
4331+ "AF .. or EF p -> EF p or AF ..",
4332+ "AF A p U q -> AF q",
4333+ "A p U !deadlock -> !deadlock",
4334+ "A deadlock U q -> q",
4335+ "A !deadlock U q -> AF q",
4336+ "A p U AF q -> AF q",
4337+ "A p U EF q -> EF q",
4338+ "A p U .. or EF q -> EF q or A p U ..",
4339+ "E p U !deadlock -> !deadlock",
4340+ "E deadlock U q -> q",
4341+ "E !deadlock U q -> EF q",
4342+ "E p U EF q -> EF q",
4343+ "E p U .. or EF q -> EF q or E p U ..",
4344+ "!! p -> p"
4345+
4346+ };
4347+ int& operator[](size_t i) { return _used[i]; }
4348+ bool negated_fireability = false;
4349+ };
4350+
4351+ /** Base condition */
4352+ class Condition {
4353+ public:
4354+ enum Result {RUNKNOWN=-1,RFALSE=0,RTRUE=1};
4355+ private:
4356+ bool _inv = false;
4357+ Result _eval = RUNKNOWN;
4358+ protected:
4359+ bool _loop_sensitive = false;
4360+ public:
4361+ /** Virtual destructor */
4362+ virtual ~Condition();
4363+ /** Perform context analysis */
4364+ virtual void analyze(AnalysisContext& context) = 0;
4365+ /** Evaluate condition */
4366+ virtual Result evaluate(const EvaluationContext& context) = 0;
4367+ virtual Result evalAndSet(const EvaluationContext& context) = 0;
4368+ virtual void visit(Visitor& visitor) const = 0;
4369+
4370+ /** Convert condition to string */
4371+ virtual void toString(std::ostream&) const = 0;
4372+ /** Export condition to TAPAAL query (add EF manually!) */
4373+ virtual void toTAPAALQuery(std::ostream&, TAPAALConditionExportContext& context) const = 0;
4374+ /** Get distance to query */
4375+ virtual uint32_t distance(DistanceContext& context) const = 0;
4376+ /** Query Simplification */
4377+ virtual Simplification::Retval simplify(SimplificationContext& context) const = 0;
4378+ /** Check if query is a reachability query */
4379+ virtual bool isReachability(uint32_t depth = 0) const = 0;
4380+
4381+ virtual bool isLoopSensitive() const { return _loop_sensitive; };
4382+ /** Prepare reachability queries */
4383+ virtual std::shared_ptr<Condition> prepareForReachability(bool negated = false) const = 0;
4384+ virtual std::shared_ptr<Condition> pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated = false, bool initrw = true) = 0;
4385+
4386+ /** Output the condition as it currently is to a file in XML */
4387+ virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
4388+ virtual void toBinary(std::ostream& out) const = 0;
4389+
4390+ /** Find interesting transitions in stubborn reduction*/
4391+ virtual void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const = 0;
4392+ /** Checks if the condition is trivially true */
4393+ bool isTriviallyTrue();
4394+ /*** Checks if the condition is trivially false */
4395+ bool isTriviallyFalse();
4396+ /** Count size of the entire formula in number of nodes */
4397+ virtual int formulaSize() const = 0;
4398+
4399+ bool isSatisfied() const
4400+ {
4401+ return _eval == RTRUE;
4402+ }
4403+
4404+ void setSatisfied(bool isSatisfied)
4405+ {
4406+ _eval = isSatisfied ? RTRUE : RFALSE;
4407+ }
4408+
4409+ void setSatisfied(Result isSatisfied)
4410+ {
4411+ _eval = isSatisfied;
4412+ }
4413+
4414+ void setInvariant(bool isInvariant)
4415+ {
4416+ _inv = isInvariant;
4417+ }
4418+
4419+ bool isInvariant()
4420+ {
4421+ return _inv;
4422+ }
4423+
4424+ virtual bool isTemporal() const { return false;}
4425+ virtual CTLType getQueryType() const = 0;
4426+ virtual Quantifier getQuantifier() const = 0;
4427+ virtual Path getPath() const = 0;
4428+ static std::shared_ptr<Condition>
4429+ initialMarkingRW(const std::function<std::shared_ptr<Condition> ()>& func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw);
4430+ virtual bool containsNext() const = 0;
4431+ virtual bool nestedDeadlock() const = 0;
4432+ protected:
4433+ //Value for checking if condition is trivially true or false.
4434+ //0 is undecided (default), 1 is true, 2 is false.
4435+ uint32_t trivial = 0;
4436+ };
4437+ typedef std::shared_ptr<Condition> Condition_ptr;
4438+ typedef std::shared_ptr<Expr> Expr_ptr;
4439+ } // PQL
4440+} // PetriEngine
4441+
4442+#endif // PQL_H
4443
4444=== added file 'include/PetriEngine/PQL/PQLParser.h'
4445--- include/PetriEngine/PQL/PQLParser.h 1970-01-01 00:00:00 +0000
4446+++ include/PetriEngine/PQL/PQLParser.h 2020-09-11 14:21:20 +0000
4447@@ -0,0 +1,34 @@
4448+/* PeTe - Petri Engine exTremE
4449+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
4450+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
4451+ * Lars Kærlund Østergaard <larsko@gmail.com>,
4452+ *
4453+ * This program is free software: you can redistribute it and/or modify
4454+ * it under the terms of the GNU General Public License as published by
4455+ * the Free Software Foundation, either version 3 of the License, or
4456+ * (at your option) any later version.
4457+ *
4458+ * This program is distributed in the hope that it will be useful,
4459+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
4460+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
4461+ * GNU General Public License for more details.
4462+ *
4463+ * You should have received a copy of the GNU General Public License
4464+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
4465+ */
4466+#ifndef PQLPARSER_H
4467+#define PQLPARSER_H
4468+
4469+#include <string>
4470+#include <memory>
4471+#include <vector>
4472+
4473+namespace PetriEngine {
4474+ namespace PQL {
4475+
4476+ class Condition;
4477+
4478+ std::shared_ptr<Condition> ParseQuery(const std::string& queryString, std::vector<std::string>& placenameforbound);
4479+ }
4480+}
4481+#endif // PQLPARSER_H
4482
4483=== added file 'include/PetriEngine/PQL/Visitor.h'
4484--- include/PetriEngine/PQL/Visitor.h 1970-01-01 00:00:00 +0000
4485+++ include/PetriEngine/PQL/Visitor.h 2020-09-11 14:21:20 +0000
4486@@ -0,0 +1,101 @@
4487+/*
4488+ * Copyright Peter G. Jensen, all rights reserved.
4489+ */
4490+
4491+/*
4492+ * File: Visitor.h
4493+ * Author: Peter G. Jensen <root@petergjoel.dk>
4494+ *
4495+ * Created on April 11, 2020, 1:07 PM
4496+ */
4497+
4498+#ifndef VISITOR_H
4499+#define VISITOR_H
4500+
4501+#include "PetriEngine/PQL/Expressions.h"
4502+#include <type_traits>
4503+
4504+namespace PetriEngine
4505+{
4506+ namespace PQL
4507+ {
4508+ class Visitor {
4509+ public:
4510+ Visitor() {}
4511+
4512+ template<typename T>
4513+ void accept(T element)
4514+ {
4515+ _accept(element);
4516+ }
4517+
4518+ protected:
4519+
4520+ virtual void _accept(const NotCondition* element) = 0;
4521+ virtual void _accept(const AndCondition* element) = 0;
4522+ virtual void _accept(const OrCondition* element) = 0;
4523+ virtual void _accept(const LessThanCondition* element) = 0;
4524+ virtual void _accept(const LessThanOrEqualCondition* element) = 0;
4525+ virtual void _accept(const GreaterThanCondition* element) = 0;
4526+ virtual void _accept(const GreaterThanOrEqualCondition* element) = 0;
4527+ virtual void _accept(const EqualCondition* element) = 0;
4528+ virtual void _accept(const NotEqualCondition* element) = 0;
4529+
4530+ virtual void _accept(const DeadlockCondition* element) = 0;
4531+ virtual void _accept(const CompareConjunction* element) = 0;
4532+ virtual void _accept(const UnfoldedUpperBoundsCondition* element) = 0;
4533+
4534+ // Quantifiers, most uses of the visitor will not use the quantifiers - so we give a default implementation.
4535+ // default behaviour is error
4536+ virtual void _accept(const EFCondition*)
4537+ { assert(false); std::cerr << "No accept for EFCondition" << std::endl; exit(0);};
4538+ virtual void _accept(const EGCondition*)
4539+ { assert(false); std::cerr << "No accept for EGCondition" << std::endl; exit(0);};
4540+ virtual void _accept(const AGCondition*)
4541+ { assert(false); std::cerr << "No accept for AGCondition" << std::endl; exit(0);};
4542+ virtual void _accept(const AFCondition*)
4543+ { assert(false); std::cerr << "No accept for AFCondition" << std::endl; exit(0);};
4544+ virtual void _accept(const EXCondition*)
4545+ { assert(false); std::cerr << "No accept for EXCondition" << std::endl; exit(0);};
4546+ virtual void _accept(const AXCondition*)
4547+ { assert(false); std::cerr << "No accept for AXCondition" << std::endl; exit(0);};
4548+ virtual void _accept(const EUCondition*)
4549+ { assert(false); std::cerr << "No accept for EUCondition" << std::endl; exit(0);};
4550+ virtual void _accept(const AUCondition*)
4551+ { assert(false); std::cerr << "No accept for AUCondition" << std::endl; exit(0);};
4552+
4553+ // shallow elements, neither of these should exist in a compiled expression
4554+ virtual void _accept(const UnfoldedFireableCondition* element)
4555+ { assert(false); std::cerr << "No accept for UnfoldedFireableCondition" << std::endl; exit(0);};
4556+ virtual void _accept(const FireableCondition* element)
4557+ { assert(false); std::cerr << "No accept for FireableCondition" << std::endl; exit(0);};
4558+ virtual void _accept(const UpperBoundsCondition* element)
4559+ { assert(false); std::cerr << "No accept for UpperBoundsCondition" << std::endl; exit(0);};
4560+ virtual void _accept(const LivenessCondition* element)
4561+ { assert(false); std::cerr << "No accept for LivenessCondition" << std::endl; exit(0);};
4562+ virtual void _accept(const KSafeCondition* element)
4563+ { assert(false); std::cerr << "No accept for KSafeCondition" << std::endl; exit(0);};
4564+ virtual void _accept(const QuasiLivenessCondition* element)
4565+ { assert(false); std::cerr << "No accept for QuasiLivenessCondition" << std::endl; exit(0);};
4566+ virtual void _accept(const StableMarkingCondition* element)
4567+ { assert(false); std::cerr << "No accept for StableMarkingCondition" << std::endl; exit(0);};
4568+ virtual void _accept(const BooleanCondition* element)
4569+ { assert(false); std::cerr << "No accept for BooleanCondition" << std::endl; exit(0);};
4570+
4571+ // Expression
4572+ virtual void _accept(const UnfoldedIdentifierExpr* element) = 0;
4573+ virtual void _accept(const LiteralExpr* element) = 0;
4574+ virtual void _accept(const PlusExpr* element) = 0;
4575+ virtual void _accept(const MultiplyExpr* element) = 0;
4576+ virtual void _accept(const MinusExpr* element) = 0;
4577+ virtual void _accept(const SubtractExpr* element) = 0;
4578+
4579+ // shallow expression, default to error
4580+ virtual void _accept(const IdentifierExpr* element)
4581+ { assert(false); std::cerr << "No accept for IdentifierExpr" << std::endl; exit(0);};
4582+ };
4583+ }
4584+}
4585+
4586+#endif /* VISITOR_H */
4587+
4588
4589=== added file 'include/PetriEngine/PetriNet.h'
4590--- include/PetriEngine/PetriNet.h 1970-01-01 00:00:00 +0000
4591+++ include/PetriEngine/PetriNet.h 2020-09-11 14:21:20 +0000
4592@@ -0,0 +1,136 @@
4593+/* PeTe - Petri Engine exTremE
4594+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
4595+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
4596+ * Lars Kærlund Østergaard <larsko@gmail.com>,
4597+ * Peter Gjøl Jensen <root@petergjoel.dk>
4598+ *
4599+ * This program is free software: you can redistribute it and/or modify
4600+ * it under the terms of the GNU General Public License as published by
4601+ * the Free Software Foundation, either version 3 of the License, or
4602+ * (at your option) any later version.
4603+ *
4604+ * This program is distributed in the hope that it will be useful,
4605+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
4606+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
4607+ * GNU General Public License for more details.
4608+ *
4609+ * You should have received a copy of the GNU General Public License
4610+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
4611+ */
4612+#ifndef PETRINET_H
4613+#define PETRINET_H
4614+
4615+#include <string>
4616+#include <vector>
4617+#include <climits>
4618+#include <limits>
4619+#include <iostream>
4620+
4621+namespace PetriEngine {
4622+
4623+ namespace PQL {
4624+ class Condition;
4625+ }
4626+
4627+ namespace Structures {
4628+ class State;
4629+ }
4630+
4631+ class PetriNetBuilder;
4632+ class SuccessorGenerator;
4633+
4634+ struct TransPtr {
4635+ uint32_t inputs;
4636+ uint32_t outputs;
4637+ };
4638+
4639+ struct Invariant {
4640+ uint32_t place;
4641+ uint32_t tokens;
4642+ bool inhibitor;
4643+ int8_t direction;
4644+ // we can pack things here, but might give slowdown
4645+ } /*__attribute__((packed))*/;
4646+
4647+ /** Type used for holding markings values */
4648+ typedef uint32_t MarkVal;
4649+
4650+ /** Efficient representation of PetriNet */
4651+ class PetriNet {
4652+ PetriNet(uint32_t transitions, uint32_t invariants, uint32_t places);
4653+ public:
4654+ ~PetriNet();
4655+
4656+ uint32_t initial(size_t id) const;
4657+ MarkVal* makeInitialMarking() const;
4658+ /** Fire transition if possible and store result in result */
4659+ bool deadlocked(const MarkVal* marking) const;
4660+ bool fireable(const MarkVal* marking, int transitionIndex);
4661+ std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const;
4662+ std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const;
4663+ uint32_t numberOfTransitions() const {
4664+ return _ntransitions;
4665+ }
4666+
4667+ uint32_t numberOfPlaces() const {
4668+ return _nplaces;
4669+ }
4670+ int inArc(uint32_t place, uint32_t transition) const;
4671+ int outArc(uint32_t transition, uint32_t place) const;
4672+
4673+
4674+ const std::vector<std::string>& transitionNames() const
4675+ {
4676+ return _transitionnames;
4677+ }
4678+
4679+ const std::vector<std::string>& placeNames() const
4680+ {
4681+ return _placenames;
4682+ }
4683+
4684+ void print(MarkVal const * const val) const
4685+ {
4686+ for(size_t i = 0; i < _nplaces; ++i)
4687+ {
4688+ if(val[i] != 0)
4689+ {
4690+ std::cout << _placenames[i] << "(" << i << ")" << " -> " << val[i] << std::endl;
4691+ }
4692+ }
4693+ }
4694+
4695+ void sort();
4696+
4697+ void toXML(std::ostream& out);
4698+
4699+ const MarkVal* initial() const {
4700+ return _initialMarking;
4701+ }
4702+
4703+ private:
4704+
4705+ /** Number of x variables
4706+ * @remarks We could also get this from the _places vector, but I don't see any
4707+ * any complexity garentees for this type.
4708+ */
4709+ uint32_t _ninvariants, _ntransitions, _nplaces;
4710+
4711+ std::vector<TransPtr> _transitions;
4712+ std::vector<Invariant> _invariants;
4713+ std::vector<uint32_t> _placeToPtrs;
4714+ MarkVal* _initialMarking;
4715+
4716+ std::vector<std::string> _transitionnames;
4717+ std::vector<std::string> _placenames;
4718+
4719+ friend class PetriNetBuilder;
4720+ friend class Reducer;
4721+ friend class SuccessorGenerator;
4722+ friend class ReducingSuccessorGenerator;
4723+ friend class STSolver;
4724+ };
4725+
4726+} // PetriEngine
4727+
4728+#endif // PETRINET_H
4729
4730=== added file 'include/PetriEngine/PetriNetBuilder.h'
4731--- include/PetriEngine/PetriNetBuilder.h 1970-01-01 00:00:00 +0000
4732+++ include/PetriEngine/PetriNetBuilder.h 2020-09-11 14:21:20 +0000
4733@@ -0,0 +1,145 @@
4734+/* PeTe - Petri Engine exTremE
4735+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
4736+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
4737+ * Lars Kærlund Østergaard <larsko@gmail.com>,
4738+ *
4739+ * This program is free software: you can redistribute it and/or modify
4740+ * it under the terms of the GNU General Public License as published by
4741+ * the Free Software Foundation, either version 3 of the License, or
4742+ * (at your option) any later version.
4743+ *
4744+ * This program is distributed in the hope that it will be useful,
4745+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
4746+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
4747+ * GNU General Public License for more details.
4748+ *
4749+ * You should have received a copy of the GNU General Public License
4750+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
4751+ */
4752+#ifndef PETRINETBUILDER_H
4753+#define PETRINETBUILDER_H
4754+
4755+#include <vector>
4756+#include <string>
4757+#include <memory>
4758+#include <chrono>
4759+#include "AbstractPetriNetBuilder.h"
4760+#include "PQL/PQL.h"
4761+#include "PetriNet.h"
4762+#include "Reducer.h"
4763+#include "NetStructures.h"
4764+#include "Reachability/ReachabilityResult.h"
4765+namespace PetriEngine {
4766+ /** Builder for building engine representations of PetriNets */
4767+ class PetriNetBuilder : public AbstractPetriNetBuilder {
4768+ public:
4769+ friend class Reducer;
4770+
4771+ public:
4772+ PetriNetBuilder();
4773+ PetriNetBuilder(const PetriNetBuilder& other);
4774+ void addPlace(const std::string& name, int tokens, double x, double y) override;
4775+ void addTransition(const std::string& name,
4776+ double x,
4777+ double y) override;
4778+ void addInputArc(const std::string& place,
4779+ const std::string& transition,
4780+ bool inhibitor,
4781+ int weight) override;
4782+ void addOutputArc(const std::string& transition, const std::string& place, int weight) override;
4783+
4784+ virtual void sort() override;
4785+ /** Make the resulting petri net, you take ownership */
4786+ PetriNet* makePetriNet(bool reorder = true);
4787+ /** Make the resulting initial marking, you take ownership */
4788+
4789+ MarkVal const * initMarking()
4790+ {
4791+ return initialMarking.data();
4792+ }
4793+
4794+ uint32_t numberOfPlaces() const
4795+ {
4796+ return _placenames.size();
4797+ }
4798+
4799+ uint32_t numberOfTransitions() const
4800+ {
4801+ return _transitionnames.size();
4802+ }
4803+
4804+ const std::unordered_map<std::string, uint32_t>& getPlaceNames() const
4805+ {
4806+ return _placenames;
4807+ }
4808+
4809+ const std::unordered_map<std::string, uint32_t>& getTransitionNames() const
4810+ {
4811+ return _transitionnames;
4812+ }
4813+
4814+ void reduce(std::vector<std::shared_ptr<PQL::Condition> >& query,
4815+ std::vector<Reachability::ResultPrinter::Result>& results,
4816+ int reductiontype, bool reconstructTrace, const PetriNet* net, int timeout, std::vector<uint32_t>& reductions);
4817+
4818+ size_t RemovedTransitions() const
4819+ {
4820+ return reducer.RemovedTransitions();
4821+ }
4822+
4823+ size_t RemovedPlaces() const
4824+ {
4825+ return reducer.RemovedPlaces();
4826+ }
4827+
4828+ void printStats(std::ostream& out)
4829+ {
4830+ reducer.printStats(out);
4831+ }
4832+
4833+ Reducer* getReducer() { return &reducer; }
4834+
4835+ std::vector<std::pair<std::string, uint32_t>> orphanPlaces() const {
4836+ std::vector<std::pair<std::string, uint32_t>> res;
4837+ for(uint32_t p = 0; p < _places.size(); p++) {
4838+ if(_places[p].consumers.size() == 0 && _places[p].producers.size() == 0) {
4839+ for(auto &n : _placenames) {
4840+ if(n.second == p) {
4841+ res.push_back(std::make_pair(n.first, initialMarking[p]));
4842+ break;
4843+ }
4844+ }
4845+ }
4846+ }
4847+ return res;
4848+ }
4849+
4850+ double getReductionTime() const {
4851+ // duration in seconds
4852+ auto end = std::chrono::high_resolution_clock::now();
4853+ return (std::chrono::duration_cast<std::chrono::microseconds>(end - _start).count())*0.000001;
4854+ }
4855+
4856+ void startTimer() {
4857+ _start = std::chrono::high_resolution_clock::now();
4858+ }
4859+
4860+ private:
4861+ uint32_t nextPlaceId(std::vector<uint32_t>& counts, std::vector<uint32_t>& pcounts, std::vector<uint32_t>& ids, bool reorder);
4862+ std::chrono::high_resolution_clock::time_point _start;
4863+
4864+ protected:
4865+ std::unordered_map<std::string, uint32_t> _placenames;
4866+ std::unordered_map<std::string, uint32_t> _transitionnames;
4867+
4868+ std::vector<Transition> _transitions;
4869+ std::vector<Place> _places;
4870+
4871+ std::vector<MarkVal> initialMarking;
4872+ Reducer reducer;
4873+ };
4874+
4875+}
4876+
4877+#endif // PETRINETBUILDER_H
4878+
4879
4880=== added directory 'include/PetriEngine/Reachability'
4881=== added file 'include/PetriEngine/Reachability/ReachabilityResult.h'
4882--- include/PetriEngine/Reachability/ReachabilityResult.h 1970-01-01 00:00:00 +0000
4883+++ include/PetriEngine/Reachability/ReachabilityResult.h 2020-09-11 14:21:20 +0000
4884@@ -0,0 +1,97 @@
4885+/* PeTe - Petri Engine exTremE
4886+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
4887+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
4888+ * Lars Kærlund Østergaard <larsko@gmail.com>,
4889+ * Peter Gjøl Jensen <root@petergjoel.dk>
4890+ *
4891+ * This program is free software: you can redistribute it and/or modify
4892+ * it under the terms of the GNU General Public License as published by
4893+ * the Free Software Foundation, either version 3 of the License, or
4894+ * (at your option) any later version.
4895+ *
4896+ * This program is distributed in the hope that it will be useful,
4897+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
4898+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
4899+ * GNU General Public License for more details.
4900+ *
4901+ * You should have received a copy of the GNU General Public License
4902+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
4903+ */
4904+#ifndef REACHABILITYRESULT_H
4905+#define REACHABILITYRESULT_H
4906+
4907+#include <vector>
4908+#include "../PQL/PQL.h"
4909+#include "../Structures/StateSet.h"
4910+#include "../Reducer.h"
4911+
4912+struct options_t;
4913+
4914+namespace PetriEngine {
4915+ class PetriNetBuilder;
4916+ namespace Reachability {
4917+
4918+ /** Result of a reachability search */
4919+
4920+ class AbstractHandler {
4921+ public:
4922+ enum Result {
4923+ /** The query was satisfied */
4924+ Satisfied,
4925+ /** The query cannot be satisfied */
4926+ NotSatisfied,
4927+ /** We're unable to say if the query can be satisfied */
4928+ Unknown,
4929+ /** The query should be verified using the CTL engine */
4930+ CTL,
4931+ /** Just ignore */
4932+ Ignore
4933+ };
4934+ virtual std::pair<Result, bool> handle(
4935+ size_t index,
4936+ PQL::Condition* query,
4937+ Result result,
4938+ const std::vector<uint32_t>* maxPlaceBound = nullptr,
4939+ size_t expandedStates = 0,
4940+ size_t exploredStates = 0,
4941+ size_t discoveredStates = 0,
4942+ int maxTokens = 0,
4943+ Structures::StateSetInterface* stateset = nullptr, size_t lastmarking = 0, const MarkVal* initialMarking = nullptr) = 0;
4944+ };
4945+
4946+ class ResultPrinter : public AbstractHandler {
4947+ protected:
4948+ PetriNetBuilder* builder;
4949+ options_t* options;
4950+ std::vector<std::string>& querynames;
4951+ Reducer* reducer;
4952+ public:
4953+ const string techniques = "TECHNIQUES COLLATERAL_PROCESSING STRUCTURAL_REDUCTION QUERY_REDUCTION SAT_SMT ";
4954+ const string techniquesStateSpace = "TECHNIQUES EXPLICIT STATE_COMPRESSION";
4955+
4956+ ResultPrinter(PetriNetBuilder* b, options_t* o, std::vector<std::string>& querynames)
4957+ : builder(b), options(o), querynames(querynames), reducer(NULL)
4958+ {};
4959+
4960+ void setReducer(Reducer* r) { this->reducer = r; }
4961+
4962+ std::pair<Result, bool> handle(
4963+ size_t index,
4964+ PQL::Condition* query,
4965+ Result result,
4966+ const std::vector<uint32_t>* maxPlaceBound = nullptr,
4967+ size_t expandedStates = 0,
4968+ size_t exploredStates = 0,
4969+ size_t discoveredStates = 0,
4970+ int maxTokens = 0,
4971+ Structures::StateSetInterface* stateset = nullptr, size_t lastmarking = 0, const MarkVal* initialMarking = nullptr) override;
4972+
4973+ std::string printTechniques();
4974+
4975+ void printTrace(Structures::StateSetInterface*, size_t lastmarking);
4976+
4977+ };
4978+ } // Reachability
4979+} // PetriEngine
4980+
4981+#endif // REACHABILITYRESULT_H
4982
4983=== added file 'include/PetriEngine/Reachability/ReachabilitySearch.h'
4984--- include/PetriEngine/Reachability/ReachabilitySearch.h 1970-01-01 00:00:00 +0000
4985+++ include/PetriEngine/Reachability/ReachabilitySearch.h 2020-09-11 14:21:20 +0000
4986@@ -0,0 +1,182 @@
4987+/* PeTe - Petri Engine exTremE
4988+ * Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
4989+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
4990+ * Lars Kærlund Østergaard <larsko@gmail.com>,
4991+ * Peter Gjøl Jensen <root@petergjoel.dk>
4992+ *
4993+ * This program is free software: you can redistribute it and/or modify
4994+ * it under the terms of the GNU General Public License as published by
4995+ * the Free Software Foundation, either version 3 of the License, or
4996+ * (at your option) any later version.
4997+ *
4998+ * This program is distributed in the hope that it will be useful,
4999+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
5000+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
The diff has been truncated for viewing.

Subscribers

People subscribed via source and target branches