dehnert
|
1b568a8691
|
Fixed some things.
Former-commit-id: 44997a1f22
|
10 years ago |
dehnert
|
cc7d44dd15
|
Added proper canHandle method to propositional model checker.
Former-commit-id: 4af714e31a
|
10 years ago |
dehnert
|
b5f907d99d
|
Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation.
Former-commit-id: 517a870d2f
|
10 years ago |
David_Korzeniewski
|
ee4c961cc9
|
fixes for compile errors. target "storm" builds without errors
tests not compiling because of property modifications.
Former-commit-id: 0366cf99cd
|
10 years ago |
David_Korzeniewski
|
547e33f0f4
|
Merge branch 'master' into cuda_integration
Conflicts:
CMakeLists.txt
src/settings/SettingsManager.cpp
src/settings/SettingsManager.h
Former-commit-id: 2811fee52e
|
10 years ago |
dehnert
|
7e847e420b
|
(Hopefully) successfully merged the changes of master into parametricSystems.
Former-commit-id: 6ef6400449
|
10 years ago |
dehnert
|
d70f65ae7f
|
Merge branch 'master' into parametricSystems
Former-commit-id: f6fb318162
|
10 years ago |
dehnert
|
18f314d7c6
|
Some more bugfixes. Damn you, clang on Mac OS!
Former-commit-id: 86a7230a61
|
10 years ago |
dehnert
|
3766c6b675
|
Merge branch 'master' into parametricSystems
Former-commit-id: 4dc72bbb3c
|
10 years ago |
dehnert
|
64fd308713
|
Another minor bugfix in the formula classes.
Former-commit-id: e1fb3929c7
|
10 years ago |
dehnert
|
fe7b6d1808
|
Merge branch 'master' into parametricSystems
Former-commit-id: 1e0629b994
|
10 years ago |
dehnert
|
f5b7554590
|
Minor bugfix for conditional probability computation.
Former-commit-id: c0b103e2aa
|
10 years ago |
dehnert
|
71e0ac470a
|
Merge branch 'master' into parametricSystems
Former-commit-id: 5763f8b9df
|
10 years ago |
dehnert
|
1fb8d72a30
|
Merged master in parametricSystems.
Former-commit-id: 2fdc349e9d
|
10 years ago |
dehnert
|
98efde80f7
|
Fixed some compile issues (and some other issues).
Former-commit-id: e07861bd92
|
10 years ago |
dehnert
|
3f724e6fe2
|
Started merging master into parametric systems.
Former-commit-id: a58be85ebd
|
10 years ago |
dehnert
|
abc222fc31
|
Fixed some compilation errors.
Former-commit-id: b344bee8d2
|
10 years ago |
David_Korzeniewski
|
ab36c5fb0d
|
Workarounds for more Windows quirks. Compiles but tests crash.
Former-commit-id: 0c47ae886d
|
10 years ago |
David_Korzeniewski
|
7da35af0bb
|
Some compile errors on Windows fixed, some still persist.
Former-commit-id: 1a9331371b
|
10 years ago |
dehnert
|
f0a2db6485
|
Enabled checking formula nodes that contain an expression in the variable of the program.
Former-commit-id: fba632e7f4
|
10 years ago |
dehnert
|
92aa2607a0
|
The labels of the models are now only built if no property was given or the given property contains the label.
Former-commit-id: d5ce5a2e1e
|
10 years ago |
dehnert
|
ee7b591db1
|
Some work on cli.
Former-commit-id: c3045f48a8
|
10 years ago |
dehnert
|
c85df2cd74
|
Conditional Probabilities working. Included two tests.
Former-commit-id: a89255c4ef
|
10 years ago |
dehnert
|
6bc6753e90
|
Some work on conditional probs. Not yet working.
Former-commit-id: 1a05e2e5dc
|
10 years ago |
dehnert
|
ae2b950e86
|
Fixed some issue in model builder.
Former-commit-id: 12a4afd591
|
10 years ago |
dehnert
|
9e8d8a2c27
|
Fixed wrong calculation of reachability rewards in state-elimination-based model checker.
Former-commit-id: bee99d61b0
|
10 years ago |
dehnert
|
89fc5be1ab
|
Fixed some things and wrote tests for elimination-based DTMC modelchecker. They fail: apparently rewards are not correctly computed in some cases.
Former-commit-id: 000ad6b049
|
10 years ago |
dehnert
|
8a4706d9c9
|
A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
Former-commit-id: bbf988c943
|
10 years ago |
dehnert
|
b60c5ffdc0
|
Fixed a lot of tests, improved some things here and there.
Former-commit-id: baec0a4963
|
10 years ago |
dehnert
|
d0917f033c
|
Adapted Markov automaton model checker to new formula classes.
Former-commit-id: c351b10ef2
|
10 years ago |
dehnert
|
89df9621a9
|
MDP model checker works again.
Former-commit-id: 2c24da6192
|
10 years ago |
dehnert
|
9026aa9ac9
|
Adapted first model checker to the new properties.
Former-commit-id: 206d6c9858
|
10 years ago |
dehnert
|
01d7bce205
|
Fixed some test.
Former-commit-id: 9750284b59
|
10 years ago |
dehnert
|
f673dccd76
|
Formula parser works again. Tests adapted.
Former-commit-id: 78ce54d69f
|
10 years ago |
dehnert
|
1699732dce
|
More work on logic classes.
Former-commit-id: 9d94e02b74
|
10 years ago |
dehnert
|
4c9d6ccfc5
|
Removed actions and filters and old logic classes.
Former-commit-id: cd487fd3b3
|
10 years ago |
dehnert
|
320641e597
|
Started working on modified property classes.
Former-commit-id: cbcf84c2f6
|
10 years ago |
David_Korzeniewski
|
447285d6dd
|
Fixed merge error
Former-commit-id: 18d5d06921
|
10 years ago |
David_Korzeniewski
|
2279710443
|
Directly use Matrix with Decomposition
Former-commit-id: 745fa7c5c9
|
10 years ago |
David_Korzeniewski
|
3e4495cad0
|
small fixes
Former-commit-id: 0d9cc58d75
|
10 years ago |
dehnert
|
e51c3b9f44
|
Conditional probabilities work for brp model from the paper by Baier et al.
Former-commit-id: 02858bf34d
|
10 years ago |
dehnert
|
d991b4a26a
|
Worked some more on conditional probabilities.
Former-commit-id: d5eb88d914
|
10 years ago |
dehnert
|
70e45d43f1
|
Started on computing conditional probabilities for parametric systems.
Former-commit-id: b42c00e28e
|
10 years ago |
David_Korzeniewski
|
78d3a392a5
|
Created settings module for TopologicalValueIterationNondeterministicLinearEquationSolver and integrated that with the solver.
Former-commit-id: fa1ad5ce2a
|
10 years ago |
dehnert
|
01bd1fbc76
|
Model building works again for parametric systems.
Former-commit-id: d3f3e357ca
|
10 years ago |
dehnert
|
12e6fac968
|
Started making generation of parametric models work again.
Former-commit-id: 93b0bc351c
|
10 years ago |
dehnert
|
217ade7cc6
|
Merged master into parametricSystems and added/reverted certain things on the way to make the tests and everything work again.
Former-commit-id: 28b859cee7
|
10 years ago |
dehnert
|
00861a7479
|
Loosened the restriction to always require GMP a bit.
Former-commit-id: 0537ff217a
|
10 years ago |
dehnert
|
fafeffe138
|
Merge branch 'master' into ExpressionModifications
Conflicts:
src/solver/Z3SmtSolver.cpp
Former-commit-id: c195760d33
|
10 years ago |
dehnert
|
2bd0e2e377
|
Improved performance of explicit model generation a bit.
Former-commit-id: 1613435eb3
|
10 years ago |