The automaton level conversions available in `veric` fall into two groups:

The former group allows the common label based synchronisation between statements, known from Prism, to be translated into protocols. The second group allows for using various integer expressions in a model, even if the final model checker understands only a simple boolean algebra.

# 1. Label Conversion

A labelled statement, whose guards can be evaluated by using a respective module's local state, can be converted to a protocol–synchronised statement. For example, the fragment below, from the model of FTC.

```    []           true -> true;
[approach1]  phase == AWAY   -> phase := WAIT;
[in1]        phase == WAIT   -> phase := TUNNEL;
[out1]       phase == TUNNEL -> phase := AWAY;
```
would be translated as follows
```    protocol {
in, none       := phase == WAIT;
out, none      := phase == TUNNEL;
approach, none := phase == AWAY;
none           := other;
};

[]  phase == AWAY && approach ->                  phase := WAIT;
[]  phase == WAIT && in && environment.in1 ->     phase := TUNNEL;
[]  phase == TUNNEL && out && environment.out1 -> phase := AWAY;
```
See that a statement with the guard being either `true` or and no state update is assigned to a special action `none`. The guard `true` allows the action `none` to occur at any local state. A guard `other`:
```    []           other -> true;
```
would in turn be true only in the local states not covered by the other actions:
```    protocol {
in       := phase == WAIT;
out      := phase == TUNNEL;
approach := phase == AWAY;
none     := other;
};
```
In the case of the model's train, the three other statements conver any local state, and thus the guard `other` is never true.

# 2. Integer Conversion

Obviously, integer arithmetic can be of a great help when specifying a model. Some model checkers only support small parts of it, sometimes being limited only to an integer comparison. In such cases, the `veric`'s ability of an automated conversion of an integer expression into a boolean equivalent may help.

An integer evaluation of an action allows a flexible definition of synchronisation patterns, for example the dining crypthographers model contains an expression:

```    mod(dc1.say_equal + dc2.say_equal + dc3.say_equal, 2) == 1
```
which would be converted to
```    ( dc1.say_equal and  dc2.say_equal and  dc3.say_equal) or
(!dc1.say_equal and !dc2.say_equal and  dc3.say_equal) or
(!dc1.say_equal and  dc2.say_equal and !dc3.say_equal) or
( dc1.say_equal and !dc2.say_equal and !dc3.say_equal)
```

The MCMAS' language ISPL lacks integer operators except for the relational ones. Even the expressions which do not contain integer action evaluation must thus be converted. A part of this initial state filter, again from the dining crypthographers model:

```   \${\$rpt("dc\$.payer", " + ", 1, .NUM)} <= 1
```
in the case of `NUM` = 3 would be converted into the following ISPL expression:
```   (dc1.payer=NO  and dc2.payer=NO  and dc3.payer=NO ) or
(dc1.payer=YES and dc2.payer=NO  and dc3.payer=NO ) or
(dc1.payer=NO  and dc2.payer=YES and dc3.payer=NO ) or
(dc1.payer=NO  and dc2.payer=NO  and dc3.payer=YES)
```
An XML output accepts anything definable in a VXS model, and thus the conversion options applicable depend solely on the checker, which will read the output file.