Challenge Problems

Systems to analyze

The ECA systems provided here basically consist of a main loop, where in each iteration an input (event) from the standard input is read and processed by the ECA engine. Depending on the internal state, the ECA engine changes its internal variables and possibly writes an output to the standard output. If an unexpected input event is provided, an error message is printed and the ECA system terminates.

In the case of the Java problems, both input and output symbols are plain character sequences (strings), usually consisting of only one character: For instance, input symbols typically are A, B, C etc., and output symbols U, W, X etc.

In the case of the C problems, both input and output symbols are plain numbers (ints), where inputs are stored in global variables named INPUT_A etc.

Properties to analyze

For each of the systems, the contestants have to answer several questions, which can be divided into two classes:

  • Reachability:

    Some assignments to internal state variables correspond to erroneous states, which cause the system to fail with a specific error code. Not all of those error states are reachable, and the goal is to check which of these states can in fact be reached (it is not expected to also provide a sequence of inputs reaching them). Those errors come in the form of either an IllegalStateException (Java) or a failed assertion (C), along with a specific error label.

  • Behavioral properties:

    An execution trace of the ECA system consists of a sequence of inputs and outputs, each from a finite alphabet. For each of the systems, a file properties.txt is provided, containing a set of 100 properties for which the contestants have to check whether they are satisfied by all traces, or if there are traces that violate them (it is not expected to also provide these traces). The properties are given both as an LTL formula and a textual description. For example,

        (G ! oU)
        output U does never occur
    

    states that it is not possible—by any sequence of input events—to make the system produce an "U" output action.

    In the LTL formulae, the atomic propositions correspond to input and output symbols, where the prefix i is used for input and o is used for output symbols, to allow a clear distinction.

    The LTL formulae are given in a standard syntax, making use of the following temporal operators:

    • X φ (next): φ has to hold after the next step
    • F φ (eventually): φ has to hold at some point in the future (or now)
    • G φ (globally): φ has to hold always (including now)
    • φ U ψ (until): φ has to hold until ψ holds (which eventually occurs)
    • φ WU ψ (weak until): φ has to hold until ψ holds (which does not necessarily occur)
    • φ R ψ (release): φ has to hold until ψ held in the previous step.

    Additionally, the boolean operators & (conjunction), | (disjunction) and ! (negation) are used.

Formal behavioral semantics

For evaluating the LTL formulae on the challenge problems, it is important to formally understand the behavioral semantics of the programs.

A program reads inputs (events) from the command line, and upon each event may or may not emit an output (for simplicity we restrict this to a finite set of outputs, of which at most one is issued before the next event occurs). Hence, an (infinite) run is an infinite word over a sequence of input and output symbols. The validity of an LTL formula over such a word is straightforward.

The LTL properties are intended to only specify the error-free behavior of the system. The rationale behind this is that it allows to formulate the specifications in a more compact way. For example, specifying that event A eventually leads to output Z being generated and interpreting it to hold for non-error runs only is probably more intuitive than specifying that A eventually leads to either Z or a fatal error.

Summing this up, an LTL property holds for a certain ECA program if and only if all possible runs which do not lead to an error satisfy the LTL property.