print · source · login   

Mealy Machines

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

Formal definition

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

Syntax

A Mealy machine is encoded as a dot file where the label on a transition has the syntax "input/output". For instance, the dot encoding for the coffee machine benchmark 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"];
    }