package edu.kit.iti.formal.pse.worthwhile.prover;

import org.junit.Assert;
import org.junit.Test;

import edu.kit.iti.formal.pse.worthwhile.common.tests.TestASTProvider;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;

/**
 * Test the functionality of the event listener mechanism in {@link SpecificationChecker}.
 * 
 * @author Leon Handreke
 */
public class ProverEventListenerTest {
	/**
	 * Test listener that counts the number of times each event was fired.
	 */
	class CountingProverEventListener extends AbstractProverEventListener {
		/**
		 * Counter for how often programVerified was called.
		 */
		private int programVerifiedCounter = 0;

		/**
		 * @return the number of times that programVerified was called
		 */
		public int getProgramVerifiedCounter() {
			return programVerifiedCounter;
		}

		@Override
		public void programVerified(final Program program, final Validity validity,
		                final ProverResult proverResult) {
			this.programVerifiedCounter++;
		}
	}

	/**
	 * Test the functionality of {@link DistributorProverEventListener}.
	 */
	@Test
	public final void testDistributorEventListener() {
		/**
		 * Test-specific event listener class that also checks for validity.
		 */
		class TestDistributorCountingProverEventListener extends CountingProverEventListener {
			@Override
			public void programVerified(final Program program, final Validity validity,
			                final ProverResult proverResult) {
				super.programVerified(program, validity, proverResult);
				Assert.assertEquals(Validity.VALID, validity);
			}
		}
		TestDistributorCountingProverEventListener firstListener = new TestDistributorCountingProverEventListener();
		TestDistributorCountingProverEventListener secondListener = new TestDistributorCountingProverEventListener();

		SpecificationChecker checker = new SpecificationChecker();
		checker.addProverEventListener(firstListener);
		checker.addProverEventListener(secondListener);

		Program p = TestASTProvider.getRootASTNode("Integer i := 0\n_assert i = 0\n");
		checker.checkProgram(p);

		Assert.assertEquals(1, firstListener.getProgramVerifiedCounter());
		Assert.assertEquals(1, secondListener.getProgramVerifiedCounter());

		checker.removeProverEventListener(secondListener);
		checker.checkProgram(p);

		Assert.assertEquals(2, firstListener.getProgramVerifiedCounter());
		Assert.assertEquals(1, secondListener.getProgramVerifiedCounter());
	}
}

@@ -164,16 +164,79 @@
 ovider;%0A
+import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;%0A
 import e
@@ -287,16 +287,16 @@
 rogram;%0A
-
 %0A/**%0A * 
@@ -968,16 +968,42 @@
 alidity,
+ final Expression formula,
 %0A%09%09     
@@ -1492,16 +1492,42 @@
 alidity,
+ final Expression formula,
 %0A%09%09%09    
@@ -1573,16 +1573,16 @@
 sult) %7B%0A
-
 %09%09%09%09supe
@@ -1617,16 +1617,25 @@
 alidity,
+ formula,
  proverR

Fix compilation errors in ProverEventListenerTest