Skip to content

Commit

Permalink
fix(mataformat): Notify about features supported in the Mata library (#…
Browse files Browse the repository at this point in the history
…471)

fix(mataformat): Notify about features supported in the Mata library #patch
  • Loading branch information
Adda0 authored Nov 22, 2024
1 parent 3aaa873 commit 041614a
Showing 1 changed file with 11 additions and 0 deletions.
11 changes: 11 additions & 0 deletions AUTOMATAFORMAT.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
# The Mata file format for automata (.mata format)

> [!WARNING]
> The Mata library currently supports only a subset of the whole format. Notably, the Mata library supports NFAs, but not AFAs nor transducers. The Mata library may also not support all the additional features described in the format, such as special formulas, tracks, etc.
## Top-level file structure
* The format is **line**-based. Lines can be connected by `\`.
* Lines are parsed into tokens. Tokens are delimited by white spaces, the format is **white space sensitive** with exception of formulas in transitions where expressions could be written without white spaces separating tokens.
Expand Down Expand Up @@ -33,6 +36,10 @@ We categorise automata by the **alphabet type**, i.e., the representation of sym
* Initial (final) states are defined by key-value line `%Initial"` (`%Final`) followed by an enumeration of states.

### AFA (Alternating finite automata)

> [!WARNING]
> The Mata library currently does not support AFAs.
* Transition lines are of the form `"<State> <Formula>"` representing the source state and the transition formula - a Boolean formula over symbol literals, states, and nodes.
* Several lines starting with the same state mean the disjunciton of the formulae. No line for the state means false.
* Initial (final) states are defined by key-value line `%Initial <Formula>"` (`"%Final <Formula>"`) where the Boolean formula is given over states.
Expand Down Expand Up @@ -91,6 +98,10 @@ q2 x & !y q3
q [a-z] s
```
## Transducer

> [!WARNING]
> The Mata library currently does not support transducers.
A transducer has named tracks, and it has a key-value line starting with `%Tracks`. We use `<lit>@x` to say that the `<lit>` belongs to the track `x`. We may also specify their names by a type-identifier or enumeration. An example:
```
@AFA-intervals
Expand Down

0 comments on commit 041614a

Please sign in to comment.