dehnert
f49d89144e
Fixed issue that could cause wrong models to be generated.
Former-commit-id: 8f1f9b4612
10 years ago
dehnert
ed4f1bb7cf
Added the possibility to build the bisimulation options from a formula in the sense that it automatically picks suitable settings for the formula.
Former-commit-id: 932c7d899a
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
dehnert
4952306092
Worked on making bisimulation decomposition a bit easier to use.
Former-commit-id: 0fe6b2af6a
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
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
dehnert
c85df2cd74
Conditional Probabilities working. Included two tests.
Former-commit-id: a89255c4ef
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
b60c5ffdc0
Fixed a lot of tests, improved some things here and there.
Former-commit-id: baec0a4963
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
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
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
dehnert
ee9533e586
Started working on making the main executable build again.
Former-commit-id: 9aaad15b9f
10 years ago
dehnert
8e71081f1e
Functional tests now work again.
Former-commit-id: 46d964ad22
10 years ago
dehnert
2eeaa06d76
Z3 runs fine again.
Former-commit-id: a725a33f01
10 years ago
dehnert
d6a299e799
MathSAT tests now running fine again.
Former-commit-id: 35083ea120
10 years ago
dehnert
99d9a9710d
Further steps to make everything work again.
Former-commit-id: 3f45a49dab
10 years ago
dehnert
809217c359
Refactored some parts of expressions. In particular, visitors now can return anything they want by using boost::any.
Former-commit-id: 0f6af138ae
10 years ago
dehnert
7b8c382303
Added tests for Mathsat expression adapter.
Former-commit-id: 4f8ef4c3c3
10 years ago
dehnert
a061cdbed8
Started refactoring MathSAT adapter.
Former-commit-id: 93b1fdedb3
10 years ago
dehnert
84bfd58884
Minor refactoring of Z3 expression adapter.
Former-commit-id: b31ae87a98
10 years ago
dehnert
b5d55335a6
All tests passing again.
Former-commit-id: ffa8bef2d2
10 years ago
dehnert
ba14ba3613
Further work on MathSAT solver.
Former-commit-id: dd67b23505
10 years ago
dehnert
7ff3dcecfb
Added test for interpolation to MathSat tests.
Former-commit-id: ac94857726
10 years ago
dehnert
6eb415f87f
Tests for MathSAT now run through on Mac OS.
Former-commit-id: 9f6cf0af6a
10 years ago
dehnert
d8be64f0d7
Started on making MathSatSmtSolver work properly.
Former-commit-id: c370658b26
10 years ago
dehnert
7014d289e8
Fixed some issues related to bisimulation in the presence of state rewards.
Former-commit-id: 7f26a7bcf9
10 years ago
dehnert
7644a74fcd
Removed some superfluous lines in test.
Former-commit-id: 2c2bd0ba67
10 years ago
dehnert
370a0ae476
Fixed some issues in bisimulation and added some tests.
Former-commit-id: 98801de9db
10 years ago
PBerger
1a4d4fd5a7
Added a test I used for finding the SCC Bug.
Former-commit-id: 5936e79d04
10 years ago
dehnert
433bae1156
Switched from an option to fix deadlocks to an option to not fix the deadlocks. Hence, deadlocks are now fixed by default unless otherwise requested.
Former-commit-id: 9434215807
10 years ago
dehnert
51becda4b3
Commit to switch workplace.
Former-commit-id: da5fac08cf
10 years ago
dehnert
5ecc96fa3a
Fixed some more places in the code to use the new option system.
Former-commit-id: 15ff64f1dc
10 years ago
dehnert
a995d7dd4a
The tests now run fine with the new option system.
Former-commit-id: 6d6c510131
10 years ago
dehnert
266d660d89
Added functions responsible for printing the help. Started adapting the tests to the new option system.
Former-commit-id: 0407d8223e
10 years ago
sjunges
5817fe50b6
post merge fixes
Former-commit-id: 2f9bc01abd
10 years ago
dehnert
9ad12616e2
Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
Former-commit-id: b3162aa86b
10 years ago
dehnert
96e1f8faf9
Renamed Settings class to SettingsManager.
Former-commit-id: 2b33f4c8d0
10 years ago
dehnert
9569426c86
Moved option registration to the settings class (so it's not deceentralized any longer). This enables to build storm as a library and on top of that build some exectuables, which saves a lot of compile time as soon as several targets have to be built or one switches between targets.
Former-commit-id: 69e0d526c7
10 years ago
dehnert
1cc930f0e4
Added proper source grouping for properties directory. Fixed one performance tests. Started on SCC-based reachability model checker.
Former-commit-id: e48c163783
10 years ago
dehnert
552b3eaab7
Fixed SCC performance tests.
Former-commit-id: a6b46e2fc5
10 years ago