Important Dates:

For Participants

Feedback

FAQ

Programming Languages: Java, C

Java Problems

The Java problems consist of a single Java class (ProblemX.java). The concrete set of inputs is specified at the top of the class definition as a set of plain character sequences (Strings) or their corresponding integer value for the integer version.

    private String[] inputs = {"D","E","A","F","B","C"};

The central method is calculateOutput, which comprises the program's logic. It is realized in terms of a sequence of nested if-then-else blocks. The state of a system is maintained in a set of attributes.

    public String calculateOutput(String input)    
    {
        if (input.equals(inputs[2])             	// EVENT
            && (b0==true && i0==9 && s0.equals("e")))   // CONDITION 
        {
            s0 = "g";                           	// ACTION
            b1 = true;
            return "X";
        } 
        else if ... {
           ...
        }
        ...
        throw new IllegalArgumentException(" Invalid input "); 
    }

At the bottom of this method, there is a sequence of if-statements, checking whether the system is in an invalid state. If this is the case, an IllegalStateException with the respective error code is thrown.

	public String calculateOutput(String input) {
		...
		if(a23 && a3 && a6 && a26 == 3 && a15 && a18.equals("e"))
			throw new IllegalStateException( "error_23" );
		...
	}

Problems come with a main method, instantiating the problem and exposing it to continuous inputs on stdin which occasionally produces output on stdout

    public static void main(String[] args) throws IOException 
    {
        // default output
        String output = "NotInitialized";

        // init eca-system and input reader
        Problem eca = new Problem();
        BufferedReader stdin = new BufferedReader(new InputStreamReader(System.in));

        // main i/o-loop
        while(true)
        {
            // read input
            String input = stdin.readLine();

            try{
              	//operate eca engine output = 
               	eca.calculateOutput(input);
            } catch(IllegalArgumentException e){
  	    	System.err.println("Invalid input: " + e.getMessage());
            }
        }
    }

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

    $ javac ProblemX.java 
    $ java ProblemX 
    A                                   
    X                                   
    .
    .
    .

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. 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 along with their integer translations.

	// inputs
	int d = 4;
	int b = 2;
	int a = 1;
	int c = 3;
	int f = 6;
	int e = 5;

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 sequence of if-statements checks 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.

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

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()
{
    // default output
    int output = -1;

    // 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
    A                                   
    X                                   
    .
    .
    .