93d9b586ed
compute 1-Pmax[in order to compute Pmin for MDPs
5 years ago
fc0ae2ea4b
removed SolveGoal in function computeLTLproabilities of SparseLTLHelper
5 years ago
1fe30f7d78
Convert acceptance formula into disjunctive normal form
5 years ago
ffe70ea056
removed model from SparseLTLHelper
5 years ago
f8d9773131
test update
5 years ago
b30713c23d
Started to restructure LTL model checking algorithms
Conflicts:
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
5 years ago
4fc3c79221
LTL tests for MDPs
5 years ago
0f5c4708ca
corrected exception
5 years ago
884b284ab5
corrected exception
5 years ago
466339059f
Call parse_prefix_ltl instead of parse_formula
5 years ago
c290e16260
Simplified LTL2DeterministicAutomaton
5 years ago
d861c377a9
fixed typo
5 years ago
6110d33bcc
Removed debug output
5 years ago
d44bc3c6c2
CMAKE: Added option to include and link against Spot
Conflicts:
CMakeLists.txt
5 years ago
d5edde05a7
Adapted ModelChecker test-cases and FormulaParser test-cases
5 years ago
1c16c17a57
FragmentCheckerTest: Fixed a few more testcaes that now correspond to invalid formulae.
5 years ago
b71cb813df
FormulaParser: Fixed parsing of multi-bounded path operator and quantile operator
5 years ago
8c669b9e8b
Fixed a FragmentCheckerTest case which considered a formula that is now considered invalid.
5 years ago
aa29ad1196
flagging multi-objective and quantile formulae as StateFormulae (fixing the previous commit)
Conflicts:
src/storm/modelchecker/AbstractModelChecker.cpp
5 years ago
cc9a4b8cb3
Adapting a parser test-case to the new parser
5 years ago
76c689a001
flagging multi-objective formulae as State formulae
5 years ago
4cf2fd7d61
Heavily refactored FormulaParser as it had become quite messy.
LTL-Operator precedence should now correctly mimic the behavior of PRISM.
5 years ago
132c293105
TYPED_TESTS for LTL modelchecker
5 years ago
7d74efd591
TYPED_TESTS for LTL modelchecker
5 years ago
10e2d85cc4
Formulas: Added parentheses to formula output to avoid ambiguity
5 years ago
bcf45f68df
modelchecker test update
5 years ago
affee2bc5b
ltl dtmc modelchecker tests
5 years ago
02b77707d4
ltl dtmc modelchecker tests
5 years ago
b6800361ce
ltl formula parser tests
5 years ago
4fe4704f60
Silenced a couple of warnings triggered by cpphoafparser.
5 years ago
9ce6076689
Silenced a warning
5 years ago
3a769b3149
ToPrefixStringVisitor: Added missing case for GameFormula
5 years ago
819d97b712
(CTMC-LTL) FragmentSpecification: cslstar and csrlstar
Conflicts:
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
5 years ago
04a8bec83f
(MDP-LTL) SparseMdpPrctlModelChecker: handle LTL
Conflicts:
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
5 years ago
615b2b5399
(MDP-LTL) SparseMdpPrctlHelper: computeSurelyAcceptingPmaxStates
5 years ago
4c70f1a160
(MDP-LTL) ProductBuilder: DA product with MDP
5 years ago
c099183063
(MDP-LTL) MaximalEndComponent: containsAnyState
Conflicts:
src/storm/storage/MaximalEndComponent.cpp
5 years ago
5855a82e80
(MDP-LTL) CheckTask: negate()
Allow a CheckTask to be negated (e.g., useful for converting from Pmin to 1-Pmax).
5 years ago
b6b31f20af
(MDP-LTL) AcceptanceCondition: extractFromDNF
Convert a generic acceptance condition to DNF.
5 years ago
cf6af6c456
(stateformula) Modelcheckers: support P[phi], Pmax/min[phi] where phi is a state formula
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.
5 years ago
af10aa8b4b
(stateformula) StateFormula: a StateFormula is a probabilistic path formula
5 years ago
a639836f6f
(stateformula) CheckResults: provide constructor for quantitative from qualitative result
5 years ago
27ca10a668
(stateformula) SymbolicQualitativeCheckResult: add getReachableStates() and getStates() accessors, like SymbolicQuantitativeCheckResult
5 years ago
1243b9300c
(LTL) SparseDtmcModelChecker: Implement LTL model checking
Conflicts:
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
5 years ago
ab32af463b
(LTL) AbstractModelChecker: detect need for LTL PMC, call (unimplemented) computeLTLProbabilities
Conflicts:
src/storm/modelchecker/AbstractModelChecker.cpp
src/storm/modelchecker/AbstractModelChecker.h
5 years ago
5427702376
WIP:needed? Boolean path formulas: allow storing context
5 years ago
fbe5236c4d
(LTL) FragmentSpecification: add pctlstar() and prctlstar() fragments
We add the star variants (allow complex path formulas).
Conflicts:
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
5 years ago
6404c526e2
WIP (LTL) LTL2DeterministicAutomaton (first hacky attempt)
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 ...
5 years ago
393dd2af87
(LTL) ExtractMaximalStateFormulasVisitor
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.
5 years ago
b04d2723c2
(LTL) Add Formula::toPrefixString()
Convert a formula into prefix format (LBTT/ltl2dstar-style LTL syntax).
Conflicts:
src/storm/logic/Formula.h
5 years ago
hannah
Tim Quatmann
Joachim Klein