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 |
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 |
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 |
chris
|
a216b5a9d9
|
added support for parsing choice labels for explicit MDPs
Former-commit-id: 89bb1817b4
|
9 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
|
10 years ago |
dehnert
|
7014d289e8
|
Fixed some issues related to bisimulation in the presence of state rewards.
Former-commit-id: 7f26a7bcf9
|
10 years ago |
dehnert
|
61e78f8d12
|
Adapted parameterized NAND example to use state rewards instead of transition rewards. Also, the unfactorized polynomials are now used to build and compute everything. We should detect cyclic models and use the factorized polynomials for them.
Former-commit-id: c4179f2029
|
10 years ago |
dehnert
|
064da9f0aa
|
Added crowds20-5 as parametric model.
Former-commit-id: 34aaf7b084
|
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
|
cb3c8abe34
|
Introduced parameter (for coin flip probability) in die example and added it to the list of parametric examples.
Former-commit-id: a59c4ebd52
|
10 years ago |
dehnert
|
60510d07f7
|
Fixed one parametric model. Added debug output.
Former-commit-id: 38a219ce0c
|
10 years ago |
dehnert
|
ccee9815bd
|
Removed Mac OS intermediate files.
Former-commit-id: 2085047809
|
10 years ago |
dehnert
|
f909387258
|
Added some new example files.
Former-commit-id: e7f6d58ddf
|
10 years ago |
dehnert
|
0776d8a74b
|
Added and fixed some example models. Added option for maximal size of SCC that gets eliminated using state elimination.
Former-commit-id: bf1e73ff61
|
10 years ago |
dehnert
|
4eea90646a
|
Fixed attributes of some example files. Added option to eliminate entry states in the very end (added option module for model checking of parametric models). Added feature to specify the formulas to check on the command line.
Former-commit-id: 4ce8932fc4
|
10 years ago |
dehnert
|
4f82c1ebb1
|
Added some parametrix models. Included percentage of eliminated states to get a feeling for the remaining running time.
Former-commit-id: bad5f32663
|
10 years ago |
dehnert
|
2fa3036dc3
|
Added functionality to replace identifiers in an expression with the values given in an valuation. State-variables now get replaced in probabilities specified by a parameterized model. Fixed and added some parameterized models.
Former-commit-id: a863a07261
|
10 years ago |
sjunges
|
14b4d2988e
|
two additional benchmarks
Former-commit-id: bd6e2517e2
|
10 years ago |
sjunges
|
a9a2bea81a
|
first example for pdtmcs
Former-commit-id: 74f0a1eab0
|
10 years ago |
dehnert
|
1cc930f0e4
|
Added proper source grouping for properties directory. Fixed one performance tests. Started on SCC-based reachability model checker.
Former-commit-id: e48c163783
|
10 years ago |
dehnert
|
f485974187
|
Fixed (asynch) leader election to comply with our grammar. Added LOG_DEBUG macro.
Former-commit-id: 7b22ecba8e
|
10 years ago |
sjunges
|
6bc50e3d76
|
brp example
Former-commit-id: 06d1553d5f
|
11 years ago |
dehnert
|
7667933caf
|
First working version of explicit model generation using the new PRISM classes and expressions.
Former-commit-id: e71408cb89
|
11 years ago |
PBerger
|
98b0bcf187
|
Reimplemented the TopologicalValueIterationNondeterministicLinearEquationSolver with splitting into submatrices.
Added a dtmc example for tests with the StronglyConnectedComponentDecomposition.
Former-commit-id: 0c33793fe6
|
11 years ago |