Matthias Volk
|
4c1958c245
|
Fixed some compiler warnings
|
6 years ago |
Jip Spel
|
ed3fa3f82b
|
Fix TODOs
|
6 years ago |
|
Jip Spel
|
e0b2869bd5
|
Fix region check
|
7 years ago |
Alexander Bork
|
450e074c5b
|
Integrated non-Markovian state elimination into Storm MA modelchecking
|
7 years ago |
|
Jip Spel
|
13f44ab7ea
|
Monotonicity Checking on Region
|
7 years ago |
|
Jip Spel
|
6db964363e
|
Update for artifact evaluation ATVA
|
7 years ago |
|
Jip Spel
|
2883f81be1
|
Move settings to separate file
|
7 years ago |
|
Jip Spel
|
4825cb254f
|
Precision as argument
|
7 years ago |
|
Jip Spel
|
0d1ddb6232
|
Make sampling in monotonicity-analysis optional
|
7 years ago |
|
Jip Spel
|
f6ea4d38bb
|
Fix assumption making and checking and testing
|
7 years ago |
|
Matthias Volk
|
87d078f897
|
Output error by STORM_LOG_ERROR
|
7 years ago |
|
Jip Spel
|
ed4f61d3ee
|
BIsmulation simplification bisimulation + fix lattice
|
7 years ago |
Sebastian Junges
|
8fbc8d56c0
|
graph preservation properties correctly computed for CTMCs
|
7 years ago |
|
Jip Spel
|
f41b61fb7b
|
Make cyclic part faster
|
7 years ago |
|
Jip Spel
|
9e690c95c6
|
Fix cyclic monotonicity check
|
7 years ago |
|
Jip Spel
|
ab14245350
|
Remove bool for stateElimination
|
7 years ago |
|
Jip Spel
|
c33a8df85f
|
Eliminate selfloop introduced by SCC elimination
|
7 years ago |
|
Jip Spel
|
48cba66d96
|
Add scc elimination
|
7 years ago |
|
Matthias Volk
|
bcde728c3c
|
Transform formulas to deterministic-time as well
|
7 years ago |
|
Matthias Volk
|
374071670a
|
Activated symbolic bisimulation for parametric models
|
7 years ago |
|
Matthias Volk
|
a1c5aa946c
|
Integrated symbolic verification of parametric systems into storm-pars
|
7 years ago |
|
Matthias Volk
|
dfd1fec8c5
|
Fixed compile issues
|
7 years ago |
|
Jip Spel
|
8d95e71c3e
|
Change output, Fix some small bugs
|
7 years ago |
TimQu
|
208ee76edb
|
storm-pars: Added possibility to compute the extremal value within a given region using parameter lifting.
|
7 years ago |
|
Jip Spel
|
748098e891
|
Output to results.txt file
|
7 years ago |
|
Jip Spel
|
f098daf2f3
|
Add stopwatches
|
7 years ago |
|
Jip Spel
|
cca2ad474e
|
First check on samples for monotonicity
|
7 years ago |
|
Jip Spel
|
c85da52e8b
|
Give message when no lattices are created
|
8 years ago |
|
Jip Spel
|
67862b0a8d
|
First implementation for cyclic parts in model
|
8 years ago |
|
Jip Spel
|
83cb103177
|
Change variable naming
|
8 years ago |
|
Jip Spel
|
24abcfb61c
|
AssumptionChecker for mdp
|
8 years ago |
|
Jip Spel
|
4afa6d8a0f
|
Make validation of assumptions optional
|
8 years ago |
|
Jip Spel
|
24a40bba80
|
Add validated assumptions to set
|
8 years ago |
|
Jip Spel
|
e23a222605
|
Add simple validation for assumptions
|
8 years ago |
|
Jip Spel
|
3fcf4f83c0
|
Clean up AssumptionMaker
|
8 years ago |
|
Jip Spel
|
92193cfb08
|
WIP: Check assumptions on samples
|
8 years ago |
|
Jip Spel
|
581410c54b
|
Add check acyclic
|
8 years ago |
|
Jip Spel
|
2e4991a75e
|
TODO added create deep copy not yet working correctly
|
8 years ago |
|
Jip Spel
|
28b77e6a7d
|
Create MonotonicityChecker and fix some bugs in AssumptionMaker
|
8 years ago |
|
Jip Spel
|
2a93b89c22
|
Create AssumptionMaker
|
8 years ago |
|
Jip Spel
|
43eebf8e05
|
Return tuple and add assumptions
|
8 years ago |
|
Jip Spel
|
34c87453fb
|
Implement extension of lattice with assumptions
|
8 years ago |
|
Jip Spel
|
b6e48b35cc
|
Implement first version of LatticeExtender
|
8 years ago |
|
Jip Spel
|
b0b0623fcf
|
Add matrix declaration
|
8 years ago |
|
Jip Spel
|
5aec480a1e
|
Clean up
|
8 years ago |
|
Jip Spel
|
e7dc7acf8e
|
Cleanup
|
8 years ago |
|
Jip Spel
|
80cf0982a9
|
WIP: parameter lifting
|
8 years ago |
|
Jip Spel
|
6f8787b6f0
|
Add one possible solution for critical states
|
8 years ago |
|
Jip Spel
|
905f6fc970
|
Create lattice from model and formulas
|
8 years ago |
|
Jip Spel
|
128d428fcc
|
Add .dot representation for mc
|
8 years ago |
