(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : researcher
 * Description      : Researcher writing papers and drinking coffee
 * Correctness      : Depends on the property
 * Scalable         : 
 * Generated        : 
 * Categories       : Toy ; Education
 * Source           : Own work
 * bibkey           : 
 * Author           : Étienne André
 * Modeling         : Étienne André
 * Input by         : Étienne André
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : 2021/01/26
 * Last modified    : 2021/02/01
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)

var

(* Clocks *)
 	x, t,
		: clock;

(* Discrete *)
	nb,
		: discrete;

(* Parameters *)
	pTotal, pNeed, MAXBREAK, pCoffee,
		: parameter;

(* Constants *)
	MINNEED = 1,
		: constant;


(************************************************************)
  automaton researcher
(************************************************************)
synclabs: done, drink, drunk, restart;

loc working: invariant x <= pTotal
	when x >= 0.8 pTotal goto workingFast;
	when x = pTotal sync done do {x := 0, t := 0} goto finished;
	when t >= pNeed & nb <= MAXBREAK - 1 sync drink do {t := 0, nb := nb + 1} goto coffeeing;

loc workingFast: invariant x <= pTotal flow{x' = 2}
	when True goto working;
	when x = pTotal sync done do {x := 0, t := 0} goto finished;
	when t >= 0.6 * pNeed & nb <= MAXBREAK - 1 sync drink do {t := 0, nb := nb + 1} goto coffeeing;

loc coffeeing: invariant t <= pCoffee stop{x}
	when t = pCoffee sync drunk do {t := 0} goto working;
	when t = pCoffee & x >= 0.8 pTotal sync drunk do {t := 0} goto workingFast;

loc finished: invariant True stop{x, t}
	when True sync restart do {x := 0, t := 0.5 pNeed, nb := 0} goto working;

end (* researcher *)



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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[researcher] = working

	(*------------------------------------------------------------*)
	(* Initial discrete assignments *)
	(*------------------------------------------------------------*)
	& nb = 0

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x = 0
	& t = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& pTotal >= 0
	& pNeed >= MINNEED
	& pCoffee >= 0
	
	& MAXBREAK >= 0
;


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