### LTL (or PSL) Formula to translateFold

Send

Use alphanumeric identifiers or double-quoted strings for atomic propositions, and parentheses for grouping.
Identifiers cannot start with the letter of a prefix operator (F, G, or X): for instance GFa means G(F(a)). Use "GFa" if you really want to refer to GFa as a proposition.
Conversely, infix letter operators are not assumed to be operators if they are part of an identifier: aUb is an atomic proposition, unlike a U b and (a)U(b).

| Constants | Unary operators (prefix) | Binary operators (infix)
--- | --- | --- | ---
Boolean | false: | 0 false | not: | ! ~ | and: | & && /\ | implies: | -> --> =>
true: | 1 true |  |  | or: | | || + \/ | equivalent: | <-> <--> <=>
|  |  |  | xor: | xor ^ |  |
LTL |  |  | eventually: | F <> | (strong) until: | U | weak until: | W
|  | always: | G [] | (weak) release: | R V | strong release: | M
|  | next: | X () |  |  |  |
SERE | ε: | [*0] | Kleene star: | [*] [*i..j] | concatenation: | ; | fusion: | :
|  | goto: | [->i..j] | intersection: | && /\ | NLM and: | &
|  | nonconsec. rep.: | [=i..j] | union: | | || + \/ |  |
PSL |  |  | weak closure: | {s} | ∀-suffix impl.: | {s}[]->p {s}|->p {s}(p) | NO ∀-suffix impl.: | {s}[]=>p {s}|=>p
|  | strong closure: | {s}! | ∃-suffix impl.: | {s}<>->p | NO ∃-suffix impl.: | {s}<>=>p

### Formula SimplificationsFold

basic rewritings allow larger formulas
syntactic implication
eventuality and universality
language containment

- Desired Output:
- Formula
- Monitor
- Büchi Automaton
- Büchi Run
- Fold

Output the (simplified) formula as:
text in Spot's syntax
text in Spin's syntax
a syntactic tree
property information
Translate the (simplified) formula as:
a deterministic monitor
Translate the (simplified) formula as:
a transition-based generalized Büchi automaton
a state-based degeneralized Büchi automaton
a Spin neverclaim
Translate the (simplified) formula as:
a transition-based generalized Büchi automaton
a state-based degeneralized Büchi automaton
then
print an accepting run
draw an accepting run on top of the automaton

- Translator Algorithm:
- Couvreur/FM
- Couvreur/LaCIM
- Tauriainen/TAA
- Fold

optimize determinism
merge states with same symbolic successor representation
branching postponement
fair-loop approximations
symbolically prune unaccepting SCCs
language containment

### Automaton SimplificationsFold

prune unaccepting SCCs
minimize obligation properties
direct simulation

### Emptiness-check AlgorithmFold

Search accepting run using algorithm:
with these options:

### ResultsFold