Matthias Volk
|
70ddde905f
|
Renaming to PLAChecker
|
8 years ago |
|
Matthias Volk
|
fd1c9a586e
|
Add PLA support
|
8 years ago |
|
Matthias Volk
|
3c7a4b49a5
|
PmcResult is CheckResult + constraints
|
8 years ago |
|
Matthias Volk
|
cc837089aa
|
Small fixes in tests
|
8 years ago |
|
Matthias Volk
|
7342428c5e
|
Improved bisimulation test
|
8 years ago |
Tom Janson
|
2b9c4b61e7
|
fix version info binding
|
8 years ago |
|
Tom Janson
|
f094216dce
|
crudely sanity-check instance matrix content
|
8 years ago |
|
Tom Janson
|
56ba8685d5
|
extract parametric prism program parse test
|
8 years ago |
|
Tom Janson
|
64701f79d0
|
more cosmetics
|
8 years ago |
|
Tom Janson
|
6652e4acf1
|
whitespace / PEP8
|
8 years ago |
|
Matthias Volk
|
20b1b01139
|
Bisimulation takes properties
|
8 years ago |
|
Matthias Volk
|
968901cca5
|
Change test for merged failed states
|
8 years ago |
|
Matthias Volk
|
9618b5ca31
|
Length for states and actions
|
8 years ago |
|
Matthias Volk
|
ed2875eb7d
|
Changed state and action for models
|
8 years ago |
|
Matthias Volk
|
c017949d0c
|
Use matrix instead of model for iterators
|
8 years ago |
|
Matthias Volk
|
26d2b90f44
|
Bindings for state labeling
|
8 years ago |
|
Matthias Volk
|
64c663a809
|
Started with Python bindings for storm-dft
|
8 years ago |
|
Matthias Volk
|
db86de9443
|
Bindings for importing DRN files
|
8 years ago |
sjunges
|
4bfa6776ed
|
prob01min and prob01max now map on prob01 for dtmcs
|
8 years ago |
|
sjunges
|
ac9a233aaf
|
ModelInstantiator for MDP & DTMC
|
8 years ago |
Sebastian Junges
|
9272bffea4
|
extended test
|
8 years ago |
|
Sebastian Junges
|
116245ecbb
|
property constructor from formula
|
8 years ago |
|
Sebastian Junges
|
93a5346c70
|
Prob 01 states also on MDPs and parametric models
|
8 years ago |
|
Sebastian Junges
|
e7db19154d
|
tests updated
|
8 years ago |
|
Matthias Volk
|
95f83a7224
|
Binding for CheckResult
|
8 years ago |
|
Sebastian Junges
|
32eae51b16
|
first working test for model instantiator
|
8 years ago |
|
Matthias Volk
|
724de252e4
|
1st version of computing prob01 states
|
8 years ago |
|
Matthias Volk
|
008a780a9d
|
Added test cases for BitVector
|
8 years ago |
|
Tom Janson
|
09b2bfcf67
|
add ShortestPathsGenerator method binding (and fancy test fixture)
|
8 years ago |
|
Tom Janson
|
5b782b5ca7
|
add ShortestPathsGenerator matrix/vector ctor bindings
|
8 years ago |
|
Tom Janson
|
1dd14e6e80
|
simplify KSP test fixture names
|
8 years ago |
|
Tom Janson
|
b85f6ae1da
|
fix KSP test model fixture scope
|
8 years ago |
|
Tom Janson
|
6f347ee354
|
add ShortestPathsGenerator binding (ctors, TODO: rest)
|
8 years ago |
|
sjunges
|
461951c52e
|
test files are part of stormpy lib now, which allows simpler access to them via stormpy.examples.files
|
8 years ago |
|
Matthias Volk
|
ad65f009ad
|
Build from prism program has default formulas = []
|
8 years ago |
|
Tom Janson
|
2c57642ca0
|
use math.isclose for float comparison asserts
|
8 years ago |
|
Sebastian Junges
|
2bd01d022f
|
examples added
|
8 years ago |
|
Sebastian Junges
|
0c79aba2c7
|
extracted from storm repo, refactored formula
|
8 years ago |
