const DernierEtage = 3 ; domain Etages = [0,DernierEtage] ; /* les boutons réagissent à : * - une action de l'utilisateur * - un signal d'extinction */ node Button state light : bool : public; event push : public; off; trans true |- push -> light := true; true |- off -> light := false; init light := false; edon /* les portes moins parfaite réagissent à : * - un signal d'ouverture * - un signal de fermeture */ node Door state closed : bool : public; stucked : bool; event open, close : public; trans ~stucked |- open -> closed := false; ~stucked |- close -> closed := true; ~stucked & closed |- open -> stucked := true; ~stucked & ~closed |- close -> stucked := true; stucked |- open -> ; stucked |- close -> ; init closed := true, stucked := false; edon /* les étages comprennent une porte et un bouton * La modélisation doit donner un sens à "la requete est satisfaite" * Elle doit choisir entre : * - lors de l'ouverture de la porte * - lors de la fermeture de la porte * Nous choisissons la seconde solution */ node Floor sub B : Button; D : Door; event close; trans ~D.closed |- close -> ; sync ; edon /* la cabine comprend une porte et un bouton par étage (ici 4) * La modélisation doit donner un sens à "la requete est satisfaite" * Elle doit choisir entre : * - lors de l'ouverture de la porte * - lors de la fermeture de la porte * Nous choisissons la seconde solution (comme dans l'étage) */ node Cage state floor : Etages : parent; sub D : Door; B0, B1, B2, B3 : Button; event up, down, close0, close1, close2, close3; trans D.closed |- up -> floor := floor + 1; D.closed |- down -> floor := floor - 1; floor = 0 |- close0 -> ; floor = 1 |- close1 -> ; floor = 2 |- close2 -> ; floor = 3 |- close3 -> ; sync ; ; ; ; init floor := 0; edon /* L'immeuble comprend une cabine et quatre étages * - l'ouverture et la fermeture des portes sont synchronisées * - l'ouverture n'est possible que si une requete existe à cet étage. * - la cabine se déplace si il existe une requete qui le necessite. * - la cabine se déplace si il n'y a pas de requete à cet étage. * - le dernier mouvement est mémorisé pour pouvoir décider du suivant. * - l'initialisation doit etre cohérente. */ node Version3 flow mayGoUp, mayGoDown : bool : private; request0, request1, request2, request3 : bool : private; state climb : bool; sub F0, F1, F2, F3 : Floor; C : Cage; event open0, open1, open2, open3; up < {open0, open1, open2, open3}; down < {open0, open1, open2, open3}; trans (C.floor = 0) & request0 |- open0 -> ; (C.floor = 1) & request1 |- open1 -> ; (C.floor = 2) & request2 |- open2 -> ; (C.floor = 3) & request3 |- open3 -> ; climb & mayGoUp |- up -> ; ~climb & ~mayGoDown & mayGoUp |- up -> climb := true; ~climb & mayGoDown |- down -> ; climb & ~mayGoUp & mayGoDown |- down -> climb := false; sync ; ; ; ; ; ; ; ; ; ; assert request0 = (C.B0.light | F0.B.light); request1 = (C.B1.light | F1.B.light); request2 = (C.B2.light | F2.B.light); request3 = (C.B3.light | F3.B.light); mayGoUp = ((C.floor=0 & (request3 | request2 | request1)) | (C.floor=1 & (request3 | request2)) | (C.floor=2 & (request3))); mayGoDown = ((C.floor=3 & (request0 | request1 | request2)) | (C.floor=2 & (request0 | request1)) | (C.floor=1 & (request0))); init climb := false; edon /* L'immeuble comprend une cabine et quatre étages * - l'ouverture et la fermeture des portes sont synchronisées * - l'ouverture n'est possible que si une requete existe à cet étage. * - la cabine se déplace si il existe une requete qui le necessite. * - la cabine se déplace si il n'y a pas de requete à cet étage. * - le dernier mouvement est mémorisé pour pouvoir décider du suivant. * - l'initialisation doit etre cohérente. * - il faut également tester la porte de l'étage avant de bouger */ node Version4 flow mayGoUp, mayGoDown : bool : private; request0, request1, request2, request3 : bool : private; state climb : bool; sub F0, F1, F2, F3 : Floor; C : Cage; event open0, open1, open2, open3; up < {open0, open1, open2, open3}; down < {open0, open1, open2, open3}; trans (C.floor = 0) & request0 |- open0 -> ; (C.floor = 1) & request1 |- open1 -> ; (C.floor = 2) & request2 |- open2 -> ; (C.floor = 3) & request3 |- open3 -> ; climb & mayGoUp |- up -> ; ~climb & ~mayGoDown & mayGoUp |- up -> climb := true; ~climb & mayGoDown |- down -> ; climb & ~mayGoUp & mayGoDown |- down -> climb := false; sync ; ; ; ; ; ; ; ; ; ; assert request0 = (C.B0.light | F0.B.light); request1 = (C.B1.light | F1.B.light); request2 = (C.B2.light | F2.B.light); request3 = (C.B3.light | F3.B.light); mayGoUp = ((C.floor=0 & F0.D.closed & (request3 | request2 | request1)) | (C.floor=1 & F1.D.closed & (request3 | request2)) | (C.floor=2 & F2.D.closed & (request3))); mayGoDown = ((C.floor=3 & F3.D.closed & (request0 | request1 | request2)) | (C.floor=2 & F2.D.closed & (request0 | request1)) | (C.floor=1 & F1.D.closed & (request0))); init climb := false; edon