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
David_Korzeniewski
25d87bae06
Builds fine, still no tests yet
Former-commit-id: 3d9d85679a
10 years ago
David_Korzeniewski
2e92d66bf3
Cmake scripts for linking mathsat and gmp or mpir which is required by mathsat
Former-commit-id: b13b68115a
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
David_Korzeniewski
40e07b2ea5
Interpolation and AllSat implemented.
Tests pending, still some issues.
Former-commit-id: 7d94cdbc0c
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
David_Korzeniewski
56edf1e126
Initial MathSat integration.
Expression adapter, solving, unsat assumptions implemented
cmake and tests missing
allsat and interpolation not yet implemented
Former-commit-id: 5177775fbe
10 years ago
dehnert
6fa974dcb9
Merge branch 'master' into sparseBisimulation
Former-commit-id: d70ec75b70
10 years ago
dehnert
af270dee8a
Enabled bisimulation quotienting.
Former-commit-id: 588827ec8d
10 years ago
dehnert
01e4dd3367
Commit to switch workplace.
Former-commit-id: 7de1f8a1b1
10 years ago
dehnert
0e0027aa8e
Further work on sparse bisimulation.
Former-commit-id: ba256b8b0a
10 years ago
dehnert
bc43ce52ab
Eliminated two bugs, more to come.
Former-commit-id: 3ea21c66b9
10 years ago
dehnert
404b12848e
More (and more) work on bisimulation minimization.
Former-commit-id: 946085c71b
10 years ago
dehnert
8c64a1911c
Still bugs in bisimulation minimization.
Former-commit-id: b0a340f260
10 years ago
dehnert
43bc81a5fb
New bisimulatin minimization works on tiny example.
Former-commit-id: 2d62985977
10 years ago
dehnert
828e46ce87
Started working on a more clever way to do bisimulation minimization.
Former-commit-id: a2939ececb
10 years ago
sjunges
6b04c33dee
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Conflicts:
src/utility/cli.h
Former-commit-id: f63886844f
10 years ago