lp:~tapaal-ltl/verifypn/reach-stub-new

Branch merges

Propose for merging

No branches dependent on this one.

Merged into lp:verifypn at revision 252

Jiri Srba: Approve on 2021-10-17

Diff: 6145 lines (+1333/-1200)

29 files modified

CMakeLists.txt (+1/-1)
include/LTL/Algorithm/ModelChecker.h (+37/-33)
include/LTL/Algorithm/NestedDepthFirstSearch.h (+29/-34)
include/LTL/Algorithm/TarjanModelChecker.h (+32/-34)
include/LTL/LTLMain.h (+5/-4)
include/LTL/Structures/BitProductStateSet.h (+4/-4)
include/LTL/Structures/ProductState.h (+9/-1)
include/LTL/Structures/ProductStateFactory.h (+4/-3)
include/LTL/Stubborn/SafeAutStubbornSet.h (+22/-5)
include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h (+1/-1)
include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h (+8/-6)
include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h (+27/-9)
include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h (+74/-81)
include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h (+27/-16)
include/PetriEngine/Reducer.h (+21/-21)
include/PetriEngine/Structures/StateSet.h (+5/-33)
include/PetriEngine/Structures/light_deque.h (+83/-24)
include/PetriEngine/SuccessorGenerator.h (+4/-4)
src/LTL/Algorithm/NestedDepthFirstSearch.cpp (+124/-124)
src/LTL/Algorithm/TarjanModelChecker.cpp (+107/-86)
src/LTL/LTLMain.cpp (+29/-63)
src/LTL/Stubborn/AutomatonStubbornSet.cpp (+1/-1)
src/LTL/Stubborn/SafeAutStubbornSet.cpp (+57/-9)
src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp (+2/-2)
src/PetriEngine/PQL/Expressions.cpp (+403/-414)
src/PetriEngine/Reducer.cpp (+160/-157)
src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp (+23/-1)
src/PetriEngine/TraceReplay.cpp (+4/-4)
src/VerifyPN.cpp (+30/-25)

api

Related source package recipes

No recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related bugs

Related blueprints

284. By <email address hidden> on 2021-10-17

increased version number to 4.2.0

283. By Nikolaj Jensen Ulrik on 2021-10-16

extraConsume in the right place

282. By Peter G. Jensen <email address hidden> on 2021-10-15

avoiding double-addition of extra-consume during ruleB trace reconstruction

281. By Nikolaj Jensen Ulrik on 2021-10-15

Fixing infinite loop in Tarjan trace generation

280. By Nikolaj Jensen Ulrik on 2021-10-14

LTL Query simplification more robust against queries without leading A/E quantifier.

279. By Nikolaj Jensen Ulrik on 2021-10-14

Probably properly fixed k-bounds in NDFS. Fixes https://bugs.launchpad.net/tapaal/+bug/1947036

278. By Peter G. Jensen <email address hidden> on 2021-10-03

fixing memleak by light_dequeue

277. By Peter G. Jensen <email address hidden> on 2021-10-03

fixing NDFS bug

276. By Peter G. Jensen <email address hidden> on 2021-10-03

no funky rewrite of path-quantifier-less ltl formulae

275. By Peter G. Jensen <email address hidden> on 2021-10-03

should fix TARJAN traces