Updates

Important Dates:

  • Nov. 08, 2018:
       RERS at ISoLA'18
  • Oct. 01 – Oct. 14, 2018:
       Solution Submission
  • Aug. 22, 2018:
       Release Parallel LTL
  • Jul. 18, 2018:
       Release Sequential LTL and
       Sequential Reachability
  • Jul. 18, 2018:
       Training benchmarks
       available

C99/C++ Problem Description

The information below is specific to the C99 versions of the problems (Sequential LTL and Sequential Reachability). Semantically, all integers are to be interpreted as 32 bit integer.

Please click here to jump to a description of the syntax and compilation of the Sequential Reachability problems.

The C99 implementation of a reactive system comes as a single source file. For maximum compatibility with existing software model checking tools, the only data type which is used is int (or int arrays). Because input and output symbols are identified by characters in the LTL properties, a corresponding translation is realized by replacing letters by their position in the Latin alphabet: "A" is replaced by 1, "X" by 24 and so on. At the top of each source file, the valid input symbols are explicitly listed in an array.

	// inputs
	int inputs[] = {3,1,6,5,2,4};
	...

The program's logic is contained in a function called calculate_output which is a sequence of nested if-then-else blocks. The state of the program is updated by assigning values to several attributes (integer variables).

    int calculate_output(int input)
    {
        if(input == 3
            && (a7 != 0 && a0 == 9 && a6 == 0))
        {
            a3 = a5[a4 + 6];
            a9 = 2;
            printf("%d\n", 24); fflush(stdout);
        }
        ...
     }

The main() function, which is also contained in the source file, consists of the main loop which connects the program to continuous inputs (via stdin) and eventually leads to outputs (via stdout). All input not in the alphabet lead to the termination of the program.

int main()
{
    // main i/o-loop
    while(1)
    {
        // read input
        int input;
        scanf("%d", &input);
        if((input != 2) && (input != 5) && (input != 3) && (input != 1) && (input != 4))
          return -2;
        // operate eca engine
        calculate_output(input);
    }
}

Problems from the Sequential LTL track can be compiled using gcc or g++ and executed without any prerequisites. For problems from the Sequential Reachability track, please see the following paragraphs.

    $ gcc -o ProblemX ProblemX.c
    $ ./ProblemX
    1
    24
    .
    .
    .

At the bottom of the calculate_output a method errorCheck is called (specific for reachability problems) that checks in a sequence of if-statements whether the system is in an invalid state. If this is the case, the external function __VERIFIER_error(int) is called with the integer that identifies the specific error ID. In the example the error ID is 5.

    int calculate_output(int input) {
        ...
        if((a23 == 0 && a3 != 0 && a26 == 3))
        __VERIFIER_error(5);
        ...
    }

To compile the problems the definition of the external function can be replaced by the following example code to explicitly imitate the behavior during previous challenges (RERS 2015 and earlier). The error is then printed on the console.

void __VERIFIER_error(int);

void __VERIFIER_error(int i) {
    fprintf(stderr, "error_%d ", i);
    assert(0);
}