Minor improvements for steady-state properties:

[tquatmann]

• Allow using topological solvers when computing steady-state probabilities in a BSCC with the EVT-based approach.
• Streamline CLI output and handle non-default filter types

For example, this invocation shows us the fraction of time each individual philosopher eats:

storm-debug --jani philosophers4.jani --steadystate  --exact --prop 'filter(sum,eat1=1,true); filter(sum,eat2=1,true); filter(sum,eat3=1,true); filter(sum,eat4=1,true)'
Storm 1.8.2 (dev)
DEBUG BUILD

Date: Tue Aug 20 11:30:08 2024
Command line arguments: --jani philosophers4.jani --steadystate --exact --prop 'filter(sum,eat1=1,true); filter(sum,eat2=1,true); filter(sum,eat3=1,true); filter(sum,eat4=1,true)'
Current working directory: /Users/tim/philosophers

Time for model input parsing: 0.003s.

Time for model construction: 0.016s.

-------------------------------------------------------------- 
Model type: 	CTMC (sparse)
States: 	29
Transitions: 	72
Reward Models:  none
State Labels: 	6 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * (eat4 = 1) -> 7 item(s)
   * (eat3 = 1) -> 4 item(s)
   * (eat2 = 1) -> 3 item(s)
   * (eat1 = 1) -> 5 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Computing steady-state probabilities ...
Result (for '(eat1 = 1)' states): 1264485277/16384334634 (approx. 0.07717648017)
Result (for '(eat2 = 1)' states): 1264485277/16384334634 (approx. 0.07717648017)
Result (for '(eat3 = 1)' states): 2498293909/16384334634 (approx. 0.1524806448)
Result (for '(eat4 = 1)' states): 726880166/2730722439 (approx. 0.2661860303)
Time for model checking: 0.002s.

[sjunges]

I dont understand this last call?

[tquatmann]

Essentially, this disables topological optimizations by setting the current linear equation solver to the one that the topological solver would use to solve the SCCs. More specifically, we set the equation solver type and whether it has been set explicitly by the user (e.g. via --topological:eqsolver native).

[sjunges]

I get generally a bit confused by this; this means that as a user (via CLI or API) I set a method, but the code overrides it and selects another solver. I wonder whether a user can understand this (and whether they have to).

(I am a bit afraid for statements like "We set storm to use topological ... " when Storm than does not use this topological optimizations, for good reasons).

[tquatmann]

I think we want the same thing. When a user enables topological optimizations, the intention should be to use topological optimizations whenever possible.

This was not the case with the previous code because we accidentally disabled topological solving in cases where it could have some benefit.

With this PR, we "fix" that by overwriting the user input only in cases where topological optimizations are known to be impossible (because the considered states are known to be strongly connected).

From a user perspective, disabling topological solving at this point does not make any difference (except maybe a performance improvement because we avoid an unnecessary graph analysis and a matrix copy)

To summarize, my aim here is to disable topological optimizations if and only if they would not have any positive effect.

[sjunges]

I dont disagree with this PR, but I have a more general discussion that we can have elsewhere :-)

[sjunges]

For future reference, can you clarify what "fix" means in algorithm selection. In terms of: who or what is affected by this fix?

[tquatmann]

Ahh I see. Basically there are two approaches to compute the steady state distribution in a BSCC.

1. Solve the "standard" linear equation system
2. apply a transformation to a new DTMC and compute expected visiting times on that DTMC (by solving a different linear equation system).

For the first case, topological optimizations are not reasonable since the equation system is always fully connected.
In the latter case, however, the transformed DTMC might have multiple SCCs, so topological optimizations can help.

The old code disabled topological optimizations in both cases. The PR "fixes" this so that topological optimizations can be used in case 2.

I edited the PR description a bit.

[sjunges]

LGTM