%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Geoffrey Brown, Indiana University <geobrown |@| cs.indiana.edu>         %%
%% Lee Pike, Galois Connections, Inc. <leepike |@| galois.com>              %%
%%                                                                          %%
%% SAL 3.0 <http://fm.csl.sri.com/>                                         %%
%%                                                                          %%
%% Fully parameterized specification and refinement of an 8N1 protocol.     %%
%% Please see <http://www.cs.indiana.edu/~lepike/pub_pages/BMP-jrnl.html    %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

uartJrnl: CONTEXT = 

BEGIN

TIME : TYPE = REAL;

TPERIOD : { x : TIME | 0 < x};
TSETTLE : { x : TIME | 0 <= x AND x < TPERIOD};
TSTABLE : TIME = TPERIOD - TSETTLE;

RSCANMIN : { x : TIME | 0 < x};
RSCANMAX : { x : TIME | RSCANMIN <= x AND x < TSTABLE};
RSAMPMIN : { x : TIME | TPERIOD + TSETTLE < x};
RSAMPMAX : { x : TIME | RSAMPMIN <= x AND
		                  x < 2 * TPERIOD - TSETTLE - RSCANMAX};
RPERIODMIN : { x : TIME | 9 * TPERIOD + TSETTLE < RSAMPMIN + 8 * x};
RPERIODMAX : { x : TIME | RPERIODMIN <= x AND
     			TSETTLE + RSCANMAX + RSAMPMAX + 8 * x < 10 * TPERIOD};

STATE : TYPE = [0..9];

REG : TYPE = ARRAY [0..7] OF BOOLEAN;

time(t1 : TIME, t2: TIME): TIME = 
  IF t1 <= t2 THEN t1 ELSE t2 ENDIF;

%---------------------------------------
%  
% Infinite-State Components
%
%---------------------------------------

tclock_rt : MODULE =
  BEGIN
     INPUT  rclk   : TIME
     OUTPUT tclk   : TIME
  INITIALIZATION
     tclk  IN {x : TIME | 0 <= x AND x <= TPERIOD};
  TRANSITION
         [
           tclk = time(tclk, rclk) -->
                   tclk' = tclk + TPERIOD;
         ]
   END;

tenv : MODULE = 
   BEGIN
     INPUT   tready : BOOLEAN
     OUTPUT  tbit   : BOOLEAN
     INITIALIZATION
         % Initialization not necessary
         tbit = TRUE;
     TRANSITION
     [
         tready --> tbit' IN {TRUE, FALSE}
     []  ELSE   --> 
     ]
   END;

% To "activate", compose tenv_reg in tx below instead of
% tenv.  Do this for both the finite-state and infinite-state cases.
tenv_reg : MODULE = 
  BEGIN
    INPUT tstate : STATE
    LOCAL treg : REG
    OUTPUT  tbit   : BOOLEAN
    INITIALIZATION
           % Initialization not necessary
           tbit = TRUE;
    TRANSITION
    [
        tstate = 9 --> treg' IN {reg: REG | TRUE}
     [] tstate < 8 --> tbit' = treg[7-tstate]
     [] tstate = 8 -->
    ]
  END;

 tenc_8N1 : MODULE =
   BEGIN
     OUTPUT  tdata  : BOOLEAN
     OUTPUT  tstate : STATE
     OUTPUT  tready : BOOLEAN
     INPUT   tbit   : BOOLEAN
     INITIALIZATION
       tstate = 9;
     DEFINITION
       tready =  tstate /=  8;
       tdata  =  (tstate = 9) OR tbit;
     TRANSITION
     [
        tstate = 9  --> tstate' = IF tbit' THEN 9 ELSE 0 ENDIF;
     [] tstate < 9  --> tstate' = tstate + 1;
     ]
END;

tx_8N1 : MODULE = tclock_rt || tenc_8N1 
% || tenv; % comment this for registers
|| tenv_reg; % UNcomment this for registers


timeout (min : TIME, max : TIME) : [TIME -> BOOLEAN]  = 
                { x : TIME | min <= x AND x <=  max};

rclock_rt : MODULE  =
        BEGIN
         INPUT tclk   : TIME
         INPUT rstate : STATE
         OUTPUT rclk  : TIME

       INITIALIZATION

         rclk IN { x : TIME | 0 <= x AND x < RSCANMAX };   

       TRANSITION
       [
          rclk = time(rclk, tclk) --> 
                rclk' IN IF (rstate' = 9) THEN
                       timeout(rclk + RSCANMIN, rclk + RSCANMAX)
                         ELSIF (rstate' = 0) THEN
                           timeout(rclk + RSAMPMIN, rclk + RSAMPMAX)
                         ELSE
                           timeout(rclk + RPERIODMIN, rclk + RPERIODMAX)
                         ENDIF;
       ]
END;


rdec_8N1 : MODULE =
   BEGIN
     OUTPUT rstate : STATE
     OUTPUT rbit   : BOOLEAN
     OUTPUT rdata  : BOOLEAN
    DEFINITION
      rdata = rbit;
    INITIALIZATION
     rbit  = TRUE;
     rstate = 9;
    TRANSITION
       [
          rstate  = 9  -->  rbit' = TRUE;
       [] rstate  = 9  -->  rbit' = FALSE;
                            rstate' = 0;
       [] rstate /= 9  -->  rbit' IN {FALSE, TRUE};
                      rstate' = rstate + 1;
       ]
     END;

% To "activiate", uncomment the module below in the rx compositions
% (both finite-state and infinite-state).
rdec_reg : MODULE = 
  BEGIN
    INPUT rbit : BOOLEAN
    INPUT rstate : STATE
    OUTPUT rreg : REG
    INITIALIZATION
      rreg = [[i:[0..7]] FALSE]
    TRANSITION
    [
        rstate < 8 --> 
             rreg' = [[i:[0..7]] IF i=0 THEN rbit' 
                                 ELSE rreg[i-1]
                                 ENDIF]
     [] ELSE -->
    ]
  END;


constraint : MODULE =
       BEGIN
          INPUT  tclk     : TIME
          INPUT  rclk     : TIME
          INPUT  rdata    : BOOLEAN
          INPUT  tdata    : BOOLEAN
          LOCAL  stable   : BOOLEAN
          LOCAL  changing : BOOLEAN
       DEFINITION
           stable = NOT changing OR (tclk - rclk < TSTABLE);
     INITIALIZATION
           changing = FALSE	  
       TRANSITION
       [
          rclk' /= rclk AND (stable => rdata' = tdata) -->
       [] tclk' /= tclk --> changing' = (tdata' /= tdata)
       ]
      END;

rx_8N1 : MODULE = rdec_8N1 || rclock_rt
%; % comment this for registers
|| rdec_reg; % UNcomment this for registers

system_8N1 : MODULE = (tx_8N1 [] rx_8N1) || constraint;

%---------------------------------------
%  
% Finite-State Components
%
%---------------------------------------

tclock_fs : MODULE =
  BEGIN
     INPUT rstate : STATE
     INPUT tstate : STATE

  TRANSITION
   [ tstate = rstate --> ]
   END;

rclock_8N1_fs : MODULE  =
       BEGIN
         INPUT tstate : STATE
         INPUT rstate : STATE

       TRANSITION
       [ rstate /= tstate OR tstate = 9 --> ]
END;

rdec_8N1_fs : MODULE =
   BEGIN
     INPUT  tdata  : BOOLEAN
     OUTPUT rstate : STATE
     OUTPUT rbit   : BOOLEAN
    INITIALIZATION
     rbit  = TRUE;
     rstate = 9;
    TRANSITION
       [
          rstate  = 9                -->  
       [] rstate  = 9  AND NOT tdata -->  rbit' = FALSE;
                                          rstate' = 0;

       [] rstate /= 9                -->  rbit' = tdata;
                                          rstate' = rstate + 1;
       ]
     END;

tx_8N1_fs : MODULE = tclock_fs || tenc_8N1 
% || tenv; % comment this for registers
|| tenv_reg; % UNcomment this for registers

rx_8N1_fs : MODULE = rclock_8N1_fs || rdec_8N1_fs 
%; % comment this for registers
|| rdec_reg; % UNcomment this for registers

system_8N1_fs : MODULE = (tx_8N1_fs [] rx_8N1_fs);

%---------------------------------------
%  
% Invariants
%
%---------------------------------------


RMAX : TIME = RSAMPMAX + RSCANMAX;

disjunct_invar(n: STATE, tstate: STATE, rstate: STATE, 
               tdata: BOOLEAN, rbit: BOOLEAN, rclk: TIME, 
               tclk: TIME, stable: BOOLEAN): BOOLEAN =
         ((tstate = n + 1) AND 
          (rstate = n) AND    
          (rclk - tclk <= 
             n * RPERIODMAX - (n+1) * TPERIOD + RMAX - TSTABLE) AND
          (rclk - tclk >= 
             n * RPERIODMIN - (n+1) * TPERIOD + RSAMPMIN - TPERIOD))
      OR
          (
           (tstate = n) AND 
           (rstate = n) AND    
           stable AND
           (tdata = rbit) AND
           (rclk - tclk <= 
                n * RPERIODMAX - n * TPERIOD + RMAX - TSTABLE) AND
           (rclk - tclk >= 
                n * RPERIODMIN - (n+1) * TPERIOD + RSAMPMIN));

rec_states(n: STATE, tstate: STATE, rstate: STATE, 
           tdata: BOOLEAN, rbit: BOOLEAN, rclk: TIME, 
            tclk: TIME, stable: BOOLEAN): BOOLEAN =
          IF n = 0 THEN 
             disjunct_invar(n, tstate, rstate, tdata, rbit, rclk, tclk, stable)
          ELSE     
            disjunct_invar(n, tstate, rstate, tdata, rbit, rclk, tclk, stable)
         OR rec_states(n - 1, tstate, rstate, tdata, rbit, rclk, tclk, stable)
          ENDIF;

%---------------------------------------
%  
% Theorems (proof commands commented)
%
%---------------------------------------

% sal-inf-bmc -d 1 -i uartJrnl.sal l1
% sal-inf-bmc -d 1 -i uartJrnl.sal l2

   l1 : LEMMA system_8N1 |- G(tclk <= (rclk + TPERIOD) OR stable);

   l2 : LEMMA system_8N1 |- G(rclk <= tclk + RSAMPMAX OR 
                              rclk <= tclk + RPERIODMAX);

%  sal-inf-bmc -l l1 -l l2 -d 2 -i  uartJrnl.sal t0
  t0 : THEOREM system_8N1 |- G( 
      % idle
       ((rstate =  9) AND  
        (tstate = 9) AND 
        (tdata AND rbit) AND
        stable AND
        (rclk - tclk <= RSCANMAX))
   OR % start bit sent, not detected
       ((rstate = 9) AND 
        (tstate = 0) AND 
        (NOT tdata AND rbit) AND 
        (rclk - tclk <= RSCANMAX - TSTABLE))
   OR % --- unwind all the other cases
      rec_states(8, tstate, rstate, tdata, rbit, rclk, tclk, stable));

% sal-inf-bmc -d 1 -i -l t0 uartJrnl.sal Uart_Thm
Uart_Thm : THEOREM system_8N1 |- G(rstate = tstate AND rstate /= 9 => rbit = tbit);

%---------------------------------------
%  
% Refinement Theorems 
% (proof commands commented)
%
%---------------------------------------

% sal-inf-bmc -d 1 -i -l t0 uartJrnl.sal const_thm
const_thm : THEOREM system_8N1 |- G((tstate /= 0 OR rstate /= 9) => stable);

% sal-inf-bmc -d 1 -i -l t0 uartJrnl.sal tclock_thm
% sal-inf-bmc -d 1 -i -l t0 uartJrnl.sal rclock_thm
  tclock_thm : THEOREM system_8N1 |- G(tclk = time(tclk,rclk) => tstate = rstate);

  rclock_thm : THEOREM system_8N1 |- G(rclk = time(rclk,tclk) =>
                                   (rstate /= tstate OR (tstate = 9)));

% sal-inf-bmc -d 2 -i -l t0 -l const_thm uartJrnl.sal rdec_thm1
% sal-inf-bmc -d 2 -i -l t0 -l const_thm uartJrnl.sal rdec_thm2
% sal-inf-bmc -d 2 -i -l t0 -l const_thm uartJrnl.sal rdec_thm3
  rdec_thm1 : THEOREM system_8N1 |- G(rstate = 9 AND X(rbit) => X(rbit) = rbit);

  rdec_thm2 : THEOREM system_8N1 |- G(rstate = 9 AND X(NOT rbit)
                                  AND X(rstate = 0) => NOT tdata);

  rdec_thm3 : THEOREM system_8N1 |- G(FORALL (i : [0..8]) :
                    rstate = i AND X(rstate = i+1) =>  X(rbit) = tdata);

%---------------------------------------
%  
% Theorems of the finite-state model
% (proof commands commented)
%
%---------------------------------------

% Run the following to ensure the finite-state model is not deadlocked.
% sal-deadlock-checker uartJrnl.sal system_8N1_fs

% sal-smc uartJrnl.sal StateThm1
StateThm1 : THEOREM system_8N1_fs |- G(rstate = tstate OR 
				((rstate + 1) MOD 10) = tstate);

% sal-smc uartJrnl.sal StateThm2
StateThm2 :  THEOREM system_8N1_fs |- G(FORALL (i : STATE) : 
             (i = rstate AND i = tstate) => X((i = rstate AND (i + 1) MOD 10 = tstate)
                                          OR (i = rstate AND i = tstate AND i = 9)));

% sal-smc uartJrnl.sal StateThm3
StateThm3 :  THEOREM system_8N1_fs |- G(FORALL (i : STATE) : 
               (i = rstate AND (i + 1) MOD 10 = tstate) => 
                   X(   ((i + 1) MOD 10 = rstate AND (i + 1) MOD 10 = tstate)
                     OR (i = 9 AND i = rstate AND 0 = tstate)));

% sal-smc uartJrnl.sal Thm
Thm :  THEOREM system_8N1_fs |- G(tstate = rstate AND rstate /= 9 => rbit = tbit);

% sal-smc uartJrnl.sal Thm_Uart_Reg
%% Uncomment register modules to prove this theorem
Thm_Uart_Reg :  THEOREM system_8N1_fs |- G(rstate = 8 => rreg = treg);

% sal-smc uartJrnl.sal Liveness
Liveness: THEOREM system_8N1_fs |- G(F(rstate /= 9) => 
                              F(tstate = 9 AND rstate = 9));


END