David_Korzeniewski
90958bb018
cuda library was not linked to tests, for now using static libraries as dlls don't work for non obvious reasons
Former-commit-id: a1cfba331f
10 years ago
David_Korzeniewski
8b4309e53c
Adapted first test to new interface. Test passes.
Former-commit-id: 49dc8228f3
10 years ago
David_Korzeniewski
8066bb6637
Small fix for test.
CPU implementation of TopologicalValueIterationMdpPrctlModelChecker seems to be working, adapted parts of tests passing!
Former-commit-id: 7ed1e11f91
10 years ago
David_Korzeniewski
3748905bcf
Fixes and test refactoring for TopologicalValueIterationMdpPrctlModelChecker
- Explicit instantiation of matrix and scc decomposition for float
- Started to adapt TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to new formulas
Former-commit-id: 4685ae4939
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
18f314d7c6
Some more bugfixes. Damn you, clang on Mac OS!
Former-commit-id: 86a7230a61
10 years ago
dehnert
64fd308713
Another minor bugfix in the formula classes.
Former-commit-id: e1fb3929c7
10 years ago
dehnert
f5b7554590
Minor bugfix for conditional probability computation.
Former-commit-id: c0b103e2aa
10 years ago
dehnert
98efde80f7
Fixed some compile issues (and some other issues).
Former-commit-id: e07861bd92
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
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
David_Korzeniewski
78d3a392a5
Created settings module for TopologicalValueIterationNondeterministicLinearEquationSolver and integrated that with the solver.
Former-commit-id: fa1ad5ce2a
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
dehnert
91e177028d
Started refactoring explicit model generator of PRISM models
Former-commit-id: 4ea82670d0
10 years ago
dehnert
4758ef73ec
Fixed an issue that gcc has problems with.
Former-commit-id: 69c9b71d01
10 years ago
dehnert
5e37c09fc0
Fixed some bugs.
Former-commit-id: dce463081d
10 years ago
dehnert
231d2223a9
Model building works again (more or less)
Former-commit-id: fa6843fcdc
10 years ago
dehnert
8ec362bb7d
Started debugging new model generation.
Former-commit-id: 704a7957f2
10 years ago
dehnert
6f2916d557
Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet.
Former-commit-id: dc60f568bf
10 years ago
dehnert
26e9eac934
Added another convenience operation to bit vector class.
Former-commit-id: 6420f3ec90
10 years ago
dehnert
827839e7fd
Changed internal representation of bit vector slightly, adjusted all operations. New bit vector operation runs fine now.
Former-commit-id: 186eefe2ad
10 years ago
dehnert
43d77e0adc
Wrote tests for the new necessary bit vector operations (they fail, because the bit vector is organized in a weird way and needs to be restructured.)
Former-commit-id: b80e4b6efa
10 years ago
dehnert
30f78b0a99
Intermediate commit. Started improving explicit model adapter performance.
Former-commit-id: 8a4aa64ac6
10 years ago
dehnert
aaefe7dfa5
Fixed some tests/parser.
Former-commit-id: d1767861c4
10 years ago
dehnert
53196f5610
Created bit vector hash map and some necessary bit vector methods.
Former-commit-id: 4a9946a743
10 years ago
dehnert
f5f2a2dd4c
Added expression evaluation (header-only) library exprtk and a corresponding evaluator class.
Former-commit-id: 950d1af6e0
10 years ago