15 lines
451 B
Text
15 lines
451 B
Text
node Valve
|
|
state rate : [0,2] : public;
|
|
stucked : [0,1] : public;
|
|
init rate := 0;
|
|
stucked := 0;
|
|
event dec, inc;
|
|
trans stucked=0 |- dec -> rate := rate - 1;
|
|
stucked=0 |- inc -> rate := rate + 1;
|
|
stucked=0 & rate=0 |- dec -> ;
|
|
stucked=0 & rate=2 |- inc -> ;
|
|
/* a problem may appear */
|
|
stucked=0 |- dec, inc -> stucked := 1;
|
|
/* After the failure, the valve is stuck */
|
|
stucked=1 |- dec, inc -> ;
|
|
edon
|