8ba4f17a92
ltl-mc with MAs
4 years ago
78058b5152
ltl-mc with ctmcs
Conflicts:
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
4 years ago
7f95f1fdbf
ctmc and mdp tests
4 years ago
a038d9658e
added TODOs
4 years ago
b06151b913
ctmc-ltl tests
4 years ago
3f030e23f0
allow external ltl2da tools
4 years ago
ca4ac3a166
transform into generalized Rabin instead of DNF
4 years ago
e838ac13de
updated ltl tests
4 years ago
667d4a0e06
documentation and renaming of some methods
Conflicts:
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
4 years ago
139ac3d0dc
flag to indicate whether condition should be in dnf
4 years ago
93d9b586ed
compute 1-Pmax[in order to compute Pmin for MDPs
4 years ago
fc0ae2ea4b
removed SolveGoal in function computeLTLproabilities of SparseLTLHelper
4 years ago
1fe30f7d78
Convert acceptance formula into disjunctive normal form
4 years ago
ffe70ea056
removed model from SparseLTLHelper
4 years ago
f8d9773131
test update
4 years ago
b30713c23d
Started to restructure LTL model checking algorithms
Conflicts:
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
4 years ago
4fc3c79221
LTL tests for MDPs
4 years ago
0f5c4708ca
corrected exception
4 years ago
884b284ab5
corrected exception
4 years ago
466339059f
Call parse_prefix_ltl instead of parse_formula
4 years ago
c290e16260
Simplified LTL2DeterministicAutomaton
4 years ago
d861c377a9
fixed typo
4 years ago
6110d33bcc
Removed debug output
4 years ago
d44bc3c6c2
CMAKE: Added option to include and link against Spot
Conflicts:
CMakeLists.txt
4 years ago
d5edde05a7
Adapted ModelChecker test-cases and FormulaParser test-cases
4 years ago
1c16c17a57
FragmentCheckerTest: Fixed a few more testcaes that now correspond to invalid formulae.
4 years ago
b71cb813df
FormulaParser: Fixed parsing of multi-bounded path operator and quantile operator
4 years ago
8c669b9e8b
Fixed a FragmentCheckerTest case which considered a formula that is now considered invalid.
4 years ago
aa29ad1196
flagging multi-objective and quantile formulae as StateFormulae (fixing the previous commit)
Conflicts:
src/storm/modelchecker/AbstractModelChecker.cpp
4 years ago
cc9a4b8cb3
Adapting a parser test-case to the new parser
4 years ago
76c689a001
flagging multi-objective formulae as State formulae
4 years ago
4cf2fd7d61
Heavily refactored FormulaParser as it had become quite messy.
LTL-Operator precedence should now correctly mimic the behavior of PRISM.
4 years ago
132c293105
TYPED_TESTS for LTL modelchecker
4 years ago
7d74efd591
TYPED_TESTS for LTL modelchecker
4 years ago
10e2d85cc4
Formulas: Added parentheses to formula output to avoid ambiguity
4 years ago
bcf45f68df
modelchecker test update
4 years ago
affee2bc5b
ltl dtmc modelchecker tests
4 years ago
02b77707d4
ltl dtmc modelchecker tests
4 years ago
b6800361ce
ltl formula parser tests
4 years ago
4fe4704f60
Silenced a couple of warnings triggered by cpphoafparser.
4 years ago
9ce6076689
Silenced a warning
4 years ago
3a769b3149
ToPrefixStringVisitor: Added missing case for GameFormula
4 years ago
819d97b712
(CTMC-LTL) FragmentSpecification: cslstar and csrlstar
Conflicts:
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
4 years ago
04a8bec83f
(MDP-LTL) SparseMdpPrctlModelChecker: handle LTL
Conflicts:
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
4 years ago
615b2b5399
(MDP-LTL) SparseMdpPrctlHelper: computeSurelyAcceptingPmaxStates
4 years ago
4c70f1a160
(MDP-LTL) ProductBuilder: DA product with MDP
4 years ago
c099183063
(MDP-LTL) MaximalEndComponent: containsAnyState
Conflicts:
src/storm/storage/MaximalEndComponent.cpp
4 years ago
5855a82e80
(MDP-LTL) CheckTask: negate()
Allow a CheckTask to be negated (e.g., useful for converting from Pmin to 1-Pmax).
4 years ago
b6b31f20af
(MDP-LTL) AcceptanceCondition: extractFromDNF
Convert a generic acceptance condition to DNF.
4 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.
4 years ago
hannah
Tim Quatmann
Joachim Klein