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 (see Clarify 'dontFixDeadlock' option description #804)
• 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. (They are checking for Zenoness, see Storm --additional-checks #803).

[Philipp15b]

Out-of-bound-states give an operational meaning to a state that is out of bounds.

What happens otherwise if the model checker occurs out-of-bounds states? Undefined behavior? An acceptable behavior would also be stopping Storm with an error.

[sjunges]

Prism models that go out of bounds are ill-defined models and as such, you have no guarantees.

[Philipp15b]

What would be the best way to "fail hard" when out-of-bounds states are found during exploration? Would one need to manually adapt all properties to handle extra states generated by --[build:]build-out-of-bounds-state?

[sjunges]

sys.call("rm -rf /")exit(-1000);

More seriously: I would check where those states are added (in the builder/generator) and raise an exception whenever we would be generating such a state.

[Philipp15b]

You'll want --no-preserve-root on that rm -rf / :)

Thanks for the pointer. If I follow the source code correctly, it seems like there are already exceptions thrown in those cases when BuilderOptions::isExplorationChecksSet() == true, i.e. when --build:explchecks is set?

https://github.com/moves-rwth/storm/blob/8fdf1fc728dcb9c16257a878e437548675caa743/src/storm/generator/JaniNextStateGenerator.cpp#L404-L413

So it seems like I just want --build:explchecks for those out of bounds checks instead of --[build:]build-out-of-bounds-state; the former is exactly what I want. Thanks!

[volkm]

It seems that exploration checks and additional checks could maybe be combined.

I agree with the point that all relevant checks should be accessible in Release mode such that everybody can use then.

[sjunges]

Philipp, you know this is an open source project, right. If things are important to you than you change them, or you convince us to change them. In particular, convincing me to change things is not about whether you are right, but whether your requests are the most important to me.

[Philipp15b]

Philipp, you know this is an open source project, right.

Thanks, this clarification was constructive.

but whether your requests are the most important to me.

Either you care about these problems, or you don't. I am simply trying to find out what can be done to enable pedantically sound model checking of probabilistic models, where by pedantically sound I mean the aspects outlined above. In particular, I still hope these changes can be done minimally invasively by having a --pedantic flag which only enables a bunch of existing features correctly, not much more. I am happy to attempt to do these changes by myself, once I know what to do!

[sjunges]

Caring for a problem is not a Boolean...

Either way, I think that adding a pedantic flag is a good idea. It is not completely clear where to draw the line though, note that by saying that something is pedantically sound, you are also raising expectations. I would suggest to err on the safe side, that is, first let it imply exact and set the exploration checks. If you really want to err on the safe side, you should probably disallow most other options as they may override things....

Note that our medium-term plan is to move the settings purely into the cli and out of the rest of the code.

[sjunges]

Additionally, the fact that I am extremely unclear where to even find these constraints makes it even more important to me to have these checks automated. I think everyone would be happy to see a formal definition of the latest variant of the prism language, but we are not the inventors of this language nor is it my priority to formalise this.

[Philipp15b]

I mostly use the JANI format, and will try my best to convince any of its authors to consider these issues. However, as explained above, I think even just stopping Storm with an error message on a possible overflow is sufficient for my design of the pedantic mode. This would not require any adaptions of formal semantics and would ideally use existing Storm features.