storm icon indicating copy to clipboard operation
storm copied to clipboard

Elimination with Policy Iteration potentially broken

Open sjunges opened this issue 4 years ago • 0 comments

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\"]"  

sjunges avatar Sep 22 '20 22:09 sjunges