print · source · login   

Mealy Machines

A Mealy Machine is a finite-state machine whose output values are determined both by its current state and the current inputs.

A Mealy machine is a structure consisting of states with transitions between them. Each transition is labelled with both an input and output action. The states model the system states; the transitions model the reactive behavior of the machine by defining for each input an output reaction.

Formal definition

Source: http://www.wikiwand.com/en/Mealy_machine

A Mealy machine can be defined as a 6-tuple (S,s0,∑,Λ,T,G) consisting of the following:

  • a finite set of states S
  • a start state (also called initial state) s0 which is an element of S
  • a finite set called the input alphabet
  • a finite set called the output alphabet Λ
  • a transition function T : S x ∑ ➔ S mapping a state and the input alphabet to the next state
  • an output function G : S x ∑ ➔ Λ mapping pairs of a state and an input symbol to the corresponding output symbol.

Above definition shows that by defining a transition and output function a Mealy machine by default is assumed to be deterministic and input enabled.

Examples

For a deterministic Mealy machine for each state and input, at most one transition is possible.

SUT model
Fig. 1: An example of a simple Mealy Machine which outputs an E if the number of 1s read so far is even and an O if it is odd.

A bigger example is the Coffee Machine used in the introduction paper to active learning "Introduction to Active Automata Learning from a Practical Perspective".

Coffee Machine
Fig. 2: An example of the Coffee Machine which is used in the introduction paper to active learning "Introduction to Active Automata Learning from a Practical Perspective"

In the benchmarks a mealy machine is given as a dot file where the label on a transition has the syntax "input/output".

The dot encoding for the coffeemachine example is :

    digraph g {
        __start0 [label="" shape="none"];
        __start0 -> s0;

    	s0 [shape="circle" label="s0"];
    	s1 [shape="circle" label="s1"];
    	s2 [shape="circle" label="s2"];
    	s3 [shape="circle" label="s3"];
    	s4 [shape="circle" label="s4"];
    	s5 [shape="circle" label="s5"];


    	s0 -> s4 [label="WATER / ok"];
    	s0 -> s2 [label="POD / ok"];
    	s0 -> s1 [label="BUTTON / error"];
    	s0 -> s0 [label="CLEAN / ok"];
    	s1 -> s1 [label="WATER / error"];
    	s1 -> s1 [label="POD / error"];
    	s1 -> s1 [label="BUTTON / error"];
    	s1 -> s1 [label="CLEAN / error"];
    	s2 -> s3 [label="WATER / ok"];
    	s2 -> s2 [label="POD / ok"];
    	s2 -> s1 [label="BUTTON / error"];
    	s2 -> s0 [label="CLEAN / ok"];
    	s3 -> s3 [label="WATER / ok"];
    	s3 -> s3 [label="POD / ok"];
    	s3 -> s5 [label="BUTTON / coffee!"];
    	s3 -> s0 [label="CLEAN / ok"];
    	s4 -> s4 [label="WATER / ok"];
    	s4 -> s3 [label="POD / ok"];
    	s4 -> s1 [label="BUTTON / error"];
    	s4 -> s0 [label="CLEAN / ok"];
    	s5 -> s1 [label="WATER / error"];
    	s5 -> s1 [label="POD / error"];
    	s5 -> s1 [label="BUTTON / error"];
    	s5 -> s0 [label="CLEAN / ok"];

    }