dehnert
|
8ed46ce1b8
|
started on learning-based verification
Former-commit-id: 24e9d81b15
|
10 years ago |
|
dehnert
|
1fb943b658
|
moved some internal structs from model builder to their own files to make them reusable
Former-commit-id: a354059fe8
|
10 years ago |
|
dehnert
|
ca354cffe4
|
moved preprocessing of PRISM program to utility to make it accessible from learning-based model checker
Former-commit-id: 704dde9ec5
|
10 years ago |
Mavo
|
2c172cd082
|
Refactoring
Former-commit-id: e9af97f7af
|
10 years ago |
|
Mavo
|
5796da9a5c
|
Refactoring
Former-commit-id: ab8665d114
|
10 years ago |
|
Mavo
|
fe7037e7fd
|
Support for POR (priority or)
Former-commit-id: f0e782bcb1
|
10 years ago |
|
dehnert
|
2df485a144
|
Merge branch 'future' into learning_engine
Former-commit-id: b9bceaa40d
|
10 years ago |
|
Mavo
|
7c60e4275d
|
Some more parametric DFT examples
Former-commit-id: a2401c9453
|
10 years ago |
|
Mavo
|
bdad8aedd7
|
Set dependencies to dont care after dependent event has failed
Former-commit-id: 506f5c3107
|
10 years ago |
|
dehnert
|
dae55eeb29
|
fixed some bugs and enabled markov automaton model checking from cli
Former-commit-id: 91b689d817
|
10 years ago |
|
Mavo
|
ebbc4ce7b4
|
Fixed compile issues introduced in merge
Former-commit-id: 059b7c84b3
|
10 years ago |
|
Mavo
|
2be3f17b91
|
Merge from future (not yet compiling)
Former-commit-id: 7ead44e805
|
10 years ago |
|
dehnert
|
aac9ba469b
|
Merge branch 'future' into learning_engine
Former-commit-id: 801a989353
|
10 years ago |
|
Mavo
|
4db05a7c20
|
Fixed bug with wrong dormancyFactor when copying elements
Former-commit-id: 3c2ddcc08a
|
10 years ago |
|
Mavo
|
6b24589966
|
Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update
Former-commit-id: a4d88f2026
|
10 years ago |
sjunges
|
472116a374
|
Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update
Former-commit-id: 44822c26d3
|
10 years ago |
|
sjunges
|
d688296022
|
even more modularisation oppurtunaties are now taken
Former-commit-id: de8fd4c848
|
10 years ago |
|
Mavo
|
25e2a9c070
|
Removed assertion
Former-commit-id: a6a6406808
|
10 years ago |
|
Mavo
|
9f3d160677
|
Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update
Former-commit-id: c002f450e1
|
10 years ago |
|
Mavo
|
2c15c89751
|
No DC propagation for failed toplevel
Former-commit-id: a2cf30e071
|
10 years ago |
|
sjunges
|
eeb289bdb8
|
Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update
Former-commit-id: 8ac6c51c92
|
10 years ago |
|
sjunges
|
e390e1c39d
|
several updates for better modularisation and support for VOT-modularisation
Former-commit-id: 97d5d03a86
|
10 years ago |
|
Mavo
|
e5fd604498
|
Flag for disabling DC propagation
Former-commit-id: 1fa850ef26
|
10 years ago |
|
dehnert
|
7dee6d3da2
|
started on learning-based MDP model checking
Former-commit-id: 9a901e619b
|
10 years ago |
|
sjunges
|
9ae9700d5c
|
modularisation on and and or
Former-commit-id: 50950ba497
|
10 years ago |
|
Mavo
|
db3c40e6d7
|
Fixed bugs
Former-commit-id: d602972afc
|
10 years ago |
|
Mavo
|
6ca6ab27e8
|
Activate failed representatives
Former-commit-id: dcda573443
|
10 years ago |
|
Mavo
|
5a066b9ae0
|
Used duplicate variable name
Former-commit-id: 3f47dfb3d1
|
10 years ago |
|
Mavo
|
150f177bcd
|
Symred on mcs seems to work now
Former-commit-id: d6a830f8a1
|
10 years ago |
|
Mavo
|
a21715cbc3
|
Nested symmetries seem to work for at least binary symmetries
Former-commit-id: dfa2052d18
|
10 years ago |
|
dehnert
|
bb7d8ca3c5
|
added learning as new engine selection in options
Former-commit-id: e00c7ad75d
|
10 years ago |
|
dehnert
|
adb42b3ac0
|
fixed minor things related to merge
Former-commit-id: f428c2808b
|
10 years ago |
|
dehnert
|
e23a7f854a
|
Merge branch 'future' into next_state_generators
Former-commit-id: bcdf6cb4b3
|
10 years ago |
|
dehnert
|
4a19d81133
|
fixed a few bugs
Former-commit-id: 70d408e653
|
10 years ago |
|
Mavo
|
306eb8a9cc
|
Construct state from bit vector
Former-commit-id: 705af6d503
|
10 years ago |
|
dehnert
|
6a99ab9ef9
|
expectation/variance now handled in formula parser
Former-commit-id: 9dbe09411c
|
10 years ago |
|
dehnert
|
51402ec853
|
removed measure type and only added measure type to reward/time operators
Former-commit-id: 16e19fe349
|
10 years ago |
|
Mavo
|
652aeb7562
|
Fixed compile error with CarlRationalNumber instead of RationalNumber
Former-commit-id: 0fbb4ad1c1
|
10 years ago |
|
Mavo
|
f394808e4a
|
Merge from future with compile errors
Former-commit-id: 36fd4385fc
|
10 years ago |
|
dehnert
|
f86bfdd46f
|
Merge branch 'future' into variance_properties
Former-commit-id: 74258afddd
|
10 years ago |
|
Mavo
|
7e8b790451
|
Preparation for pseudo state generation from bit vector
Former-commit-id: a273f13a67
|
10 years ago |
|
dehnert
|
39acf24448
|
fix for weak bisimulation on CTMCs
Former-commit-id: 4eee2e0997
|
10 years ago |
|
Mavo
|
a2a3a734a6
|
First version of symmetry for shared spares. Still some problems in contrast to Dortmund which had absolutely no problems with Tottenham.
Former-commit-id: c03062d4bd
|
10 years ago |
|
dehnert
|
016ab53f42
|
making the logic formulas better
Former-commit-id: bd5dd26c51
|
10 years ago |
|
Mavo
|
4284c633f4
|
StateGenerationInfo does not use DFS for symmetries
Former-commit-id: 7111f5764a
|
10 years ago |
|
dehnert
|
5e1e5b55a1
|
renamed expected time formulas to time formulas
Former-commit-id: 50a11fe446
|
10 years ago |
|
dehnert
|
9cda76c675
|
Merge branch 'future' into variance_properties
Former-commit-id: 13fe1e8531
|
10 years ago |
TimQu
|
6e8602413e
|
ModelInstantiator + test
Former-commit-id: f3c9980067
|
10 years ago |
|
TimQu
|
69c5ba604e
|
Helper functions for parametric stuff
Former-commit-id: 288e4de3da
|
10 years ago |
|
TimQu
|
a3aededd3a
|
public access to model ingredients: RewardModel and exitRates
Former-commit-id: b8dbe8576e
|
10 years ago |
