pta

// Pacemaker model: the pacemaker is composed by 5 components (LRI, AVI, URI, PVARP, VRP). 

const int TAVI = 150;
const int TLRI = 1000;
const int TPVARP = 100;
const int TVRP = 150;
const int TURI = 400;
const int TPVAB = 50;
const int tstep = 2;

// LRI component

module LRI

s_lri:[0..1] init 1;
t_lri : clock;

// Invariants for clock t_lri
  invariant
    (s_lri=1 => t_lri<=TLRI-TAVI)
  endinvariant

[VP] (s_lri=0) -> (s_lri'=1) & (t_lri'=0);
[VS] (s_lri=0) -> (s_lri'=1) & (t_lri'=0);
[AS] (s_lri=0) -> (s_lri'=0);

[VP] (s_lri=1) -> (s_lri'=1) & (t_lri'=0);
[VS] (s_lri=1) -> (s_lri'=1) & (t_lri'=0);
[AS] (s_lri=1) -> (s_lri'=0);
// This should be an output
[AP] (s_lri=1) & (t_lri>=TLRI-TAVI) -> (s_lri'=1) & (t_lri'=0);

endmodule

module AVI

s_avi:[0..2] init 0;
t_avi : clock;

// Invariants for clock t_avi & clk
  invariant
       (s_avi = 1 => (t_avi <= TAVI))  &
       (s_avi = 2 => (clk<=TURI))
  endinvariant

[AS] (s_avi = 0) -> (s_avi'=1) & (t_avi'=0);
[AP] (s_avi = 0) -> (s_avi'=1) & (t_avi'=0);
[VS] (s_avi = 0) -> (s_avi'=0);

[VS] (s_avi = 1) -> (s_avi'=0);
[AS] (s_avi = 1) -> (s_avi'=1);
[AP] (s_avi = 1) -> (s_avi'=1);
[]   (s_avi = 1) & (t_avi >= TAVI) & (clk <=TURI-2) -> (s_avi'=2); 

// This should be an output 
[VP] (s_avi=1) & (t_avi >= TAVI) & (clk >=TURI) -> (s_avi'=0); 
[VS] (s_avi = 2) -> (s_avi'=0);
// This should be an output 
[VP] (s_avi = 2) & (clk >=TURI) -> (s_avi'=0);  
[AS] (s_avi = 2) -> (s_avi'=2);
[AP] (s_avi = 2) -> (s_avi'=2);
endmodule

module URI

s_uri : [0..1] init 0;
clk : clock; //This is the shared clock to all the modules

[VS] (s_uri = 0) -> (s_uri' = 0) & (clk' = 0);
[VP] (s_uri = 0) -> (s_uri' = 0) & (clk' = 0);
endmodule

module PVARP

s_pvarp:[0..3] init 0;
t_pvarp : clock;

// Invariants for clock t_pvarp
  invariant
       (s_pvarp = 1 => (t_pvarp <= 0))  &
       (s_pvarp = 2 => (t_pvarp <= TPVAB))  &
       (s_pvarp = 3 => t_pvarp <= TPVARP)
  endinvariant
 
[Aget] (s_pvarp = 0) -> (s_pvarp' = 1) & (t_pvarp' = 0);
[VS]   (s_pvarp = 0) -> (s_pvarp' = 2) & (t_pvarp' = 0);
[VP]   (s_pvarp = 0) -> (s_pvarp' = 2) & (t_pvarp' = 0);

// This should be an output
[AS] (s_pvarp = 1) -> (s_pvarp' = 0) & (t_pvarp'=0);

[]     (s_pvarp = 2) & (t_pvarp >= TPVAB) -> (s_pvarp' = 3);
[VS] (s_pvarp = 2) -> (s_pvarp'=2);
[VP] (s_pvarp = 2) -> (s_pvarp'=2);
[Aget] (s_pvarp = 2) -> (s_pvarp'=2);

[]     (s_pvarp = 3) & (t_pvarp >= TPVARP) -> (s_pvarp' = 0);
[VS] (s_pvarp = 3) -> (s_pvarp'=3);
[VP] (s_pvarp = 3) -> (s_pvarp'=3);
[Aget] (s_pvarp = 3) -> (s_pvarp'=3);
endmodule

module VRP

s_vrp:[0..2] init 0;
t_vrp : clock;

// Invariants for clock t_vrp
  invariant
       (s_vrp = 2 => (t_vrp <= TVRP)) &
       (s_vrp = 1 => (t_vrp <= 0 )) 
  endinvariant

[Vget] (s_vrp = 0) -> (s_vrp' = 1) & (t_vrp'=0);
[VP]  (s_vrp = 0) -> (s_vrp' = 2) & (t_vrp' = 0);

// This should be an output
[VS]  (s_vrp = 1) -> (s_vrp' = 2) & (t_vrp'=0);

[]    (s_vrp = 2) & (t_vrp >= TVRP) -> (s_vrp' = 0);
//[VP]  (s_vrp = 2) -> (s_vrp'=2);
endmodule
