domain modes = [0,1]; node ServerPerfect state mode : modes : public; init mode := 0; event a, b : public; trans // features or services. mode = 0 |- a -> mode := 1; mode = 1 |- b -> mode := 0; edon node ServerReal state mode : modes : public; init mode := 0; flow // on = true means the server is operational on : bool; // a variable to be able to "restart" from every modes. modeForRestart : modes : public; assert on => (mode=modeForRestart); event a, b, restart : public; trans // features and services on & mode = 0 |- a -> mode := 1; on & mode = 1 |- b -> mode := 0; // to restart the server from any state ~on |- restart -> mode := modeForRestart; edon node ServerHot sub S : ServerReal; state status : {on, ko} : parent; init status := on; assert // S server is operational if and only if this server is "on". // REPLACE TRUE BY THE CORRECT CONSTRAINT true; event failure, repairAndRestart; trans status=on |- failure -> status := ko; status=ko |- repairAndRestart -> status := on; sync // As soon as this server is repaired, S server must be operational. // REPLACE THE NEXT LINE BY THE CORRECT SYNCHRONIZATION ; edon node ServerCold sub S : ServerReal; state status : {on, ko, ready} : parent; init status := ready; assert // S server is operational if and only if this server is "on". // REPLACE TRUE BY THE CORRECT CONSTRAINT true; event failure, repair, start; trans // REPLACE GUARDS AND ASSIGNMENTS IN THE THREE NEXT TRANSITIONS false |- start -> ; false |- failure -> ; false |- repair -> ; sync // As soon as this server is required, S server must be operational. ; edon node SystemHot sub S : ServerHot[2]; state lastFail : [0,1]; flow currentMode : modes; assert // The two Systems in use are in the same mode. (S[0].S.mode = S[1].S.mode) | S[0].status!=on | S[1].status!=on; // Definition of the current mode (S[0].status=on) => (currentMode = S[0].S.mode); (S[1].status=on) => (currentMode = S[1].S.mode); (S[0].status!=on & S[1].status!=on & lastFail=0) => (currentMode = S[0].S.mode); (S[0].status!=on & S[1].status!=on & lastFail=1) => (currentMode = S[1].S.mode); // Definition of the two modeForRestart "parameters" S[0].S.modeForRestart = currentMode; S[1].S.modeForRestart = currentMode; event failure[2]; trans // Memorization of the last server which fail // REPLACE GUARDS AND ASSIGNMENTS IN THE TWO NEXT TRANSITIONS false |- failure[0] -> ; false |- failure[1] -> ; sync // Maximum features and services in parallel if possible. >= 1; >= 1; // Failures are failures of servers. // ADD THE TWO CORRECTS SYNCHRONIZATION edon node SystemCold sub S : ServerCold[2]; state lastFail : [0,1]; flow currentMode : modes; assert // Never two ServerCold "on" at the same time. // ADD THE CORRECT CONSTRAINT // Definition of the current mode (S[0].status=on) => (currentMode = S[0].S.mode); (S[1].status=on) => (currentMode = S[1].S.mode); (S[0].status!=on & S[1].status!=on & lastFail=0) => (currentMode = S[0].S.mode); (S[0].status!=on & S[1].status!=on & lastFail=1) => (currentMode = S[1].S.mode); // Definition of the two modeForRestart "parameters" S[0].S.modeForRestart = currentMode; S[1].S.modeForRestart = currentMode; event failure[2]; trans // Memorization of the last ServerCold which fail // REPLACE GUARDS AND ASSIGNMENTS IN THE TWO NEXT TRANSITIONS false |- failure[0] -> ; false |- failure[1] -> ; sync // Independant starts of ServerCold ; ; // Failure of a server starts the other server (if possible) // ADD THE TWO CORRECTS SYNCHRONIZATION edon