Exact mode should check probability sums in DTMCs

[kleinj]

The parametric model builder that is used as well for the exact engine of PRISM normalizes the probabilities by dividing by the sum of the outgoing probabilities. Thus, in the exact mode, for

dtmc

module M1
  s: [0..2] init 0;

  [] s=0 -> 1/3:(s'=1) + 1/3:(s'=2);
  [] s>0 -> true;
endmodule

and -pf 'P=?[ F s=1 ]' -exact the result will be 1/2, as the actual probabilities in the model will be (1/3) / (2/3) = 1/2. In contrast, the symbolic and explicit engine report an error, as the probabilties don't sum to one.

Suggested fix: Provide the param engine with a flag that tells it whether it's in exact or parametric mode (depending on whether it's called from checkParametric or checkExact). In exact mode, don't normalize and throw an error when the sum of outgoing probabilities (as a BigRational) does not equal 1 for a DTMC or MDP.

[davexparker]

Do we know why it normalises?

[kleinj]

Well, my guess would be that it makes the underlying assumption for the parametric checking (no changes in graph structure due to parameter changes, the result of inserting the parameter values result in a DTMC, i.e., outgoing transitions sum to 1) easier to enforce. I.e., if you have

  [] s=0 -> p:(s'=1) + q:(s'=2);

it would implicitly treat that as p/(p+q) and q/(p+q) which maintains the second assumption automatically. The first assumption (no graph changes) would not hold for (p+q) = 0 but that is currently not checked / reported.

However, arguably, the solution would not actually be a solution in the sense that you could plug in any value in the valid region as a constant into the PRISM model file and obtain a working model that satisfies the property... I guess that should be documented. Or we could have two modes, one with normalization and one without and then actually determine the constraints on the parameters where both assumptions are actually valid.

[davexparker]

OK, i just realised that it should normalise. The PRISM semantics for a DTMC is to normalise across commands to deal with local nondeterminism. So the problem is not that it normalises, but that it fails to check that the individual commands have probabilities summing to 1.

[kleinj]

Have a look at

https://github.com/prismmodelchecker/prism-svn/compare/master...kleinj:issue-6?expand=1

for a proposed fix for this issue.

[kleinj]

We now throw an error if the outgoing sum (for DTMC and MDP) does not sum to 1 (exact mode) or if the parametric function for the outgoing sum is not equal to 1. This check can be disabled using the '-noprobchecks' option.