lp:~verifydtapn-contributers/verifydtapn/partial-order
Created by
Peter Gjøl Jensen
and last modified
- Get this branch:
- bzr branch lp:~verifydtapn-contributers/verifydtapn/partial-order
Members of
verifydtapn-contributers
can upload to this branch. Log in for directions.
Branch merges
Propose for merging
No branches
dependent on this one.
- Jiri Srba: Approve
-
Diff: 11921 lines (+5598/-3307)89 files modifiedmakefile.linux64 (+2/-2)
src/Core/ArgsParser.cpp (+54/-2)
src/Core/ArgsParser.hpp (+1/-0)
src/Core/QueryParser/AST.cpp (+13/-13)
src/Core/QueryParser/AST.hpp (+461/-384)
src/Core/QueryParser/Generated/lexer.cpp (+118/-108)
src/Core/QueryParser/Generated/location.hh (+104/-86)
src/Core/QueryParser/Generated/parser.cpp (+945/-835)
src/Core/QueryParser/Generated/parser.hpp (+412/-271)
src/Core/QueryParser/Generated/position.hh (+94/-79)
src/Core/QueryParser/Generated/stack.hh (+91/-74)
src/Core/QueryParser/NormalizationVisitor.cpp (+54/-54)
src/Core/QueryParser/NormalizationVisitor.hpp (+14/-14)
src/Core/QueryParser/Visitor.hpp (+13/-13)
src/Core/QueryParser/flex.ll (+4/-2)
src/Core/QueryParser/grammar.yy (+4/-2)
src/Core/TAPN/TimeInterval.cpp (+10/-2)
src/Core/TAPN/TimeInterval.hpp (+33/-4)
src/Core/TAPN/TimeInvariant.cpp (+7/-4)
src/Core/TAPN/TimeInvariant.hpp (+2/-1)
src/Core/TAPN/TimedArcPetriNet.cpp (+10/-1)
src/Core/TAPN/TimedArcPetriNet.hpp (+2/-1)
src/Core/TAPN/TimedPlace.hpp (+3/-0)
src/Core/TAPN/TimedTransition.cpp (+35/-0)
src/Core/TAPN/TimedTransition.hpp (+11/-1)
src/Core/TAPNParser/TAPNXmlParser.cpp (+49/-27)
src/Core/TAPNParser/TAPNXmlParser.hpp (+4/-1)
src/Core/VerificationOptions.cpp (+1/-0)
src/Core/VerificationOptions.hpp (+24/-2)
src/DiscreteVerification/DataStructures/MarkingEncoder.h (+22/-8)
src/DiscreteVerification/DataStructures/MarkingStore.h (+100/-0)
src/DiscreteVerification/DataStructures/MetaData.h (+63/-0)
src/DiscreteVerification/DataStructures/NonStrictMarking.hpp (+1/-40)
src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp (+24/-10)
src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp (+11/-0)
src/DiscreteVerification/DataStructures/PTrieMarkingStore.h (+107/-0)
src/DiscreteVerification/DataStructures/PWList.hpp (+1/-1)
src/DiscreteVerification/DataStructures/SimpleMarkingStore.h (+160/-0)
src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp (+1/-1)
src/DiscreteVerification/DataStructures/TimeDartPWList.hpp (+1/-1)
src/DiscreteVerification/DataStructures/Waiting.h (+178/-0)
src/DiscreteVerification/DataStructures/binarywrapper.h (+11/-4)
src/DiscreteVerification/DataStructures/light_deque.h (+70/-0)
src/DiscreteVerification/DataStructures/ptrie.h (+140/-85)
src/DiscreteVerification/DeadlockVisitor.cpp (+37/-37)
src/DiscreteVerification/DeadlockVisitor.hpp (+13/-13)
src/DiscreteVerification/DiscreteVerification.cpp (+91/-15)
src/DiscreteVerification/Generator.cpp (+482/-0)
src/DiscreteVerification/Generator.h (+69/-0)
src/DiscreteVerification/PlaceVisitor.cpp (+22/-22)
src/DiscreteVerification/PlaceVisitor.hpp (+14/-14)
src/DiscreteVerification/QueryVisitor.hpp (+47/-33)
src/DiscreteVerification/ReducingGenerator.cpp (+577/-0)
src/DiscreteVerification/ReducingGenerator.hpp (+85/-0)
src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp (+14/-14)
src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp (+13/-13)
src/DiscreteVerification/SearchStrategies/NonStrictBFS.hpp (+0/-2)
src/DiscreteVerification/SearchStrategies/NonStrictDFS.hpp (+0/-2)
src/DiscreteVerification/SearchStrategies/NonStrictDFSHeuristic.hpp (+0/-2)
src/DiscreteVerification/SearchStrategies/NonStrictDFSRandom.hpp (+0/-2)
src/DiscreteVerification/SearchStrategies/NonStrictHeuristic.hpp (+0/-2)
src/DiscreteVerification/SearchStrategies/NonStrictRandom.hpp (+0/-2)
src/DiscreteVerification/SearchStrategies/SearchFactory.h (+3/-2)
src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp (+14/-14)
src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp (+13/-13)
src/DiscreteVerification/SearchStrategies/WorkflowMinFirst.hpp (+0/-2)
src/DiscreteVerification/SuccessorGenerator.hpp (+0/-463)
src/DiscreteVerification/TimeDartSuccessorGenerator.cpp (+0/-232)
src/DiscreteVerification/TimeDartSuccessorGenerator.hpp (+0/-63)
src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp (+40/-14)
src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp (+9/-8)
src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp (+3/-4)
src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp (+0/-120)
src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp (+105/-12)
src/DiscreteVerification/VerificationTypes/SafetySynthesis.cpp (+310/-0)
src/DiscreteVerification/VerificationTypes/SafetySynthesis.h (+86/-0)
src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp (+6/-6)
src/DiscreteVerification/VerificationTypes/TimeDartLiveness.hpp (+2/-2)
src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp (+7/-8)
src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.hpp (+4/-4)
src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp (+27/-5)
src/DiscreteVerification/VerificationTypes/TimeDartVerification.hpp (+7/-5)
src/DiscreteVerification/VerificationTypes/Verification.hpp (+2/-2)
src/DiscreteVerification/VerificationTypes/Workflow.hpp (+4/-4)
src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp (+5/-5)
src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp (+2/-4)
src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp (+5/-5)
src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp (+2/-3)
src/main.cpp (+13/-1)
Related source package recipes
Branch information
Recent revisions
- 374. By Peter Gjøl Jensen
-
reduced size of stubborn set by not including zt transitions when *some* zt element is already in the stubborn set
Branch metadata
- Branch format:
- Branch format 7
- Repository format:
- Bazaar repository format 2a (needs bzr 1.16 or later)
- Stacked on:
- lp:verifydtapn
