A Mealy machine is a finite-state machine whose output values are determined both by its current state and its current input.
See: http://www.wikiwand.com/en/Mealy_machine
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"];
}