storm
storm copied to clipboard
Elimination with Policy Iteration potentially broken
Hi,
when trying to combine policy iteration with state elimination, I run into the following bug. Is this combination of methods somehow not a good idea, or does this force the elimination solver in a corner case?
Best, Sebastian
Command line arguments: -drn unrolling.out --prop 'Pmax=? [F "_goal"]' '--minmax:method' pi --eqsolver elimination
Time for model construction: 0.004s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 17
Transitions: 36
Choices: 20
Reward Models: none
State Labels: 2 labels
* init -> 1 item(s)
* _goal -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "1": Pmax=? [F "_goal"] ...
ERROR (EliminatorBase.cpp:51): The scaling mode 'divide-one-minus' requires a non-one value in the given column.
Assertion failed: (columnValue != storm::utility::one<ValueType>()), function eliminate, file storm/solver/stateelimination/EliminatorBase.cpp, line 51.
ERROR: The program received signal 6 and will be aborted in 3s.
[1] 85131 abort storm -drn unrolling.out --prop "Pmax=? [F \"_goal\"]"