dehnert
8c1870eb54
Intermediate commit.
Former-commit-id: e5f251718f
10 years ago
dehnert
0f0baf61a4
Made DD-based model construction work for all DTMC benchmarks we have. Included tests for both DD-based and excplicit model generation from PRISM models.
Former-commit-id: e4af6d9f8a
10 years ago
dehnert
c3c83fbe4f
Fixed some compilation errors.
Former-commit-id: dc626450b8
10 years ago
David_Korzeniewski
00ddce497d
corrected identifier name.
One should actually read documentation, not just look at it...
Former-commit-id: 69d8154496
10 years ago
David_Korzeniewski
4b44e625d0
Adapted Death-Tests in BitVectorTest.cpp to return codes upon assertion failure on Windows and deactivate them everywhere if the macro NDEBUG is defined (as that disables assertions)
Former-commit-id: be04a49e57
10 years ago
David_Korzeniewski
e41922347d
Adapted ExpressionTest.cpp to weird behavior of windows when using temporary shared_ptr in make_pair in initializer_list.
Now using const_pointer_cast instead of static_cast to modify shared pointers. (Although it worked with static_casts, but you never know)
Former-commit-id: d42487bb0c
10 years ago
David_Korzeniewski
0f9c753778
Fixed Windows build error
Former-commit-id: a59eafdaf8
10 years ago
David_Korzeniewski
84f8a41302
More tests adapted, decreased verbosity of TopologicalValueIterationNondeterministicLinearEquationSolver
Former-commit-id: 6e0b492533
10 years ago
David_Korzeniewski
8b4309e53c
Adapted first test to new interface. Test passes.
Former-commit-id: 49dc8228f3
10 years ago
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