(******************************************************************************* * IMITATOR MODEL * * Title : NuclearPlant * Description : Toy example of a nuclear plant that may explode * Correctness : The nuclear plant must not blow up * Scalable : * Generated : * Categories : Education ; Toy * Source : "SITH" course final examination at Institut Galilée, Université Paris 13 (2013-2014) * bibkey : * Author : Étienne André * Modeling : Étienne André * Input by : Étienne André * License : * * Created : 2014/03/21 * Last modified : 2020/08/13 * Model version : * * IMITATOR version : 3 ******************************************************************************) var x1, x2 : clock; p1, (* Min duration between heating start and explosion *) p2, (* Exact duration between heating start and alarm triggering *) p3, (* Exact duration between alarm triggering and watering start *) p4 (* Max duration between watering start and watering end *) : parameter; (************************************************************) automaton plant (************************************************************) synclabs: startHeating, tooHot, triggerAlarm, startWatering, endWatering, restart; initially normal; loc normal: invariant True when True do {x1 := 0, x2 := 0} sync startHeating goto heating; loc heating: invariant x1 <= p1 & x2 <= p2 when x1 >= p1 sync tooHot goto boom; when x2 = p2 do{x2 := 0} sync triggerAlarm goto ringing; loc ringing: invariant x1 <= p1 & x2 <= p3 when x1 >= p1 sync tooHot goto boom; when x2 = p3 do{x2 := 0} sync startWatering goto watering; loc watering: invariant x1 <= p1 & x2 <= p4 when x1 >= p1 sync tooHot goto boom; when x2 <= p4 do {x1 := 0, x2 := 0} sync endWatering goto stopped; (* reset to try to reduce state space *) loc stopped: invariant True when True do {x1 := 0, x2 := 0} sync restart goto normal; (* reset to try to reduce state space *) loc boom: invariant True end (* plant *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* INITIAL LOCATION *) (*------------------------------------------------------------*) & loc[plant] = normal (*------------------------------------------------------------*) (* INITIAL CLOCKS *) (*------------------------------------------------------------*) & x1 = 0 & x2 = 0 (*------------------------------------------------------------*) (* PARAMETER CONSTRAINTS *) (*------------------------------------------------------------*) & p1 >= 0 & p2 >= 0 & p3 >= 0 & p4 >= 0 (* & p3 > 0 & p1 > p2 & p4 = 0 *) (* & p3 = 0 & p1 = 2 & p2 = 2 & p4 = 0 *) (* & p2 >= p1 & p2 >=p2 + p3 *) (* & p1 < p2+p3 *) (* & p1 < p3 *) (* & p1 = 10 & p2 = 12 & p3 = 14 & p4 = 15*) (* & p2 + p3 >= p1 & p1 = p2 & p3 = 0*) (*------------------------------------------------------------*) (* Parameter valuation to ensure not EF boom *) (*------------------------------------------------------------*) (* & p1 = 10 & p2 = 2 & p3 = 3 & p4 = 4*) (*------------------------------------------------------------*) (* Parameter valuation to ensure AF boom *) (*------------------------------------------------------------*) (* & p1 = 2 & p2 = 2 & p3 = 3 & p4 = 4 *) ; (************************************************************) (* The end *) (************************************************************) end