Pedantic mode

[Philipp15b]

Hello Team Storm!

Because this conversation keeps coming up internally (brought up by me 😂), I'd like to suggest a new --pedantic flag to Storm which enables...

• a sound algorithm to compute results (not standard value iteration)
• either rational arithmetic or sound rounding or sound checking (via certificates?) of floating-computed values
• explicit overflow checks (under what circumstances does model exploration have undefined behavior w.r.t. over-/underflow/other arithmetic?)
  • Both for explicitly bounded integers, as well as "unbounded" integers (which seem to have a default precision of 32 bits?)
• I have also heard that building in DEBUG mode enables additional checks. Are these potentially valuable as well?

If valuable checks are only available in DEBUG mode, then --pedantic should always crash with an error in RELEASE mode.
Similarly, if some specific problem could only be tackled by an implementation which cannot give sound results, Storm should exit with an error.

In short, I'd like the pedantic flag to enable as pedantic computations as possible. Maybe there are more choices you can come up with?
To be clear, the pedantic flag should only guarantee pedantic soundness modulo Storm bugs.
To enable all of the additional checks for debugging, there could be another --paranoid flag? :)

More on some individual flags I found:

• --exact also, as I understood, switches the solver to an equation solver instead of e.g. (sound?) value iteration in addition to switching to rational arithmetic.

  • I often just want sound approximations and do not need actually exact results.

• --[build:]nofixdl (ndl) ............................................. If the model contains deadlock states, they need to be fixed by setting this option.

  The name suggests otherwise, but according to the description one needs to set this flag to properly handle deadlocks?

• --[build:]explchecks (ec) ........................................... If set, additional checks (if available) are performed during model exploration to debug the model

  What are these additional checks?

• --[build:]build-out-of-bounds-state ................................. If set, a state for out-of-bounds valuations is added

  This seems to be the option for out of bounds checks?

• --[debug:]additional-checks ......................................... If set, additional sanity checks are performed during execution.

  Are these just for debugging Storm internally or are these additional checks on the model that might affect soundness?

[volkm]

Hi Philipp,
thanks for the suggestion.
I think there are two parts we could streamline a bit:

1. Model building. We currently only do some checks during the model building but disable some more expensive checks for sake of performance. Here I agree that one flag to enable all checks would be useful.
2. Model checking. Typically setting the --exact flag will ensure that only sound methods are used. In case of floating point numbers, the flag --sound should use sound methods with guaranteed error bounds.

[sjunges]

Hey,

thanks for the suggestion. More strongly, I do believe that there is no reason to ever have an unsound method (modulo floating point) should ever be default. Regarding floating point vs other implementations: Here I personally think that it should be up to the users. I can imagine that --pendantic disables floating-point representations of models (what would sound rounding of 0.3333 on the input of a model even mean?).

More generally, I think there are two parts to storm and it may potentially be good to split the discussion.

The first is about verifying a given MDP inside the storm data structures, the second is about how you specify this MDP.

If you insert an MDP into the storm data structures, then checking whether it is a valid MDP and the verification routine itself are two individual questions. I agree that a pendantic mode should check whether an MDP is indeed well-defined and I think this should be possible, but note that this may be not that easy: For example, if the user has a floating point representation of the MDP in mind, when is the MDP well-defined? Sure, one could say that pendantic does not support specifying MDPs in floating points, but other questions arise as well: Is a MDP with deadlocks a valid MDP (with the interpretation that deadlocks are just self-loops?)

However, fixing this first point gives you no guarantee at all that the MDP inside storm is the MDP you had in mind.
That is, the second point is about modelling languages. Storm takes the point that a model needs to satisfy a bunch of constraints and that otherwise, its behavior is undefined. This mostly stems from the fact that storm, in the end, relies on c++ to evaluate expressions. So, the semantics of higher-level modelling languages are interpreted in terms of c++ semantics, for better or worse.

Finally, I do think you cannot expect pendantic mode to only work in debug compilations: I don't want to compile Storm myself in debug mode just because I want to use pendantic mode and it is completely understandable that code in debug mode has way more (useful) checks. You would basically tell people to not use storm in release mode.

• The nofixdl is indeed swapped in terms of description. The default is to fix deadlocks by self-loops
• Exploration checks are a variety of checks regarding typing and bounds.
• Out-of-bound-states give an operational meaning to a state that is out of bounds. The idea here is that you can say that there is a unique global (meta) state that contains all states that are out of bounds. You can use this to use the model checker to find a path to an out-of-bounds state and/or understand how much probability mass actually goes out of bounds. This can be useful for debugging purposes, or if you want to cut your model size.
• I don't know what additional checks are doing.