mdp

module UtilisateurEtBoutons
prog : [0..1] init 0; // 0 : eco 1: intensif
bonoff : bool init false; //bouton on/off avec 2 positions
bsr : [0..2] init 0; //ce bouton compte les pressions
[BOnOff] true -> (bonoff’=!bonoff)& (bsr’=0);
[Bsr] (bsr<2) -> (bsr’=bsr+1);
[Bsr] (bsr=2) -> (bsr’=0);
[eco] true -> (prog’=0) & (bsr’=0);
[intensif] true -> (prog’=1) & (bsr’=0);
[] true-> (bsr’=0);
endmodule

module Affichage //affichage indépendant de l’état de machine
qa : [0..2] init 0; // 0:off 1:affichage 3: clignotement
von : bool init false;
vrincage : bool init false;
vlavage : bool init false;
vsechage : bool init false;

[BOnOff] (qa=0) -> (qa’=1)& (vrincage’=false) & (vlavage’=false) & (vsechage’=false) & (von’=true);

[BOnOff] (qa>0) -> (qa’=0)& (vrincage’=false) & (vlavage’=false) & (vsechage’=false) & (von’=false);

[DebutR] (qa=1) -> (vrincage’=true);
[R2L] (qa=1) -> (vrincage’=false) & (vlavage’=true);
[DebutL] (qa=1) -> (vlavage’=true) ;
[L2S] (qa=1) -> (vlavage’=false) & (vsechage’=true) ;
[FinS] (qa=1) -> (qa’=2) & (vrincage’=false) & (vlavage’=false) & (vsechage’=false);
[Clignote] (qa=2) -> (vrincage’=!vrincage) & (vlavage’=!vlavage) & (vsechage’=!vsechage) ;
endmodule

module Controleur
qm : [0..3] init 0; // 0:off 1:attente 2:marche 3: fin
ql : [0..4] init 0; // 0:pret, 1: rincage, 2:lavage, 3:sechage, 4:fin
timer: [0..10] init 0;

   [BOnOff] (qm=0) -> (qm'=1);
   [BOnOff] (qm>0) -> (qm'=0);
   [Bsr] (qm=0) -> (qm'=0) ;
   [Bsr] (qm>0) & (bsr=2) -> (qm'=1);
   [Bsr] (qm=1) & (bsr<2)-> (qm'=2) & (ql'=0); 
   [Bsr] (qm>1) & (bsr<2)-> true; 
   
   [DebutL] (ql=0) & (qm=2) & (prog=0)-> (ql'=2) & (timer'=0); // debut eco 
   [DebutR] (ql=0) & (qm=2) & (prog=1)-> (ql'=1) & (timer'=0); // debut intensif

   [R2L] (ql=1) & (qm=2) & (timer=10) -> (ql'=2) & (timer'=0) ; //fin rincage
   [L2S] (ql=2) & (qm=2) & (timer=10) -> (ql'=3) & (timer'=0) ; //fin lavage
   [FinS](ql=3) & (qm=2) & (timer=10) -> (ql'=4) & (qm'=3) ; //fin sechage
   [tick] (ql>0) & (ql<4) & (qm=2) & (timer<10) -> (timer'=timer+1); 

endmodule

label “attente” = (qm=1);
label “marche” = (qm=2);
label “fin” = (qm=3);
label “fin2” = (ql=4);
label “Bonoff” = (bonoff=true);
label “Bsr” = (bsr>0);
label “Von” = (von=true);
label “Vrincage” = (vrincage=true);
label “Vlavage” = (vlavage=true);
label “Vsechage” = (vsechage=true);
label “Peco” = (prog=0);
label “Pintensif” = (prog=1);
label “Poff” = (qm=0);
label “Pon” = (qm > 0);
label “dBsr” = (bsr=2);
label “Pbt” = (bonoff=true);
label “Pinit” = (qm=0) & (ql=0);