158 lines
4.9 KiB
Text
158 lines
4.9 KiB
Text
node ValvePerfect
|
|
state rate : [0,2] : public;
|
|
init rate := 0;
|
|
event dec, inc;
|
|
trans true |- dec -> rate := rate - 1;
|
|
true |- inc -> rate := rate + 1;
|
|
rate = 0 |- dec -> ;
|
|
rate = 2 |- inc -> ;
|
|
edon
|
|
|
|
node Valve
|
|
state rate : [0,2] : public;
|
|
stucked : bool;
|
|
init rate := 0;
|
|
stucked := false;
|
|
event dec, inc;
|
|
trans ~stucked |- dec -> rate := rate - 1;
|
|
~stucked |- inc -> rate := rate + 1;
|
|
~stucked |- dec -> stucked := true;
|
|
~stucked |- inc -> stucked := true;
|
|
stucked |- dec -> ;
|
|
stucked |- inc -> ;
|
|
rate = 0 |- dec -> ;
|
|
rate = 2 |- inc -> ;
|
|
edon
|
|
|
|
node Tank
|
|
state level : [0,4] : public;
|
|
init level := 2;
|
|
flow amont : [0,4];
|
|
aval : [0,2];
|
|
event time;
|
|
trans amont > aval |- time -> level := level + 1;
|
|
amont < aval |- time -> level := level - 1;
|
|
amont = aval & amont = 0 |- time -> ;
|
|
amont = aval & amont > 0 |- time -> level := level + 1;
|
|
amont = aval & amont > 0 |- time -> level := level - 1;
|
|
amont = aval & amont > 0 |- time -> ;
|
|
level = 4 & (amont > aval) |- time -> ;
|
|
level = 0 & (amont < aval) |- time -> ;
|
|
edon
|
|
|
|
node Ctrl
|
|
// les observations du controleur
|
|
flow r : [0,2][3];
|
|
l : [0,4];
|
|
event ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
|
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
|
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn;
|
|
trans
|
|
true |-
|
|
ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
|
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
|
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn
|
|
-> ;
|
|
edon
|
|
|
|
node SystemPerfect
|
|
sub V : ValvePerfect[3];
|
|
T : Tank;
|
|
//C : Ctrl;
|
|
C : Ctrl_SystemPerfect;
|
|
state ctrl : bool;
|
|
init ctrl := true;
|
|
// d pour dec, i pour inc, n pour nop
|
|
event action;
|
|
time;
|
|
trans
|
|
ctrl |- action -> ctrl := false;
|
|
~ctrl |- time -> ctrl := true;
|
|
assert
|
|
T.amont = (V[0].rate + V[1].rate);
|
|
T.aval = V[2].rate;
|
|
// liens avec le controleur
|
|
C.r[0] = V[0].rate;
|
|
C.r[1] = V[1].rate;
|
|
C.r[2] = V[2].rate;
|
|
C.l = T.level;
|
|
sync <action, C.ddd, V[0].dec, V[1].dec, V[2].dec>;
|
|
<action, C.ddi, V[0].dec, V[1].dec, V[2].inc>;
|
|
<action, C.ddn, V[0].dec, V[1].dec>;
|
|
<action, C.did, V[0].dec, V[1].inc, V[2].dec>;
|
|
<action, C.dii, V[0].dec, V[1].inc, V[2].inc>;
|
|
<action, C.din, V[0].dec, V[1].inc>;
|
|
<action, C.dnd, V[0].dec, V[2].dec>;
|
|
<action, C.dni, V[0].dec, V[2].inc>;
|
|
<action, C.dnn, V[0].dec>;
|
|
<action, C.idd, V[0].inc, V[1].dec, V[2].dec>;
|
|
<action, C.idi, V[0].inc, V[1].dec, V[2].inc>;
|
|
<action, C.idn, V[0].inc, V[1].dec>;
|
|
<action, C.iid, V[0].inc, V[1].inc, V[2].dec>;
|
|
<action, C.iii, V[0].inc, V[1].inc, V[2].inc>;
|
|
<action, C.iin, V[0].inc, V[1].inc>;
|
|
<action, C.ind, V[0].inc, V[2].dec>;
|
|
<action, C.ini, V[0].inc, V[2].inc>;
|
|
<action, C.inn, V[0].inc>;
|
|
<action, C.ndd, V[1].dec, V[2].dec>;
|
|
<action, C.ndi, V[1].dec, V[2].inc>;
|
|
<action, C.ndn, V[1].dec>;
|
|
<action, C.nid, V[1].inc, V[2].dec>;
|
|
<action, C.nii, V[1].inc, V[2].inc>;
|
|
<action, C.nin, V[1].inc>;
|
|
<action, C.nnd, V[2].dec>;
|
|
<action, C.nni, V[2].inc>;
|
|
<action, C.nnn>;
|
|
<time, T.time>;
|
|
edon
|
|
|
|
node System
|
|
sub V : Valve[3];
|
|
T : Tank;
|
|
//C : Ctrl;
|
|
C : Ctrl_System;
|
|
state ctrl : bool;
|
|
init ctrl := true;
|
|
// d pour dec, i pour inc, n pour nop
|
|
event action;
|
|
time;
|
|
trans
|
|
ctrl |- action -> ctrl := false;
|
|
~ctrl |- time -> ctrl := true;
|
|
assert
|
|
T.amont = (V[0].rate + V[1].rate);
|
|
T.aval = V[2].rate;
|
|
// liens avec le controleur
|
|
C.r[0] = V[0].rate;
|
|
C.r[1] = V[1].rate;
|
|
C.r[2] = V[2].rate;
|
|
C.l = T.level;
|
|
sync <action, C.ddd, V[0].dec, V[1].dec, V[2].dec>;
|
|
<action, C.ddi, V[0].dec, V[1].dec, V[2].inc>;
|
|
<action, C.ddn, V[0].dec, V[1].dec>;
|
|
<action, C.did, V[0].dec, V[1].inc, V[2].dec>;
|
|
<action, C.dii, V[0].dec, V[1].inc, V[2].inc>;
|
|
<action, C.din, V[0].dec, V[1].inc>;
|
|
<action, C.dnd, V[0].dec, V[2].dec>;
|
|
<action, C.dni, V[0].dec, V[2].inc>;
|
|
<action, C.dnn, V[0].dec>;
|
|
<action, C.idd, V[0].inc, V[1].dec, V[2].dec>;
|
|
<action, C.idi, V[0].inc, V[1].dec, V[2].inc>;
|
|
<action, C.idn, V[0].inc, V[1].dec>;
|
|
<action, C.iid, V[0].inc, V[1].inc, V[2].dec>;
|
|
<action, C.iii, V[0].inc, V[1].inc, V[2].inc>;
|
|
<action, C.iin, V[0].inc, V[1].inc>;
|
|
<action, C.ind, V[0].inc, V[2].dec>;
|
|
<action, C.ini, V[0].inc, V[2].inc>;
|
|
<action, C.inn, V[0].inc>;
|
|
<action, C.ndd, V[1].dec, V[2].dec>;
|
|
<action, C.ndi, V[1].dec, V[2].inc>;
|
|
<action, C.ndn, V[1].dec>;
|
|
<action, C.nid, V[1].inc, V[2].dec>;
|
|
<action, C.nii, V[1].inc, V[2].inc>;
|
|
<action, C.nin, V[1].inc>;
|
|
<action, C.nnd, V[2].dec>;
|
|
<action, C.nni, V[2].inc>;
|
|
<action, C.nnn>;
|
|
<time, T.time>;
|
|
edon
|