Updates

  • 26/07/17 results and solutions uploaded
  • 12/06/17 parallel problems updated
  • 26/05/17 parallel problems released
  • 01/03/17 parallel training problems released
  • 15/02/17 sequential problems released
  • 01/02/17 training sequential up, challenge problems postponed
  • 27/01/17 update on parallel problems

Important Dates:

  • 12/07/17
       RERS at ISSTA/SPIN
  • 01/02/17
       Release Sequential Training    Problems
  • 15/02/17
       Release Sequential    Problems
  • 01/03/17
       Release Parallel Training    Problems
  • 26/05/17
       Release Parallel Problems
  • 01/02/17 - 01/07/17
       Challenge Phase
  • 15/02/17 - 01/07/17
       Solution Submission

Java Problems

The information below is specific to the Java versions of the problems (reachability and LTL). Syntax and compilation of the Reachability 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).

    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 (cf && input.equals(inputs[2])             	
            && (b0==true && i0==9 && s0.equals("e"))) {
            s0 = "g";                           	
            b1 = true;
            System.out.println("Z");
        } 
        else if ... {
           ...
        }
        ...
    	if(cf)
    	throw new IllegalArgumentException("Current state has no transition for this input!");

    }

Problems come with a main method, instantiating the problem and exposing it to continuous inputs on stdin which always produce output on stdout. All input not in the alphabet lead to the termination of the program.

    public static void main(String[] args) throws IOException 
    {
        // init system
        Problem eca = new Problem();
        BufferedReader stdin = new BufferedReader(new InputStreamReader(System.in));

        // main i/o-loop
        while(true)
        {
            // read input
            String input = stdin.readLine();
            if((input.equals("B")) && (input.equals("E")) && (input.equals("C")) && (input.equals("A")) && (input.equals("D")))
                throw new IllegalArgumentException("Current state has no transition for this input!");
            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                                   
    .
    .
    .

At the bottom of the calculateOutput 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 Errors.__VERIFIER_error(int) is called with the integer that identifies the specific error ID. In the example the error ID is 5.

    private void errorCheck() {
        ...
        if(a23 && a3 && a6 && a26 == 3 && a15 && a18.equals("e"))
            Errors.__VERIFIER_error(5);
        ...
    }

To compile the problems, an additional file Errors.java has to be created in the same directory. The source code with an example implementation of the semantics can be seen below. Errors.java has to be compiled before the problem can be run.

public class Errors { 
           
    public static void __VERIFIER_error(int i) {
        throw new IllegalStateException( "error_" + i );
    }
}