(************************************************************
 *                         IMITATOR
 *
 * Modeling the FMTV challenge, problem 1A for n=1
 * References      : "Verification of Two Real-Time Systems Using Parametric Timed Automata" (2015) by 
 *                      Youcheng Sun, Étienne André and Giuseppe Lipari
 *
 * Author          : Étienne André and Youcheng Sun
 * Created         : 2015/03/19
 * Last modified   : 2020/08/18
 *
 * IMITATOR version: 3
 ************************************************************)

var

    (** CONSTANTS **)
	
    (* Frames *)
    FRAME_EMPTY = 0, (* no frame *)
    
    FRAME_OTHER = 1, 
    FRAME_OTHER2 = 2,
    FRAME_OTHER3 = 3,
    
    FRAME_THEFRAME = 200, (* the actual frame produced by the camera *)

    (* Timings from the specification *)
    T1WCET = 28,
    T2BCL = 17,
    T2WCL = 19, 
     
    T3CET = 8,
	
    T4CET_empty = 1,
    T4CET_nonempty = 10,
	
	
    (* P1, P3 and P4 are task official periods *)
    P3 = 40/3,
    P4 = 40,
     
    (*P1_delta, P3_delta and P4_delta are possible variations of the periods *)
    (*OFFICIAL VALUES*)
    P3_delta = 1/150 (*40/3 * 0,0005*),
    P4_delta = 0.004 (*40 * 0,0001*),
    : parameter;
    
    (** CLOCKS **)
    
    ckT1T2, ckT3, ckT4
    : clock;
    
    (** DISCRETE **)
    
    (* Current frame in tasks 3 and 4 *)
    frame_in_3,
    frame_in_4,
    
    (* Frame in the register (of capacity 1) between T2 and T3; we assume it cannot be empty (TODO: justify!) *)
    register23,
    
    (* Current frame in the buffer (n=1) between T3 and T4 *)
    buffer34,
    (* Highest frame number in the buffer (n=1) between T3 and T4 (because "if the buffer has already stored a frame with a given index, any additional frame with the same index is discarded") *)
    buffer34_highest,
    
    : discrete;
    
    (** PARAMETERS **)
    
    (* The end-to-end latency *)
    e2e,
    (*P1_uncertain, P3_uncertain and P4_uncertain are constant task periods with a little of uncertainty *)
    (*P1_uncertain, *)P3_uncertain, P4_uncertain
    : parameter;


(************************************************************)
  automaton cameraT1T2
(************************************************************)
(* This PTA models the camera, task T1 and task T2 *)
(* This PTA also models the buffer initialization, and sends a broadcast signal 'start' when done *)
synclabs: start, T2done, init_buffer_empty, init_buffer_nonempty;

(* Nondeterministic choice to fill the buffer *)
(*** NOTE: we have to first assign the buffer to something, and then (in a different transition) sync on start, because other tasks need to *read* the buffer value ***)
loc camera0: invariant ckT1T2 = 0
	(* No frame in buffer *)
	when True sync init_buffer_empty do {buffer34 := FRAME_EMPTY, buffer34_highest := FRAME_EMPTY} goto camera1;
	when True sync init_buffer_nonempty goto camera1;

loc camera1: invariant ckT1T2 = 0
	when True goto camera2;

loc camera2: invariant ckT1T2 = 0
	when True do {register23 := FRAME_EMPTY} goto camera3;
	when True goto camera3;

loc camera3: invariant ckT1T2 = 0
	when True do {frame_in_3 := FRAME_EMPTY} goto camera4;
	when True goto camera4;

(* Now launch the Start signal *)
loc camera4: invariant ckT1T2 = 0
	when True sync start goto T1T2;

(* Process T1 and T2 together *)
loc T1T2: invariant ckT1T2 <= T2WCL
	(* Add the frame to the register *)
	when ckT1T2 >= T2BCL sync T2done do {register23 := FRAME_THEFRAME} goto T1T2done;

(* The end *)
loc T1T2done: invariant True

end (* cameraT1T2 *)


(************************************************************)
  automaton T3
(************************************************************)
synclabs: start, T3_done, T3_start;

(* Wait for start signal *)
loc T3preinit: invariant True
	(* Initially, T3 can be either processing or waiting *)
	when ckT3 <= T3CET sync start goto T3process;
	when True sync start goto T3wait;

(* Processing *)
loc T3process: invariant ckT3 <= T3CET
	(* If buffer not full AND frame not yet written: write frame from the current register *)
	when ckT3 = T3CET & buffer34 = FRAME_EMPTY & buffer34_highest < frame_in_3 sync T3_done do {buffer34 := frame_in_3, buffer34_highest := frame_in_3} goto T3wait;
	(* If buffer not full BUT frame already stored earlier: discard *)
	when ckT3 = T3CET & buffer34 = FRAME_EMPTY & buffer34_highest >= frame_in_3 sync T3_done goto T3wait;

	(* If buffer full: discard frame, i.e., do nothing with the buffer *)
	when ckT3 = T3CET & buffer34 > FRAME_EMPTY sync T3_done goto T3wait;

(* Waiting after processing *)
loc T3wait: invariant ckT3 <= P3_uncertain
	(* Copy the frame from the register into the task *)
	when ckT3 = P3_uncertain sync T3_start do {ckT3 := 0, frame_in_3 := register23} goto T3process;

end (* T3 *)


(************************************************************)
  automaton T4
(************************************************************)
synclabs: start, T4_start_empty, T4_start_nonempty, T4_done;

(* Wait for start signal *)
loc T4preinit: invariant True
	(* Initially, T4 can be either processing or waiting *)
	when True sync start goto T4wait;
	
(* Processing a non-empty frame *)
loc T4process_nonempty: invariant ckT4 <= T4CET_nonempty
	(* If another frame: wait for next round *)
	when ckT4 = T4CET_nonempty & frame_in_4 < FRAME_THEFRAME sync T4_done goto T4wait;
	(* If THE frame: the end! Update clock to stop time *)
	when ckT4 = T4CET_nonempty & frame_in_4 = FRAME_THEFRAME & ckT1T2 + T1WCET= e2e do {ckT4 := 0} sync T4_done goto T4end_ok;

(* Processing an empty frame *)
loc T4process_empty: invariant ckT4 <= T4CET_empty
	when ckT4 = T4CET_empty sync T4_done goto T4wait;

(* Waiting after processing *)
loc T4wait: invariant ckT4 <= P4_uncertain
	(* 0 frame in buffer *)
	when ckT4 = P4_uncertain & buffer34 = FRAME_EMPTY do {ckT4 := 0} sync T4_start_empty goto T4process_empty;

	(* 1 frame in buffer *)
	when ckT4 = P4_uncertain & FRAME_EMPTY < buffer34 do {ckT4 := 0, frame_in_4 := buffer34, buffer34 := FRAME_EMPTY} sync T4_start_nonempty goto T4process_nonempty;


(* The end! *)
loc T4end_ok: invariant ckT4 = 0

end (* T4 *)


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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[cameraT1T2] = camera0
	& loc[T3] = T3preinit
	& loc[T4] = T4preinit

	(*------------------------------------------------------------
	   INITIAL CLOCKS
	  ------------------------------------------------------------*)
	(* Start exactly when the camera has output the frame *)
	& ckT1T2 = 0
	(* Other components can be in any state *)
	& 0 <= ckT3 & ckT3 <= P3_uncertain
	& 0 <= ckT4 & ckT4 <= P4_uncertain

	(*------------------------------------------------------------
	   INITIAL DISCRETE VARIABLES
	  ------------------------------------------------------------*)
	(* Required by IMITATOR, but in fact will be nondeterministically initialized by the PTA cameraT1T2 *)
	& frame_in_4 = FRAME_OTHER
	
        (* Required by IMITATOR, but in fact will be nondeterministically initialized by the PTA cameraT1T2 *)
	& buffer34 = FRAME_OTHER
	& buffer34_highest = FRAME_OTHER

	(* We assume there is another frame in the task 3 (again, this has no importance *)
	& frame_in_3 = FRAME_OTHER2
	
	(* We assume there is another frame in the register (this has no importance *)
	& register23 = FRAME_OTHER3
	

	(*------------------------------------------------------------
	   PARAMETER CONSTRAINTS
	  ------------------------------------------------------------*)
	& e2e >= 0

	& P3 - P3_delta <= P3_uncertain & P3_uncertain <= P3 + P3_delta
	& P4 - P4_delta <= P4_uncertain & P4_uncertain <= P4 + P4_delta
	
	(* Obvious but safer *)
	& T2BCL <= T2WCL
	& T3CET <= P3_uncertain
	& T4CET_empty <= T4CET_nonempty
	& T4CET_nonempty <= P4_uncertain

;


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