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 |
| Automaton Type: Nondeterministic Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 746 | Author: Ming-Hsien Tsai | #2 | ID: 547 | Author: GOAL | #3 | N/A | ||||
| St: 6 | Tr: 22 | Date: 2011-08-23 00:00:00 | St: 8 | Tr: 30 | Date: 2010-01-12 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | ||||||||||
|
Acceptance condition: {s0, s1, s2, s3, s4, s5} |
Acceptance condition: {s1, s3, s4, s5, s6, s7} |
||||||||||
|
|
||||||||||
| Automaton Type: Deterministic Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2567 | Author: GOAL | #2 | ID: 2540 | Author: GOAL | #3 | N/A | ||||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 337 | Tr: 1348 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | ||||||||||
|
Acceptance condition: {s0, s1, s2, s3, s4, s5} |
Acceptance condition: {s0, s2, s6, s8, s10, s11, s12, s13, s14, s15, s17, s19, s23, s27, s30, s31, s32, s33, s35, s37, s38, s39, s42, s43, s51, s67, s69, s72, s73, s76, s81, s82, s83, s84, s91, s92, s98, s99, s100, s103, s112, s113, s114, s120, s123, s125, s130, s132, s144, s145, s146, s148, s149, s151, s158, s159, s160, s162, s163, s164, s165, s166, s171, s174, s176, s199, s203, s205, s211, s214, s215, s219, s221, s224, s225, s227, s228, s229, s230, s231, s235, s236, s237, s289, s291, s293, s295, s296, s298, s307, s309, s312, s313, s314, s319, s321, s322, s325, s326, s330} |
||||||||||
|
|
||||||||||
| Automaton Type: Nondeterministic Co-Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2340 | Author: GOAL | #2 | ID: 2263 | Author: GOAL | #3 | N/A | ||||
| St: 8 | Tr: 32 | Date: 2011-12-07 00:00:00 | St: 10 | Tr: 40 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: {s0, s7} |
Acceptance condition: {s0, s4, s5, s9} |
||||||||||
|
|
||||||||||
| Automaton Type: Deterministic Co-Büchi | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2340 | Author: GOAL | #2 | ID: 2263 | Author: GOAL | #3 | N/A | ||||
| St: 8 | Tr: 32 | Date: 2011-12-07 00:00:00 | St: 10 | Tr: 40 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: {s0, s7} |
Acceptance condition: {s0, s4, s5, s9} |
||||||||||
|
|
|
||||||||||
| Automaton Type: Nondeterministic Muller | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 1068 | Author: GOAL | #2 | ID: 953 | Author: GOAL | #3 | N/A | ||||
| St: 6 | Tr: 22 | Date: 2011-12-07 00:00:00 | St: 8 | Tr: 30 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: { {s0}, {s1}, {s2}, {s3}, {s4}, {s5} } |
Acceptance condition: { {s1}, {s3}, {s4}, {s5}, {s6}, {s7} } |
||||||||||
|
|
||||||||||
| Automaton Type: Nondeterministic Rabin | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 1393 | Author: GOAL | #2 | ID: 1275 | Author: GOAL | #3 | N/A | ||||
| St: 6 | Tr: 22 | Date: 2011-12-07 00:00:00 | St: 8 | Tr: 30 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: { (∅, {s0, s1, s2, s3, s4, s5}) } |
Acceptance condition: { (∅, {s1, s3, s4, s5, s6, s7}) } |
||||||||||
|
|
||||||||||
| Automaton Type: Nondeterministic Streett | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 1718 | Author: GOAL | #2 | ID: 1600 | Author: GOAL | #3 | N/A | ||||
| St: 6 | Tr: 22 | Date: 2011-12-07 00:00:00 | St: 8 | Tr: 30 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: { ({s0, s1, s2, s3, s4, s5}, {s0, s1, s2, s3, s4, s5}) } |
Acceptance condition: { ({s1, s3, s4, s5, s6, s7}, {s0, s1, s2, s3, s4, s5, s6, s7}) } |
||||||||||
|
|
||||||||||
| Automaton Type: Nondeterministic Parity | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2043 | Author: GOAL | #2 | ID: 1925 | Author: GOAL | #3 | N/A | ||||
| St: 6 | Tr: 22 | Date: 2011-12-07 00:00:00 | St: 8 | Tr: 30 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: 0: {s0, s1, s2, s3, s4, s5} |
Acceptance condition: 0: {s1, s3, s4, s5, s6, s7}, 1: {s0, s2} |
||||||||||
|
|
||||||||||
| Automaton Type: Deterministic Parity | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| #1 | ID: 2885 | Author: GOAL | #2 | ID: 2779 | Author: GOAL | #3 | N/A | ||||
| St: 7 | Tr: 28 | Date: 2011-12-07 00:00:00 | St: 9 | Tr: 36 | Date: 2011-12-07 00:00:00 | ||||||
| Description: | Description: | ||||||||||
| Download: GFF Add to Cart | Download: GFF Add to Cart | ||||||||||
|
Acceptance condition: 0: {s0, s1, s2, s3, s4, s5}, 1: {s6} |
Acceptance condition: 0: {s0, s1, s2, s5, s6, s7}, 2: {s4}, 3: {s3, s8} |
||||||||||
|
|
||||||||||