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

The C implementations of the program come as a single C99 source file. For maximum compatibility with existing software model checking tools, the only data type which is used is int (or int arrays). Since input and outputs are expected as (one-letter) strings, the 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 method called calculate_output, which is a sequence of nested if-then-else blocks. The state of the program is maintained in a set of attributes.

    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);
    }
}

The systems can be compiled using gcc or g++ and executed without any prerequisites.

    $ 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 of the RERS 2015 problems. The error is then printed on the console.

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