Added output of MEC statistics.

[tquatmann]

When computing reachability probabilities or expected total reachability rewards, the MEC quotient of the "maybestates"-subsystem might be computed (either because it is required by the used algorithm or because the user has set the --force-require-unique. If this is the case and the --verbose has been set, some interesting statistics on the MECs will now be printed.

This is only relevant for Pmax or Rmin queries.

storm-debug --prism sen3.prism --prop 'Pmax=? [ F  x=1 ]' --force-require-unique --verbose
Storm 1.8.2 (dev)
DEBUG BUILD

Date: Wed May 29 09:38:50 2024
Command line arguments: --prism sen3.prism --prop 'Pmax=? [ F  x=1 ]' --force-require-unique --verbose
Current working directory: /Users/tim/git/diss/benchmarking/multi/models/sen

Time for model input parsing: 0.024s.

Time for model construction: 2.153s.

-------------------------------------------------------------- 
Model type:     MDP (sparse)
States:     66051
Transitions:    263526
Choices:    245802
Reward Models:  none
State Labels:   3 labels
   * init -> 1 item(s)
   * deadlock -> 0 item(s)
   * (x = 1) -> 2508 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": Pmax=? [F (x = 1)] ...
 INFO (SparseMdpPrctlHelper.cpp:699): Preprocessing: 5016 states with probability 1, 12969 with probability 0 (48066 states remaining).
 INFO (SparseMdpPrctlHelper.cpp:649): MEC decomposition statistics: There are 21016 MECs out of which 18108 are trivial, i.e., consist of a single state. 38868 out of 66051 states (58.8454%) are on some MEC. 20760 states (31.4303%) are on a non-trivial mec. The smallest non-trivial MEC has 2 states and the largest non-trivial MEC has 330 states.
 INFO (TopologicalMinMaxLinearEquationSolver.cpp:69): SCC decomposition computed in 0.021s. Found 29410 SCC(s) containing a total of 30214 states. Average SCC size is 1.02734.
Result (for initial states): 0.992
Time for model checking: 3.895s.

[sjunges]

LGTM!