/*******************************************************************************
 * Copyright (c) 2015 Microsoft Research. All rights reserved. 
 *
 * The MIT License (MIT)
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy 
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in all
 * copies or substantial portions of the Software. 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
 * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *
 * Contributors:
 *   Markus Alexander Kuppe - initial API and implementation
 ******************************************************************************/
package tlc2.tool.liveness;

import static org.junit.Assert.fail;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

import org.junit.Before;

import tlc2.TLC;
import tlc2.TLCGlobals;
import tlc2.TestMPRecorder;
import tlc2.output.MP;
import tlc2.tool.CommonTestCase;
import util.FileUtil;
import util.ToolIO;

public abstract class ModelCheckerTestCase extends CommonTestCase {
	
	protected String path = "";
	protected final String spec;
	protected String[] extraArguments = new String[0];

	public ModelCheckerTestCase(String spec) {
		super(new TestMPRecorder());
		this.spec = spec;
	}

	public ModelCheckerTestCase(String spec, String path) {
		this(spec);
		this.path = path;
	}
	
	public ModelCheckerTestCase(String spec, String path, String[] extraArguments) {
		this(spec, path);
		this.extraArguments  = extraArguments; 
	}
	
	/* (non-Javadoc)
	 * @see junit.framework.TestCase#setUp()
	 */
	@Before
	public void setUp() {
		try {
			// TEST_MODEL is where TLC should look for user defined .tla files
			ToolIO.setUserDir(BASE_DIR + TEST_MODEL + path);
			
			MP.setRecorder(recorder);
			
			// Increase the liveness checking threshold to prevent liveness
			// checking of an incomplete graph. Most tests check that the 
			// state queue is empty and fail if not. This is only given 
			// when liveness checking is executed when all states have been
			// generated.
			TLCGlobals.livenessThreshold = Double.MAX_VALUE;
			
			final TLC tlc = new TLC();
			// * We want *no* deadlock checking to find the violation of the
			// temporal formula
			// * We use (unless overridden) a single worker to simplify
			// debugging by taking out threading
			// * MC is the name of the TLA+ specification to be checked (the file
			// is placed in TEST_MODEL
			final List<String> args = new ArrayList<String>(6);
			
			// *Don't* check for deadlocks. All tests are interested in liveness
			// checks which are shielded away by deadlock checking. TLC finds a
			// deadlock (if it exists) before it finds most liveness violations.
			args.add("-deadlock");
			
			args.add("-workers");
			args.add(Integer.toString(getNumberOfThreads()));
			
			// Never create checkpoints. They distort performance tests and are
			// of no use anyway.
			args.add("-checkpoint");
			args.add("0");
			
			// Always print the state graph in dot file notation.
			args.add("-dump");
			args.add("dot");
			args.add("${metadir}" + FileUtil.separator + getClass().getCanonicalName() + ".dot");

			args.addAll(Arrays.asList(extraArguments));
			
			args.add(spec);
			tlc.handleParameters(args.toArray(new String[args.size()]));
			
			// Run the ModelChecker
			tlc.process();
			
		} catch (Exception e) {
			fail(e.getMessage());
		}
	}

	/**
	 * @return The number of worker threads TLC should use.
	 */
	protected int getNumberOfThreads() {
		return 1;
	}
}

@@ -1471,16 +1471,48 @@
 .fail;%0A%0A
+import java.lang.reflect.Field;%0A
 import j
@@ -1531,16 +1531,16 @@
 ayList;%0A
-
 import j
@@ -1954,16 +1954,36 @@
 ring%5B0%5D;
+%0A%09protected TLC tlc;
 %0A%0A%09publi
@@ -2928,18 +2928,8 @@
 %0A%09%09%09
-final TLC 
 tlc 
@@ -4309,16 +4309,16 @@
 ads() %7B%0A
-
 %09%09return
@@ -4324,10 +4324,646 @@
 n 1;%0A%09%7D%0A
+%09%0A%09/**%0A%09 * E.g. %0A%09 * ILiveCheck liveCheck = (ILiveCheck) getField(AbstractChecker.class, %22liveCheck%22,%0A%09 * %09%09%09%09getField(TLC.class, %22instance%22, tlc));%0A%09 */%0A%09protected Object getField(Class%3C?%3E targetClass, String fieldName, Object instance) %7B%0A%09%09try %7B%0A%09%09%09Field field = targetClass.getDeclaredField(fieldName);%0A%09%09%09field.setAccessible(true);%0A%09%09%09return field.get(instance);%0A%09%09%7D catch (NoSuchFieldException e) %7B%0A%09%09%09e.printStackTrace();%0A%09%09%7D catch (SecurityException e) %7B%0A%09%09%09e.printStackTrace();%0A%09%09%7D catch (IllegalArgumentException e) %7B%0A%09%09%09e.printStackTrace();%0A%09%09%7D catch (IllegalAccessException e) %7B%0A%09%09%09e.printStackTrace();%0A%09%09%7D%0A%09%09return null;%0A%09%7D%0A
 %7D%0A

Add framework support to read private fields of instances under test.