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 x≠y 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 f_k : D_i x D_V -> {false,true} is a conjunction of atomic boolean formulas of the form true, false, x=y or x≠y, with x,y ∈ V ∪ P_i.
• the update function u_k : D_i x D_V -> D_V is limited to an assignment where a register is assigned either a register or an input parameter
• the output function p_k : D_i x D_V -> D_p 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

• a Register automata model
• a SUT tool model which uses the Uppaal [BDL04] GUI as an editor for its own specific EFSM syntax.

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 name="IPleaseAck">
            </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 from="id5" symbol="IPleaseAck" to="id1">
        </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 from="id3" symbol="IPleaseAck" to="id2">
        </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>