CTL checker

[mondokm]

• Symbolic CTL model checking over the MDD backend via MddCtlChecker (EX, EU, EG, plus derived CTL ops).
• Constrained-saturation support for EU through AndNextStateDescriptor, this means we have two different algorithms for EU
• New common/ctl module with ANTLR grammar + parser

[github-actions]

Release Preview

Version: 7.1.0
Tag: v7.1.0

Release Notes:

Modified subprojects (since v7.0.3):
cfa/cfa-cli
common/analysis
common/ctl
sts/sts-cli
xcfa/xcfa-cli
xsts/xsts-analysis
xsts/xsts-cli

Files to be uploaded:

upload/EmergenTheta-svcomp.zip
upload/Theta-cfa.zip
upload/Theta-chccomp.zip
upload/Theta-sts.zip
upload/Theta-svcomp.zip
upload/Theta-xsts.zip
upload/Theta-xta.zip
upload/Thorn-svcomp.zip
upload/theta-cfa-cli.jar
upload/theta-solver-smtlib-cli.jar
upload/theta-sts-cli.jar
upload/theta-xcfa-cli.jar
upload/theta-xsts-cli.jar
upload/theta-xta-cli.jar

[github-actions]

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition	Correct	Incorrect	All	Status
CHC-COMP_Portfolio	147	0	195	✅
Hardware_CEGAR	47	0	54	✅
PLC_CEGAR	9	0	9	✅
PetriNet_MDD	60	0	122	✅
PetriNet_PN_MDD	70	0	122	✅
SV-COMP_Portfolio_Emergent	46	0	46	✅
SV-COMP_Portfolio_Horn	44	0	46	✅
SV-COMP_Portfolio_Stable	46	0	46	✅
Statechart_CEGAR	110	0	126	✅