9859f60db0
Fixed solver tests
8 years ago
f44ce8801c
"fixed" the tests that failed because of unsound value iteration
8 years ago
ea507a0b13
added dd-based partial quotient extraction for DTMCs
8 years ago
ab12e4ff3d
started on partial quotient extraction in symbolic bisimulation
8 years ago
c0f07557ed
simplified state signature computation in dd-based bisimulation
8 years ago
a427eae699
fixed severe bug in symbolic bisimulation minimization
8 years ago
45a4b63a2e
fixed some issue in sylvan sharpen and forward minmax bounds to linear equation solver
8 years ago
b09cb95254
fixed wrong call in sylvan double to rational number conversion
8 years ago
da02237769
work towards symbolic rational search
8 years ago
6e8465e9f1
started on symbolic rational search
8 years ago
df05711f3e
finished rational search for MinMax solver, preparing rational search for NativeLinearEquationSolver
8 years ago
36c3a4d9ef
Avoided conversion of memory states. They are now directly represented as 64 bit integers
8 years ago
cb849a9ab8
started on computing upper bounds for rewards for interval value iteration
8 years ago
ade8078759
added test for lower bounded properties
8 years ago
b054b67312
first version for lower bounded properties
8 years ago
bba2832e5b
finished Walker-Chae method
8 years ago
47ab74a16b
implemented single objective queries
8 years ago
8b466f1fa7
extended multidimensional bounded until formulas to have different subformulas in each dimension
8 years ago
c77b9ce404
gauss-seidel style multiplication for gmm++
8 years ago
00f88ed452
gauss-seidel-style value iteration
8 years ago
dd035f7f5e
allow for summand in matrix-vector multiplication
8 years ago
ff8c7813bb
commented out failing tests in the fragmentchecker
8 years ago
83fdffadc6
adapted tests; in particular enabled previously disabled rewards test
8 years ago
e81d979d56
hybrid MDP helper respecting solver requirements
8 years ago
e48c822941
fixed csma test
8 years ago
4adee85fa5
added checking requirements of MinMax solvers to model checker helpers
8 years ago
591a53582a
fixed test
8 years ago
e1aba323bf
more tests for reward unfolding
8 years ago
06ec288296
enabled pcaa test that uses rational numbers
8 years ago
172b17d7ae
simple testcase for the reward unfolding
8 years ago
d2a493a92d
fixed several crucial bugs related to dd bisimulation, tests now passing
8 years ago
a7dcdcd84d
started on tests and added a ton of debug output
8 years ago
d23547d99f
started optimizing some DdManager methods
8 years ago
50e1fe0c15
increment() function for BitVector
8 years ago
9ca14a54fc
templated the LpSolvers
8 years ago
e38ec10459
fixed permissive scheduler test (which is only compiled when gurobi is there)
8 years ago
31b5d77560
fixed expected results which have been too imprecise for the LP-based MinMaxLinearEquationSolver
8 years ago
6a986d2490
tests for MinMaxLinearEquationSolver
8 years ago
39549f6ebd
Moved some functionality of StandardMinMaxSolver into a subclass
8 years ago
11b9c60515
Adapted fragment checker test to new multiobjective-fragment specification
8 years ago
9591157996
new features for storm-pars api:
- depth limit for iterative refinement
- the regions with inconclusive result are now also part of the result
- when analyzing a region, a hypothesis (AllSat or AllViolated) can now be given
8 years ago
980f1864af
test cases
8 years ago
bb897a94c6
Moved ModelInstantiatorTest to storm-pars
8 years ago
4191d17f1e
Moved main testfiles into tests/storm/ and the storm-pars testfiles into tests/storm-pars
8 years ago
2f49255db6
Improved storage::Scheduler. We can now consider arbitrary finite memory schedulers, potentially employing randomization.
8 years ago
2794de2342
added missing include to make gcc happy
8 years ago
35c9b58fda
added a test case for SparseMatri::restrictRows and fixed it
8 years ago
ac566a64c3
Removed some whitespace
8 years ago
179cd8308e
remove old API files
8 years ago
ea02ea0838
started overhaul of cli/api
8 years ago
TimQu
dehnert
Sebastian Junges
Matthias Volk