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 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.