Updates

Important Dates:

  • July 31th, 2022:
       Final submission, sequential
  • May 31st, 2022:
       Sequential problems
  • April 4th, 2022:
       Training problems

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 integers as listed in the alphabet mapping file provided together with the benchmarks. 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 funtions like the following, which are if-then-else blocks or a sequence of assignments and a print statement. The state of the program is updated by assigning values to several attributes (integer variables).

void g9919() {
    if((v53878 < v25968)){
        g10189();
    } else {
        g218();
    }
}
...
void g10056() {
    tv59919 = ((498 * v25968) + 804);
    tv25968 = ((498 * v10616) + 804);
    ...
    v59919 = tv59919;
    v25968 = tv25968;
    ...
    
    printf(%d\n",11); fflush(stdout);
    globRet = 2;
}
...

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(int argc, char const* argv[]) {
    int nextCall = 1;
    while(true){				
        switch(nextCall){
            case 1:{
                g0();
                nextCall = globRet;
                break;
            }
            case 2:{
                g1();
                nextCall = globRet;
                break;
            }
            default:{
                fprintf(stderr, "Error during evaluation!");
                return 1;
            }
        }
        int ret = scanf("%d", &i);
        if(ret != 1 || (i != 1) && (i != 2) && ...)
            return -2;
    }
}

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
    .
    .
    .

If the system is in an invalid state, 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.

...
void g233() {
    __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);
}