(*******************************************************************************
 *                                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    : 2023/11/16
 * Model version    : 
 * 
 * IMITATOR version : 3.4-beta
 ******************************************************************************)

var

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

(* Discrete *)
	nb,
		: discrete;

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

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


(************************************************************)
  automaton researcher
(************************************************************)
actions: finished, drink, drunk, restart;

loc working: invariant x <= pTotal
	when x >= 0.8 pTotal goto workingFast;
	when x = pTotal sync finished 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 finished 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 := {
  discrete =
  	(*------------------------------------------------------------*)
  	(* Initial location *)
  	(*------------------------------------------------------------*)
  	loc[researcher] := working,

  	(*------------------------------------------------------------*)
  	(* Initial discrete assignments *)
  	(*------------------------------------------------------------*)
  	nb := 0,
  ;

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

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

  	& MAXBREAK >= 0
  ;
}

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