Support for has_cycle() on sparse models #103
Conversation
| } | ||
| } | ||
| } | ||
| return storm::utility::graph::hasCycle(matrix, subStates); |
There was a problem hiding this comment.
This is problematic for MDPs, when we have one self-loop row first and then one non-selfloop row which induces a cycle with other states, right?
I think the "hasCycle" would need to have a "subChoices" input to make this work?
Alternatively, this method could also build an SCC decomposition and we then check if each SCC has size 1.
There was a problem hiding this comment.
You are right, this is indeed problematic.
I am open for other suggestion. The SCC decomposition might be a good idea.
I actually just wanted to have a simple function to check for acyclity. Unfortunately, hasCycle is not exactly giving me what I want. Maybe it makes sense to implement a better function in Storm directly.
|
Shall we close this PR? |
|
Yes, we can close it. |
3 participants
Checking whether a model is acyclic should be quite helpful.
Note that the current implementation first needs to find and exclude all states with self-loops, because the underlying Storm function is considering self-loops as cycles.
Thanks to @jipspel for some help.