Additional timelock check

[SchneiderSven]

Setting

According to the manual on PTA, PRISM assumes that the given PTA has no timelocks. However, it is said as well that PRISM also checks for timelocks and reports an error if one is found.
Obviously, this is just best effort as forward (games) and backward algorithms do not always traverse even all reachable states.

Problem

PRISM does not detect the following kind of timelock.

Example

A location (s=0 in the following example) with an invariant (x<=20 in the following example) preventing the further passage of time while there are transitions exiting this location but which are all disabled because some of their edges (the edge to s=2 in the following example) leads to a location with an invariant (y<=10 in the following example) that would be violated when that edge would be taken to late (e.g. at x=20 in the following example).

pta

module M

        s : [0..5] init 0;
        x : clock;
        y : clock;

        invariant
                (s=0 => x<=20)
                &(s=2 => y<=10)
        endinvariant

        [] s=0 & x>=1 ->
                  0.5:(s'=1)&(x'=0)&(y'=1)
                + 0.5:(s'=2)&(x'=0);
        [] s=2 & y=10 -> (y'=0);

endmodule

Checking the property Pmax=? [ F s=2 ] would then fail describing the timelock:

Output with changed code

Building forwards reachability graph...
Error: Badly formed PTA at location (s=0) when {0<=x<=20,0<=y<=20,x=y} has exiting transitions but all may be disabled by the invariants of some of their targets..

Explanation of code for example

What happens is as follows for the edge to s=1

// LocZone before the step
SS1: ((s=0),{0<=x<=20,0<=y<=20,x=y})
// LocZone after the application of the edge
SS2: ((s=1),{x=0,y=1,x-y=-1})
// Cloned
SS3: ((s=1),{x=0,y=1,x-y=-1})
// LocZone after undoing the step; some information on y and the relation to x is now lost but from each valuation belonging to that zone, we may got to the LocZone from the previous line.
SS4: ((s=0),{1<=x<=20,y>=0,x-y<=20})
// Complement: We cannot go to the LocZone with s=1 from above from any of these valuations
SS4b: [{0<=x<1,y>=0,x-y<1}, {x>20,y>=0}]
// However, we know that the guard is satisfied and we are in the initial LocZone for s=0 and no step is possible? First add the guard to eliminate the first variant in which x is too small for the guard.
SS5: [empty, {x>20,y>=0}]
// Now we check add the initial LocZone for s=0 and exclude by that the second area describing valuations for which we cannot apply the edge.
SS6: []
// The result is empty, so the edge can always be applied according to the invariant of the target state (which is trivially true here).

What happens is as follows for the edge to s=2

// now the same procedure as above.
SS1: ((s=0),{0<=x<=20,0<=y<=20,x=y})
SS2: ((s=2),{x=0,1<=y<=10,-10<=x-y<=-1})
SS3: ((s=2),{x=0,1<=y<=10,-10<=x-y<=-1})
// this is where we may start from
SS4: ((s=0),{1<=x<=20,1<=y<=10,-9<=x-y<=19})
// Complement: all versions where the guard is not satisfied, where y is too large, where x is too large, or where x and y cannot be equal.
SS4b: [
	{0<=x<1,y>=0,x-y<1}, // guard not satisfied
	{x>=0,0<=y<1,y-x<1}, // x cannot be equal to y
	{x>20,y>=0}, // x is too large
	{x>19,y>=0,y-x<-19}, // x cannot be equal to y
	{x>=0,y>10}, // y too large! basically the violation
	{x>=0,y>9,x-y<-9} // x cannot be equal to y
	]
// now we have added the guard and some versions are removed	
SS5: [
	empty, 
	{x>=1,0<=y<1,y<x}, // x cannot be equal to y
	{x>20,y>=0}, // x is too large
	{x>19,y>=0,y-x<-19}, // x cannot be equal to y 
	{x>=1,y>10} // y too large! basically the violation
	]
// now with the initial LocZone for s=0 all what remains is the problematic zone.
// every valuation in this zone 
// (a) was reachable from before as it is part of the initial LocZone for s=0 
// (b) satisfies the guard of the considered transition
// (c) cannot make a step using the given edge
// We see that the existence of the transition and the existence of a step from the initial LocZone for s=0 using that transition are not enough. Basically, the user should set the invariant to x<=10 for s=0.
SS6: [{10<x<=20,10<y<=20,x=y}]