Redundant output displayed by Storm

[HubertGaravel]

Hi,

Storm displays twice the same group of 14 lines, surrounded by dashes
(see below).

I guess that this is expected to be the model before pre-processing and
the model after pre-processing.

But in the case pre-processing is not done, or not effective (the log
indicates it takes 0 seconds), it is superfluous to repeat the same
piece of text twice. This is painful when many models and formulas
are verified in sequence, e.g., using a shell script.

A single line of text ("pre-processing was not applied" or "pre-processing
made no change") would be sufficient and more helpful than repeating
the text and letting the reader examine all lines to know if changes occur.

`Storm 1.9.0

Date: Sun Nov 17 09:34:34 2024
Command line arguments: -v --prism 56_0007_010.ma --prop 5.prop
Current working directory: /home/user/MA

Time for model input parsing: 2.305s.

INFO (properties.cpp:36): Loading properties from file: 5.prop

Explored 1760 states in 5 seconds (currently 352 states per second).
Explored 3575 states in 10 seconds (currently 363 states per second).
Explored 5206 states in 15 seconds (currently 326 states per second).
Explored 6699 states in 20 seconds (currently 298 states per second).
Explored 8118 states in 25 seconds (currently 283 states per second).
Time for model construction: 27.194s.

---

Model type: Markov Automaton (sparse)
States: 8560
Transitions: 36427
Choices: 9224
Markovian St.: 8008
Max. Rate: 146.16404
Reward Models: none
State Labels: 3 labels

• deadlock -> 0 item(s)
• init -> 1 item(s)
• avail -> 6145 item(s)
  Choice Labels: none

---

Time for model preprocessing: 0.000s.

---

Model type: Markov Automaton (sparse)
States: 8560
Transitions: 36427
Choices: 9224
Markovian St.: 8008
Max. Rate: 146.16404
Reward Models: none
State Labels: 3 labels

• deadlock -> 0 item(s)
• init -> 1 item(s)
• avail -> 6145 item(s)
  Choice Labels: none

---

`

[volkm]

Dear Hubert,

thanks for the report.
The second part for the preprocessing usually only occurs if some pre-processing took place (for instance bisimulation minimization). For MAs, we apply the maximal progress assumptions which allows to remove Markovian transitions in some cases. I agree that a second output only makes sense if this pre-processing actually lead to a change.

I will look into it.

[tquatmann]

By the way: maximal progress is already enforced during model construction, so it is very common that enforcing this again during preprocessing has no effect.

We still need to do this, e.g., for DRN models