PLTL+RV_2_Lustre.lus

-- Runtime Monitoring Operators (Start, End, Interval, First, Last)

-- Start(\phi) := \phi is true in the current state and false in the previous state
node Start(i: bool) returns (o:bool);
let
   o = i and (not Y(i));  
tel

--node Start(i: bool) returns (o:bool);
--let
--   o = i and (not (false -> pre(i)));  
--tel

-- End \phi is false in the current state and true in the previous state
node End(i: bool) returns (o:bool);
let
   o = not i and Y(i);  
tel

--node End(i: bool) returns (o:bool);
--let
--   o = not i and Y(i);  
--tel

-- Interval [\phi,\psi) := \psi was never true since last time \phi was true, include the state when \phi was true.
node Interval(i, j: bool) returns (o:bool);
let
   o = (not j) and S (Y(not j),  i);  
tel

--node Interval(i, j: bool) returns (o:bool);
--let
--   o = (not j) and S (false -> pre (not j),  i);  
--tel

-- Intervalw [\phi,\psi) := weak internal
node Intervalw(i, j: bool) returns (o:bool);
let
   o = (not j) and S (Z(not j),  i);  
tel

-- First
node First(i: bool) returns (o:bool);
let
    o = i and Sofar(Z(not i));
tel

--node First( i : bool ) returns ( o : bool );
--let
--    o = i and Sofar(true -> pre(not i));
--tel

-- Last
node Last(i: bool) returns (o:bool);
let
   o = First(not i);
tel

-- Past Time LTL Temporal Operators (Y, Z, O, H, S, T) in Lustre.
-- [Reference for Past Time LTL:]
-- Cimatti, Alessandro, Marco Roveri, and Daniel Sheridan. "Bounded verification of past LTL." 
-- In International Conference on Formal Methods in Computer-Aided Design, 
-- pp. 245-259. Springer, Berlin, Heidelberg, 2004.


-- Yesterday := Y(\phi) is true iff \phi holds at the previous time instant while it is always false at time point zero.

node Y(i: bool) returns (o:bool);
let
    o = false -> (pre i);
tel

-- Weak Yesterday := Z(\phi) is true iff \phi holds at the previous time instant while it is always true at time point zero.

node Z(i: bool) returns (o:bool);
let
    o = true -> (pre i);
tel

-- Usage: not(Y(i)) = Z (not(i))


-- Once := O(\phi) was true iff \phi is true at some past time instance including the present time point.
node O(i: bool) returns (o:bool);
let
    o = i or Y(o);
tel

-- alternative definition
--node O(i: bool) returns (o:bool);
--let
--    o = i or (false -> pre o);
--tel


-- -- Sofar(\phi) is true at any point iff \phi has been true from the beginning until that point
node Sofar( i : bool ) returns ( o : bool );
let
 o = i -> (i and (pre o));
tel

-- Historically := H(\phi) is true if and only if \phi is always true in the past including the present time.
node H(i: bool) returns (o:bool);
let
    o = i and Z(o);
tel

--node H(i: bool) returns (o:bool);
--let
--    o = i and (true -> pre o);
--tel


-- X Since Y  
-- \phi Since \psi is true if and only if \psi is true in the past and \phi is true from then up to now.
node S(i, j: bool) returns (o:bool);
let
    o = j or (i and Y(o));
tel

--node S(i, j: bool) returns (o:bool);
--let
--    o = j or (i and (false ->(o)));
--tel

node Sw(i, j: bool) returns (o:bool);
let
    o = j or (i and Z(o));
tel

--node Sw(i, j: bool) returns (o:bool);
--let
--    o = j or (i and (true -> pre o));
--tel
-- Since X Y. 
-- Since(\phi,\psi) is true precisely when \phi has been true at some point and \psi has been continuously true afterwards.
-- node Since( X, Y : bool ) returns ( Z : bool );
-- let
--  Z =  X or (Y and (false -> pre Z));
--tel


-- T (Trigger)
-- Usage: \phi T \psi = \not (\not\phi S \not\psi)
-- \phi T \psi is true if and only if \psi continuously holds in the past or \psi holds until \phi holds 
node T(i: bool; j:bool) returns (o:bool);
let
    o = j and (i or Z(o));
tel

--node T(i: bool; j:bool) returns (o:bool);
--let
--    o = j and (i or (true -> o));
--tel


node EQ_PLTL(phi:bool; psi:bool) returns (o:bool);
var p1: bool;
var p2: bool;
var p3: bool;
var p4: bool;
var p5: bool;
var p6: bool;
var p7: bool;
var p8: bool;
var p9: bool;

var p10: bool;
var p11: bool;
var p12: bool;
var p13: bool;
var p14: bool;
var p15: bool;

let

    p1 = Y(phi) = (false -> pre(phi));
    --%PROPERTY "Y(\phi) = false -> pre(\phi)" p1;

    p2 = Z(not phi) = not Y(phi) ;
    --%PROPERTY "Z(not \phi) = not Y(\phi)" p2;

    p3 = O(not phi) = not H(phi);
    --%PROPERTY "O(not \phi) = not H(\phi)" p3;

    p4 = H(not phi) = not O(phi);
    --%PROPERTY "H(not \phi) = not O(\phi)" p4;

    p5 = T(not phi, not psi) = not S(phi, psi) ;
    --%PROPERTY "T(not \phi, not \psi) = not S(\phi,\psi)" p5;
    
    p6 = Sofar(phi) = H(phi);
    --%PROPERTY "Sofar(\phi) = H(\phi)" p6;

    ---------------------------------------------------------------
    
    -- Proposition1 Ref[]
    p7 = O(phi) = S(true, phi);
    --%PROPERTY "O(\phi) =  S(true, \phi)" p7;

    p8 = H(phi) = not O(not phi);
    --%PROPERTY "H(\phi) = not O(not \phi)" p8;
    
    p9 = H(phi) = Sw(phi, false);
    --%PROPERTY "H(phi) = S(phi, false)" p9;
    
    p10 = Sw(phi, psi) = (H(phi) or S(phi, psi));
    --%PROPERTY "Sw(\phi, \psi) = H(\phi) or S(\phi, \psi)" p10;

    p11 = S(phi, psi) = (O(psi) and Sw(phi, psi));
    --%PROPERTY "S(\phi, \psi) = O(\psi) and Sw(\phi, \psi)" p11;
    
    ---------------------------------------------------------------
   
    p12 = Start(phi) = (phi and not Y(phi));
    --%PROPERTY p12;
    
    p13 = End(phi) = (not phi and Y(phi));
    --%PROPERTY p13;
    
    p14 = Interval(phi, psi) = (not psi and S(Y(not psi), phi));
    --%PROPERTY p14;
    
    p15 = Intervalw(phi, psi) = (not psi and Sw(Y(not psi), phi));

    ---------------------------------------------------------------

tel