(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : AVTS_imitator
 * Description      : Preemptive model
 * Correctness      : 
 * Scalable         : 
 * Generated        : 
 * Categories       : 
 * Source           : Thales
 * bibkey           : 
 * Author           : Baptiste Parquier
 * Modeling         : Baptiste Parquier
 * Input by         : Baptiste Parquier, Étienne André
 * License          : 
 * 
 * Created          : 2016/08/29
 * Last modified    : 2021/10/12
 * Model version    : 
 * 
 * IMITATOR version : 3.2
 ******************************************************************************)

var

(* Clocks *)
	x2p, (* Periodic Event T2_1's clock *)
	x2, (* Process T2_1's clock *)
	x6p, (* Periodic Event T6_1's clock and Jitter's clock *)
	x61, x5, x62, x63, (* clocks for T6 and T5 *)
	x7, (* T7_1's clocks *)
	t1, t2 (* observer's clocks *)
		: clock;

(* Discrete *)
	c2, c61, c5, c62, c63, c7, (* for each task: compute the number of activations waiting *)
	chemin_T6_1, chemin_T7_1 (* NOTE: could be replaced with bool? *)
		: int;

(* Parameters *)
	 WT
		: parameter;

(* Contants *)
	jitter = 30, offset = 0
		: constant;

(************************************************************)
automaton periodic_event_T2_1
(************************************************************)
actions: recommence_T2_1;

loc p20: invariant x2p <= offset
	when x2p >= offset do {x2p := 0} goto p2;

loc p2: invariant x2p <= 40
	when x2p = 40 sync recommence_T2_1 do {x2p := 0} goto p2;

end (* periodic_event_T2_1 *)


(************************************************************)
automaton memoire_lancement_T2_1
(************************************************************)
actions: recommence_T2_1, lance_T2_1, fin_T2_1;

loc m20: invariant True
	when True sync recommence_T2_1 do {c2 := c2 + 1} goto m21;
	when True sync fin_T2_1 do {c2 := c2 - 1} goto m21;

urgent loc m21: invariant True
	when c2 = 1 sync lance_T2_1 goto m20;
	when c2 <> 1 goto m20;

end (* memoire_lancement_T2_1 *)


(************************************************************)
automaton periodic_event_T6_1
(************************************************************)
actions: recommence_T6_1;

loc p60: invariant x6p <= 100
	when x6p = 100 do {x6p := 0} goto p61;

loc p61: invariant x6p <= jitter
	when True sync recommence_T6_1 goto p60;

end (* periodic_event_T6_1 *)


(************************************************************)
automaton memoire_lancement_T6_1
(************************************************************)
actions: recommence_T6_1, lance_T6_1, fin_T6_1;

loc m610: invariant True
	when True sync recommence_T6_1 do {c61 := c61 + 1} goto m611;
	when True sync fin_T6_1 do {c61 := c61 - 1} goto obs61;

urgent loc m611: invariant True
	when c61 = 1 sync lance_T6_1 goto m610;
	when c61 <> 1 goto m610;

urgent loc obs61: invariant True
	when chemin_T6_1 = 1 do {chemin_T6_1 := 2} goto m611;
	when chemin_T6_1 = 2 do {chemin_T6_1 := 1} goto m611;

end (* memoire_lancement_T6_1 *)


(************************************************************)
automaton memoire_lancement_T5_1
(************************************************************)
actions: fin_T6_1, lance_T5_1, fin_T5_1;

loc m510: invariant True
	when True sync fin_T6_1 do {c5 := c5 + 1} goto m511;
	when True sync fin_T5_1 do {c5 := c5 - 1} goto m511;

urgent loc m511: invariant True
	when c5 = 1 sync lance_T5_1 goto m510;
	when c5 <> 1 goto m510;

end (* memoire_lancement_T5_1 *)


(************************************************************)
automaton memoire_lancement_T6_2
(************************************************************)
actions: fin_T6_2, lance_T6_2, fin_T5_1;

loc m620: invariant True
	when True sync fin_T5_1 do {c62 := c62 + 1} goto m621;
	when True sync fin_T6_2 do {c62 := c62 - 1} goto m621;

urgent loc m621: invariant True
	when c62 = 1 sync lance_T6_2 goto m620;
	when c62 <> 1 goto m620;

end (* memoire_lancement_T6_2 *)


(************************************************************)
automaton memoire_lancement_T6_3
(************************************************************)
actions: fin_T6_3, lance_T6_3, fin_T6_2;

loc m630: invariant True
	when True sync fin_T6_2 do {c63 := c63 + 1} goto m631;
	when True sync fin_T6_3 do {c63 := c63 - 1} goto m631;

urgent loc m631: invariant True
	when c63 = 1 sync lance_T6_3 goto m630;
	when c63 <> 1 goto m630;

end (* memoire_lancement_T6_3 *)


(************************************************************)
automaton memoire_lancement_T7_1
(************************************************************)
actions: fin_T6_2, lance_T7_1, fin_T7_1;

loc m70: invariant True
	when True sync fin_T6_2 do {c7 := c7 + 1} goto m71;
	when True sync fin_T7_1 do {c7 := c7 - 1} goto obs7;

urgent loc m71: invariant True
	when c7 = 1 sync lance_T7_1 goto m70;
	when c7 <> 1 goto m70;

urgent loc obs7: invariant True
	when chemin_T7_1 = 1 do {chemin_T7_1 := 2} goto m71;
	when chemin_T7_1 = 2 do {chemin_T7_1 := 1} goto m71;

end (* memoire_lancement_T7_1 *)




(************************************************************)
automaton tasks
(************************************************************)
actions : lance_T2_1, lance_T6_1, lance_T5_1, lance_T6_2, lance_T6_3, lance_T7_1,
	fin_T2_1, fin_T6_1, fin_T5_1, fin_T6_2, fin_T6_3, fin_T7_1;

loc l0: invariant True
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when True sync lance_T6_1 do {x61 := 0} goto l61;
	when True sync lance_T5_1 do {x5 := 0} goto l5;
	when True sync lance_T6_2 do {x62 := 0} goto l62;
	when True sync lance_T6_3 do {x63 := 0} goto l63;
	when True sync lance_T7_1 do {x7 := 0} goto l7;

loc l2: invariant x2 <= 17 stop{x63, x62, x61, x5, x7}
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when x2 >= 17 sync fin_T2_1 goto l2U;
	when True sync lance_T6_3 do {x63 := 0} goto l2;
	when True sync lance_T6_2 do {x62 := 0} goto l2;
	when True sync lance_T6_1 do {x61 := 0} goto l2;
	when True sync lance_T5_1 do {x5 := 0} goto l2;
	when True sync lance_T7_1 do {x7 := 0} goto l2;

urgent loc l2U: invariant True
	when c63 > 0 goto l63;
	when c63 = 0 & c62 > 0 goto l62;
	when c63 = 0 & c62 = 0 & c61 > 0 goto l61;
	when c63 = 0 & c62 = 0 & c61 = 0 & c5 > 0 goto l5;
	when c63 = 0 & c62 = 0 & c61 = 0 & c5 = 0 & c7 > 0 goto l7;
	when c63 = 0 & c62 = 0 & c61 = 0 & c5 = 0 & c7 = 0 goto l0;
	when True sync lance_T6_3 do {x63 := 0} goto l2U;
	when True sync lance_T6_2 do {x62 := 0} goto l2U;
	when True sync lance_T6_1 do {x61 := 0} goto l2U;
	when True sync lance_T5_1 do {x5 := 0} goto l2U;
	when True sync lance_T7_1 do {x7 := 0} goto l2U;

loc l63: invariant x63 <= 5 stop{x62, x61, x5, x7}
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when True sync lance_T6_3 do {x63 := 0} goto l63;
	when x63 >= 4 sync fin_T6_3 goto l63U;
	when True sync lance_T6_2 do {x62 := 0} goto l63;
	when True sync lance_T6_1 do {x61 := 0} goto l63;
	when True sync lance_T5_1 do {x5 := 0} goto l63;
	when True sync lance_T7_1 do {x7 := 0} goto l63;

urgent loc l63U: invariant True
	when c62 > 0 goto l62;
	when c62 = 0 & c61 > 0 goto l61;
	when c62 = 0 & c61 = 0 & c5 > 0 goto l5;
	when c62 = 0 & c61 = 0 & c5 = 0 & c7 > 0 goto l7;
	when c62 = 0 & c61 = 0 & c5 = 0 & c7 = 0 goto l0;
	when True sync lance_T6_2 do {x62 := 0} goto l63U;
	when True sync lance_T6_1 do {x61 := 0} goto l63U;
	when True sync lance_T5_1 do {x5 := 0} goto l63U;
	when True sync lance_T7_1 do {x7 := 0} goto l63U;

loc l62: invariant x62 <= 10 stop{x61, x5, x7}
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when True sync lance_T6_3 do {x63 := 0} goto l63;
	when True sync lance_T6_2 do {x62 := 0} goto l62;
	when x62 >= 9 sync fin_T6_2 goto l62U;
	when True sync lance_T6_1 do {x61 := 0} goto l62;
	when True sync lance_T5_1 do {x5 := 0} goto l62;
	when True sync lance_T7_1 do {x7 := 0} goto l62;

urgent loc l62U: invariant True
	when c61 > 0 goto l61;
	when c61 = 0 & c5 > 0 goto l5;
	when c61 = 0 & c5 = 0 & c7 > 0 goto l7;
	when c61 = 0 & c5 = 0 & c7 = 0 goto l0;
	when True sync lance_T6_1 do {x61 := 0} goto l62U;
	when True sync lance_T5_1 do {x5 := 0} goto l62U;
	when True sync lance_T7_1 do {x7 := 0} goto l62U;

loc l61: invariant x61 <= 4 stop{x5, x7}
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when True sync lance_T6_3 do {x63 := 0} goto l63;
	when True sync lance_T6_2 do {x62 := 0} goto l62;
	when True sync lance_T6_1 do {x61 := 0} goto l61;
	when x61 >= 4 sync fin_T6_1 goto l61U;
	when True sync lance_T5_1 do {x5 := 0} goto l61;
	when True sync lance_T7_1 do {x7 := 0} goto l61;

urgent loc l61U: invariant True
	when c5 > 0 goto l5;
	when c5 = 0 & c7 > 0 goto l7;
	when c5 = 0 & c7 = 0 goto l0;
	when True sync lance_T5_1 do {x5 := 0} goto l61U;
	when True sync lance_T7_1 do {x7 := 0} goto l61U;

loc l5: invariant x5 <= 7 stop{x7}
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when True sync lance_T6_3 do {x63 := 0} goto l63;
	when True sync lance_T6_2 do {x62 := 0} goto l62;
	when True sync lance_T6_1 do {x61 := 0} goto l61;
	when True sync lance_T5_1 do {x5 := 0} goto l5;
	when x5 >= 4 sync fin_T5_1 goto l5U;
	when True sync lance_T7_1 do {x7 := 0} goto l5;

urgent loc l5U: invariant True
	when c7 > 0 goto l7;
	when c7 = 0 goto l0;
	when True sync lance_T7_1 do {x7 := 0} goto l5U;

loc l7: invariant x7 <= 14
	when True sync lance_T2_1 do {x2 := 0} goto l2;
	when True sync lance_T6_3 do {x63 := 0} goto l63;
	when True sync lance_T6_2 do {x62 := 0} goto l62;
	when True sync lance_T6_1 do {x61 := 0} goto l61;
	when True sync lance_T5_1 do {x5 := 0} goto l5;
	when True sync lance_T7_1 do {x7 := 0} goto l7;
	when x7 >= 11 sync fin_T7_1 goto l0;

end (* tasks *)




(************************************************************)
(* Observateur *)
(************************************************************)

automaton Observateur1

actions: lance_T6_1, fin_T7_1, obs1_bloc;

loc obs10: invariant True stop {t1}
	when chemin_T6_1 = 1 sync lance_T6_1 do {t1 := 0} goto obs11;
	when chemin_T6_1 <> 1 sync lance_T6_1 goto obs10;
	when True sync fin_T7_1 goto obs10;

loc obs11: invariant True
	when chemin_T7_1 = 1 sync fin_T7_1 goto obs13;
	when chemin_T7_1 <> 1 sync fin_T7_1 goto obs11;
	when True sync lance_T6_1 goto obs11;

urgent loc obs13: invariant True stop {t1}
	when t1 > WT sync obs1_bloc goto bloque1;
	when t1 <= WT goto obs10;

loc bloque1: invariant True

end (* Observateur1 *)


automaton Observateur2

actions: lance_T6_1, fin_T7_1, obs2_bloc;

loc obs20: invariant True stop {t2}
	when chemin_T6_1 = 2 sync lance_T6_1 do {t2 := 0} goto obs21;
	when chemin_T6_1 <> 2 sync lance_T6_1 goto obs20;
	when True sync fin_T7_1 goto obs20;

loc obs21: invariant True
	when chemin_T7_1 = 2 sync fin_T7_1 goto obs23;
	when chemin_T7_1 <> 2 sync fin_T7_1 goto obs21;
	when True sync lance_T6_1 goto obs21;

urgent loc obs23: invariant True stop {t2}
	when t2 > WT sync obs2_bloc goto bloque2;
	when t2 <= WT goto obs20;

loc bloque2: invariant True

end (* Observateur2 *)


automaton Observateur

actions: obs1_bloc, obs2_bloc;

loc obsI: invariant True
	when True sync obs1_bloc goto obsF;
	when True sync obs2_bloc goto obsF;

loc obsF: invariant True

end (* Observateur *)




(************************************************************)
(* Initial state *)
(************************************************************)

init := {
	discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[periodic_event_T2_1] := p20,
		loc[memoire_lancement_T2_1] := m20,
		loc[periodic_event_T6_1] := p60,
		loc[memoire_lancement_T6_1] := m610,
		loc[memoire_lancement_T5_1] := m510,
		loc[memoire_lancement_T6_2] := m620,
		loc[memoire_lancement_T6_3] := m630,
		loc[memoire_lancement_T7_1] := m70,
		loc[tasks] := l0,
		loc[Observateur1] := obs10,
		loc[Observateur2] := obs20,
		loc[Observateur] := obsI,

		(*------------------------------------------------------------*)
		(* Initial discrete assignments *)
		(*------------------------------------------------------------*)
		c2 := 0,
		c61 := 0,
		c5 := 0,
		c62 := 0,
		c63 := 0,
		c7 := 0,
		chemin_T6_1 := 1,
		chemin_T7_1 := 1,
	;

	continuous =
		(*------------------------------------------------------------*)
		(* Initial clock constraints *)
		(*------------------------------------------------------------*)
		& x2p = 0
		& x2 = 0
		& x6p = 0
		& x61 = 0
		& x62 = 0
		& x63 = 0
		& x5 = 0
		& x7 = 0
		& t1 = 0
		& t2 = 0

		(*------------------------------------------------------------*)
		(* Parameter constraints *)
		(*------------------------------------------------------------*)
		& WT >= 0
	;
}

(************************************************************)
(* The end *)
(************************************************************)
end