dehnert
|
7d0ae06f9f
|
Fixed creation of empty blocks under certain circumstances in bisimulation.
Former-commit-id: f1240e234b
|
11 years ago |
dehnert
|
3231ea6c06
|
Moved to new macros.
Former-commit-id: d97c947c22
|
11 years ago |
dehnert
|
91084a5da4
|
APs true/false can now be queried for a state.
Former-commit-id: 3c16df4509
|
11 years ago |
dehnert
|
0bc685969d
|
Moved from call to list::size to counting member in bisimulation partition to avoid gcc's O(n) list::size.
Former-commit-id: aaae9886b7
|
11 years ago |
dehnert
|
894c3bb497
|
Added missing header.
Former-commit-id: 30d5444d23
|
11 years ago |
dehnert
|
39fb2650cd
|
Included missing header.
Former-commit-id: dd278656bf
|
11 years ago |
dehnert
|
7014d289e8
|
Fixed some issues related to bisimulation in the presence of state rewards.
Former-commit-id: 7f26a7bcf9
|
11 years ago |
svkurowski
|
287281d053
|
Enable checking MDP models from the CLI
(cherry picked from commit 30b9811512 [formerly fa0555dd74 ])
Former-commit-id: 271bda31cb
|
11 years ago |
dehnert
|
609a948495
|
Put noexcept in Macro and use deprecated throw() for MSVC to make it happy.
Former-commit-id: 3d83fefcda
|
11 years ago |
dehnert
|
79798e2cb1
|
Fixed the reward-issue even harder.
Former-commit-id: 2ca1c229e1
|
11 years ago |
dehnert
|
a7bce9e520
|
Removed debug output and fixed the reward issue a bit more.
Former-commit-id: ecbbeff14e
|
11 years ago |
dehnert
|
7cd0dfe8b0
|
Fixed an issue regarding the reward model generation.
Former-commit-id: 237acf99f9
|
11 years ago |
dehnert
|
1b4d2a92db
|
Started working on making bisimulation work for models with (state-based) rewards.
Former-commit-id: b1029210f6
|
11 years ago |
dehnert
|
370a0ae476
|
Fixed some issues in bisimulation and added some tests.
Former-commit-id: 98801de9db
|
11 years ago |
dehnert
|
f8a06b69f5
|
Fixed a clang-warning related to a throws declaration.
Former-commit-id: 933ad7925a
|
11 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
|
11 years ago |
PBerger
|
9fc68a554c
|
Cherry-picked a fix for GCC from branch.
Former-commit-id: 98f7c52b34
|
11 years ago |
David_Korzeniewski
|
25d87bae06
|
Builds fine, still no tests yet
Former-commit-id: 3d9d85679a
|
11 years ago |
PBerger
|
1cf8674fa5
|
Added noexcept Destructors to the exceptions to fix the picky Clang3.5 compiler errors.
Former-commit-id: f620e5ed7d
|
11 years ago |
dehnert
|
aa4836e085
|
Minor bugfix in bisimulation options.
Former-commit-id: 7a579aef50
|
11 years ago |
dehnert
|
ed6f3dae9f
|
Renamed the newly added method.
Former-commit-id: 72ea9afb61
|
11 years ago |
dehnert
|
2437601a85
|
Added function to compute distances of states to some other set of states.
Former-commit-id: 2bf19c1b2d
|
11 years ago |
dehnert
|
f3048d31c2
|
Small bugfix for bisimulation decomposition.
Former-commit-id: eae1447df4
|
11 years ago |
dehnert
|
e6904dcb21
|
Renamed bisimulation decomposition class to reflect that now also weak bisimulations can be computed.
Former-commit-id: 1a654b7110
|
11 years ago |
dehnert
|
f90ac5c8c3
|
First working version of weak bisimulation for DTMCs.
Former-commit-id: 8a7d76de4f
|
11 years ago |
dehnert
|
7257bb23c3
|
Further work on weak bisimulation. Model checking can now be done from tne command line again.
Former-commit-id: 5f338260e6
|
11 years ago |
dehnert
|
391f3225e4
|
Added unparameterized NAND example. Further work on weak bisimulation.
Former-commit-id: 0936743f1e
|
11 years ago |
dehnert
|
5bc593174e
|
Further work on weak bisimulation.
Former-commit-id: 3ad48ee0a3
|
11 years ago |
dehnert
|
56aec18a48
|
Added bisimulation settings. Further work on weak bisimulation.
Former-commit-id: c04759575a
|
11 years ago |
dehnert
|
97158ee72e
|
Started on weak bisimulation.
Former-commit-id: 595caab54e
|
11 years ago |
dehnert
|
754e168ace
|
Bugfix for bisimulation.
Former-commit-id: da93a5d4db
|
11 years ago |
dehnert
|
d3fc2d8fbf
|
Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC.
Former-commit-id: 07358dc2e8
|
11 years ago |
PBerger
|
e54a774e80
|
Minor spellcheck.
Former-commit-id: cc9ce2cfae
|
11 years ago |
dehnert
|
08ac566db2
|
Corrected typedef. Clang and gcc should now also be fine under Linux.
Former-commit-id: 46f8d43d47
|
11 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
|
11 years ago |
dehnert
|
3dfc6a7b74
|
Pimped bisimulation a bit.
Former-commit-id: a27ea8b996
|
11 years ago |
dehnert
|
0fdda922cd
|
Added more detailed statistics for bisim.
Former-commit-id: 7f0ff4a419
|
11 years ago |
David_Korzeniewski
|
40e07b2ea5
|
Interpolation and AllSat implemented.
Tests pending, still some issues.
Former-commit-id: 7d94cdbc0c
|
11 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
|
11 years ago |
TimQu
|
c38ce8cf68
|
Small fix for autoParser
Former-commit-id: f22b6031ce
|
11 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
|
11 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
|
11 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
|
11 years ago |
dehnert
|
af270dee8a
|
Enabled bisimulation quotienting.
Former-commit-id: 588827ec8d
|
11 years ago |
dehnert
|
01e4dd3367
|
Commit to switch workplace.
Former-commit-id: 7de1f8a1b1
|
11 years ago |
dehnert
|
0e0027aa8e
|
Further work on sparse bisimulation.
Former-commit-id: ba256b8b0a
|
11 years ago |
dehnert
|
bc43ce52ab
|
Eliminated two bugs, more to come.
Former-commit-id: 3ea21c66b9
|
11 years ago |
dehnert
|
404b12848e
|
More (and more) work on bisimulation minimization.
Former-commit-id: 946085c71b
|
11 years ago |
dehnert
|
8c64a1911c
|
Still bugs in bisimulation minimization.
Former-commit-id: b0a340f260
|
11 years ago |
dehnert
|
43bc81a5fb
|
New bisimulatin minimization works on tiny example.
Former-commit-id: 2d62985977
|
11 years ago |