# Input and Output Formats

`Owl` understand several text-based input and output formats, summarized in the following table:

Format | In | Out
--- | --- | ---
LTL (+ rLTL) | X | X
TLSF | X |
HOA | X | X
PGSolver |  | X

A more detailed description and links to relevant papers are provided below.

## Linear Temporal Logic (LTL)

The grammar for LTL aims to support Spot-style LTL.
For further details on temporal logic, e.g., semantics, see here.

The following constructs are supported:

### Propositional Logic

- True: `tt`, `true`, `1`
- False: `ff`, `false`, `0`
- Atom: `[a-zA-Z_][a-zA-Z_0-9]*` or quoted `"[^"]+"`
- Negation: `!`, `NOT`
- Implication: `->`, `=>`, `IMP`
- Bi-implication: `<->`, `<=>`, `BIIMP`
- Exclusive Disjunction: `^`, `XOR`
- Conjunction: `&&`, `&`, `AND`
- Disjunction: `||`, `|`, `OR`
- Parenthesis: `(`, `)`

### Modal Logic

- Finally: `F`
- Globally: `G`
- Next: `X`
- (Strong) Until: `U`
- Weak Until: `W`
- (Weak) Release: `R`
- Strong Release: `M`

### Precedence Rules

The parser uses the following precedence:

`OR` < `AND` < Binary Expressions < Unary Expressions < Literals, Constants, Parentheses

For chained binary expressions (without parentheses), the rightmost binary operator takes precedence.
For example, `a -> b U c` is parsed as `a -> (b U c)`.

### Robust LTL (rLTL)

`Owl` also supports parsing robust LTL, immediately translating it to LTL, given particular truth values.

## Hanoi Omega-Automaton Format (HOA)

`Owl` supports most of the HOA format, using jhoafparser as back-end.

Caveats:

- Alternation is not supported
- Internally, acceptance is encoded as transition acceptance, hence parsing and serializing an automaton with state acceptance may blow up the state space.

## Temporal Logic Synthesis Format (TLSF)

For use in a synthesis toolchain, `Owl` supports the basic format of TLSF.

Use syfco to transform other formats into TLSF or LTL.

## PGSolver Format

Serialization of parity games into the format used by PGSolver and other parity game solvers like Oink is also supported. See Sec. 3.5 here for a description of the format.