Mavo
1e9fedb7ba
Order symmetries in decreasing order
Former-commit-id: 7ba21b0b9e
9 years ago
TimQu
fb0cdf336b
some benchmarking scripts and example regions...
Former-commit-id: b7b4a5870a
9 years ago
Mavo
6685b358f0
Symmetry mirrored in state vector
Former-commit-id: 7e5a578c44
9 years ago
sjunges
f89cc46576
two more small examples
Former-commit-id: 9d420a62b2
9 years ago
Mavo
371ba87f1c
Fixed activation of spares
Former-commit-id: f62ccdc79a
9 years ago
Mavo
c78d9ff802
Fixed problems with pdeps
Former-commit-id: c46c88b177
9 years ago
Mavo
0a78ba13f5
MA to CTMC for trivial nondeterminism
Former-commit-id: 8a342f032e
9 years ago
Mavo
3636b9ac0d
Added more benchmarks
Former-commit-id: b6936dfb7b
9 years ago
Mavo
72b09a693c
More examples
Former-commit-id: e4ea9cf5dc
9 years ago
Mavo
32c52d2271
Parse PDEPs
Former-commit-id: 623afd494f
9 years ago
Mavo
c6663ba74a
Added FDep bechmarks
Former-commit-id: 885b7a9531
9 years ago
Mavo
933194c155
Added debuglevel to benchmark script
Former-commit-id: 7904066261
9 years ago
Mavo
efdd9f25ae
Changed expected result
Former-commit-id: 0fb88af944
9 years ago
Mavo
ed6d299d46
Benchmark script for DFTs
Former-commit-id: 574c46528e
9 years ago
dehnert
7997b0596d
fixed brp (pMDP version) to also work with PRISM
Former-commit-id: 930a222a9e
9 years ago
Mavo
0775bdf549
Disabled some debug output
Former-commit-id: 31ae65f255
9 years ago
Mavo
d6b7331a5c
Fixed problem with multiple transitions to one state
Former-commit-id: 2fe612028e
9 years ago
Mavo
8b59a26fe0
More dft files
Former-commit-id: b1b7906604
9 years ago
TimQu
cb08583881
another script for remaining benchmarks
Former-commit-id: fc7239a4f8
9 years ago
TimQu
6484e431f5
modified selection of benchmarks
Former-commit-id: a0a00e7383
9 years ago
TimQu
d9b734e6d7
forgot something
Former-commit-id: 564958637e
9 years ago
TimQu
5f678f96ae
parallel execution of benchmarks and larger models
Former-commit-id: 1abf08d530
9 years ago
TimQu
56be3c183b
implemented refinement of regions plus benchmarks
Former-commit-id: 09faedc1be
9 years ago
TimQu
3ce8643d96
Added benchmarks
Former-commit-id: 6979a9aece
9 years ago
TimQu
9a41b4a95e
examples...
Former-commit-id: 694a1cdc58
9 years ago
TimQu
f86c4f65f7
examples and small fix regarding changes of elimination model checker
Former-commit-id: 2cc4247372
9 years ago
Mavo
e024f314eb
Added dft examples
Former-commit-id: 43e43c3846
9 years ago
dehnert
3e23a9ad40
some typos
Former-commit-id: 8b28f77ab4
9 years ago
dehnert
0ffbda5aff
initial draft of long-run rewards for parametric models
Former-commit-id: 991512a57d
9 years ago
dehnert
52dedca2a0
added tiny example for long-run properties
Former-commit-id: 245d0c96c9
9 years ago
TimQu
91fb664910
Refactored a little and implemented functions for prophesy
Former-commit-id: a61f1eaff2
10 years ago
TimQu
b4a4a81bb1
Renamed, moved, added some benchmarks
Former-commit-id: 670448c26f
10 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
10 years ago
TimQu
77c2f397a9
fix for approximation model, additional test for mdps, minor changes
Former-commit-id: cc837ddf3e
10 years ago
TimQu
d26f38b9a2
minor stuff, some more pmdp examples and an mdp test case
Former-commit-id: f48e308e5f
10 years ago
TimQu
c94e9c25a6
Added Mdp Region checking in storm.h, Some STORM_LOG_DEBUGs, fixes for sampling to work on Mdps
Former-commit-id: ab42fefd92
10 years ago
TimQu
d377e6b289
Minor improvements everywhere. Also implemented some tests
Former-commit-id: be74e5f459
10 years ago
chris
a216b5a9d9
added support for parsing choice labels for explicit MDPs
Former-commit-id: 89bb1817b4
10 years ago
David_Korzeniewski
7d84b0a4c5
Added ability to check properties from property file to cli utility.
Added minimal example for lra on dtmc
Former-commit-id: eec774f05a
10 years ago
dehnert
e4968b1dde
Fixed minor issue in cli
Former-commit-id: ed63925765
10 years ago
dehnert
e1761fa774
Enabled hybrid CTMC model checker in cli. Further work on hybrid CTMC model checker (not yet working). Fixed some minor issues in sparse CTMC model checker.
Former-commit-id: f9c0f976e1
10 years ago
dehnert
49bed497b0
Fixed a model building problem. Included checking of reward properties on CTMCs and wrote tests for it.
Former-commit-id: a137bd20ac
10 years ago
dehnert
799cbce775
Added function tests for CTMC creation and time-bounded reachability.
Former-commit-id: e56f860a70
10 years ago
dehnert
7fa6b568b4
Currently debugging the computation of transient probabilities in CTMCs.
Former-commit-id: 6671e0205d
10 years ago
dehnert
c6521221bd
Added tiny text example for ctmc mc.
Former-commit-id: 498bbec1f2
10 years ago
dehnert
99bcd337f1
Made the executable not choke if no model file/property was given. Added the benchmark models to the repo (replacing the old ones).
Former-commit-id: d0a53bcdf4
10 years ago
dehnert
1fb8d72a30
Merged master in parametricSystems.
Former-commit-id: 2fdc349e9d
10 years ago
dehnert
e51c3b9f44
Conditional probabilities work for brp model from the paper by Baier et al.
Former-commit-id: 02858bf34d
10 years ago
dehnert
b305a3b498
Switched to FactorizedPolynomial as the basis for rational functions and added missing reward construct for one NAND model.
Former-commit-id: 8bb62ee1d2
11 years ago
dehnert
7014d289e8
Fixed some issues related to bisimulation in the presence of state rewards.
Former-commit-id: 7f26a7bcf9
11 years ago