- Introduced OptimalPre and OptimalPost shields
- Renamed *Safety to PreShield and PostShield
- Introduced min case for shields
- fixed coalition states in shield handling
LTL Model Checking
Also includes a reset of
src/storm-parsers/parser/FormulaParserGrammar.cpp
src/storm-parsers/parser/FormulaParserGrammar.h
since there have been to many changes to fix them individually. Will
follow up with a commit to introduce shield and smg formula parsing
Conflicts:
src/storm-parsers/parser/FormulaParserGrammar.cpp
src/storm-parsers/parser/FormulaParserGrammar.h
src/storm/logic/CloneVisitor.cpp
src/storm/logic/Formula.h
src/storm/logic/FragmentChecker.cpp
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
src/storm/logic/ToPrefixStringVisitor.cpp
src/storm/logic/ToPrefixStringVisitor.h
src/storm/modelchecker/AbstractModelChecker.cpp
src/storm/modelchecker/AbstractModelChecker.h
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
src/storm/storage/MaximalEndComponent.cpp
src/storm/storage/Scheduler.cpp
src/storm/storage/Scheduler.h
src/storm/storage/jani/JSONExporter.cpp
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
Previously, the formula parser only supported AND, OR and NOT over state formulas.
For LTL, we need those over path formulas.
We tweak the grammar, the AST types and visitors, to also handle
UnaryBooleanPathFormula and BinaryBooleanPathformula. During parsing,
we determine on-demand whether to generate the path or state formula
variant by looking at the subformulas - if they are state formulas,
the boolean operator will be a state formula as well.
Conflicts:
src/storm-parsers/parser/FormulaParserGrammar.cpp
src/storm-parsers/parser/FormulaParserGrammar.h
src/storm/logic/CloneVisitor.cpp
src/storm/logic/Formula.cpp
src/storm/logic/Formula.h
src/storm/logic/FragmentChecker.cpp
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
src/storm/storage/jani/JSONExporter.cpp
Note: Syntax of HOA path formulas will change!
Conflicts:
src/storm-parsers/parser/FormulaParserGrammar.cpp
src/storm-parsers/parser/FormulaParserGrammar.h
Note: Syntax of HOA path formulas will change!
Conflicts:
src/storm-parsers/parser/FormulaParserGrammar.cpp
src/storm-parsers/parser/FormulaParserGrammar.h
* PrismProgram::CheckValidity and PrismProgram::simplify now treat SMGs properly
* PrismProgram is now responsible for moduleIndex->playerIndex and actionIndex->playerIndex assignment
* More defined behavior for actions that don't have a player (work in progress)
* Fixed issues related to module renaming that resulted from setting the module indices already in the first run
* Fixed a few uint_fast32_t vs uint_fast64_t issues, created alias PlayerIndex
Stefan Pranger
Tim Quatmann
Joachim Klein
Lukas Posch
Sebastian Junges
Matthias Volk