% -----------------------------------------------------------
% Lee Pike
% NASA Langley Formal Methods Group
% lepike@indiana.edu
%
% SAL 2.4
% -----------------------------------------------------------
spider_clock_synchII: CONTEXT =
BEGIN

REALTIME            : TYPE = REAL;
CLOCKTIME           : TYPE = INTEGER;
OFFSET              : TYPE = {T: CLOCKTIME | T >= 0};
RND                 : TYPE = NATURAL; 
rho                 : REALTIME = 1/10000; 
d_nom               : {t: REALTIME | t >= 0} = 5; 
ERROR               : TYPE = {t: REALTIME |     t >= 0 
                                            AND t < d_nom};
e_l                 : ERROR = 5/10000; 
e_u                 : ERROR = 5/10000; 
d_min               : REALTIME = (1 - rho) * (d_nom - e_l);
d_max               : CLOCKTIME = (1 + rho) * (d_nom + e_u);
% floor((1 - rho) * (d_nom - e_l))
fl_d_min               : CLOCKTIME = 4;
% ceiling((1 + rho) * (d_nom + e_u))
ce_d_max               : CLOCKTIME = 6;

NODES               : TYPE = [0..1];
SCHEDS              : TYPE = ARRAY NODES OF CLOCKTIME;

independent?(r: RND): BOOLEAN = FALSE; 

scheds_update(s: SCHEDS, scheds: SCHEDS, S: OFFSET, 
              R: OFFSET, P: OFFSET, C: OFFSET): BOOLEAN =
  FORALL (i: NODES): 
        s[i] >= scheds[i] + R + C
    AND s[i] < scheds[i] + P + C
    AND FORALL (j: NODES): s[i] - s[j] <= S;

% -- constraints on time-triggered systems ------------------
constraint1(P: OFFSET, pre_scheds: SCHEDS, 
            scheds: SCHEDS): BOOLEAN = 
  FORALL (i: NODES):     0 < P 
                     AND P < scheds[i] - pre_scheds[i];

constraint2(D: CLOCKTIME, S: OFFSET, L: OFFSET): BOOLEAN = 
  D >= S + L - fl_d_min;

constraint3(P: OFFSET, D: CLOCKTIME, S: OFFSET,
            L: OFFSET): BOOLEAN = 
  P > D + S + L + ce_d_max;

constraint4(r: RND, D: CLOCKTIME): BOOLEAN = 
  (NOT independent?(r)) => D >= 0;

constraint5(pre_P: OFFSET, D: CLOCKTIME,
            pre_scheds: SCHEDS, scheds: SCHEDS): BOOLEAN =
  FORALL (i: NODES): D >=   pre_P
                          - scheds[i] + pre_scheds[i];

constraint6(D: CLOCKTIME, R: OFFSET, 
            S: OFFSET, L: OFFSET): BOOLEAN = 
  R - 1 <= D + fl_d_min - S - L;
% -----------------------------------------------------------

system: MODULE =
BEGIN
LOCAL
  r                      : RND,
  scheds                 : SCHEDS,
  D                      : CLOCKTIME, 
  P, R, S, L             : OFFSET,
  ind                    : BOOLEAN,
  c1, c2, c3, c4, c5, c6 : BOOLEAN
INITIALIZATION
  scheds            = [[i: NODES] 0];
  r                 = 0;
  D                 = 1;  
  P                = 12;
  S                 = 4;
  L                 = 0;
  R                = 2;

  c1                = TRUE; 
  c2                = constraint2(D, S, L);
  c3                = constraint3(P, D, S, L);
  c4                = constraint4(r, D);
  c5                = TRUE;
  c6                = constraint6(D, R, S, L);
TRANSITION
[
    r = 0
    -->
      r'      = r + 1;
      D' = 4;
      scheds' IN {s: SCHEDS | scheds_update(s, scheds, S', 
                                            R, P, 40)};
      L' = S'; 
      R' = 0;
      P' = 20;
  
      c1' = constraint1(P', scheds, scheds');
      c2' = constraint2(D', S', L');
      c3' = constraint3(P', D', S', L');
      c4' = constraint4(r', D');
      c5' = constraint5(P, D', scheds, scheds');
      c6' = constraint6(D', R', S', L')
 []
    r = 1
    -->
      r'  = r + 1;
      S'  = 2;
      D' = 4;
      P' = 15;
      R' = 5;
      scheds' IN {s: SCHEDS | scheds_update(s, scheds, S',
                                            R, P, 70)};
      L' = S'; 
    
     c1' = constraint1(P', scheds, scheds');
     c2' = constraint2(D', S', L');
     c3' = constraint3(P', D', S', L');
     c4' = constraint4(r', D');
     c5' = constraint5(P, D', scheds, scheds');
     c6' = constraint6(D', R', S', L')
 []
    r = 2
    -->
      r'      = r + 1;
      P'      = 16;
      S'   = 2; 
      R' = 2;
      scheds' IN {s: SCHEDS | scheds_update(s, scheds, S',
                                            R, P, 120)};
      L' = S'; 

      c1' = constraint1(P', scheds, scheds');
      c2' = constraint2(D', S', L');
      c3' = constraint3(P', D', S', L');
      c4' = constraint4(r', D');
      c5' = constraint5(P, D', scheds, scheds');
      c6' = constraint6(D', R', S', L')
   []
     r = 3
     -->
      scheds' IN {s: SCHEDS | scheds_update(s, scheds, 0, 
                                            R, P, 100)};
      r' = 0;
      D' = 1;  
      P' = 12;
      S' = 4;
      L' = 0;
      R' = 2;

      c1' = constraint1(P', scheds, scheds');
      c2' = constraint2(D', S', L');
      c3' = constraint3(P', D', S', L');
      c4' = constraint4(r', D');
      c5' = constraint5(P, D', scheds, scheds');
      c6' = constraint6(D', R', S', L')
]
END;


% sal-inf-bmc -i -d 2 spider_clock_synchII.sal constraints
constraints: LEMMA system |- G(    c1 AND c2 AND c3 
                               AND c4 AND c5 AND c6);

% For k >= 0, the following should be false:
% sal-inf-bmc -i -d k spider_clock_synchII.sal liveness 
liveness: LEMMA system |- G(r < 3);
END