// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  more LTL theorems
//
// **************************************************************************

module LTL1(bool a,b,c,q)  {
nothing;
} satisfies {

// ---- implementing temporal operators by watchdogs ----------

WatchWU : assert A (!q & G(X q <-> q | b)    -> ( [a WU b] <-> G(q|a|b)  ));
WatchWB : assert A (!q & G(X q <-> q | a&!b) -> ( [a WB b] <-> G(q|!b)   ));
WatchWW : assert A (!q & G(X q <-> q | b)    -> ( [a WW b] <-> G(q|a|!b) ));
WatchSU : assert A (!q & G(X q <-> q | b)    -> ( [a SU b] <-> G(q|a|b)  & F b));
WatchSB : assert A (!q & G(X q <-> q | a&!b) -> ( [a SB b] <-> G(q|!b)   & F a));
WatchSW : assert A (!q & G(X q <-> q | b)    -> ( [a SW b] <-> G(q|a|!b) & F b));

// ---- recursion laws of temporal operators ------------------

RecurG  : assert A ((G a) <-> a & X G a);
RecurF  : assert A ((F a) <-> a | X F a);
RecurSU : assert A ([a SU b] <->  b | a & X[a SU b]);
RecurWU : assert A ([a WU b] <->  b | a & X[a WU b]);
RecurSB : assert A ([a SB b] <-> !b & (a | X[a SB b]));
RecurWB : assert A ([a WB b] <-> !b & (a | X[a WB b]));
RecurSW : assert A ([a SW b] <->  b & a | !b & X[a SW b]);
RecurWW : assert A ([a WW b] <->  b & a | !b & X[a WW b]);

RecurPG  : assert A ((PG a) <-> a & PWX PG a);
RecurPF  : assert A ((PF a) <-> a | PSX PF a);
RecurPSU : assert A ([a PSU b] <->  b | a & PSX[a SU b]);
RecurPWU : assert A ([a PWU b] <->  b | a & PWX[a WU b]);
RecurPSB : assert A ([a PSB b] <-> !b & (a | PSX[a SB b]));
RecurPWB : assert A ([a PWB b] <-> !b & (a | PWX[a WB b]));
RecurPSW : assert A ([a PSW b] <->  b & a | !b & PSX[a SW b]);
RecurPWW : assert A ([a PWW b] <->  b & a | !b & PWX[a WW b]);

// ---- negation normal form -----------------------

NotG  : assert   A (!G a <-> F !a);
NotF  : assert   A (!F a <-> G !a);
NotX  : assert   A (!X a <-> X !a);
NotSU : assert   A (![a SU b] <-> [(!a) WB b]);
NotSB : assert   A (![a SB b] <-> [(!a) WU b]);
NotSW : assert   A (![a SW b] <-> [(!a) WW b]);
NotWU : assert   A (![a WU b] <-> [(!a) SB b]);
NotWB : assert   A (![a WB b] <-> [(!a) SU b]);
NotWW : assert   A (![a WW b] <-> [(!a) SW b]);

NotPG  : assert  A (!PG a <-> PF !a);
NotPF  : assert  A (!PF a <-> PG !a);
NotPSX : assert  A (!PSX a <-> PWX !a);
NotPSU : assert  A (![a PSU b] <-> [(!a) PWB b]);
NotPSB : assert  A (![a PSB b] <-> [(!a) PWU b]);
NotPSW : assert  A (![a PSW b] <-> [(!a) PWW b]);
NotPWX : assert  A (!PWX a <-> PSX !a);
NotPWU : assert  A (![a PWU b] <-> [(!a) PSB b]);
NotPWB : assert  A (![a PWB b] <-> [(!a) PSU b]);
NotPWW : assert  A (![a PWW b] <-> [(!a) PSW b]);

// ---- CONJUNCTIVE_NORMAL_FORM --------------------

Conj_X   : assert A G (X (a & b) <-> X a & X b);
Conj_G   : assert A G (G (a & b) <-> G a & G b);
Conj_WW  : assert A G ([(a & b) WW c] <-> [a WW c] & [b WW c]);
Conj_SW  : assert A G ([(a & b) SW c] <-> [a SW c] & [b SW c]);
Conj_WU  : assert A G ([(a & b) WU c] <-> [a WU c] & [b WU c]);
Conj_SU  : assert A G ([(a & b) SU c] <-> [a SU c] & [b SU c]);
Conj_WB  : assert A G ([c WB (a | b)] <-> [c WB a] & [c WB b]);
Conj_SB  : assert A G ([c SB (a | b)] <-> [c SB a] & [c SB b]);
Conj_PWX : assert A G (PWX (a & b) <-> PWX a & PWX b);
Conj_PSX : assert A G (PSX (a & b) <-> PSX a & PSX b);
Conj_PG  : assert A G (PG (a & b) <-> PG a & PG b);
Conj_PWW : assert A G ([(a & b) PWW c] <-> [a PWW c] & [b PWW c]);
Conj_PSW : assert A G ([(a & b) PSW c] <-> [a PSW c] & [b PSW c]);
Conj_PWU : assert A G ([(a & b) PWU c] <-> [a PWU c] & [b PWU c]);
Conj_PSU : assert A G ([(a & b) PSU c] <-> [a PSU c] & [b PSU c]);
Conj_PWB : assert A G ([c PWB (a | b)] <-> [c PWB a] & [c PWB b]);
Conj_PSB : assert A G ([c PSB (a | b)] <-> [c PSB a] & [c PSB b]);

// ---- DISJUNCTIVE_NORMAL_FORM --------------------------------

Disj_X   : assert A G (X (a | b) <-> (X a | X b));
Disj_F   : assert A G (F (a | b) <-> (F a | F b));
Disj_WW  : assert A G ([(a | b) WW c] <-> ([a WW c] | [b WW c]));
Disj_SW  : assert A G ([(a | b) SW c] <-> ([a SW c] | [b SW c]));
Disj_WU  : assert A G ([a WU (b | c)] <-> ([a WU b] | [a WU c]));
Disj_SU  : assert A G ([a SU (b | c)] <-> ([a SU b] | [a SU c]));
Disj_WB  : assert A G ([(a | b) WB c] <-> ([a WB c] | [b WB c]));
Disj_SB  : assert A G ([(a | b) SB c] <-> ([a SB c] | [b SB c]));
Disj_PWX : assert A G (PWX (a | b) <-> (PWX a | PWX b));
Disj_PSX : assert A G (PSX (a | b) <-> (PSX a | PSX b));
Disj_PF  : assert A G (PF (a | b) <-> (PF a | PF b));
Disj_PWW : assert A G ([(a | b) PWW c] <-> ([a PWW c] | [b PWW c]));
Disj_PSW : assert A G ([(a | b) PSW c] <-> ([a PSW c] | [b PSW c]));
Disj_PWU : assert A G ([a PWU (b | c)] <-> ([a PWU b] | [a PWU c]));
Disj_PSU : assert A G ([a PSU (b | c)] <-> ([a PSU b] | [a PSU c]));
Disj_PWB : assert A G ([(a | b) PWB c] <-> ([a PWB c] | [b PWB c]));
Disj_PSB : assert A G ([(a | b) PSB c] <-> ([a PSB c] | [b PSB c]));

// ---- SU and PSU are expressively complete ------------------

G_as_SU  : assert    A (G a <-> ![true SU (!a)]);
F_as_SU  : assert    A (F a <->  [true SU a]);
SB_as_SU : assert    A ([a SB b] <->  [(!b) SU (a&!b)]);
SW_as_SU : assert    A ([a SW b] <->  [(!b) SU (a&b)]);
WU_as_SU : assert    A ([a WU b] <-> ![(!b) SU (!a&!b)]);
WB_as_SU : assert    A ([a WB b] <-> ![(!a) SU b]);
WW_as_SU : assert    A ([a WW b] <-> ![(!a|!b) SU (!a&b)]);

PG_as_PSU  : assert  A (PG a <-> ![true PSU (!a)]);
PF_as_PSU  : assert  A (PF a <->  [true PSU a]);
PSB_as_PSU : assert  A ([a PSB b] <->  [(!b) PSU (a&!b)]);
PSW_as_PSU : assert  A ([a PSW b] <->  [(!b) PSU (a&b)]);
PWU_as_PSU : assert  A ([a PWU b] <-> ![(!b) PSU (!a&!b)]);
PWB_as_PSU : assert  A ([a PWB b] <-> ![(!a) PSU b]);
PWW_as_PSU : assert  A ([a PWW b] <-> ![(!a|!b) PSU (!a&b)]);

// ---- WU and PWU are expressively complete ------------------

G_as_WU  : assert    A (G a <->  [a WU false]);
F_as_WU  : assert    A (F a <-> ![(!a) WU false]);
SU_as_WU : assert    A ([a WU b] <-> ![(!b) SU (!a&!b)]);
SB_as_WU : assert    A ([a SB b] <-> ![(!a) WU b]);
SW_as_WU : assert    A ([a SW b] <-> ![(!a|!b) WU (!a&b)]);
WB_as_WU : assert    A ([a WB b] <->  [(!b) WU (a&!b)]);
WW_as_WU : assert    A ([a WW b] <->  [(!b) WU (a&b)]);

PG_as_PWU  : assert  A (PG a <->  [a PWU false]);
PF_as_PWU  : assert  A (PF a <-> ![(!a) PWU false]);
PSU_as_PWU : assert  A ([a PWU b] <-> ![(!b) PSU (!a&!b)]);
PSB_as_PWU : assert  A ([a PSB b] <-> ![(!a) PWU b]);
PSW_as_PWU : assert  A ([a PSW b] <-> ![(!a|!b) PWU (!a&b)]);
PWB_as_PWU : assert  A ([a PWB b] <->  [(!b) PWU (a&!b)]);
PWW_as_PWU : assert  A ([a PWW b] <->  [(!b) PWU (a&b)]);

// ---- SB and PSB are expressively complete ------------------

G_as_SB  : assert    A (G a <-> ![(!a) SB false]);
F_as_SB  : assert    A (F a <-> [a SB false]);
SU_as_SB : assert    A ([a SU b] <->  [b SB (!a & !b)]);
SB_as_SB : assert    A ([a WU b] <-> ![(!a) SB b]);
SW_as_SB : assert    A ([a SW b] <->  [b SB (!a & b)]);
WB_as_SB : assert    A ([a WW b] <-> ![b SB (a & b)]);
WW_as_SB : assert    A ([a WB b] <-> ![b SB (a & !b)]);

PG_as_PSB  : assert  A (PG a <-> ![(!a) PSB false]);
PF_as_PSB  : assert  A (PF a <-> [a PSB false]);
PSU_as_PSB : assert  A ([a PSU b] <->  [b PSB (!a & !b)]);
PSB_as_PSB : assert  A ([a PWU b] <-> ![(!a) PSB b]);
PSW_as_PSB : assert  A ([a PSW b] <->  [b PSB (!a & b)]);
PWB_as_PSB : assert  A ([a PWW b] <-> ![b PSB (a & b)]);
PWW_as_PSB : assert  A ([a PWB b] <-> ![b PSB (a & !b)]);

// ---- WB and PWB are expressively complete ------------------

G_as_WB  : assert    A (G a <->  [false WB (!a)]);
F_as_WB  : assert    A (F a <-> ![false WB a]);
SU_as_WB : assert    A ([a SU b] <-> ![(!a) WB b]);
WU_as_WB : assert    A ([a WU b] <->  [b WB (!a & !b)]);
SW_as_WB : assert    A ([a SW b] <-> ![b WB (a & b)]);
SB_as_WB : assert    A ([a SB b] <-> ![b WB (a & !b)]);
WW_as_WB : assert    A ([a WW b] <->  [(a & b) WB (!a & b)]);

PG_as_PWB  : assert  A (PG a <->  [false PWB (!a)]);
PF_as_PWB  : assert  A (PF a <-> ![false PWB a]);
PSU_as_PWB : assert  A ([a PSU b] <-> ![(!a) PWB b]);
PWU_as_PWB : assert  A ([a PWU b] <->  [b PWB (!a & !b)]);
PSW_as_PWB : assert  A ([a PSW b] <-> ![b PWB (a & b)]);
PWW_as_PWB : assert  A ([a PWW b] <->  [(a & b) PWB (!a & b)]);
PSB_as_PWB : assert  A ([a PSB b] <-> ![b PWB (a & !b)]);

// ---- SW and PSW are expressively complete ------------------

G_as_SW  : assert    A (G a <-> ![true SW (!a)]);
F_as_SW  : assert    A (F a <->  [true SW a]);
SU_as_SW : assert    A ([a SU b] <->  [b SW (a -> b)]);
WU_as_SW : assert    A ([a WU b] <-> ![(!b) SW (a -> b)]);
WB_as_SW : assert    A ([a WB b] <-> ![b SW (a | b)]);
SB_as_SW : assert    A ([a SB b] <->  [(!b) SW (a | b)]);
WW_as_SW : assert    A ([a WW b] <-> ![(!a) SW b]);

PG_as_PSW  : assert  A (PG a <-> ![true PSW (!a)]);
PF_as_PSW  : assert  A (PF a <->  [true PSW a]);
PSU_as_PSW : assert  A ([a PSU b] <->  [b PSW (a -> b)]);
PWU_as_PSW : assert  A ([a PWU b] <-> ![(!b) PSW (a -> b)]);
PWW_as_PSW : assert  A ([a PWW b] <-> ![(!a) PSW b]);
PSB_as_PSW : assert  A ([a PSB b] <->  [(!b) PSW (a | b)]);
PWB_as_PSW : assert  A ([a PWB b] <-> ![b PSW (a | b)]);

// ---- WW and PWW are expressively complete ------------------

G_as_WW  : assert    A (G a <->  [false WW (!a)]);
F_as_WW  : assert    A (F a <-> ![false WW a]);
SU_as_WW : assert    A ([a SU b] <-> ![(!b) WW (a -> b)]);
WU_as_WW : assert    A ([a WU b] <->  [  b  WW (a -> b)]);
WB_as_WW : assert    A ([a WB b] <->  [(!b) WW (a | b)]);
SB_as_WW : assert    A ([a SB b] <-> ![  b  WW (a | b)]);
SW_as_WW : assert    A ([a SW b] <-> ![(!a) WW b]);

PG_as_PWW  : assert  A (PG a <->  [false PWW (!a)]);
PF_as_PWW  : assert  A (PF a <-> ![false PWW a]);
PSU_as_PWW : assert  A ([a PSU b] <-> ![(!b) PWW (a -> b)]);
PWU_as_PWW : assert  A ([a PWU b] <->  [  b  PWW (a -> b)]);
PSW_as_PWW : assert  A ([a PSW b] <-> ![(!a) PWW b]);
PSB_as_PWW : assert  A ([a PSB b] <-> ![  b  PWW (a | b)]);
PWB_as_PWW : assert  A ([a PWB b] <->  [(!b) PWW (a | b)]);

MoreEvent : assert A(
([a WW b] <-> [(a & b) WW b]) &
([a WU b] <-> [(a & !b) WU b]) &
([a WB b] <-> [(a & !b) WB b]) &
([a SW b] <-> [(a & b) SW b]) &
([a SU b] <-> [(a & !b) SU b]) &
([a SB b] <-> [(a & !b) SB b]) &
([a PWW b] <-> [(a & b) PWW b]) &
([a PWU b] <-> [(a & !b) PWU b]) &
([a PWB b] <-> [(a & !b) PWB b]) &
([a PSW b] <-> [(a & b) PSW b]) &
([a PSU b] <-> [(a & !b) PSU b]) &
([a PSB b] <-> [(a & !b) PSB b])
);

// ------- immediate presence of event that is awaited for ---------

ImmediateEvent : assert A (b ->
([a WW b] <-> a) &
([a WU b] <-> true) &
([a WB b] <-> false) &
([b WB a] <-> !a) &
([a SW b] <-> a) &
([a SU b] <-> true) &
([a SB b] <-> false) &
([b SB a] <-> !a) &
([a PWW b] <-> a) &
([a PWU b] <-> true) &
([a PWB b] <-> false) &
([b PWB a] <-> !a) &
([a PSW b] <-> a) &
([a PSU b] <-> true) &
([a PSB b] <-> false) &
([b PSB a] <-> !a)
);

// ---- INITIALISATION ----------------------

Init_PWX : assert    A(  PWX a);
Init_PSX : assert    A( !PSX a);
Init_PG  : assert    A( PG a <-> a);
Init_PF  : assert    A( PF a <-> a);
Init_PSU : assert    A( [a PSU b] <-> b);
Init_PSW : assert    A( [a PSW b] <-> a & b);
Init_PSB : assert    A( [a PSB b] <-> a & !b);
Init_PWU : assert    A( [a PWU b] <-> a | b);
Init_PWW : assert    A( [a PWW b] <-> a | !b);
Init_PWB : assert    A( [a PWB b] <-> !b);

// ---- FIXPOINTS -----------------------------------------------

Fix_G   : assert A( G(q <-> a & X q)      <-> G(q <-> G a) | G!q );
Fix_F   : assert A( G(q <-> a | X q)      <-> G(q <-> F a) | G q);
Fix_U   : assert A( G(q <-> b | a & X q)      <-> G(q <-> [a WU b]) | G(q <-> [a SU b]));
Fix_W   : assert A( G(q <-> b & a | !b & X q) <-> G(q <-> [a WW b]) | G(q <-> [a SW b]));
Fix_B   : assert A( G(q <-> !b & (a | X q))   <-> G(q <-> [a WB b]) | G(q <-> [a SB b]));
Fix_PG  : assert A( G(q <-> a & PWX q)    <-> G(q <-> PG a));
Fix_PF  : assert A( G(q <-> a | PSX q)    <-> G(q <-> PF a));
Fix_PSU : assert A( G(q <-> b | a & PSX q)    <-> G(q <-> [a PSU b]));
Fix_PWU : assert A( G(q <-> b | a & PWX q)    <-> G(q <-> [a PWU b]));
Fix_PSB : assert A( G(q <-> !b & (a | PSX q)) <-> G(q <-> [a PSB b]));
Fix_PWB : assert A( G(q <-> !b & (a | PWX q)) <-> G(q <-> [a PWB b]));
Fix_PSW : assert A( G(q <-> a & b | !b & PSX q) <-> G(q <-> [a PSW b]));
Fix_PWW : assert A( G(q <-> a & b | !b & PWX q) <-> G(q <-> [a PWW b]));

// ---- invariant reduction of weak temporal operators -----------

Invariant_G  : assert A (q & G(q      -> a & X q) -> G a );
Invariant_WU : assert A (q & G(q & !b -> a & X q) -> [a WU b] );
Invariant_WB : assert A (q & G(q & !(a&!b) -> !b & X q) -> [a WB b] );
Invariant_WW : assert A (q & G(q & !(a& b) -> !b & X q) -> [a WW b] );

}