PBerger
f0f3e8cbb3
Fixed test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp when MathSAT support is unavailable.
Former-commit-id: c4b91a2ac5
9 years ago
TimQu
3ce8643d96
Added benchmarks
Former-commit-id: 6979a9aece
9 years ago
dehnert
0f6e6e4da1
added feature to compute step-bounded until probabilities in parametric models
Former-commit-id: 172e87cb55
9 years ago
TimQu
1225b056f2
a little refactoring
Former-commit-id: 9af14c006c
9 years ago
sjunges
1e1400d68d
merge
Former-commit-id: eb9efc4bb2
9 years ago
dehnert
0d912ee59d
finalized sylvan tests
Former-commit-id: e20160ce2c
9 years ago
dehnert
d0e15d1a4f
more work (and stuff, you know?)
Former-commit-id: ec9f6746b8
9 years ago
dehnert
b297cdf38f
added some syntatic sugar to PRISM parser in order to enhance performance tests of symbolic model checker
Former-commit-id: d85ce26536
9 years ago
dehnert
329fee6b32
added performance tests for symbolic DTMC model checker
Former-commit-id: 10814c4cdc
9 years ago
dehnert
0708672a68
removed ite for ADDs as this operation should be formed with a BDD as the first argument. as a compensation, we provide a version of ite that takes a BDD and two ADDs and returns the corresponding ADD
Former-commit-id: 720dc3a9c4
9 years ago
dehnert
f8fc39870a
hybrid and symbolic model checkers working with sylvan
Former-commit-id: d01b92e328
9 years ago
dehnert
7376eaf866
made symbolic MDP model checker tests work
Former-commit-id: e2e0d07a55
9 years ago
dehnert
7f75db2790
ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working.
Former-commit-id: b11b2f7476
9 years ago
dehnert
f2a01afbdf
ODD-based stuff working for Sylvan. Almost all tests passing
Former-commit-id: a6eef37d37
9 years ago
dehnert
36a6e9e76e
more work on sylvan ODD-related stuff
Former-commit-id: 142f57620a
9 years ago
dehnert
50e7bbfe35
fixed a tests, all tests running again
Former-commit-id: b271ae5e84
9 years ago
dehnert
ebe9ccbb15
some work on DD stuff
Former-commit-id: 50ca51d264
9 years ago
dehnert
8657fb0181
introduced relational product operations to prob0/1 algorithms (where possible)
Former-commit-id: 7fcd642030
9 years ago
dehnert
e43bdfaaaa
more work on the dd stuff *sigh*
Former-commit-id: df8e227336
9 years ago
dehnert
fb4c103320
merged sylvan updates into the sylvan copy. made more tests work
Former-commit-id: 18023e03c2
9 years ago
TimQu
91fb664910
Refactored a little and implemented functions for prophesy
Former-commit-id: a61f1eaff2
9 years ago
dehnert
10996b4ab5
more work on sylvan
Former-commit-id: c1bfcd83ee
9 years ago
dehnert
7ea0cb19b3
added some new functions to sylvan. isolated new code to make it easier to update sylvan to newer versions later
Former-commit-id: 6b489993a5
9 years ago
dehnert
8eb3720f91
more work on sylvan integration
Former-commit-id: 1bd63e5373
9 years ago
dehnert
6c1a21c43f
added more functions in sylvan
Former-commit-id: f2e0c158a6
9 years ago
dehnert
2c69232560
started cleaning ADD interface
Former-commit-id: f67fe7cf47
9 years ago
dehnert
472851508c
changed return type of equal, notEqual, less, lessOrEqual, greater, greaterOrEqual to BDD since returning an ADD is logically not quite correct
Former-commit-id: 64bf8b0704
9 years ago
dehnert
8194454621
more work on making sylvan mtbdds work
Former-commit-id: 98454b0ff4
9 years ago
dehnert
99f096635f
started integrating sylvan
Former-commit-id: 2aec043047
9 years ago
TimQu
f7992f5aa7
Forgot adaptation of test...
Former-commit-id: 263da953bc
9 years ago
TimQu
b4a4a81bb1
Renamed, moved, added some benchmarks
Former-commit-id: 670448c26f
9 years ago
dehnert
a258d1ab48
restructured ODD to be independent of the DD library being used
Former-commit-id: 83f08ba203
9 years ago
dehnert
19029cd905
functional tests compile and run again, yay!
Former-commit-id: 60d3ce16b9
9 years ago
TimQu
4a874a5a29
Added some benchmark models from param website
Fixed two bugs considering nonatomic subformulae and constant results
Qualitative modelchecking needs to be done when applying a policy!
Former-commit-id: bd88228214
9 years ago
TimQu
bf450688b4
The variable pool of carl needs to be cleared after executing a test.
Sampling for mdps now uses the policy of the previous iteration as initial guess
Former-commit-id: 3b8b25f30f
9 years ago
dehnert
4e86ef2e47
moved CUDD-based DD implementation to own folder
Former-commit-id: a828f92518
9 years ago
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
TimQu
1860502a3a
Deterministic states with only constant outgoing transitions are now eliminated
Former-commit-id: be5bf4f7cc
9 years ago
TimQu
77c2f397a9
fix for approximation model, additional test for mdps, minor changes
Former-commit-id: cc837ddf3e
9 years ago
dehnert
b3ce727f6c
fixed minor bug, tests for smt-based permissive schedulers (for upper-bounded properties) now passing
Former-commit-id: bf0261e981
9 years ago
dehnert
59501dd347
removed some object files of xerces. started working on smt-based permissive schedulers
Former-commit-id: de95333225
9 years ago
sjunges
160f9e476f
test descr for milp perm sched
Former-commit-id: 54dfa2587e
9 years ago
TimQu
046afd3804
Refactored SamplingModel
Former-commit-id: b51ed752b4
9 years ago
dehnert
de58c73c5a
forgot to commit some files
Former-commit-id: 74aaea662a
9 years ago
sjunges
e4aab761d2
updates to perm schedulers
Former-commit-id: b3404cac21
9 years ago