# KAC : Kleene Algebras with Converse

## Equation checker

### How to use this :

Write an equation in the input field of the applet, and see its validity just to the right (a green tick meaning yes and a red cross meaning no).

Equations should be entered like this: `<expr1> <cmp> <expr2>`.

An expression can use strings as variables/letters, and the operations:

• `0`: the empty relation
• `1`: the identity relation
• `<expr1> | <expr2>`: the set union
• `<expr1> . <expr2>`: the composition of relations
• `<expr1>~ `: the converse of a relation
• `<expr1>*`: the reflexive transitive closure of a relation.
• `<expr1>+`: the transitive closure of a relation.
• `<expr1>{int}` : the iteration of a relation. For instance, `(a.b){3}` is a shorthand for `(a.b).(a.b).(a.b)`.

You can also use brackets `(...)`. For letters/variables, you may use `a'` instead of `a~`. The valid comparaisons `<cmp>` are:

• `<=`: loose inclusion
• `>=`: converse of the loose inclusion
• `<`: strict inclusion
• `>`: converse of the strict inclusion
• `=`: equality
• `=/=`: negation of the equality
• `<>`: means that the two expressions are incomparable, i.e. neither one of them is included in the other.

For instance, `((1|a'|b)+|C)~.a=/=0` is an acceptable equation.

## Automata builder

### How to use this :

Simply input an automaton in the text box, choose from one of the constructions on the left scroll box, and click "Build" to generate the automaton and its closure.

An automaton is specified through the following syntax:

```initial : <list of initial states separated by spaces>
final : <list of final states separated by spaces>
<source> -- <label> --> <target>
<source> -- <label> --> <target>
...```

See below for an example.

### Applet

 BP - ND BP - D BES - D
 Initial automaton:
 Closure automaton: