// ************************************************************************** // // 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])); }