Important Dates:

For Participants

General

C Problems

The information below is specific to the C problems.

The C implementations of the program come as a single C 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 along with all errors than can occur.

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

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                               // EVENT
            && (a7 != 0 && a0 == 9 && a6 == 0))	    // CONDITION		
        {
            a3 = 4;                                 // ACTION
            a9 = 2;
            return 24;
        }
        ...
     }

At the bottom of this function, a method errorCheck is called that checks in a sequence of if-statements whether the system is in an invalid state. If this is the case, an error is raised by a failed assertion. To identify the specific error in the source code, the assertion is labeled with the error ID. On execution of the compiled file, the error label will also be printed to the console.

    int calculate_output(int input) {
        ...
        if((a23 == 0 && a3 != 0 && a26 == 3))
error_6: 	assert(!error_6);
        ...
    }

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 occasionally leads to outputs (via stdout).

int main()
{
    // main i/o-loop
    while(1)
    {
        // read input
        int input;
        scanf("%d", &input);        

        // operate eca engine
        calculate_output(input);
    }
}

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

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