CristalCaveGem » LustreC » Lustrec-Tests

--Historically

node H(X:bool) returns (Y:bool);

let

    Y = X -> (X and (pre Y));

tel

--Y since inclusive X

node SI(X,Y: bool) returns (Z:bool);

let

Z = Y and (X or (false -> pre Z));

tel

--Y since X

node S(X,Y: bool) returns (Z:bool);

let

Z = X or (Y and (false -> pre Z));

tel

--Once

node O(X:bool) returns (Y:bool);

let

 Y = X or (false -> pre Y);

tel

node First( X : bool ) returns ( Y : bool );

let

  Y = X -> pre Y;

tel

--Timed Once: less than or equal to N

node OTlore(const N: int; X: bool; ) returns (Y: bool);

    var C:int;

let

    C = if X then 0

        else (-1 -> pre C + (if pre C <0 then 0 else 1));

    Y = First(X)

        ->

        (if pre C < 0  then false

         else C <= N

        );

tel

-- Timed Historically: less than or equal to N

node HTlore(const N: int; X: bool) returns (Y: bool);

let

  Y = not OTlore(N, not X);

tel

-- Timed Since: less than or equal to N

node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);

let

  Z = S(X, Y) and OTlore(N, X);

tel

-- Timed Since Inclusive: less than or equal to N

node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);

let

  Z = SI(X,Y) and OTlore(N, X);

tel

node abs(x:real)

returns(y:real);

let

	y = if x >= 0.0 then x else - x;

tel

node max(x1, x2:real)

returns(y:real);

let

	y = if x1 >= x2 then x1 else x2;

tel

node min(x1, x2:real)

returns(y:real);

let

	y = if x1 >= x2 then x2 else x1;

tel

node ToInt (X: bool) returns (N: int) ;

let

  N = if X then 1 else 0 ;

tel

node Count (X: bool) returns (N: int) ;

let

  N = ToInt(X) -> ToInt(X) + pre N ;  

tel

(*@

contract TriplexSignalMonitorSpec(Tlevel:real; ia:real; ib:real; ic:real; PCLimit: int; ) returns (FC: int; set_val: real; TC: int; PC: int);

--Block Path: triplex_12B

let

var FTP:bool = true -> false;

 var absAB: real = abs(ia - ib);

 var absAC: real = abs(ia - ic);

 var absBC: real = abs(ib - ic);

 var avg: real = (ia + ib + ic) / 3.0;

 var mid_value:real = if (abs(ia - avg) > abs(ic - avg) and abs(ib - avg) > abs(ic - avg)) then ic 

                      else if (abs(ia - avg) > abs(ib - avg)) then ib 

                      else ia;

var preFC: int = 0 -> pre FC;

var prePC: int = 0 -> pre PC;

var prePCLimit: int = 0 -> pre PCLimit;

var prevSet_val: real = 0.0 -> pre set_val;

-- calculate is_a_miscompare 

var C1:bool = absAB > Tlevel;

var C2:bool = absBC > Tlevel;

var C3:bool = absAC > Tlevel;

var is_a_miscompare : bool =  (not C1 and C2 and C3)  or (C1 and not C2 and C3) or (C1 and C2 and not C3);

-- Assumptions

assume PCLimit > 0 ;

assume true -> PCLimit = prePCLimit;

assume true -> Tlevel = pre Tlevel;

-- when preFC = 0 & prePC > prePCLimit TriplexSignalMonitor shall immediately satisfy FC > 0

--guarantee "RM001" S( (((preFC = 0 and prePC > prePCLimit) => (FC > 0)) and FTP), ((preFC = 0 and prePC > prePCLimit) => (FC > 0)) );

--guarantee "RM001V2" is_a_miscompare and prePC > PCLimit => FC > 0;

-- when FC =1 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ib)

--guarantee "RM003a" (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )) or (S( ((set_val = 0.5 * ( ia + ib )) and ((FC = 1) and (FTP or (pre (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )))))), (set_val = 0.5 * ( ia + ib )) ));

--guarantee "RM003aV2" FC = 1 => set_val = 0.5 * (ia +ib);

-- when FC =2 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ic).

--guarantee "RM003b"  (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )) or (S( ((set_val = 0.5 * ( ia + ic )) and ((FC = 2) and (FTP or (pre (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )))))), (set_val = 0.5 * ( ia + ic )) ));

--guarantee "RM003bV2" FC = 2 => set_val = 0.5 * (ia +ic);

-- when FC =4 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ib +ic)

--guarantee "RM003c" (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )) or (S( ((set_val = 0.5 * ( ib + ic )) and ((FC = 4) and (FTP or (pre (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )))))), (set_val = 0.5 * ( ib + ic )) ));

--guarantee "RM003cV2" FC = 4 => set_val = 0.5 * (ib +ic);

-- when preFC =0 TriplexSignalMonitor shall immediately satisfy set_val = mid_value

--guarantee "RM002" S( (((preFC = 0) => (set_val = mid_value)) and FTP), ((preFC = 0) => (set_val = mid_value)) );

--guarantee "RM002V2" FC = 0 => set_val = mid_value;

-- when (absAB > Tlevel & absAC >Tlevel) | (absAB > Tlevel & absBC > Tlevel) | (absAC > Tlevel & absBC > Tlevel) TriplexSignalMonitor shall always satisfy set_val = prevSet_val

--guarantee "RM004" (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )) or (S( ((set_val = prevSet_val) and ((( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel )) and (FTP or (pre (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )))))), (set_val = prevSet_val) ));

--Explanaton from document: 

--    -A miscompare that persists but has not yet been declared failed is known as a failure in progress.

--       can be expressed as "is_a_miscompare and prePC > 0 and prePC < PCLimit"

--    -A second failure can be expressed as "Count(FC > 0) = 1"

--[RM-004] If a second failure is in progress, the selected value shall remain unchanged from the previous selected value.

guarantee "RM004V2"  Count(FC > 0) = 1   and is_a_miscompare and prePC > 0 and prePC < PCLimit => set_val = prevSet_val;

--guarantee true ->   Count(FC > 0) = 1  and ia <> pre ia and ib <> pre ib  and ic <> pre ic  and prePC > 0  and prePC < PCLimit => set_val   <> prevSet_val;

tel

*)