# Register automata

Register automata, also known as scalarset Mealy machines,

• are Mealy extended finite state machines
• where the update function is limited to only basic assignment to a register or input parameter; so no operations are allowed on data
• and the enabling function is limited to a boolean expression of the form true, false, x=y or xy where x and y are either registers or input parameters

## Formal definition Register Automaton

A register automaton is a Mealy EFSM where

• the enabling function fk : Di x DV -> {false,true} is a conjunction of atomic boolean formulas of the form true, false, x=y or x≠y, with x,y ∈ V ∪ Pi.
• the update function uk : Di x DV -> DV is limited to an assignment where a register is assigned either a register or an input parameter
• the output function pk : Di x DV -> Dp is limited to an assignment where a output parameter is assigned either a register or an input parameter.

From the above definition it follows that a register automaton doesn't allow any operations on data neither in the update nor the output functions. However the above definition allows a Register automaton to be non-deterministic and not input enabled, however most of the time a Register Automaton is assumed to be deterministic and input enabled.

Note that we often call the state variables of a register automaton registers instead. This because registers only store values from the environment without any operations on it.

## Syntax Register automata model

In the benchmarks a register automata is either given as

The state machine diagram of the register model for the ABP Receiver model looks like :

Fig. 1: SUT Model : ABP Receiver

This format is developed as a simple xml format to exchange register automata. Its syntax is defined as :

<register-automaton>
<alphabet>
<inputs>
<symbol name="<<name_input_symbol>>">
<param name="<<name_param>>" type="<<type_param>>"></param>
...
</symbol>
...
</inputs>
<outputs>
<symbol name="<<name_output_symbol>>">
<param name="<<name_param>>" type="<<type_param>>"></param>
...
</symbol>
...
</outputs>
</alphabet>
<constants>
<constant name="<<name_constant>>" type="<<type_constant>>">
<<value_constant>>
</constant>
...
</constants>
<globals>
<variable name="<<name_global_variable>>" type="<<type_global_variable>>">
<<initial_value_global_variable>>
</variable>
...
</globals>
<locations>
<location name="<<name_location>>"></location>
...
</locations>
<transitions>
<transition from="<<from_location>>" symbol="<<symbol_name>>"
params="<<comma_separated_list_of_param_names>>" to="<<to_location>>">
<guard>
<<guard_expression>>
</guard>
<assignments>
<assign to="<<global_variable_name>>">
<<value_param_or_global_variable_to_assign>>
</assign>
...
</assignments>
</transition>
....
</transitions>
</register-automaton>

notes:
- specifying the outputs in the <alphabet> tag is optional
- if there is no guard in the transition you can leave out the <guard> tag
- if there are no assignments in the transition you can leave out the <assignments> tag

As an example the source of the register model for the ABP Receiver model shown above is :

<register-automaton>
<alphabet>
<inputs>
</symbol>
<symbol name="IFrame">
<param name="p0" type="int">
</param>
<param name="p1" type="int">
</param>
</symbol>
</inputs>
<outputs>
<symbol name="OOut">
<param name="p0" type="int">
</param>
</symbol>
<symbol name="OAck">
<param name="p0" type="int">
</param>
</symbol>
<symbol name="ONOK">
</symbol>
</outputs>
</alphabet>
<constants>
<constant name="constant0" type="int">
0
</constant>
<constant name="constant1" type="int">
1
</constant>
</constants>
<globals>
<variable name="vb" type="int">
0
</variable>
<variable name="vd" type="int">
0
</variable>
<variable name="expectedBit" type="int">
0
</variable>
</globals>
<locations>
<location name="id4">
</location>
<location initial="true" name="id5">
</location>
<location name="id2">
</location>
<location name="id3">
</location>
<location name="id0">
</location>
<location name="id1">
</location>
</locations>
<transitions>
<transition from="id0" symbol="ONOK" to="id3">
</transition>
<transition from="id3" params="d,b" symbol="IFrame" to="id0">
</transition>
<transition from="id1" symbol="ONOK" to="id5">
</transition>
</transition>
<transition from="id2" params="0" symbol="OAck" to="id5">
<guard>
expectedBit==0
</guard>
<assignments>
<assign to="expectedBit">
1
</assign>
</assignments>
</transition>
<transition from="id2" params="1" symbol="OAck" to="id5">
<guard>
expectedBit==1
</guard>
<assignments>
<assign to="expectedBit">
0
</assign>
</assignments>
</transition>
</transition>
<transition from="id4" symbol="ONOK" to="id5">
<guard>
(vb==1 && expectedBit==0) ||
(vb==0 && expectedBit==1) ||
vb > 1
</guard>
</transition>
<transition from="id4" params="vd" symbol="OOut" to="id3">
<guard>
(vb==0 && expectedBit==0) ||
(vb==1 && expectedBit==1)
</guard>
</transition>
<transition from="id5" params="d,b" symbol="IFrame" to="id4">
<assignments>
<assign to="vd">
d
</assign>
<assign to="vb">
b
</assign>
</assignments>
</transition>
</transitions>
</register-automaton>