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}; }