Equivalent
Complement
- ¬ (F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q))
- F p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))) W (p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))))
Classification
| Temporal Hierarchy |
|---|
| Safety |
| Spec Patterns |
|---|
| Bounded Existence |
| DBW-Recognizable |
|---|
| Yes |
| ID: 2567 |
|
| Author: GOAL | |
| St: 7 | |
| Tr: 28 | |
|
Acceptance Condition: {s0, s1, s2, s3, s4, s5} |
|