Hang in simulator on CTMC with terminal state

[kleinj]

Trying to replicate the bug report in https://sourceforge.net/p/prism-mc/bugs/20/, I stumbled upon another bug: The simulator hangs indefinitely sampling a path for the second property.

bug.prism:

stochastic

const int M; // number of possible elements of FGF

const double k5=1; // an hour

 module SYSTEM

        reloc : [0..M] init 0; // relocated FGFR

        [] reloc<M -> k5 : (reloc'=reloc+1);
//      [] true -> k5 : (reloc'=min(M,reloc+1));

endmodule

bug.props:

const int L;
const double T;

P=? [ true U<=T reloc>=L ]
P=? [ true U[T,T] reloc>=L ]

Invocation:

prism bug.prism bug.props -fixdl -const L=0,T=100,M=10 -sim -simsamples 100 -simpathlen 1000

Observed behaviour: PRISM does not terminate.

[kleinj]

The problem appears to be the following: In SimulatorEngine.doSampling, the method automaticTransition is iteratively called as long as there are samplers that have an unknown value and as long as the maximal path length is not yet exceeded. However, if the path formula has a time / step bound, then the maximal path length is ignored.

If the current state of the path is a deadlock state (as for reloc=M in the model), automaticTransition fails, returning false. In particular, the samplers are not updated and the sampler for P=?[ true U[T,T] reloc>=L] will never signal success/failure; the loop will continue indefinitely.

Possible fixes:

• Check the return value of automaticTransition and simply break out of the loop. This leads to the error message Error: One or more of the properties being sampled could not be checked on a sample. Consider increasing the maximum path length. This is might be adapted to indicate the problem with the deadlock.
• Silently handle the deadlock, i.e., just extend the path by a self-loop transition. Might be worthwile to discuss in which situations that should happen (only for CTMCs? only with explicit -fixdl flag?)