CristalCaveGem » LustreC

-- |=================================================================|

--

--                       Specification nodes.

--

-- |=================================================================|

node Rise 

  (I : bool)

returns 

  (O : bool);

let 

  O = false -> (not pre I) and I;

tel;

-- |=================================================================|

--

--                            System nodes.

--

-- |=================================================================|

node PFS_Logic

  (riseTS, riseOSPF : bool;

   Primary_Side : bool; 

   PFS_Initial_Value : bool)

returns 

  (PFS : bool);

var

  -- Pfs_change:  bool; 

  -- Has_happened:  bool;

  Start_to_Pilot_Flying:  bool;

  Start_to_Inhibited:  bool;

  Inhibited_to_Listening:  bool;

  Inhibited_to_Inhibited: bool;

  Listening_to_Pilot_Flying: bool;

  Pilot_Flying_to_Inhibited : bool;

  State : int;

  Inhibit_count:  int;

  Inhibit_count_bounded : bool;

  Pfs_state_consistency : bool;

  State_bounded : bool;

  St_Inhibited:  int;

  St_Listening :  int;

  St_Pilot_Flying : int;

  St_Start :  int;

  St_Stop : int;

  Inhibit_count_max: int;

let

  -- MAIN;

  assert Primary_Side = (Primary_Side -> pre( Primary_Side));

  assert PFS_Initial_Value =  (PFS_Initial_Value -> pre( PFS_Initial_Value));

  assert State>=0 and State <=5;

  assert  Inhibit_count>=0 and  Inhibit_count <=2;

  Inhibit_count_max = 2 -> pre(Inhibit_count_max);

  St_Inhibited = 2 -> pre(St_Inhibited);

  St_Listening = 3 -> pre(St_Listening);

  St_Pilot_Flying = 4 -> pre(St_Pilot_Flying);

  St_Start =  1 -> pre(St_Start);

  St_Stop = 5-> pre(St_Stop);

  Start_to_Pilot_Flying = 

    ((St_Start -> pre(State)) = St_Start) and Primary_Side;

  Start_to_Inhibited = 

    ((St_Start -> pre(State)) = St_Start) and (not Primary_Side);

  Inhibited_to_Listening = 

    ((St_Start -> pre(State)) = St_Inhibited) and 

      (0 -> pre( Inhibit_count)) >=  Inhibit_count_max;

  Inhibited_to_Inhibited = 

    ((St_Start -> pre(State)) = St_Inhibited) and 

      not Inhibited_to_Listening;

  Listening_to_Pilot_Flying = 

    ((St_Start -> pre(State)) = St_Listening) and riseTS;

  Pilot_Flying_to_Inhibited = 

    ((St_Start -> pre(State)) = St_Pilot_Flying) and riseOSPF;

  State =

    if

      Inhibited_to_Inhibited or 

      Pilot_Flying_to_Inhibited or 

      Start_to_Inhibited

    then 

      St_Inhibited 

    else if 

      Inhibited_to_Listening 

    then 

      St_Listening

    else if 

      Listening_to_Pilot_Flying or 

      Start_to_Pilot_Flying 

    then 

      St_Pilot_Flying 

    else 

      (St_Start -> pre(State));

  PFS = 

    if 

      Listening_to_Pilot_Flying 

    then 

      true

    else if 

      Pilot_Flying_to_Inhibited 

    then 

      false

    else if 

      Start_to_Pilot_Flying 

    then 

      true

    else if 

      Start_to_Inhibited 

    then 

      false

    else 

      PFS_Initial_Value -> pre(PFS);

   Inhibit_count = 

    if 

      Inhibited_to_Inhibited 

    then 

      (0 -> pre( Inhibit_count)) + 1

    else if 

      Pilot_Flying_to_Inhibited 

    then 

      0

    else if 

      Start_to_Inhibited 

    then 

      0

    else 

      0 -> pre( Inhibit_count);

  Pfs_state_consistency = 

    not (State = St_Start) => (PFS = (State = St_Pilot_Flying));

  -- PROPERTY Pfs_state_consistency;

  -- Proved as property before 

  -- assert Pfs_state_consistency;

   Inhibit_count_bounded = 

     Inhibit_count >= 0 and  Inhibit_count <=  Inhibit_count_max;

  -- PROPERTY  Inhibit_count_bounded;

  -- Proved as property before 

  -- assert  Inhibit_count_bounded;

  State_bounded = State >= St_Start and State < St_Stop;

  -- -- PROPERTY State_bounded;

  -- Proved as property before 

  -- assert State_bounded;

tel;

node PFS_Side

  (TS, OSPF : bool;

   Primary_Side : bool; 

   PFS_Initial_Value : bool)

returns 

  (PFS : bool);

var

  PFSL_PFS : bool;

  riseTS_O : bool;

  riseOSPF_O : bool;

let

  -- assert Primary_Side= (Primary_Side -> pre(Primary_Side));

  -- assert  PFS_Initial_Value= (PFS_Initial_Value -> pre(PFS_Initial_Value));

  -- MAIN;

  PFSL_PFS =

    PFS_Logic(riseTS_O, riseOSPF_O, Primary_Side, PFS_Initial_Value);

  riseTS_O = Rise(TS);

  riseOSPF_O = Rise(OSPF);

  PFS = PFSL_PFS;

tel;

node Cross_Channel_Bus

  (I : bool;

   O_Initial_Value : bool; 

   prev_I_Initial_Value : bool)

returns

  (O : bool);

var

  Prev_I : bool;

  Start_to_Step : bool;

  Step_to_Step : bool;

  -- State_bounded : bool;

  --state : subrange [1,3] of int;

  State : int;

  -- state : enum { St_Step, St_Start };

-- const St_Step = 2;

-- const St_Start = 1;

-- const St_Stop = 3;

   St_Step :  int;

   St_Start :  int;

   St_Stop :  int;

let

  -- assert  O_Initial_Value=  (O_Initial_Value ->  pre(O_Initial_Value));

  -- assert    prev_I_Initial_Value =   (prev_I_Initial_Value -> pre(   prev_I_Initial_Value ));

  assert State>=1 and State <=3;

  St_Step = 2 -> pre(St_Step);

  St_Start = 1 -> pre(St_Start);

  St_Stop = 3 -> pre(St_Stop);

  Start_to_Step = (St_Start -> pre(State)) = St_Start;

  Step_to_Step = (St_Start -> pre(State)) = St_Step;

  State = 

    if 

      Start_to_Step or Step_to_Step 

    then 

      St_Step 

    else 

      (St_Start -> pre(State));

  Prev_I = 

    if Start_to_Step then I

    else if Step_to_Step then I

    else prev_I_Initial_Value -> pre(Prev_I);

  O = 

    if

      Start_to_Step 

    then 

      prev_I_Initial_Value -> pre(Prev_I)

    else if 

      Step_to_Step 

    then 

      prev_I_Initial_Value -> pre(Prev_I)

    else 

      O_Initial_Value -> pre(O);

tel;

-- |=================================================================|

--

--                   Top level environment nodes.

--

-- |=================================================================|

node PRESSED (p : bool) returns (b : bool);

let

  b = false -> (not pre p and p);

tel;

node PRESSED_SEEN (p, c : bool) returns (b : bool);

let

  b = false -> (not pre p and pre c) and (p and c);

tel;

node CHANGED (p : bool) returns (b : bool);

let

  b = false ->  not (p = pre p);

tel;

node false_longer_than (p: bool; n: int) returns (ok: bool);

var

  c: int;

let

  -- assert n = (n -> pre(n));

  c = if p then 0 else (1 -> pre c + 1);

  ok = c > n;

tel;

node quiescent

  (TS, CLK1, CLK3, CLK2, CLK4 : bool)

returns

  (out : bool) ;

let

  out =

    false_longer_than(PRESSED(TS), 46) and

    false_longer_than(PRESSED(TS), 46) and

    false_longer_than(PRESSED(TS), 46) and

    false_longer_than(PRESSED(TS), 46) ;

tel

-- |=================================================================|

--

--                           Top level node.

--

-- |=================================================================|

node PFS

  (TS, CLK1, CLK3, CLK2, CLK4 : bool) 

returns 

  (LPFS, RPFS : bool) ;

var

  RL_O : bool;

  RS_PFS : bool;

  LR_O : bool;

  LS_PFS : bool;

let

  LS_PFS = 

    -- condact(CLK1, PFS_Side(TS, RL_O, true, true), true);

    PFS_Side(TS, RL_O, true, true);

  RS_PFS = 

    -- condact(CLK3, PFS_Side(TS, LR_O, false, false), false);

    PFS_Side(TS, LR_O, false, false);

  LR_O = 

    -- condact(CLK2, Cross_Channel_Bus (LS_PFS, true, true), true);

     ((*! /inlining/: true; *)Cross_Channel_Bus (LS_PFS,  true,  true));

  RL_O =  

    -- condact(CLK4, Cross_Channel_Bus (RS_PFS, false, false), false);

      Cross_Channel_Bus (RS_PFS, false, false);

  LPFS = LS_PFS;

  RPFS = RS_PFS;

tel;

-- node PFS_contract_R5

--   (TS, CLK1, CLK3, CLK2, CLK4 : bool)

-- returns

--   (OK : bool) ;

--   var 

--   LPFS: bool;

--   RPFS: bool;

--   req: bool;

-- let

--   req = quiescent(TS, CLK1, CLK2, CLK3, CLK4) ;

--   assert req;

--   LPFS,  RPFS = PFS (TS, CLK1, CLK3, CLK2, CLK4);

--   OK =  not (CHANGED(RPFS) or CHANGED(LPFS)) ;

--   --!PROPERTY :  OK;

--   --!MAIN : true;  

-- tel

-- node PFS_contract_R3

--   (TS, CLK1, CLK3, CLK2, CLK4 : bool)

-- returns

--   (OK : bool) ;

--   var 

--   LPFS: bool;

--   RPFS: bool;

--   req: bool;

-- let

--   LPFS,  RPFS = PFS (TS, CLK1, CLK3, CLK2, CLK4);

--   req =  true -> pre quiescent(TS, CLK1, CLK2, CLK3, CLK4) ;

--   assert req;

--   OK =  true -> (

--     (not pre LPFS and PRESSED_SEEN(TS, CLK1) => LPFS) and

--     (not pre RPFS and PRESSED_SEEN(TS, CLK3) => RPFS)

--   ) ;

--   --!PROPERTY :  OK;

--   --!MAIN : true;  

-- tel

node top

  (TS, CLK1, CLK3, CLK2, CLK4 : bool)

returns

  (OK : bool) ;

  var 

  LPFS: bool;

  RPFS: bool;

  req: bool;

let

  LPFS,  RPFS = PFS (TS, CLK1, CLK3, CLK2, CLK4);

  req =  quiescent(TS, CLK1, CLK2, CLK3, CLK4) ;

  --assert req;

  OK = LPFS = not RPFS ;

  --!PROPERTY :  OK;

  --!MAIN : true;

tel