Automata Wiki

A table with a list of all the benchmarks and sources in KISS format:

• circuits.zip

For more information about the models see circuits.txt.

KISS2 format

A KISS2 file just consist of a list of transitions. As an example for an transition in a KISS2 file we consider a transition "01-- s1 s2 0-". Here "01--" is the input bit vector, "s1", "s2" are the source, target states resp. and "0-" is the output bit vector. A dash "-" means "don't care". In this example all the bit vectors "0100", "0101", "0110" and "0111" will trigger the transition.

The KISS2 can be viewed as Mealy machines in several ways. For the output we can interpret the meaning of don't care bits in (at least) two ways:

• Don't cares are observable. This means that "0-", "00" and "01" are three distinct values. This does not correspond to the physical behaviour of circuits.
• Don't cares keep the output bit unchanged. In this semantics an initial output bit vector is assumed (all zeroes) and "0-" will either output "00" or "01" depending on the state of the output bit vector.

In both cases, the models are deterministic, possibly partial Mealy machines.

deterministic, complete Mealy models

We used two ways of completing the KISS2 models:

• Self-loops. Whenever a transition is missing, remain in the same state and output "--" of correct length.
• Sink-state. Whenever a transition is missing, go to a sink (or crash) state with output "--" of correct length.

In both cases we will obtain a (deterministic, complete) Mealy machine. We provide all 4 semantics (2*2 combinations of above). If two or more semantics give equivalent results, we have included only one of them in the benchmark suite. The obtained models are stored in the DOT format listed on the Mealy page.

The circuit benchmarks have been used recently for Mealy machine testing by Hierons and Türker [HT15]. They choose a semantics with observable don't cares and self-loops (with a distinct null output instead of a don't care output).