lp:~tapaal-ltl/verifypn/ltl-model-checker
Created by
Nikolaj Jensen Ulrik
and last modified
- Get this branch:
- bzr branch lp:~tapaal-ltl/verifypn/ltl-model-checker
Members of
tapaal-ltl
can upload to this branch. Log in for directions.
Branch merges
Propose for merging
No branches
dependent on this one.
- VerifyPN Maintainers: Pending requested
-
Diff: 8302 lines (+5490/-752) (has conflicts)60 files modifiedCMakeLists.txt (+12/-1)
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 (+39/-0)
include/LTL/BuchiSuccessorGenerator.h (+95/-0)
include/LTL/LTL.h (+34/-0)
include/LTL/LTLToBuchi.h (+123/-0)
include/LTL/LTLValidator.h (+210/-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 (+84/-0)
include/LTL/Structures/ProductStateFactory.h (+46/-0)
include/PetriEngine/PQL/CTLVisitor.h (+200/-0)
include/PetriEngine/PQL/Expressions.h (+288/-111)
include/PetriEngine/PQL/PQL.h (+47/-43)
include/PetriEngine/PQL/QueryPrinter.h (+131/-0)
include/PetriEngine/PQL/Visitor.h (+15/-3)
include/PetriEngine/Reachability/ReachabilityResult.h (+2/-0)
include/PetriEngine/Reducer.h (+8/-3)
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 (+80/-14)
include/PetriEngine/SuccessorGenerator.h (+10/-1)
include/PetriEngine/options.h (+45/-10)
src/CMakeLists.txt (+8/-4)
src/LTL/Algorithm/CMakeLists.txt (+8/-0)
src/LTL/Algorithm/LTLToBuchi.cpp (+170/-0)
src/LTL/Algorithm/ModelChecker.cpp (+71/-0)
src/LTL/Algorithm/NestedDepthFirstSearch.cpp (+185/-0)
src/LTL/Algorithm/ProductPrinter.cpp (+70/-0)
src/LTL/Algorithm/ProductSuccessorGenerator.cpp (+152/-0)
src/LTL/Algorithm/RandomNDFS.cpp (+107/-0)
src/LTL/Algorithm/TarjanModelChecker.cpp (+216/-0)
src/LTL/CMakeLists.txt (+10/-0)
src/LTL/Simplification/CMakeLists.txt (+8/-0)
src/LTL/Simplification/SpotToPQL.cpp (+160/-0)
src/LTL/_LTL.cpp (+52/-0)
src/PetriEngine/PQL/CMakeLists.txt (+2/-2)
src/PetriEngine/PQL/CTLVisitor.cpp (+526/-0)
src/PetriEngine/PQL/Expressions.cpp (+388/-216)
src/PetriEngine/PQL/PQL.cpp (+6/-0)
src/PetriEngine/PQL/QueryPrinter.cpp (+300/-0)
src/PetriEngine/PetriNetBuilder.cpp (+3/-2)
src/PetriEngine/Reachability/ResultPrinter.cpp (+1/-1)
src/PetriEngine/Reducer.cpp (+168/-124)
src/PetriEngine/Structures/AlignedEncoder.cpp (+1/-1)
src/PetriEngine/Structures/Queue.cpp (+16/-2)
src/PetriEngine/SuccessorGenerator.cpp (+27/-0)
src/PetriParse/QueryBinaryParser.cpp (+22/-4)
src/PetriParse/QueryXMLParser.cpp (+58/-116)
src/VerifyPN.cpp (+350/-86)
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)
Related source package recipes
Branch information
Recent revisions
- 257. By Simon Virenfeldt
-
Merge lp:~tapaal-ltl/verifypn/traceable-tarjan@259
- 255. By Simon Virenfeldt
-
Enable parsing LTL formulae that does now start with an A or an E condition.
Branch metadata
- Branch format:
- Branch format 7
- Repository format:
- Bazaar repository format 2a (needs bzr 1.16 or later)
- Stacked on:
- lp:verifypn
