92 lines
2.1 KiB
Text
92 lines
2.1 KiB
Text
// node vanne
|
|
// state debit : [0,2];
|
|
// init debit := 0;
|
|
// event inc, dec;
|
|
// trans
|
|
// debit < 2 |- inc -> debit := debit + 1;
|
|
// debit > 0 |- dec -> debit := debit - 1;
|
|
// edon
|
|
|
|
|
|
node Vanne
|
|
state debit : [0,2];
|
|
state panne : bool;
|
|
init debit := 0;
|
|
init panne := false;
|
|
event inc, dec, estEnPanne, estRepare;
|
|
trans
|
|
~panne |- inc -> debit := debit + 1;
|
|
~panne |- dec -> debit := debit - 1;
|
|
// La panne est une transition comme les autres
|
|
// elle intervien de maniere non deterministe
|
|
// comme le Zabbix
|
|
~panne |- inc -> panne := true;
|
|
~panne |- dec -> panne := true;
|
|
panne |- inc -> ;
|
|
panne |- dec -> ;
|
|
debit = 0 |- dec ->;
|
|
debit = 2 |- inc ->;
|
|
edon
|
|
|
|
node Cuve
|
|
state niveau : [0,4];
|
|
flow
|
|
amont: [0,4];
|
|
aval: [0,2];
|
|
init niveau := 2;
|
|
event time;
|
|
trans
|
|
// On modelise exactement ce qui est dit dans l'énoncé
|
|
amont > aval |- time -> niveau := niveau + 1;
|
|
amont < aval |- time -> niveau := niveau - 1;
|
|
amont = aval & amont = 0 |- time ->;
|
|
amont = aval & amont = 0 |- time -> niveau := niveau + 1;
|
|
amont = aval & amont = 0 |- time -> niveau := niveau - 1;
|
|
amont = aval & amont = 0 |- time ->;
|
|
edon
|
|
|
|
node Controlleur
|
|
|
|
edon
|
|
|
|
node Systeme
|
|
sub
|
|
// Valves amont
|
|
Am: Vanne[2];
|
|
//Valve Aval
|
|
Av: Vanne;
|
|
C: Cuve;
|
|
Ctrl: Controlleur;
|
|
assert
|
|
C.amont = (Am[0].debit + Am[1].debit);
|
|
C.aval = Av.debit;
|
|
sync
|
|
// d decremente, i incrémente, n nop
|
|
<ddd, V[0].dec, V[1].dec, V[2].dec>;
|
|
|
|
<ddi, V[0].dec, V[1].dec, V[2].inc>;
|
|
<did, V[0].dec, V[1].inc, V[2].dec>;
|
|
<idd, V[0].inc, V[1].dec, V[2].dec>;
|
|
|
|
<iid, V[0].inc, V[1].inc, V[2].dec>;
|
|
<dii, V[0].dec, V[1].inc, V[2].inc>;
|
|
<idi, V[0].inc, V[1].dec, V[2].inc>;
|
|
|
|
<iii, V[0].inc, V[1].inc, V[2].inc>;
|
|
|
|
<nii, V[1].inc, V[2].inc>;
|
|
<ini, V[0].inc, V[2].inc>;
|
|
<iin, V[0].inc, V[1].inc>;
|
|
|
|
<nni, V[2].inc>;
|
|
<nin, V[1].inc>;
|
|
<inn, V[0].inc>;
|
|
|
|
<ddn, V[0].dec, V[1].dec>;
|
|
<dnd, V[0].dec, V[2].dec>;
|
|
<ndd, V[1].dec, V[2].dec>;
|
|
<nnd, V[2].dec>;
|
|
<nnn,>
|
|
|
|
edon
|
|
|