← Back to branch summary

~tapaal-ltl/verifypn/resuming-stubborn-tarjan

~tapaal-ltl/verifypn/resuming-stubborn-tarjan

Viewing all changes in revision 259.

Committer: Nikolaj Jensen Ulrik
Date: 2021-03-05 09:02:55 UTC
Revision ID: nikolaj@njulrik.dk-20210305090255-2h34frq1618r1m28

alternate resuming tarjan model checker now correct(er)

files modified:
include/LTL/Algorithm/ResumingStubbornTarjan.h

include/LTL/Algorithm/TarjanModelChecker.h

include/LTL/ProductSuccessorGenerator.h

include/LTL/Structures/BitProductStateSet.h

include/LTL/Stubborn/LTLStubbornSet.h

include/PetriEngine/ReducingSuccessorGenerator.h

include/PetriEngine/Stubborn/ReachabilityStubbornSet.h

include/PetriEngine/Stubborn/StubbornSet.h

include/PetriEngine/SuccessorGenerator.h

src/LTL/Algorithm/LTLToBuchi.cpp

src/LTL/Algorithm/ResumingStubbornTarjan.cpp

src/LTL/Algorithm/TarjanModelChecker.cpp

src/LTL/LTLMain.cpp

src/LTL/Stubborn/LTLStubbornSet.cpp

src/PetriEngine/ReducingSuccessorGenerator.cpp

src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp

src/PetriEngine/SuccessorGenerator.cpp

Show diffs side-by-side

added added

removed removed

include/LTL/Algorithm/ResumingStubbornTarjan.h

include/LTL/Algorithm/TarjanModelChecker.h

include/LTL/ProductSuccessorGenerator.h

include/LTL/Structures/BitProductStateSet.h

include/LTL/Stubborn/LTLStubbornSet.h

include/PetriEngine/ReducingSuccessorGenerator.h

include/PetriEngine/Stubborn/ReachabilityStubbornSet.h

include/PetriEngine/Stubborn/StubbornSet.h

include/PetriEngine/SuccessorGenerator.h

src/LTL/Algorithm/LTLToBuchi.cpp

src/LTL/Algorithm/ResumingStubbornTarjan.cpp

src/LTL/Algorithm/TarjanModelChecker.cpp

src/LTL/LTLMain.cpp

src/LTL/Stubborn/LTLStubbornSet.cpp

src/PetriEngine/ReducingSuccessorGenerator.cpp

src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp

src/PetriEngine/SuccessorGenerator.cpp

Older »