SPEC

local p,q,r,s,t,u : bool

macro first = !(-)true

PROPERTY a : <>p /\ []q <==> <>(p /\ []q)                       % not valid
PROPERTY b : <>p /\ []q <==> [](<>p /\ q)                       % not valid
PROPERTY c : <>[]p /\ <>[]q <==> <>([]p /\ []q)                 % valid
PROPERTY d : (p Until q) Until q <==> p Until q                 % valid
PROPERTY e : p Until q <==>((!p)Until q --> p Until q)          % not valid
PROPERTY f : p Until q /\ q Until r <==> p Until r              % not valid
PROPERTY g : <>p <==> [](<>p \/ <->p)                           % not valid
PROPERTY h : <><->p <==> <-><>p                                 % valid

PROPERTY i : (q ==> <->p) <--> (!q) Awaits p                    % valid
PROPERTY j : ([]p \/ []q) <--> []([-]p \/ [-]q)                 % valid
PROPERTY k : (p --> []q) <--> [](<->p --> q)                    % not valid
PROPERTY l : <>(p/\<->q) <--> <>(q/\ <>p)                       % valid
PROPERTY m : (<>p /\ <>q) <--> <>(<->p /\ <->q)                 % valid


PROPERTY n : ([]p \/<>q) <==> p Awaits(<>q)
PROPERTY o : (p ==> <>q) <--> []<>((!p) Backto q)
PROPERTY p : (p ==> <>q) <==> []<>((!p) Backto q)
PROPERTY q : ([]<>p /\ []<>q) <--> []<>(q /\ !(-)!((!q) Backto p))
PROPERTY r : <>p <--> <><->p
PROPERTY s : (p ==> <>[]q) <--> <>[](<->p --> q)
PROPERTY t : (<>[]p \/ <>[]q) <--> <>[](q \/ !(-)!(p Backto(p /\ !q))) 
PROPERTY u : <>[](p --> []q) <--> (<>[]q \/ <>[] !p)
PROPERTY v : ()()p <==> [](((-)(-)first) --> p)
PROPERTY w : p Until q <--> <>(q /\ !(-)![-]p)
PROPERTY x : (p ==> (!q) Awaits r) <--> (q ==> (!p) Backto r)
PROPERTY y : !(p Until q) <--> (!q) Awaits(!p /\ !q)
PROPERTY z : !(p Until q) <==> (!q) Awaits(!p /\ !q)