This a bit of a weird corner-case. Consider P>0[ s=0 ] or P=?[ s=0 ].
Those are not PCTL-formula (the P-operator requires a temporal
operator) and they are not particularly useful, as we just need to
evaluate the state formula and the threshold (or turn the satisfaction
set into a quantitative result).
They can be dealt with by the LTL machinery (DA-construction, product,
...), but this is quite expensive (and not implemented yet for all
engines). So, we just deal with it by special treatment.
Conflicts:
src/storm/modelchecker/AbstractModelChecker.cpp
src/storm/modelchecker/AbstractModelChecker.h
It looks like you may be committing a cherry-pick.
If this is not correct, please run
git update-ref -d CHERRY_PICK_HEAD
and try again.
Requires a script ltl2da on the PATH that takes two arguments, first
an LTL formula in prefix format, second the DA automaton output
filename. E.g., it could be called via
ltl2da "& p1 F G p0" out.hoa
and should produce a complete deterministic automaton (with arbitrary
acceptance) for the LTL formula 'p1 & F (G p0)' and write it to the
out.hoa file.
Optionally, you can set the LTL2DA environment variable to provide
the path to the script, e.g., invoking storm via
LTL2DA=../ltl2da-script bin/storm ...
For PRCTL*-model checking, we need to extract the maximal state
subformulas in a path formula and substitute those with new
labels, e.g., for
(F P>0.5[...]) & G (s=0 & d=1)
we would get
(F a_1) & G a_2
as the resulting formula, with
a_1 => P>0.5[...]
a_2 => s=0 & d=1
This then allows the recursive computation of the satisfaction sets of
the maximal state subformulas and using those in the computation for
the (simplified) path formula.
We want to differentiate between a simple path formula (single G, F,
U, X, with negation over state formulas) and complex path formulas
(nested temporal operators, conjunction/disjunction, etc).
Adapt FormulaInformation and FormulaInformationVisitor accordingly.
Additionally, we tweak the FormulaInformationVisitor so that we can
optionally prohibit recursing into operator subformulas (e.g.,
P>0[...]). For PRCTL*, such subformulas are treated just as state
subformulas, and we would like to have the ability to get
FormulaInformation just for the structure of the "surface-level"
formula, without looking into the probability, long-run, reward,
... sub-formulas.
refactor FormulaInformationVisitor to support stopping recursion into nested operators and for detecting complex path formulas
Conflicts:
src/storm/logic/Formula.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
Note: syntax of the HOA path formula will change!
We have added checks for boundedGloballyFormulae hence the conflicts
Conflicts:
src/storm/logic/CloneVisitor.cpp
src/storm/logic/Formula.cpp
src/storm/logic/Formula.h
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
src/storm/storage/jani/JSONExporter.cpp
For model-automaton product constructions, we would like to add
automatically generated labels to the result, so we need a way to
ensure that we can get those without clashing with existing labels.
Joachim Klein
Stefan Pranger
Lukas Posch
Tim Quatmann