Leaking Gaz Burner: FAST Encoding




Three integer variables are used: l as leak for the cumulated leak, t as global system time for the seconds and x as state timer.
When in its first state, the gaz burner is leaking, but it cannot leak forever and, after a while, it reaches its non-leaking state. Then again, it starts leaking.
Numerical constants control the transitions between the leaking and non-leaking states. The system cannot be in the leaking state more than a numerically given amount of time (9 below). And the system must stay in the non-leaking state for more than another given amount of time (50 below).


model gb {

var l, t, x;

states ell,hen;

transition t1 := {
 from   := ell;
 to     := ell;
 guard  := x<=9;
 action := l'=l+1,x'=x+1,t'=t+1;
};

transition t2 := {
 from   := ell;
 to     := hen;
 guard  := true;
 action := x'=0;
};

transition t3 := {
 from   := hen;
 to     := hen;
 guard  := true;
 action := t'=t+1, x'=x+1;
};

transition t4 := {
 from   := hen;
 to     := ell;
 guard  := x>=50;
 action := x'=0;
};


}

strategy s1 {

Region init := {state=ell && t=0 && l=0 && x=0};

Region bad := {6l>t+50};
}