Add --not-graph-preserving flag

[linusheck]

Why this flag

I ran into the issue that bisimulation chooses the measure-driven initial partition mode for until formulas, which assumes that all instantiations of a parametric model are graph-preserving. I added a flag --not-graph-preserving to storm-pars which changes this mode to the label-based initial partitions. It further throws an error when trying to compute a solution function, which also assumes that all instantiations are graph-preserving. If the input region appears to be non-graph-preserving (we cannot know for sure) and the flag is not set, I added a warning. This is currently not reachable, as parseRegions throws an error anyway, as no methods are currently implemented that support non-graph-preserving regions.

Demonstration

Consider the following pMC:

dtmc

const p;

module nongraphpreserving
	s : [0..3] init 0;
	
	[] s=0 -> p : (s'=1) + 1-p : (s'=3);
	[] s=1 -> p : (s'=1) + 1-p : (s'=2);
	[] s=2 -> 1 : (s'=2);
	[] s=3 -> 1 : (s'=3);
endmodule

label "target" = s=2;

Behavior of storm:

./bin/storm-pars --prism non_graph_preserving.pm -prop "P=? [F \"target\"]" --mode sampling --samples "p=1"
Result (initial states) for instance [p=1]: 0

# Incorrect result when using bisim without the flag
./bin/storm-pars --prism non_graph_preserving.pm -prop "P=? [F \"target\"]" --mode sampling --samples "p=1" -bisim
Result (initial states) for instance [p=1]: 1

./bin/storm-pars --prism non_graph_preserving.pm -prop "P=? [F \"target\"]" --mode sampling --samples "p=1" -bisim --not-graph-preserving
Result (initial states) for instance [p=1]: 0

Original pMC:

after incorrect transformation:

[sjunges]

Hi,

I do see the need to differentiate where we make the graph-preserving assumption and where not. The fix for the bisim is good.
However, I am not convinced by the semantics of this flag/what the default is.

In my understanding, it should be clear from the command line whether we assume graph-preserving or not.
For example, the solution function as we compute it currently maps only graph-preserving instantiations to values. We should maybe be explicit about it, but the function is otherwise not a function.

I can imagine that we want to be more liberal and say that the function is a general mapping, then we should throw an error if it the algorithm does not preserve the correctness.

In those cases, I would then expect a flag --assume-graph-preserving that a user can add to sstill get a result, if that is intended.

Sebastian

[linusheck]

Do you mean we should always throw an error when computing the solution function except when the user specifies --assume-graph-preserving? That's what I wanted to avoid by making the flag negative.

[sjunges]

I think for solution functions you could say that the semantics of that operation is to generate a mapping from graph-preserving fragment. In the past, we also sometimes explicitly exported/printed the graph-preserving models.

However, I am not too afraid of throwing an error if that makes things explicit.

[linusheck]

Ok! Another thought: we would change the default behavior of storm-pars then. So omitting the --assume-graph-preserving flag would have bisim be less powerful so it can preserve graph preservingness, but then the solution function is invoked which does assume it, which might give different answers than before.

[linusheck]

If we add --assume-graph-preserving, Storm should still automatically check whether the region is graph-preserving and if so, run everything in graph-preserving mode.