Extended handling of terminal states for POMDPs

moves-rwth / storm

A Modern Probabilistic Model Checker

https://www.stormchecker.org

GNU General Public License v3.0

138 stars 75 forks source link

Extended handling of terminal states for POMDPs #617

Open AlexBork opened 2 months ago

AlexBork commented 2 months ago

This PR extends the handling of states marked as terminal in the PrismNextStateGenerator. In particular, terminal states in POMDPs are expanded with self-loops for all enabled actions, preventing erroneous behavior if there are other states with the same observation as a terminal state present in the model.

Resolves #603

tquatmann commented 4 weeks ago

I don't like the code duplication introduced here. However, I see that this is the lesser evil as the alternatives would be

doing this "properly"; requiring a more involved rewrite of the PrismNextStateGenerator or
ignoring the issue

LGTM