package jkind;

import java.io.File;
import java.io.IOException;

import jkind.analysis.StaticAnalyzer;
import jkind.lustre.Node;
import jkind.lustre.Program;
import jkind.lustre.parsing.LustreLexer;
import jkind.lustre.parsing.LustreParser;
import jkind.lustre.parsing.LustreParser.ProgramContext;
import jkind.lustre.parsing.LustreToAstVisitor;
import jkind.lustre.parsing.StdoutErrorListener;
import jkind.processes.Director;
import jkind.slicing.LustreSlicer;
import jkind.translation.InlineConstants;
import jkind.translation.InlineNodeCalls;
import jkind.translation.InlineTypes;
import jkind.translation.Specification;

import org.antlr.v4.runtime.ANTLRFileStream;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.RecognitionException;

public class Main {
	final public static String VERSION = "1.1";
	
	public static void main(String args[]) throws IOException, RecognitionException, InterruptedException {
		String filename = ArgumentParser.parse(args);
		if (!new File(filename).exists()) {
			System.out.println("Cannot find file " + filename);
			System.exit(-1);
		}
		
		Program program = parseLustre(filename);
		if (program.main == null) {
			System.out.println("Error: no main node");
			System.exit(-1);
		}
		
		if (!StaticAnalyzer.check(program)) {
			System.exit(-1);
		}

		program = InlineTypes.program(program);
		program = InlineConstants.program(program);
		Node main = InlineNodeCalls.program(program);
		
		main = LustreSlicer.slice(main);
		Specification spec = new Specification(filename, main);
		new Director(spec).run();
		System.exit(0); // Kills all threads
	}

	private static Program parseLustre(String filename) throws IOException, RecognitionException {
		CharStream stream = new ANTLRFileStream(filename);
		LustreLexer lexer = new LustreLexer(stream);
		CommonTokenStream tokens = new CommonTokenStream(lexer);
		LustreParser parser = new LustreParser(tokens);
		
		parser.removeErrorListeners();
		parser.addErrorListener(new StdoutErrorListener());
		
		ProgramContext program = parser.program();
		if (parser.getNumberOfSyntaxErrors() > 0) {
			System.exit(-1);
		}
		
		return new LustreToAstVisitor().program(program);
	}
}

@@ -678,32 +678,80 @@
 TLRFileStream;%0D%0A
+import org.antlr.v4.runtime.BailErrorStrategy;%0D%0A
 import org.antlr
@@ -851,23 +851,185 @@
 runtime.
-Recogni
+DefaultErrorStrategy;%0D%0Aimport org.antlr.v4.runtime.RecognitionException;%0D%0Aimport org.antlr.v4.runtime.atn.PredictionMode;%0D%0Aimport org.antlr.v4.runtime.misc.ParseCancella
 tionExce
@@ -1057,16 +1057,17 @@
 s Main %7B
+%0D
 %0A%09final 
@@ -1105,17 +1105,16 @@
 %221.1%22;%0D%0A
-%09
 %0D%0A%09publi
@@ -1188,17 +1188,21 @@
 ception,
- 
+%0D%0A%09%09%09
 Interrup
@@ -1215,16 +1215,17 @@
 eption %7B
+%0D
 %0A%09%09Strin
@@ -1383,26 +1383,24 @@
 (-1);%0D%0A%09%09%7D%0D%0A
-%09%09
 %0D%0A%09%09Program 
@@ -1533,26 +1533,24 @@
 (-1);%0D%0A%09%09%7D%0D%0A
-%09%09
 %0D%0A%09%09if (!Sta
@@ -1743,26 +1743,24 @@
 (program);%0D%0A
-%09%09
 %0D%0A%09%09main = L
@@ -2233,122 +2233,666 @@
 );%0D%0A
-%09%09%0D%0A%09%09parser.removeErrorListeners();%0D%0A%09%09parser.addErrorListener(new StdoutErrorListener());%0D%0A%09%09%0D%0A%09%09ProgramContext 
+%0D%0A%09%09ProgramContext program;%0D%0A%0D%0A%09%09// Due to performance issues in the Antlr 4.0 release, we use a 2-stage%0D%0A%09%09// parsing approach. This may not be necessary in the future.%0D%0A%09%09// https://github.com/antlr/antlr4/issues/192%0D%0A%09%09parser.removeErrorListeners();%0D%0A%09%09parser.getInterpreter().setPredictionMode(PredictionMode.SLL);%0D%0A%09%09parser.setErrorHandler(new BailErrorStrategy());%0D%0A%09%09try %7B%0D%0A%09%09%09program = parser.program();%0D%0A%09%09%7D catch (ParseCancellationException e) %7B%0D%0A%09%09%09tokens.reset();%0D%0A%09%09%09parser.addErrorListener(new StdoutErrorListener());%0D%0A%09%09%09parser.setErrorHandler(new DefaultErrorStrategy());%0D%0A%09%09%09parser.getInterpreter().setPredictionMode(PredictionMode.LL);%0D%0A%09%09%09
 prog
@@ -2912,24 +2912,31 @@
 program();%0D%0A
+%09%09%7D%0D%0A%0D%0A
 %09%09if (parser
@@ -2996,18 +2996,16 @@
 ;%0D%0A%09%09%7D%0D%0A
-%09%09
 %0D%0A%09%09retu

Use 2-stage parsing to avoid performance issues