← Back to branch summary

~tapaal-ltl/verifypn/answer-for-gui

~tapaal-ltl/verifypn/answer-for-gui

« back to all changes in this revision

Viewing changes to include/PetriEngine/TAR/Solver.h

Committer: srba.jiri at gmail
Date: 2021-04-02 18:13:50 UTC
mfrom: (230.1.28 mcc2021)
Revision ID: srba.jiri@gmail.com-20210402181350-k71xtjut3r48l1o5

merged in lp:~tapaal-ltl/verifypn/mcc2021 adding LTL, colored fixed-point unfolding for CPN and other performance improvements

files added:
include/LTL

include/LTL/Algorithm

include/LTL/Algorithm/ModelChecker.h

include/LTL/Algorithm/NestedDepthFirstSearch.h

include/LTL/Algorithm/ProductPrinter.h

include/LTL/Algorithm/RandomNDFS.h

include/LTL/Algorithm/TarjanModelChecker.h

include/LTL/AlgorithmTypes.h

include/LTL/BuchiSuccessorGenerator.h

include/LTL/LTL.h

include/LTL/LTLToBuchi.h

include/LTL/LTLValidator.h

include/LTL/ProductSuccessorGenerator.h

include/LTL/Simplification

include/LTL/Simplification/SpotToPQL.h

include/LTL/Structures

include/LTL/Structures/BuchiAutomaton.h

include/LTL/Structures/ProductState.h

include/LTL/Structures/ProductStateFactory.h

include/PetriEngine/Colored/ArcIntervals.h

include/PetriEngine/Colored/BindingGenerator.h

include/PetriEngine/Colored/GuardRestrictor.h

include/PetriEngine/Colored/IntervalGenerator.h

include/PetriEngine/Colored/Intervals.h

include/PetriEngine/PQL/CTLVisitor.h

include/PetriEngine/PQL/QueryPrinter.h

include/PetriEngine/Stubborn

include/PetriEngine/Stubborn/InterestingTransitionVisitor.h

include/PetriEngine/Stubborn/ReachabilityStubbornSet.h

include/PetriEngine/Stubborn/StubbornSet.h

src/LTL

src/LTL/Algorithm

src/LTL/Algorithm/CMakeLists.txt

src/LTL/Algorithm/LTLToBuchi.cpp

src/LTL/Algorithm/ModelChecker.cpp

src/LTL/Algorithm/NestedDepthFirstSearch.cpp

src/LTL/Algorithm/ProductPrinter.cpp

src/LTL/Algorithm/ProductSuccessorGenerator.cpp

src/LTL/Algorithm/RandomNDFS.cpp

src/LTL/Algorithm/TarjanModelChecker.cpp

src/LTL/CMakeLists.txt

src/LTL/Simplification

src/LTL/Simplification/CMakeLists.txt

src/LTL/Simplification/SpotToPQL.cpp

src/LTL/_LTL.cpp

src/PetriEngine/Colored/BindingGenerator.cpp

src/PetriEngine/Colored/GuardRestrictor.cpp

src/PetriEngine/PQL/CTLVisitor.cpp

src/PetriEngine/PQL/QueryPrinter.cpp

src/PetriEngine/Stubborn

src/PetriEngine/Stubborn/CMakeLists.txt

src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp

src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp

src/PetriEngine/Stubborn/StubbornSet.cpp

test_models/LTL

test_models/LTL/Bounded

test_models/LTL/Bounded/model.pnml

test_models/LTL/Bounded/query.xml

test_models/LTL/generator.pnml

test_models/LTL/generator.xml

files modified:
CMakeLists.txt

Scripts/MCC20/competition-scripts/tapaal.sh *

include/CTL/Algorithm/CertainZeroFPA.h

include/CTL/DependencyGraph/Configuration.h

include/CTL/DependencyGraph/Edge.h

include/CTL/PetriNets/PetriConfig.h

include/PetriEngine/Colored/ColoredNetStructures.h

include/PetriEngine/Colored/ColoredPetriNetBuilder.h

include/PetriEngine/Colored/Colors.h

include/PetriEngine/Colored/Expressions.h

include/PetriEngine/PQL/Contexts.h

include/PetriEngine/PQL/Expressions.h

include/PetriEngine/PQL/PQL.h

include/PetriEngine/PQL/Visitor.h

include/PetriEngine/PetriNet.h

include/PetriEngine/Reachability/ReachabilityResult.h

include/PetriEngine/Reachability/ReachabilitySearch.h

include/PetriEngine/Reducer.h

include/PetriEngine/ReducingSuccessorGenerator.h

include/PetriEngine/Simplification/Member.h

include/PetriEngine/Structures/Queue.h

include/PetriEngine/Structures/State.h

include/PetriEngine/Structures/StateSet.h

include/PetriEngine/Structures/binarywrapper.h

include/PetriEngine/Structures/light_deque.h

include/PetriEngine/SuccessorGenerator.h

include/PetriEngine/TAR/ContainsVisitor.h

include/PetriEngine/TAR/PlaceUseVisitor.h

include/PetriEngine/TAR/RangeContext.h

include/PetriEngine/TAR/RangeEvalContext.h

include/PetriEngine/TAR/Solver.h

include/PetriEngine/TAR/range.h

include/PetriEngine/options.h

include/PetriParse/PNMLParser.h

include/PetriParse/QueryParser.h

include/PetriParse/QueryXMLParser.h

src/CMakeLists.txt

src/CTL/Algorithm/CertainZeroFPA.cpp

src/CTL/Algorithm/LocalFPA.cpp

src/CTL/DependencyGraph/Configuration.cpp

src/CTL/PetriNets/OnTheFlyDG.cpp

src/CTL/SearchStrategy/HeuristicSearch.cpp

src/PetriEngine/CMakeLists.txt

src/PetriEngine/Colored/CMakeLists.txt

src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp

src/PetriEngine/Colored/Colors.cpp

src/PetriEngine/Colored/Multiset.cpp

src/PetriEngine/PQL/CMakeLists.txt

src/PetriEngine/PQL/Expressions.cpp

src/PetriEngine/PQL/PQL.cpp

src/PetriEngine/PQL/PQLQueryParser.y

src/PetriEngine/PetriNet.cpp

src/PetriEngine/PetriNetBuilder.cpp

src/PetriEngine/Reachability/ResultPrinter.cpp

src/PetriEngine/Reducer.cpp

src/PetriEngine/ReducingSuccessorGenerator.cpp

src/PetriEngine/Structures/AlignedEncoder.cpp

src/PetriEngine/Structures/Queue.cpp

src/PetriEngine/SuccessorGenerator.cpp

src/PetriEngine/TAR/PlaceUseVisitor.cpp

src/PetriEngine/TAR/RangeContext.cpp

src/PetriEngine/TAR/RangeEvalContext.cpp

src/PetriEngine/TAR/Solver.cpp

src/PetriParse/PNMLParser.cpp

src/PetriParse/QueryBinaryParser.cpp

src/PetriParse/QueryXMLParser.cpp

src/VerifyPN.cpp

Show diffs side-by-side

added added

removed removed

include/PetriEngine/TAR/Solver.h

16

16

#include "range.h"

17

17

#include "PetriEngine/PQL/PQL.h"

18

18

#include "TraceSet.h"

19

#include "PetriEngine/SuccessorGenerator.h"

19

20

20

21

#include <utility>

21

22

#include <cinttypes>

Older »