The given LTL formulas S1S1 and S2S2 are not equivalent.

LS1∧¬S2LS1∧¬S2 represents a set of ωω-words that only satisfy S1S1.

L¬S1∧S2L¬S1∧S2 represents a set of ωω-words that only satisfy S2S2.

Please construct **two** LTL formulas φ1φ1 and φ2φ2 that satisfy the following requirements:

- Lφ1≠Lφ2Lφ1≠Lφ2
- Lφi≠{}Lφi≠{}
**Case 1: **Lφ1⊊LS1∧¬S2Lφ1⊊LS1∧¬S2 and Lφ2⊊LS1∧¬S2Lφ2⊊LS1∧¬S2

or

**Case 2: **Lφ1⊊L¬S1∧S2Lφ1⊊L¬S1∧S2 and Lφ2⊊L¬S1∧S2Lφ2⊊L¬S1∧S2

where LφiLφi represents a set of ωω-words that satisfy φiφi.

Please use '**;**' to seperate the LTL formulas.

For Case 1, submit your solution in the form:

**1 ; G (!a) ; F b**

For Case 2, submit your solution in the form:

**2 ; G (!a) ; F b**

**b)** S1=S1=[c WB [b WB a]]

S2=S2=[c SB [b SB a]]

How to solve this?