Tim Quatmann
bc623d1203
MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler.
Renamed the 'hasNoEndComponents' solver requirement to 'hasUniqueSolution' as this is the actual thing we require for, e.g. sound value iteration.
7 years ago
TimQu
208ee76edb
storm-pars: Added possibility to compute the extremal value within a given region using parameter lifting.
7 years ago
dehnert
a08cb4ac18
making game solver respect equation solver format
8 years ago
dehnert
d557ef1075
started to make game solver flexible enough to also solve the (explicit) games of game-based abstraction
8 years ago
TimQu
3310f51857
allowed for more fine grained solver requirements
8 years ago
TimQu
69a27ddad6
fixed compiling storm-pars
8 years ago
TimQu
02d2cf07b6
using multiplier in PLA
8 years ago
Sebastian Junges
5a62a60e17
fix in pla without simplifications allowed
8 years ago
TimQu
a2bd1e0026
renamed argument from getRequirements so that it is easier to understand
8 years ago
TimQu
355510c808
Fixed call of wrong 'specify' method
8 years ago
TimQu
eab7e409e9
Fixed Running PLA without simplification
8 years ago
Sebastian Junges
8cd3f1bc1a
added a switch to disable simplifications within PLA
8 years ago
TimQu
ebeb34b791
implemented heuristic for pla that helps to decide with respect to which parameters a region should be splitted
8 years ago
TimQu
45279f9914
storm-pars compiles now
8 years ago
TimQu
bb63ac6089
Linear equation solver + game solvers now respect the environment as well
8 years ago
TimQu
b10dcce21a
fixed 'canHandle' method in pla checker
8 years ago
TimQu
dcef30104c
storm-pars compiles again
8 years ago
TimQu
31ba64f018
bugfixes
8 years ago
dehnert
edec805e37
added some missing clone functions for check results
8 years ago
TimQu
33585c811f
MinMax Solver requirements now respect whether the solution is known to be unique or not.
9 years ago
TimQu
a9a1c4feed
Region model checker can now also return a (quantitative) upper/lower bound for a given region
9 years ago
TimQu
5ad60051c3
Region model checker can now also return a (quantitative) upper/lower bound for a given region
9 years ago
TimQu
f83dbf741b
fixed wrong template argument
9 years ago
TimQu
50ba6866eb
checking solver requirements for PLA
9 years ago
TimQu
4991a3ec5e
checking solver requirements for PLA
9 years ago
dehnert
d8d3404b87
fixed termination criteria and equipped interval value iteration methods with check whether the method converged for the relevant states
9 years ago
dehnert
3c4de8ace3
moved requirements to new file
9 years ago
TimQu
39549f6ebd
Moved some functionality of StandardMinMaxSolver into a subclass
9 years ago
TimQu
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
9 years ago
Sebastian Junges
3de51e28e5
towards reward-bounded properties
9 years ago
TimQu
68213ace06
fixed computation of player 1 matrix for parameter lifting on pMDPs with infinite reward at some states
9 years ago
TimQu
ed550e6255
fixed invocation of instantiation checkers
9 years ago
TimQu
f2294fadb0
fixed compiling storm-pars cli and improved output a little
9 years ago
TimQu
1dd8cc2d3f
Added Validating Parameter Lifting region model checker
9 years ago
TimQu
9350187895
Fixed tests
9 years ago
TimQu
62d50b336b
Moved parametric model simplification inside the Parameter lifting checker
9 years ago
TimQu
9f82c34429
storm-pars library
9 years ago
TimQu
c7b83ffb5f
moved parameter lifting related code out of the main library/executable
9 years ago