← Back to branch summary

~verifydtapn-contributers/verifydtapn/trunk

~verifydtapn-contributers/verifydtapn/trunk

Viewing all changes in revision 337.

Committer: Jiri Srba
Date: 2018-01-13 20:41:28 UTC
mfrom: (334.3.44 new-succs)
Revision ID: srba@cs.aau.dk-20180113204128-rqtixr1vlhk75z20

merged in branch lp:~verifydtapn-contributers/verifydtapn/partial-order
Adds zero-time partial order reduction to the engine.
Adds support for timed-safety-games to the engine.
Also refactores all around for improved performance.
New successor-generator, used by all engines.

files added:
src/DiscreteVerification/DataStructures/MarkingStore.h

src/DiscreteVerification/DataStructures/MetaData.h

src/DiscreteVerification/DataStructures/PTrieMarkingStore.h

src/DiscreteVerification/DataStructures/SimpleMarkingStore.h

src/DiscreteVerification/DataStructures/Waiting.h

src/DiscreteVerification/DataStructures/light_deque.h

src/DiscreteVerification/Generator.cpp

src/DiscreteVerification/Generator.h

src/DiscreteVerification/ReducingGenerator.cpp

src/DiscreteVerification/ReducingGenerator.hpp

src/DiscreteVerification/VerificationTypes/SafetySynthesis.cpp

src/DiscreteVerification/VerificationTypes/SafetySynthesis.h

files removed:
src/DiscreteVerification/SuccessorGenerator.hpp

src/DiscreteVerification/TimeDartSuccessorGenerator.cpp

src/DiscreteVerification/TimeDartSuccessorGenerator.hpp

src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp

files modified:
makefile.linux64

src/Core/ArgsParser.cpp

src/Core/ArgsParser.hpp

src/Core/QueryParser/AST.cpp

src/Core/QueryParser/AST.hpp

src/Core/QueryParser/Generated/lexer.cpp

src/Core/QueryParser/Generated/location.hh

src/Core/QueryParser/Generated/parser.cpp

src/Core/QueryParser/Generated/parser.hpp

src/Core/QueryParser/Generated/position.hh

src/Core/QueryParser/Generated/stack.hh

src/Core/QueryParser/NormalizationVisitor.cpp

src/Core/QueryParser/NormalizationVisitor.hpp

src/Core/QueryParser/Visitor.hpp

src/Core/QueryParser/flex.ll

src/Core/QueryParser/grammar.yy

src/Core/TAPN/TimeInterval.cpp

src/Core/TAPN/TimeInterval.hpp

src/Core/TAPN/TimeInvariant.cpp

src/Core/TAPN/TimeInvariant.hpp

src/Core/TAPN/TimedArcPetriNet.cpp

src/Core/TAPN/TimedArcPetriNet.hpp

src/Core/TAPN/TimedPlace.hpp

src/Core/TAPN/TimedTransition.cpp

src/Core/TAPN/TimedTransition.hpp

src/Core/TAPNParser/TAPNXmlParser.cpp

src/Core/TAPNParser/TAPNXmlParser.hpp

src/Core/VerificationOptions.cpp

src/Core/VerificationOptions.hpp

src/DiscreteVerification/DataStructures/MarkingEncoder.h

src/DiscreteVerification/DataStructures/NonStrictMarking.hpp

src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp

src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp

src/DiscreteVerification/DataStructures/PWList.hpp

src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp *

src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp *

src/DiscreteVerification/DataStructures/TimeDartPWList.cpp *

src/DiscreteVerification/DataStructures/TimeDartPWList.hpp *

src/DiscreteVerification/DataStructures/WaitingList.hpp *

src/DiscreteVerification/DataStructures/binarywrapper.h

src/DiscreteVerification/DataStructures/ptrie.h

src/DiscreteVerification/DeadlockVisitor.cpp

src/DiscreteVerification/DeadlockVisitor.hpp

src/DiscreteVerification/DiscreteVerification.cpp

src/DiscreteVerification/PlaceVisitor.cpp

src/DiscreteVerification/PlaceVisitor.hpp

src/DiscreteVerification/QueryVisitor.hpp

src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp

src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp

src/DiscreteVerification/SearchStrategies/NonStrictBFS.hpp

src/DiscreteVerification/SearchStrategies/NonStrictDFS.hpp

src/DiscreteVerification/SearchStrategies/NonStrictDFSHeuristic.hpp

src/DiscreteVerification/SearchStrategies/NonStrictDFSRandom.hpp

src/DiscreteVerification/SearchStrategies/NonStrictHeuristic.hpp

src/DiscreteVerification/SearchStrategies/NonStrictRandom.hpp

src/DiscreteVerification/SearchStrategies/SearchFactory.h

src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp

src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp

src/DiscreteVerification/SearchStrategies/WorkflowMinFirst.hpp

src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp

src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp

src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp

src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp

src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp

src/DiscreteVerification/VerificationTypes/TimeDartLiveness.hpp

src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp

src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.hpp

src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp

src/DiscreteVerification/VerificationTypes/TimeDartVerification.hpp

src/DiscreteVerification/VerificationTypes/Verification.hpp

src/DiscreteVerification/VerificationTypes/Workflow.hpp

src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp

src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp

src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp

src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp

src/main.cpp

Show diffs side-by-side

added added

removed removed

makefile.linux64

src/Core/ArgsParser.cpp

src/Core/ArgsParser.hpp

src/Core/QueryParser/AST.cpp

src/Core/QueryParser/AST.hpp

src/Core/QueryParser/Generated/lexer.cpp

src/Core/QueryParser/Generated/location.hh

src/Core/QueryParser/Generated/parser.cpp

src/Core/QueryParser/Generated/parser.hpp

src/Core/QueryParser/Generated/position.hh

src/Core/QueryParser/Generated/stack.hh

src/Core/QueryParser/NormalizationVisitor.cpp

src/Core/QueryParser/NormalizationVisitor.hpp

src/Core/QueryParser/Visitor.hpp

src/Core/QueryParser/flex.ll

src/Core/QueryParser/grammar.yy

src/Core/TAPN/TimeInterval.cpp

src/Core/TAPN/TimeInterval.hpp

src/Core/TAPN/TimeInvariant.cpp

src/Core/TAPN/TimeInvariant.hpp

src/Core/TAPN/TimedArcPetriNet.cpp

src/Core/TAPN/TimedArcPetriNet.hpp

src/Core/TAPN/TimedPlace.hpp

src/Core/TAPN/TimedTransition.cpp

src/Core/TAPN/TimedTransition.hpp

src/Core/TAPNParser/TAPNXmlParser.cpp

src/Core/TAPNParser/TAPNXmlParser.hpp

src/Core/VerificationOptions.cpp

src/Core/VerificationOptions.hpp

src/DiscreteVerification/DataStructures/MarkingEncoder.h

src/DiscreteVerification/DataStructures/MarkingStore.h

src/DiscreteVerification/DataStructures/MetaData.h

src/DiscreteVerification/DataStructures/NonStrictMarking.hpp

src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp

src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp

src/DiscreteVerification/DataStructures/PTrieMarkingStore.h

src/DiscreteVerification/DataStructures/PWList.hpp

src/DiscreteVerification/DataStructures/SimpleMarkingStore.h

src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp

src/DiscreteVerification/DataStructures/TimeDartPWList.hpp

src/DiscreteVerification/DataStructures/Waiting.h

src/DiscreteVerification/DataStructures/binarywrapper.h

src/DiscreteVerification/DataStructures/light_deque.h

src/DiscreteVerification/DataStructures/ptrie.h

src/DiscreteVerification/DeadlockVisitor.cpp

src/DiscreteVerification/DeadlockVisitor.hpp

src/DiscreteVerification/DiscreteVerification.cpp

src/DiscreteVerification/Generator.cpp

src/DiscreteVerification/Generator.h

src/DiscreteVerification/PlaceVisitor.cpp

src/DiscreteVerification/PlaceVisitor.hpp

src/DiscreteVerification/QueryVisitor.hpp

src/DiscreteVerification/ReducingGenerator.cpp

src/DiscreteVerification/ReducingGenerator.hpp

src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp

src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp

src/DiscreteVerification/SearchStrategies/NonStrictBFS.hpp

src/DiscreteVerification/SearchStrategies/NonStrictDFS.hpp

src/DiscreteVerification/SearchStrategies/NonStrictDFSHeuristic.hpp

src/DiscreteVerification/SearchStrategies/NonStrictDFSRandom.hpp

src/DiscreteVerification/SearchStrategies/NonStrictHeuristic.hpp

src/DiscreteVerification/SearchStrategies/NonStrictRandom.hpp

src/DiscreteVerification/SearchStrategies/SearchFactory.h

src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp

src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp

src/DiscreteVerification/SearchStrategies/WorkflowMinFirst.hpp

src/DiscreteVerification/SuccessorGenerator.hpp

src/DiscreteVerification/TimeDartSuccessorGenerator.cpp

src/DiscreteVerification/TimeDartSuccessorGenerator.hpp

src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp

src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp

src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp

src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp

src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp

src/DiscreteVerification/VerificationTypes/SafetySynthesis.cpp

src/DiscreteVerification/VerificationTypes/SafetySynthesis.h

src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp

src/DiscreteVerification/VerificationTypes/TimeDartLiveness.hpp

src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp

src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.hpp

src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp

src/DiscreteVerification/VerificationTypes/TimeDartVerification.hpp

src/DiscreteVerification/VerificationTypes/Verification.hpp

src/DiscreteVerification/VerificationTypes/Workflow.hpp

src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp

src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp

src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp

src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp

Older »