storm
storm copied to clipboard
Missing handling of terminal states for POMDPs
States that are marked as terminal while building a POMDP model (for example due to violating the left-hand side of an Until) are not handled appropriately. By default, for terminal states, only one self-loop without action label is added. This, however, may lead to violation of the requirement that states with the same observation must have the same actions enabled.
This can be worked around with by using option --buildfull
, but terminal states should be handled properly to reduce model building times.
This issue is based on the discussion on issue #48.