package gov.nasa.jpf.test.listener;

import gov.nasa.jpf.util.test.TestJPF;

import java.io.ByteArrayOutputStream;
import java.io.PrintStream;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import org.junit.Test;

/**
 * Tests the CallMonitor listener.
 *
 * @author Franck van Breugel
 */
public class CallMonitorTest extends TestJPF {
	/**
	 * JPF's application properties.
	 */
	private static final String[] CONFIGURATION = { "+listener=gov.nasa.jpf.listener.CallMonitor", "+classpath=C:/Users/franck/Documents/teaching/2019-20/4315/workspace/franck/bin/", "+native_classpath=C:/Users/franck/Documents/teaching/2019-20/4315/workspace/franck/bin/" };

	/**
	 * Tests the CallMonitor listener on an empty app.
	 */
	@Test
	public void emptyTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			// do nothing
		} else {
			System.setOut(out);
			assertTrue("", stream.toString().contains("0:")); // main thread invokes a method
		}
	}

	/**
	 * Method used in staticMethodTest.
	 */
	private static void staticMethod() {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to staticMethod.
	 */
	@Test
	public void staticMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			staticMethod();
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.staticMethod\\(\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in methodTest.
	 */
	private void method() {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to method.
	 */
	@Test
	public void methodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			method();
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.method\\(\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in staticIntMethodTest.
	 */
	private static void staticIntMethod(int i) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to staticIntMethod.
	 */
	@Test
	public void staticIntMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			staticIntMethod(0);
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.staticIntMethod\\(0\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in intMethodTest.
	 */
	private void intMethod(int i) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to intMethod.
	 */
	@Test
	public void intMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			intMethod(0);
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.intMethod\\(0\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in staticDoubleMethodTest.
	 */
	private static void staticDoubleMethod(double d) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to staticDoubleMethod.
	 */
	@Test
	public void staticDoubleMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			staticDoubleMethod(1.0);
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.staticDoubleMethod\\(1\\.0\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in doubleMethodTest.
	 */
	private void doubleMethod(double d) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to doubleMethod.
	 */
	@Test
	public void doubleMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			doubleMethod(1.0);
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.doubleMethod\\(1\\.0\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in staticNullMethodTest
	 */
	private static void staticNullMethod(Object o) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to staticNullMethod.
	 */
	@Test
	public void staticNullMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			staticNullMethod(null);
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.staticNullMethod\\(null\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in nullMethodTest.
	 */
	private void nullMethod(Object o) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to nullMethod.
	 */
	@Test
	public void nullMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			nullMethod(null);
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.nullMethod\\(null\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}

	/**
	 * Method used in staticObjectMethodTest.
	 */
	private static void staticObjectMethod(Object o) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to staticObjectMethod.
	 */
	@Test
	public void staticObjectMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			staticObjectMethod(new Object());
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.staticObjectMethod\\(java\\.lang\\.Object.*\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}
	
	/**
	 * Method used in objectMethodTest.
	 */
	private static void objectMethod(Object o) {}

	/**
	 * Tests the CallMonitor listener on an app containing a call to staticObjectMethod.
	 */
	@Test
	public void objectMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			objectMethod(new Object());
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.objectMethod\\(java\\.lang\\.Object.*\\).*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}
	
	/**
	 * Method that creates a thread and is used in createsThreadMethodTest.
	 */
	private void createsThreadMethod() {
		(new Thread() {
			private void method() {}
			
			public void run() {
				method();
			}
		}).start();
	}
	
	/**
	 * Tests the CallMonitor listener on an app containing two threads.
	 */
	@Test
	public void createsThreadMethodTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			createsThreadMethod();
		} else {
			System.setOut(out);
			Pattern pattern = Pattern.compile(".*0:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\.createsThreadMethod.*", Pattern.DOTALL);
			Matcher matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
			pattern = Pattern.compile(".*1:.*gov\\.nasa\\.jpf\\.test\\.listener\\.CallMonitorTest\\$1\\.method.*", Pattern.DOTALL);
			matcher = pattern.matcher(stream.toString());
			assertTrue("Output produced by JPF:\n" + stream + "\ndoes not match " + pattern, matcher.matches());
		}
	}
	
	/**
	 * Returns the number of spaces in the given string before the character at the given index.
	 * 		
	 * @param word a string
	 * @param index an index within the string
	 * @return the number of spaces in the given string before the character at the given index
	 */
	private static int numberOfPreceedingSpaces(String word, int index) {
		int number = 0;
		while (index > 0 && word.charAt(index - 1) == ' ') {
			index--;
			number++;
		}
		return number;
	}
	
	/**
	 * Method used in atSameDepthTest.
	 */
	private static void first() {}
	
	/**
	 * Method used in atSameDepthTest and atDifferentDepthTest.
	 */
	private static void second() {}
	
	/**
	 * Tests the CallMonitor listener on an app with two method calls at the same depth.
	 */
	@Test
	public void atSameDepthTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			first();
			second();
		} else {
			System.setOut(out);
			String output = stream.toString();
			int first = output.indexOf("gov.nasa.jpf.test.listener.CallMonitorTest.first");
			assertTrue("Output produced by JPF:\n" + output + "\ndoes not contain first", first >= 0);
			int second = output.indexOf("gov.nasa.jpf.test.listener.CallMonitorTest.second");
			assertTrue("Output produced by JPF:\n" + output + "\ndoes not contain second", second >= 0);
			assertEquals("Output produced by JPF:\n" + output, numberOfPreceedingSpaces(output, first), numberOfPreceedingSpaces(output, second));
		}
	}
	
	/**
	 * Method used in atDifferentDepthTest.
	 */
	private static void third() {
		second();
	}
	
	/**
	 * Tests the CallMonitor listener on an app with two method calls at the same depth.
	 */
	@Test
	public void atDifferentDepthTest() {
		PrintStream out = null;
		ByteArrayOutputStream stream = null;
		if (!isJPFRun()) {
			out = System.out;
			stream = new ByteArrayOutputStream();
			System.setOut(new PrintStream(stream));
		}
		if (verifyNoPropertyViolation(CONFIGURATION)) {
			third();
		} else {
			System.setOut(out);
			String output = stream.toString();
			int second = output.indexOf("gov.nasa.jpf.test.listener.CallMonitorTest.second");
			assertTrue("Output produced by JPF:\n" + output + "\ndoes not contain second", second >= 0);
			int third = output.indexOf("gov.nasa.jpf.test.listener.CallMonitorTest.third");
			assertTrue("Output produced by JPF:\n" + output + "\ndoes not contain third", third >= 0);
			assertEquals("Output produced by JPF:\n" + output, numberOfPreceedingSpaces(output, third) + 1, numberOfPreceedingSpaces(output, second));
		}
	}
	
	/**
	 * Runs the test methods with the given names.  If no names are given, all test methods are run.
	 *
	 * @param testMethods the names of the test methods to be run.
	 */
	public static void main(String[] testMethods) {
		runTestsOfThisClass(testMethods);
	}
}