dehnert
894c3bb497
Added missing header.
Former-commit-id: 30d5444d23
10 years ago
dehnert
39fb2650cd
Included missing header.
Former-commit-id: dd278656bf
10 years ago
dehnert
7014d289e8
Fixed some issues related to bisimulation in the presence of state rewards.
Former-commit-id: 7f26a7bcf9
10 years ago
svkurowski
287281d053
Enable checking MDP models from the CLI
(cherry picked from commit 30b9811512
[formerly fa0555dd74
])
Former-commit-id: 271bda31cb
10 years ago
dehnert
980b7790a7
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: c0ccc12e57
10 years ago
dehnert
609a948495
Put noexcept in Macro and use deprecated throw() for MSVC to make it happy.
Former-commit-id: 3d83fefcda
10 years ago
dehnert
fd617efc91
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 4e2f42814a
10 years ago
dehnert
79798e2cb1
Fixed the reward-issue even harder.
Former-commit-id: 2ca1c229e1
10 years ago
dehnert
b07963bd46
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 78421578db
10 years ago
dehnert
a7bce9e520
Removed debug output and fixed the reward issue a bit more.
Former-commit-id: ecbbeff14e
10 years ago
dehnert
0d2440d4a9
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 0f0e18abad
10 years ago
dehnert
7cd0dfe8b0
Fixed an issue regarding the reward model generation.
Former-commit-id: 237acf99f9
10 years ago
dehnert
7644a74fcd
Removed some superfluous lines in test.
Former-commit-id: 2c2bd0ba67
10 years ago
dehnert
1b4d2a92db
Started working on making bisimulation work for models with (state-based) rewards.
Former-commit-id: b1029210f6
10 years ago
dehnert
370a0ae476
Fixed some issues in bisimulation and added some tests.
Former-commit-id: 98801de9db
10 years ago
dehnert
f8a06b69f5
Fixed a clang-warning related to a throws declaration.
Former-commit-id: 933ad7925a
10 years ago
dehnert
2f20abf47f
The user can now select on the command line which reward model of a symbolic model is to be used (as a second [optional] argument to --symbolic).
Former-commit-id: 02f998e5dd
10 years ago
svkurowski
a0b54fbca4
Add src/utility/storm-version.cpp to ignored files
This file is generated by CMake.
A more robust solution would be to configure this file out-of-source
much like build/include/storm-config.h.
Former-commit-id: 05eacc7a5b
10 years ago
PBerger
9fc68a554c
Cherry-picked a fix for GCC from branch.
Former-commit-id: 98f7c52b34
10 years ago
PBerger
1cf8674fa5
Added noexcept Destructors to the exceptions to fix the picky Clang3.5 compiler errors.
Former-commit-id: f620e5ed7d
10 years ago
dehnert
aa4836e085
Minor bugfix in bisimulation options.
Former-commit-id: 7a579aef50
10 years ago
dehnert
ed6f3dae9f
Renamed the newly added method.
Former-commit-id: 72ea9afb61
10 years ago
dehnert
2437601a85
Added function to compute distances of states to some other set of states.
Former-commit-id: 2bf19c1b2d
10 years ago
dehnert
f3048d31c2
Small bugfix for bisimulation decomposition.
Former-commit-id: eae1447df4
10 years ago
dehnert
72c178dd08
Merge branch 'weakBisimulation'
Former-commit-id: a602e8e58f
10 years ago
dehnert
e6904dcb21
Renamed bisimulation decomposition class to reflect that now also weak bisimulations can be computed.
Former-commit-id: 1a654b7110
10 years ago
dehnert
f90ac5c8c3
First working version of weak bisimulation for DTMCs.
Former-commit-id: 8a7d76de4f
10 years ago
dehnert
7257bb23c3
Further work on weak bisimulation. Model checking can now be done from tne command line again.
Former-commit-id: 5f338260e6
10 years ago
dehnert
391f3225e4
Added unparameterized NAND example. Further work on weak bisimulation.
Former-commit-id: 0936743f1e
10 years ago
dehnert
5bc593174e
Further work on weak bisimulation.
Former-commit-id: 3ad48ee0a3
10 years ago
dehnert
eeb859272f
Added (non-parametric) brp case study.
Former-commit-id: 30950730be
10 years ago
dehnert
56aec18a48
Added bisimulation settings. Further work on weak bisimulation.
Former-commit-id: c04759575a
10 years ago
dehnert
97158ee72e
Started on weak bisimulation.
Former-commit-id: 595caab54e
10 years ago
PBerger
1a4d4fd5a7
Added a test I used for finding the SCC Bug.
Former-commit-id: 5936e79d04
10 years ago
PBerger
cc9ad6beab
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Conflicts:
CMakeLists.txt
Former-commit-id: b88be0c91f
10 years ago
PBerger
eb9c1de59b
Added Boost DECLTYPE for MSVC.
Former-commit-id: c70dfa5e63
10 years ago
dehnert
754e168ace
Bugfix for bisimulation.
Former-commit-id: da93a5d4db
10 years ago
dehnert
d3fc2d8fbf
Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC.
Former-commit-id: 07358dc2e8
10 years ago
PBerger
94a83e423e
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: da54b8db45
10 years ago
dehnert
ba4b71a353
Added boost define BOOST_RESULT_OF_USE_DECLTYPE for gcc.
Former-commit-id: b346362805
10 years ago
PBerger
ec95f8f16d
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: a7d84533e7
10 years ago
PBerger
e54a774e80
Minor spellcheck.
Former-commit-id: cc9ce2cfae
10 years ago
dehnert
08ac566db2
Corrected typedef. Clang and gcc should now also be fine under Linux.
Former-commit-id: 46f8d43d47
10 years ago
dehnert
74351f9884
Switched from const_iterator to iterator in bisimulation to make stdlibc++ happy (libc++ is already happy, though).
Former-commit-id: 37fc55d0cf
10 years ago
dehnert
3dfc6a7b74
Pimped bisimulation a bit.
Former-commit-id: a27ea8b996
10 years ago
dehnert
0fdda922cd
Added more detailed statistics for bisim.
Former-commit-id: 7f0ff4a419
10 years ago
dehnert
484bbf3e83
Atomic propositions in formulas can now also be surrounded by quotation marks (to be compatible with the PRISM syntax).
Former-commit-id: e31a8c832a
10 years ago
TimQu
c38ce8cf68
Small fix for autoParser
Former-commit-id: f22b6031ce
10 years ago
dehnert
843a1d1fdf
Added comparator use for checking validity of probability matrices such that only if the value is actually constant it is required to be one.
Former-commit-id: 3224422976
10 years ago
dehnert
1c091d7640
Renamed some classes to indicate that only strong bisimulation can be computed. Added option to start with an initial partition that preserves only certain formulas. Added ConstantsComparator concept that is to be used when constants have to be compared with other constants.
Former-commit-id: feacadfa38
10 years ago