// **************************************************************************
//
//    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 LTL2(bool a,b,c,d,q)  {
    nothing;
} satisfies {

// ---- Eliminating nestings of X with past temporal operators ---------

  Separate_X_Conj_PWX : assert A (X (a & PWX b) <-> (b & X a)) ;
  Separate_X_Conj_PSX : assert A (X (a & PSX b) <-> (b & X a)) ;
  Separate_X_Conj_PSU : assert A (X (a & [b PSU c]) <-> (X (a & c) |  [b PSU c] & X (a & b)));
  Separate_X_Conj_PWB : assert A (X (a & [b PWB c]) <-> (X (a & b & !c) | [b PWB c] & X (a & !c)));

  Separate_X_Disj_PWX : assert A (X (a | PWX b) <-> (b | X a));
  Separate_X_Disj_PSX : assert A (X (a | PSX b) <-> (b | X a));
  Separate_X_Disj_PSU : assert A (X (a | [b PSU c]) <-> (X (a |  c) | [b PSU c] & X b));
  Separate_X_Disj_PWB : assert A (X (a | [b PWB c]) <-> (X (a | !c) & ([b PWB c] | X (a | b))));



// ---- Eliminating nestings of SU with past temporal operators ---------

  Separate_SU_Conj_PWX : assert A ([a SU (b & PWX c)] <-> (b & PWX c | [a SU (a & c & X b)]));
  Separate_SU_Conj_PSX : assert A ([a SU (b & PSX c)] <-> (b & PSX c | [a SU (a & c & X b)]));
  Separate_SU_Conj_PSU : assert A ([a SU (b & [c PSU d])] <-> ([c PSU d] & [(a &  X c) SU b] | [a SU (d & [(a & X c) SU b])]));
  Separate_SU_Conj_PWB : assert A ([a SU (b & [c PWB d])] <-> ([c PWB d] & [(a & !X d) SU b] | [a SU (c & !d & [(a & !X d) SU b])]));

  Separate_SU_Conj_Left  : assert A ([(a & b) SU c] <-> ([a SU c] & [b SU c]));
  Separate_SU_Disj_Right : assert A ([a SU (b | c)] <-> ([a SU b] | [a SU c]));

  Separate_SU_Disj_PWX : assert A ([(a | PWX b) SU c] <-> (c | (a | PWX b) & [(b | X a) SU (X c)]));
  Separate_SU_Disj_PSX : assert A ([(a | PSX b) SU c] <-> (c | (a | PSX b) & [(b | X a) SU (X c)]));
  Separate_SU_Disj_PSU : assert A ([(a | [b PSU c]) SU d] 
				<-> ( ([b PSU c] | [(d | X c) WB (!a & !d)]) &
				      [(b | c | [(d | X c) WB (!a & !d) ]) SU d]));
  Separate_SU_Disj_PWB : assert A ([(a | [b PWB c]) SU d]
				<-> ( ([b PWB c] | [(d | X b) WB (!a & !d)]) &
				      [(!c | [(d | X b) WB (!a & !d)]) SU d]));



// ---- Eliminating nestings of WB with past temporal operators ---------

  Separate_WB_Disj_Left  : assert A ([(a | b) WB c] <-> ([a WB c] | [b WB c]));
  Separate_WB_Disj_Right : assert A ([a WB (b | c)] <-> ([a WB b] & [a WB c]));

  Separate_WB_Conj_Right_PWX : assert A ([a WB (b & PWX c)] <-> !(b & PWX c) & (a | [(X a) WB (c & X b)]));
  Separate_WB_Conj_Right_PSX : assert A ([a WB (b & PSX c)] <-> !(b & PSX c) & (a | [(X a) WB (c & X b)]));
  Separate_WB_Conj_Right_PSU : assert A ([a WB (b & [c PSU d])] 
				<-> ( [(!c) PWB d] | [(a | !X c) WB b]) &
				    [a WB (d & [(!a & X c) SU b])]);
  Separate_WB_Conj_Right_PWB : assert A ([a WB (b & [c PWB d])] 
				<-> ([(!c) PSU d] | [(a | X d) WB b]) &
				    [a WB (c & !d & [(!a & !X d) SU b])]);

  Separate_WB_Conj_Left_PWX : assert A ([(a & PWX b) WB c] <-> !c & a & PWX b | !c & [(b & X a) WB (X c)]);
  Separate_WB_Conj_Left_PSX : assert A ([(a & PSX b) WB c] <-> !c & a & PSX b | !c & [(b & X a) WB (X c)]);
  Separate_WB_Conj_Left_PSU : assert A ([(a & [b PSU c]) WB d]
				<-> [b PSU c] & [(!d & X b) SU (a & !d)] |
				    [(c & [(!d & X b) SU (a & !d)]) WB d]); 
  Separate_WB_Conj_Left_PWB : assert A ([(a & [b PWB c]) WB d]
				<-> [b PWB c] & [(!d & !X c) SU (a & !d)] |
				    [(b & !c &  [(!d & !X c) SU (a & !d)]) WB d]);


// ---- Eliminating nestings of PWX with future temporal operators ---------

  Separate_PWX_Conj_X  : assert A (PWX (a & X b) <-> ( (PWX false) | b & PWX a));
  Separate_PWX_Conj_SU : assert A (PWX (a & [b SU c]) <-> ( PWX (a & c) | [b SU c] & PWX (a & b)));
  Separate_PWX_Conj_WB : assert A (PWX (a & [b WB c]) <-> ( PWX (a & b & !c) | [b WB c] & PWX (a & !c) ));
  Separate_PWX_Disj_X  : assert A (PWX (a | X b) <-> (b | PWX a));
  Separate_PWX_Disj_SU : assert A (PWX (a | [b SU c]) <-> (PWX (a |  c) | [b SU c] & PWX b));
  Separate_PWX_Disj_WB : assert A (PWX (a | [b WB c]) <-> (PWX (a | !c) & ([b WB c] | PWX (a | b))));



// ---- Eliminating nestings of PSU with future temporal operators ---------

  Separate_PSU_Conj_X  : assert A ([a PSU (b & X c)] <-> (b & X c | [a PSU (a & c & PSX b)]));
  Separate_PSU_Conj_SU : assert A ([a PSU (b & [c SU d])] <-> 
				([c SU d] & [(a & PWX c) PSU b] | 
				 [a PSU (d & [(a & PWX c) PSU b])]));
  Separate_PSU_Conj_WB : assert A ([a PSU (b & [c WB d])] <-> 
				([c WB d] & [(a & !PWX d) PSU b] | 
				 [a PSU (c & !d & [(a & !PWX d) PSU b])]));

  Separate_PSU_Conj_Left  : assert A ([(a & b) PSU c] <-> ([a PSU c] & [b PSU c]));
  Separate_PSU_Disj_Right : assert A ([a PSU (b | c)] <-> ([a PSU b] | [a PSU c]));

  Separate_PSU_Disj_X  : assert A ([(a | X b) PSU c] <-> (c | (a | X b) & [(b | PWX a) PSU (PSX c)]));
  Separate_PSU_Disj_SU : assert A ([(a | [b SU c]) PSU d] 
				<-> ( ([b SU c] | [(d | PWX c) PWB (!a & !d)]) &
				      [(b | c | [(d | PWX c) PWB (!a & !d) ]) PSU d]));
  Separate_PSU_Disj_WB : assert A ([(a | [b PWB c]) PSU d] 
				<-> ( ([b PWB c] | [(d | PSX b) PWB (!a & !d)]) &
				      [(!c | [(d | PSX b) PWB (!a & !d)]) PSU d]));
}