Profile

 1 ```--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 ``` ```(*@ ``` ```contract integrator_12BSpec(BL:real; ic:real; reset:bool; T:real; TL:real; xin:real; ) returns (yout: real; ); ``` ```--Block Path: integrator_12B ``` ```let ``` ```var FTP:bool = true -> false; ``` ```var xinpv: real = 0.0 -> pre xin; ``` ```var ypv: real = 0.0 -> pre yout; ``` ```var normal: bool = not reset and yout <= TL and yout >= BL; ``` ```var normal_yout : real = T * 0.5 * ( xin + xinpv ) + ypv; ``` ```assume BL <= TL; ``` ```--assume T > 0.0; ``` ```guarantee "TUI-002" S( ((yout <= TL and yout >= BL) and FTP), (yout <= TL and yout >= BL) ); ``` ```guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP)); ``` ```guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout; ``` ```guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre ( not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre ( not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre ( not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))); ``` ```tel ``` ```*) ```