Equivalent
- ¬ (¬ p W p W ¬ p W p W G ¬ p)
- (((F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))) U (¬ p ∧ (F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p)))) U (p ∧ ((F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))) U (¬ p ∧ (F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))))
Complement
Classification
Temporal Hierarchy |
---|
Guarantee |
Spec Patterns |
---|
Unknown |
DBW-Recognizable |
---|
Yes |
Automaton Type: Nondeterministic Büchi | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 655 | Author: GOAL | #2 | ID: 2976 | Author: GOAL | #3 | ID: 731 | Author: R.Ehlers / NBWMinimizer | |||
St: 6 | Tr: 12 | Date: 2010-01-19 00:00:00 | St: 7 | Tr: 14 | Date: 2012-05-24 08:28:01 | St: 6 | Tr: 17 | Date: 2011-06-27 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | |||||||||
Acceptance condition: {s5} |
Acceptance condition: s3, s6 |
Acceptance condition: {s5} |
|||||||||
Automaton Type: Deterministic Büchi | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 2499 | Author: GOAL | #2 | ID: 2976 | Author: GOAL | #3 | N/A | ||||
St: 7 | Tr: 14 | Date: 2011-12-07 00:00:00 | St: 7 | Tr: 14 | Date: 2012-05-24 08:28:01 | ||||||
Description: | Description: | ||||||||||
Download: GFF Promela Add to Cart | Download: GFF Promela Add to Cart | ||||||||||
Acceptance condition: {s0, s6} |
Acceptance condition: s3, s6 |
||||||||||
Automaton Type: Nondeterministic Co-Büchi | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 2307 | Author: GOAL | #2 | ID: 2333 | Author: GOAL | #3 | ID: 2283 | Author: GOAL | |||
St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 10 | Tr: 20 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: {s0, s1, s2, s3, s4} |
Acceptance condition: {s0, s1, s2, s3, s4} |
Acceptance condition: {s0, s1, s2, s4, s5} |
|||||||||
Automaton Type: Deterministic Co-Büchi | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 2307 | Author: GOAL | #2 | ID: 2333 | Author: GOAL | #3 | ID: 2283 | Author: GOAL | |||
St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 10 | Tr: 20 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: {s0, s1, s2, s3, s4} |
Acceptance condition: {s0, s1, s2, s3, s4} |
Acceptance condition: {s0, s1, s2, s4, s5} |
|||||||||
Automaton Type: Nondeterministic Muller | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 1014 | Author: GOAL | #2 | ID: 1058 | Author: GOAL | #3 | ID: 989 | Author: GOAL | |||
St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 6 | Tr: 17 | Date: 2011-12-07 00:00:00 | St: 9 | Tr: 21 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: { {s5} } |
Acceptance condition: { {s5} } |
Acceptance condition: { {s7} } |
|||||||||
Automaton Type: Nondeterministic Rabin | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 1339 | Author: GOAL | #2 | ID: 1383 | Author: GOAL | #3 | ID: 1311 | Author: GOAL | |||
St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 6 | Tr: 17 | Date: 2011-12-07 00:00:00 | St: 9 | Tr: 21 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: { (∅, {s5}) } |
Acceptance condition: { (∅, {s5}) } |
Acceptance condition: { (∅, {s3, s5, s7}) } |
|||||||||
Automaton Type: Nondeterministic Streett | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 1664 | Author: GOAL | #2 | ID: 1708 | Author: GOAL | #3 | ID: 1636 | Author: GOAL | |||
St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 6 | Tr: 17 | Date: 2011-12-07 00:00:00 | St: 9 | Tr: 21 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: { ({s5}, {s0, s1, s2, s3, s4, s5}) } |
Acceptance condition: { ({s5}, {s0, s1, s2, s3, s4, s5}) } |
Acceptance condition: { ({s3, s5, s7}, {s0, s1, s2, s3, s4, s5, s6, s7, s8}) } |
|||||||||
Automaton Type: Nondeterministic Parity | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 1989 | Author: GOAL | #2 | ID: 2033 | Author: GOAL | #3 | ID: 1961 | Author: GOAL | |||
St: 6 | Tr: 12 | Date: 2011-12-07 00:00:00 | St: 6 | Tr: 17 | Date: 2011-12-07 00:00:00 | St: 9 | Tr: 21 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: 0: {s5}, 1: {s0, s1, s2, s3, s4} |
Acceptance condition: 0: {s5}, 1: {s0, s1, s2, s3, s4} |
Acceptance condition: 0: {s3, s5, s7}, 1: {s0, s1, s2, s4, s6, s8} |
|||||||||
Automaton Type: Deterministic Parity | |||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|
#1 | ID: 2839 | Author: GOAL | #2 | ID: 2878 | Author: GOAL | #3 | ID: 2813 | Author: GOAL | |||
St: 7 | Tr: 14 | Date: 2011-12-07 00:00:00 | St: 8 | Tr: 16 | Date: 2011-12-07 00:00:00 | St: 16 | Tr: 32 | Date: 2011-12-07 00:00:00 | |||
Description: | Description: | Description: | |||||||||
Download: GFF Add to Cart | Download: GFF Add to Cart | Download: GFF Add to Cart | |||||||||
Acceptance condition: 0: {s0, s6}, 1: {s1, s2, s3, s4, s5} |
Acceptance condition: 0: {s0}, 2: {s7}, 3: {s1, s2, s3, s4, s5, s6} |
Acceptance condition: 0: {s0, s8, s9}, 2: {s6}, 3: {s11, s12, s13}, 5: {s1, s2, s3, s4, s5, s7, s10, s14, s15} |
|||||||||