dehnert
1d49bc6dd0
extracting the bisimulation quotient for MDPs; tests for MDP bisimulation
Former-commit-id: 5613c653ba
9 years ago
dehnert
7833025829
reenabled all bisimulation tests
Former-commit-id: 24e8629270
9 years ago
dehnert
46fee522ff
made strong bisim for DTMCs work again
Former-commit-id: e42bafef4d
9 years ago
dehnert
1428f1647b
commented in some more tests, however the main entry points need to be fixed because of the new templating of the bisimulation class
Former-commit-id: 7133025049
9 years ago
dehnert
11c21eb338
on my way of making (the refactored version) bisimulation work again for deterministic models
Former-commit-id: 79c089a693
9 years ago
dehnert
96954ddd15
refactoring of bisimulation class in the prospect of extending it to (CT)MDPs, not yet done
Former-commit-id: 09f47ad977
9 years ago
dehnert
27e06940a9
templated all explicit parsers so that they may now be modified to produce non-double models
Former-commit-id: dd7f8767f8
9 years ago
dehnert
b94e978843
another round of fixes
Former-commit-id: 67f4e4be47
9 years ago
sjunges
d4ba7905fa
Extra constructor for simple testing.
Former-commit-id: 0fcef3d5e7
9 years ago
dehnert
972c391eb1
fixed some more bugs/warnings
Former-commit-id: 2748793daf
9 years ago
dehnert
b3178e17f6
more bug fixes
Former-commit-id: 0b33b30efa
9 years ago
sjunges
f85d28325e
Further work towards faster and more modular compilation
Former-commit-id: 9de50910b8
9 years ago
sjunges
3c2040f4b7
Removed many superfluous includes, added some source files -- towards faster compilation
Former-commit-id: a575a97d40
9 years ago
dehnert
56b4f53ce7
got rid of more warnings
Former-commit-id: 5c39f63c69
9 years ago
dehnert
e338cbe069
fixed a lot of warnings in the tests
Former-commit-id: b6752202ac
9 years ago
dehnert
9d5c3e7e2f
added functionality to flatten the modules of a PRISM program into one module
Former-commit-id: 04faac9c67
9 years ago
dehnert
6c4162fae4
more work towards steady state for CTMCs
Former-commit-id: c3e17d1fc0
10 years ago
dehnert
dd399c5f85
Finalized hybrid MDP model checker. It passes its tests now.
Former-commit-id: 47de0b9433
10 years ago
dehnert
3b4dca1a03
Improved Jacobi method a bit.
Former-commit-id: f4affeebf6
10 years ago
dehnert
e83d191be3
ODDs can now also be constructed from BDDs directly (without a transformation step to ADDs).
Former-commit-id: d19bbc3ff5
10 years ago
dehnert
c8d8f75a10
Working on ODD generation for BDDs (not yet working).
Former-commit-id: 5665dd1f24
10 years ago
dehnert
60701cebdb
ADDs and BDDs are no longer mixed in the abstraction layer.
Former-commit-id: 3c31063ea6
10 years ago
dehnert
c70d93f4d3
Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.
Former-commit-id: 3215a38c44
10 years ago
dehnert
a1dae8849e
Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented.
Former-commit-id: d4e6df30b5
10 years ago
dehnert
706ea56963
Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster.
Former-commit-id: 07ffb5882d
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
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
dehnert
4952306092
Worked on making bisimulation decomposition a bit easier to use.
Former-commit-id: 0fe6b2af6a
10 years ago
dehnert
01d7bce205
Fixed some test.
Former-commit-id: 9750284b59
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
99d9a9710d
Further steps to make everything work again.
Former-commit-id: 3f45a49dab
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
51becda4b3
Commit to switch workplace.
Former-commit-id: da5fac08cf
10 years ago
dehnert
fff4e61fc3
Changed interface of matrix builder slightly to be able to also not force the resulting matrix to certain dimensions, but merely to reserve the desired space.
Former-commit-id: e36d05398e
10 years ago
dehnert
ab58103555
Started to pimp matrix. First step: added proper methods setColumn/setValue that operate on a matrix entry and removed the non-const versions of getColumn/getValue. Added a typedef for the index type in the matrix so that it becomes possible to have matrices with a different index type (e.g. 32-bit values).
Former-commit-id: 3cc0fdf9ee
10 years ago
PBerger
d2f4c85711
Made changes to comply with new SparseMatrix Interface (YUCK).
Fixed tests, all that stuff.
Former-commit-id: c78de5f8ce
11 years ago
dehnert
caf96c04e0
Extended DD interface by methods to generate explicit row-grouped matrices from DDs.
Former-commit-id: 1945d7be6d
11 years ago