lp:~tapaal-ltl/verifypn/mcc2021

CMakeLists.txt (+23/-9)
include/CTL/Algorithm/CertainZeroFPA.h (+1/-2)
include/CTL/DependencyGraph/Configuration.h (+12/-15)
include/CTL/DependencyGraph/Edge.h (+11/-5)
include/CTL/PetriNets/PetriConfig.h (+0/-2)
include/LTL/Algorithm/ModelChecker.h (+72/-0)
include/LTL/Algorithm/NestedDepthFirstSearch.h (+91/-0)
include/LTL/Algorithm/ProductPrinter.h (+31/-0)
include/LTL/Algorithm/RandomNDFS.h (+59/-0)
include/LTL/Algorithm/TarjanModelChecker.h (+140/-0)
include/LTL/AlgorithmTypes.h (+40/-0)
include/LTL/BuchiSuccessorGenerator.h (+95/-0)
include/LTL/LTL.h (+34/-0)
include/LTL/LTLToBuchi.h (+131/-0)
include/LTL/LTLValidator.h (+201/-0)
include/LTL/ProductSuccessorGenerator.h (+146/-0)
include/LTL/Simplification/SpotToPQL.h (+42/-0)
include/LTL/Structures/BuchiAutomaton.h (+31/-0)
include/LTL/Structures/ProductState.h (+81/-0)
include/LTL/Structures/ProductStateFactory.h (+46/-0)
include/PetriEngine/Colored/ArcIntervals.h (+108/-0)
include/PetriEngine/Colored/BindingGenerator.h (+71/-0)
include/PetriEngine/Colored/ColoredNetStructures.h (+22/-12)
include/PetriEngine/Colored/ColoredPetriNetBuilder.h (+64/-43)
include/PetriEngine/Colored/Colors.h (+127/-21)
include/PetriEngine/Colored/Expressions.h (+777/-66)
include/PetriEngine/Colored/GuardRestrictor.h (+83/-0)
include/PetriEngine/Colored/IntervalGenerator.h (+197/-0)
include/PetriEngine/Colored/Intervals.h (+630/-0)
include/PetriEngine/PQL/CTLVisitor.h (+197/-0)
include/PetriEngine/PQL/Contexts.h (+6/-6)
include/PetriEngine/PQL/Expressions.h (+304/-187)
include/PetriEngine/PQL/PQL.h (+70/-71)
include/PetriEngine/PQL/QueryPrinter.h (+127/-0)
include/PetriEngine/PQL/Visitor.h (+82/-6)
include/PetriEngine/PetriNet.h (+1/-0)
include/PetriEngine/Reachability/ReachabilityResult.h (+4/-2)
include/PetriEngine/Reachability/ReachabilitySearch.h (+12/-2)
include/PetriEngine/Reducer.h (+8/-3)
include/PetriEngine/ReducingSuccessorGenerator.h (+25/-54)
include/PetriEngine/Simplification/Member.h (+1/-1)
include/PetriEngine/Structures/Queue.h (+2/-0)
include/PetriEngine/Structures/State.h (+40/-7)
include/PetriEngine/Structures/StateSet.h (+85/-14)
include/PetriEngine/Structures/binarywrapper.h (+2/-2)
include/PetriEngine/Structures/light_deque.h (+4/-5)
include/PetriEngine/Stubborn/InterestingTransitionVisitor.h (+175/-0)
include/PetriEngine/Stubborn/ReachabilityStubbornSet.h (+40/-0)
include/PetriEngine/Stubborn/StubbornSet.h (+146/-0)
include/PetriEngine/SuccessorGenerator.h (+10/-1)
include/PetriEngine/TAR/ContainsVisitor.h (+0/-10)
include/PetriEngine/TAR/PlaceUseVisitor.h (+0/-2)
include/PetriEngine/TAR/RangeContext.h (+0/-2)
include/PetriEngine/TAR/RangeEvalContext.h (+0/-2)
include/PetriEngine/TAR/Solver.h (+1/-0)
include/PetriEngine/TAR/range.h (+19/-1)
include/PetriEngine/options.h (+82/-44)
include/PetriParse/PNMLParser.h (+6/-1)
include/PetriParse/QueryParser.h (+2/-3)
include/PetriParse/QueryXMLParser.h (+1/-1)
src/CMakeLists.txt (+13/-4)
src/CTL/Algorithm/CertainZeroFPA.cpp (+81/-51)
src/CTL/Algorithm/LocalFPA.cpp (+1/-11)
src/CTL/DependencyGraph/Configuration.cpp (+21/-2)
src/CTL/PetriNets/OnTheFlyDG.cpp (+20/-19)
src/CTL/SearchStrategy/HeuristicSearch.cpp (+1/-1)
src/LTL/Algorithm/CMakeLists.txt (+8/-0)
src/LTL/Algorithm/LTLToBuchi.cpp (+162/-0)
src/LTL/Algorithm/ModelChecker.cpp (+71/-0)
src/LTL/Algorithm/NestedDepthFirstSearch.cpp (+185/-0)
src/LTL/Algorithm/ProductPrinter.cpp (+71/-0)
src/LTL/Algorithm/ProductSuccessorGenerator.cpp (+153/-0)
src/LTL/Algorithm/RandomNDFS.cpp (+107/-0)
src/LTL/Algorithm/TarjanModelChecker.cpp (+216/-0)
src/LTL/CMakeLists.txt (+14/-0)
src/LTL/Simplification/CMakeLists.txt (+8/-0)
src/LTL/Simplification/SpotToPQL.cpp (+160/-0)
src/LTL/_LTL.cpp (+52/-0)
src/PetriEngine/CMakeLists.txt (+2/-1)
src/PetriEngine/Colored/BindingGenerator.cpp (+161/-0)
src/PetriEngine/Colored/CMakeLists.txt (+3/-1)
src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp (+305/-138)
src/PetriEngine/Colored/Colors.cpp (+59/-9)
src/PetriEngine/Colored/GuardRestrictor.cpp (+382/-0)
src/PetriEngine/Colored/Multiset.cpp (+22/-14)
src/PetriEngine/PQL/CMakeLists.txt (+2/-2)
src/PetriEngine/PQL/CTLVisitor.cpp (+492/-0)
src/PetriEngine/PQL/Expressions.cpp (+461/-778)
src/PetriEngine/PQL/PQL.cpp (+6/-0)
src/PetriEngine/PQL/PQLQueryParser.y (+2/-2)
src/PetriEngine/PQL/QueryPrinter.cpp (+292/-0)
src/PetriEngine/PetriNet.cpp (+5/-7)
src/PetriEngine/PetriNetBuilder.cpp (+12/-14)
src/PetriEngine/Reachability/ResultPrinter.cpp (+1/-1)
src/PetriEngine/Reducer.cpp (+168/-124)
src/PetriEngine/ReducingSuccessorGenerator.cpp (+31/-302)
src/PetriEngine/Structures/AlignedEncoder.cpp (+1/-1)
src/PetriEngine/Structures/Queue.cpp (+16/-2)
src/PetriEngine/Stubborn/CMakeLists.txt (+3/-0)
src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp (+326/-0)
src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp (+41/-0)
src/PetriEngine/Stubborn/StubbornSet.cpp (+302/-0)
src/PetriEngine/SuccessorGenerator.cpp (+27/-0)
src/PetriEngine/TAR/PlaceUseVisitor.cpp (+0/-12)
src/PetriEngine/TAR/RangeContext.cpp (+0/-10)
src/PetriEngine/TAR/RangeEvalContext.cpp (+0/-10)
src/PetriEngine/TAR/Solver.cpp (+1/-1)
src/PetriParse/PNMLParser.cpp (+221/-60)
src/PetriParse/QueryBinaryParser.cpp (+24/-6)
src/PetriParse/QueryXMLParser.cpp (+73/-133)
src/VerifyPN.cpp (+447/-102)
test_models/LTL/Bounded/model.pnml (+133/-0)
test_models/LTL/Bounded/query.xml (+36/-0)
test_models/LTL/generator.pnml (+60/-0)
test_models/LTL/generator.xml (+52/-0)