Updates

Important Dates:

  • Oct. 30 – Nov. 13 (tba), 2018:
       RERS at ISoLA'18
  • Oct. 01 – Oct. 14, 2018:
       Solution Submission
  • Aug. 20, 2018:
       Release Parallel LTL
  • Jul. 18, 2018:
       Release Sequential LTL and
       Sequential Reachability
  • Jul. 18, 2018:
       Training benchmarks
       available

Java Problem Description

The information below is specific to the Java versions of the problems (Sequential LTL and Sequential Reachability).

Please click here to jump to a description of the syntax and compilation of the Sequential 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 program's logic is contained in a method called calculateOutput which is a sequence of nested if-then-else blocks. The state of the program is updated by assigning values to several attributes (integer variables).

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

Problems from the Sequential LTL track can be compiled using javac and executed using java without any prerequisites. For problems from the Sequential Reachability track, please see the following paragraphs.

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