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