A PHP Error was encountered

Severity: Notice

Message: Undefined index: SyntaxForm

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: Format2Form

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: UnicodeForm

Filename: models/formulaemodel.php

Line Number: 316

Büchi Store

Sorted by


Refresh


Filtered by

Automaton Type

Select / Deselect All














State Size

Select / Deselect All






Formula Length

Select / Deselect All






Temporal Hierarchy

Select / Deselect All








Spec Patterns

Select / Deselect All











Refresh


Grouped By


Refresh

Equivalent:
Complement:
NBW
X X X p Equivalent: X X X p
Complement:
NBW
X X F p Equivalent: X X F p
Complement:
DBW
F (p ∧ q) ∨ G F p Equivalent: F (p ∧ q) ∨ G F p
Complement:
NBW
F r → (p → ¬ r U (q ∧ ¬ r)) U r Equivalent: F r → (p → ¬ r U (q ∧ ¬ r)) U r
Complement: ¬ (F r → (p → ¬ r U (q ∧ ¬ r)) U r)
NBW
G ¬ q ∨ F (q ∧ F p) Equivalent: G ¬ q ∨ F (q ∧ F p)
Complement: ¬ (G ¬ q ∨ F (q ∧ F p))
NBW
G (p → F (q ∧ F r)) Equivalent: G (p → F (q ∧ F r))
Complement: F (p ∧ G (¬ q ∨ G ¬ r)) ¬ G (p → F (q ∧ F r))
DBW
F ¬ p ∨ F (p ∧ ¬ q W r) Equivalent: F ¬ p ∨ F (p ∧ ¬ q W r)
Complement: G p ∧ G (¬ p ∨ ¬ r U (q ∧ ¬ r)) ¬ (F ¬ p ∨ F (p ∧ ¬ q W r))
NBW
G ¬ r ∨ F (r ∧ ¬ p W q) Equivalent: G ¬ r ∨ F (r ∧ ¬ p W q)
Complement: ¬ (G ¬ r ∨ F (r ∧ ¬ p W q))
NBW
G (p → F (q ∧ ¬ r ∧ X (¬ r U s))) Equivalent: G (p → F (q ∧ ¬ s ∧ X (¬ s U r))) G (p → F (q ∧ ¬ r ∧ X (¬ r U s)))
Complement: ¬ G (p → F (q ∧ ¬ r ∧ X (¬ r U s))) F (p ∧ G (¬ q ∨ r ∨ X (¬ s W (r ∧ ¬ s))))
NBW
G F ¬ a ∨ G F b Equivalent: G F ¬ a ∨ G F b
Complement:
NBW
F X X X p Equivalent: F X X X p
Complement:
NBW
G (DESTINO → X (MOSTRAR U (INGRESO ∧ X (ERROR ∨ OK)))) Equivalent: G (DESTINO → X (MOSTRAR U (INGRESO ∧ X (ERROR ∨ OK))))
Complement:
NBW
G p → X (X q ∨ X r) Equivalent: G p → X (X q ∨ X r)
Complement:
NBW
F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s)) Equivalent: F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))
Complement: ¬ (F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))) F p ∧ (¬ p ∧ (¬ r ∨ q ∨ X (¬ s W (q ∧ ¬ s)))) W (q ∧ ¬ p ∧ (¬ r ∨ q ∨ X (¬ s W (q ∧ ¬ s))))
NBW