hannah
|
ca6b3b8ce2
|
missing include
|
3 years ago |
Tim Quatmann
|
4cdd70949c
|
FormulaParser: HOA formulas shall only consider state-subformulas
|
3 years ago |
|
hannah
|
bf3894d2f8
|
DA state output
|
3 years ago |
|
hannah
|
57734226e2
|
channged data structure for extracted formulas
|
3 years ago |
|
hannah
|
71f72d84b2
|
Ma ltl-MC and tests
|
3 years ago |
|
hannah
|
225169b2b3
|
added ltl2da option
|
3 years ago |
|
hannah
|
1d5860de8d
|
use same labels for equivalent maximal state formulas
|
3 years ago |
|
hannah
|
75ddf49f2b
|
compute SatSets via LTLHelper
|
3 years ago |
|
hannah
|
ecd4637df3
|
AP simplifications in LTL-Formula
|
3 years ago |
|
hannah
|
1332e39b8c
|
updated canHandle
Conflicts:
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
|
3 years ago |
|
hannah
|
b75c16297f
|
fixed some typos
|
3 years ago |
|
hannah
|
8ba4f17a92
|
ltl-mc with MAs
|
3 years ago |
|
hannah
|
78058b5152
|
ltl-mc with ctmcs
Conflicts:
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
|
3 years ago |
|
hannah
|
7f95f1fdbf
|
ctmc and mdp tests
|
3 years ago |
|
hannah
|
a038d9658e
|
added TODOs
|
3 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
|
4 years ago |
|
hannah
|
667d4a0e06
|
documentation and renaming of some methods
Conflicts:
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
|
4 years ago |
|
hannah
|
139ac3d0dc
|
flag to indicate whether condition should be in dnf
|
4 years ago |
|
hannah
|
93d9b586ed
|
compute 1-Pmax[in order to compute Pmin for MDPs
|
4 years ago |
|
hannah
|
fc0ae2ea4b
|
removed SolveGoal in function computeLTLproabilities of SparseLTLHelper
|
4 years ago |
|
hannah
|
1fe30f7d78
|
Convert acceptance formula into disjunctive normal form
|
4 years ago |
|
hannah
|
ffe70ea056
|
removed model from SparseLTLHelper
|
4 years ago |
|
hannah
|
f8d9773131
|
test update
|
4 years ago |
|
hannah
|
b30713c23d
|
Started to restructure LTL model checking algorithms
Conflicts:
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
|
4 years ago |
|
hannah
|
4fc3c79221
|
LTL tests for MDPs
|
4 years ago |
|
hannah
|
0f5c4708ca
|
corrected exception
|
4 years ago |
|
hannah
|
884b284ab5
|
corrected exception
|
4 years ago |
|
hannah
|
466339059f
|
Call parse_prefix_ltl instead of parse_formula
|
4 years ago |
|
hannah
|
c290e16260
|
Simplified LTL2DeterministicAutomaton
|
4 years ago |
|
hannah
|
d861c377a9
|
fixed typo
|
4 years ago |
|
Tim Quatmann
|
6110d33bcc
|
Removed debug output
|
4 years ago |
|
Tim Quatmann
|
d44bc3c6c2
|
CMAKE: Added option to include and link against Spot
Conflicts:
CMakeLists.txt
|
4 years ago |
|
hannah
|
d5edde05a7
|
Adapted ModelChecker test-cases and FormulaParser test-cases
|
4 years ago |
|
Tim Quatmann
|
1c16c17a57
|
FragmentCheckerTest: Fixed a few more testcaes that now correspond to invalid formulae.
|
4 years ago |
|
Tim Quatmann
|
b71cb813df
|
FormulaParser: Fixed parsing of multi-bounded path operator and quantile operator
|
4 years ago |
|
Tim Quatmann
|
8c669b9e8b
|
Fixed a FragmentCheckerTest case which considered a formula that is now considered invalid.
|
4 years ago |
|
Tim Quatmann
|
aa29ad1196
|
flagging multi-objective and quantile formulae as StateFormulae (fixing the previous commit)
Conflicts:
src/storm/modelchecker/AbstractModelChecker.cpp
|
4 years ago |
|
Tim Quatmann
|
cc9a4b8cb3
|
Adapting a parser test-case to the new parser
|
4 years ago |
|
Tim Quatmann
|
76c689a001
|
flagging multi-objective formulae as State formulae
|
4 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.
|
4 years ago |
|
hannah
|
132c293105
|
TYPED_TESTS for LTL modelchecker
|
4 years ago |
|
hannah
|
7d74efd591
|
TYPED_TESTS for LTL modelchecker
|
4 years ago |
|
Tim Quatmann
|
10e2d85cc4
|
Formulas: Added parentheses to formula output to avoid ambiguity
|
4 years ago |
|
hannah
|
bcf45f68df
|
modelchecker test update
|
4 years ago |
|
hannah
|
affee2bc5b
|
ltl dtmc modelchecker tests
|
4 years ago |
|
hannah
|
02b77707d4
|
ltl dtmc modelchecker tests
|
4 years ago |
|
hannah
|
b6800361ce
|
ltl formula parser tests
|
4 years ago |
