(************************************************************ * IMITATOR MODEL * * Small problem with a nuclear plant that may explode * * Description : Toy example of a nuclear plant that may explode * Correctness : The nuclear plant must not blow up * Source : "SITH" course final examination at Institut Galilée, Université Paris 13 (2013-2014) * Author : Étienne André * Modeling : Étienne André * Input by : Étienne André * * Created : 2014/03/21 * Last modified : 2015/07/30 * * IMITATOR version: 2.7.1 ************************************************************) 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: while True wait {} when True do {x1' = 0, x2' = 0} sync startHeating goto heating; loc heating: while x1 <= p1 & x2 <= p2 wait {} when x1 >= p1 sync tooHot goto boom; when x2 = p2 do{x2' = 0} sync triggerAlarm goto ringing; loc ringing: while x1 <= p1 & x2 <= p3 wait {} when x1 >= p1 sync tooHot goto boom; when x2 = p3 do{x2' = 0} sync startWatering goto watering; loc watering: while x1 <= p1 & x2 <= p4 wait {} 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: while True wait {} when True do {x1' = 0, x2' = 0} sync restart goto normal; (* reset to try to reduce state space *) loc boom: while True wait {} 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 *) ; (************************************************************) (* Property specification *) (************************************************************) property := unreachable loc[plant] = boom (************************************************************) (* The end *) (************************************************************) end