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