geteta — Generalized Test Tables Codacy Badge CircleCI

Generalized Test Tables ensures safety in automation software.


Getting Started


These are jar files include all dependencies:

From Source

$ git clone
$ mvn package

Getting started

Ensure, that you have installed nuXmv. You need to set the NUXMV environment variable to the nuXmv executable.

export NUXMV=/home/weigl/work/nuXmv-1.1.1-Linux/bin/nuXmv

After this, you can call geteta with:

java -jar geteta-${project.version}.jar -c -t testtable.xml [-x]

Command Line Arguments

  • -x geteta writes the output in an XML format.
  • -m <mode>
  • -t <table.xml>
  • -c <>
  • -v (IC3|INVAR|LTL|BMC)

XML-Format of Generalized Test tables

What is a test table?

A test table describe a behaviour of a reactive system by ensuring allowed input and output values for specific time frames.


A system is conform to a test table if and only if the system response with the corresponding (after the test table) output sequence given a valid sequence of input values.

Input format

The test tables are serialized into XML, following the scheme of `exteta-1.0.xsd <>`__. The XML contains three parts under the root entry.


These tag contains the two types of variables: i/o and constraint.



Name Description
identifier variable identifier
io input or output
data-type IEC61131-3 builtin datatype. Currently supported: AnyInt and AnyBit
  • I/O variables talk about the the input and output variables of the given program.


Constraint variables (specification variable) are not visible to the program.


Name Description
identifier variable identifier
constraint a valid cell expression
data-type IEC61131-3 builtin datatype. Currently supported: AnyInt and AnyBit


<region> and <step>

The <steps> tag contains the row (<step>) of the test tables. Each row the value of the cells (cell expressions) in the order of the defined i/o variables.

You repeat a bunch of steps, by wrapping them into a region block.

A region and step tag has the duration attribute, which defines how often the step is applied. The duration is an interval [m,n] with constant values for m,n.

Cell Expression (<cell>)

Formally, a cell expression is generated by the `grammar <>`__. Informally, a cell expression is a boolean expression over the following operators

  • arithmetic +, -, *, /
  • logical and, or, xor.

The syntax and semantic, e.g. the operator precedence is tight on the definition of Structured Text and SMV (nuXmv). For example, OR and | is allowed for logical or.

Additionally, we introduce abbreviations.

  • Constants

A simple constant means the equivalence with this value.

5 means X = 5 and FALSE is NOT X.

  • Single-sided comparison

A construct with a relational operator, <,<=,<>,=, >=, >, compares the column variable X with the given expression.

Example: <1 means X<1 resp. >=a+2 expands to X>=a+2.

  • Interval

You can specify an interval [m,n] to enforce a lower and upper bound for X: m<=X & X>=n.

Example: [x+2, x+4] means (x+2) <= X <= (x+4).

  • Don’t-Care

If you don’t want to force a value, you can use “don’t-care” -.

Operators with Precedence

  1. constants and variable names
  2. parens () and unary operators ! NOT -
  3. point operators MOD % / *
  4. Substraction and Addition + -
  5. Comparision < <= >= >
  6. equality
  7. antivalence
  8. logical and & AND
  9. logical or | OR
  10. logical xor xor XOR


Options are key-value pairs of the kind <option key="" value=""/>. They give additional information for the processing of the given table.

Currently allowed options:

Program mode
  • Key: mode

The mode of test tables has following effect:

  • CONFORMANCE - default Checks the system conformity against the test table. Returns a counter example, iff the system is not compilant against the above semantic.
  • CONCRETE_TABLE Returns a counter example, that represents a concrete run through the test table.
  • INPUT_SEQUENCE_EXISTS The above semantics has one problem, if no possible input sequence extension exists. This mode checks if there exists always an input extension.
Cycles through the steps

In dependence of mode = CONCRETE_TABLE you can give the wanted cycle count for each step.

  • Keys: cycles.<id>
  • Value: int

where <id> is the number of the region/step (starting with zero, in order of appearance).

Data types

You can select the bit width of the ST data types. currently not implemented


Between this tag you can define arbitrary function as Structured Text code. These function are usable within the cell expressions as regular function calls.