/* AlloyTester - Decompiled by JODE
 * Visit http://jode.sourceforge.net/
 */
package alloy.tester;
import java.io.BufferedInputStream;
import java.io.BufferedReader;
import java.io.FileInputStream;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.StringTokenizer;

import alloy.api.AlloyRunner;
import alloy.ast.Command;
import alloy.ast.Commands;
import alloy.transl.TranslException;
import alloy.util.CleanupManager;
import alloy.util.Dbg;
import alloy.util.Params;

import gnu.getopt.Getopt;

public class AlloyTester
{
    private static final boolean DEBUG = true;
    private static Dbg.DbgMsgListener _infoListener
	= new Dbg.DbgMsgStreamPrinter(System.out);
    private static boolean _verbose = false;
    private static final String _helpMsg
	= "Alloy Tester command line options:\n  -v : verbose output";
    
    private static class TestSpecs
    {
	private List _configFilenames = new ArrayList();
	private Map _modelToCommandResults = new HashMap();
	
	public TestSpecs(String string) throws IOException {
	    _parseSpecFile(string);
	}
	
	public void runTests() {
	    Iterator iterator = _configFilenames.iterator();
	    while (iterator.hasNext()) {
		String string = (String) iterator.next();
		System.out.println
		    ("#####################################################");
		System.out
		    .println("running with configuration file " + string);
		System.out.println
		    ("#####################################################");
		try {
		    BufferedInputStream bufferedinputstream
			= new BufferedInputStream(new FileInputStream(string));
		    Params.glob = Params.load(bufferedinputstream);
		} catch (IOException ioexception) {
		    System.err.println("Could not load configuration file "
				       + string);
		    break;
		}
		Iterator iterator_0_
		    = _modelToCommandResults.entrySet().iterator();
		while (iterator_0_.hasNext()) {
		    Map.Entry entry = (Map.Entry) iterator_0_.next();
		    String string_1_ = (String) entry.getKey();
		    Map map = (Map) entry.getValue();
		    _runTestsForModel(string_1_, map);
		    System.err.println
			("---------------------------------------------");
		}
	    }
	}
	
	private void _runTestsForModel(String string, Map map) {
	    System.out.println("compiling model " + string);
	    System.gc();
	    boolean bool = false;
	    try {
		bool = AlloyRunner.prepareSpec(string);
	    } catch (RuntimeException runtimeexception) {
		_failTest("tool crashed while compiling " + string
			  + " with exception " + runtimeexception);
		runtimeexception.printStackTrace(System.out);
		return;
	    }
	    boolean bool_2_ = map.isEmpty();
	    if (bool && bool_2_)
		_failTest("model " + string + " should not have compiled");
	    else if (!bool && !bool_2_)
		_failTest("model " + string + " should have compiled");
	    else {
		if (bool)
		    _passTest("model " + string + " compiled");
		else {
		    _passTest("model " + string + " did not compile");
		    return;
		}
		HashMap hashmap = new HashMap();
		Commands commands = AlloyRunner.getCommands();
		Iterator iterator = commands.getCommandIter();
		while (iterator.hasNext()) {
		    Command command = (Command) iterator.next();
		    if (command.name != null)
			hashmap.put(command.name, command);
		}
		Iterator iterator_3_ = map.entrySet().iterator();
		while (iterator_3_.hasNext()) {
		    Map.Entry entry = (Map.Entry) iterator_3_.next();
		    String string_4_ = (String) entry.getKey();
		    boolean bool_5_
			= ((Boolean) entry.getValue()).booleanValue();
		    if (!hashmap.containsKey(string_4_))
			System.err.println("No command named " + string_4_
					   + " can be found.");
		    else {
			Command command = (Command) hashmap.get(string_4_);
			System.out.println("Analyzing command " + string_4_
					   + ": " + command);
			Object object = null;
			alloy.api.SolutionData solutiondata;
			try {
			    AlloyRunner.clearState();
			    solutiondata = null;
			    try {
				solutiondata
				    = (AlloyRunner.analyzeCommand
				       (AlloyRunner.translateCommand(command),
					System.currentTimeMillis()));
			    } catch (TranslException translexception) {
				System.out.println
				    ("Could not translate command " + string_4_
				     + " of model " + string + ": "
				     + translexception);
			    }
			} catch (RuntimeException runtimeexception) {
			    _failTest("tool crash while analyzing command "
				      + string_4_ + " of model " + string
				      + " with exception " + runtimeexception);
			    runtimeexception.printStackTrace(System.out);
			    continue;
			}
			boolean bool_6_ = solutiondata != null;
			if (bool_6_ && !bool_5_)
			    _failTest
				("command " + string_4_ + " of model " + string
				 + " should have no solution, but solution found\n"
				 + solutiondata);
			else if (!bool_6_ && bool_5_)
			    _failTest("command " + string_4_ + " of model "
				      + string + " should have a solution");
			else if (bool_6_)
			    _passTest("solution found for command " + string_4_
				      + " of model " + string);
			else
			    _passTest("no solution found for command "
				      + string_4_ + " of model " + string);
		    }
		}
	    }
	}
	
	private void _parseSpecFile(String string) throws IOException {
	    BufferedReader bufferedreader
		= new BufferedReader(new FileReader(string));
	    StringTokenizer stringtokenizer
		= new StringTokenizer(bufferedreader.readLine());
	    while (stringtokenizer.hasMoreTokens())
		_configFilenames.add(stringtokenizer.nextToken());
	    String string_7_;
	    while ((string_7_ = bufferedreader.readLine()) != null) {
		StringTokenizer stringtokenizer_8_
		    = new StringTokenizer(string_7_);
		String string_9_ = stringtokenizer_8_.nextToken();
		HashMap hashmap = new HashMap();
		while (stringtokenizer_8_.hasMoreTokens()) {
		    String string_10_ = stringtokenizer_8_.nextToken();
		    int i = Integer.parseInt(stringtokenizer_8_.nextToken());
		    Boolean var_boolean = new Boolean(i > 0);
		    hashmap.put(string_10_, var_boolean);
		}
		_modelToCommandResults.put(string_9_, hashmap);
	    }
	}
	
	private void _failTest(String string) {
	    System.out.println("FAIL: " + string);
	}
	
	private void _passTest(String string) {
	    System.out.println("PASS: " + string);
	}
	
	public String toString() {
	    return ("config files: " + _configFilenames + ", tests: "
		    + _modelToCommandResults);
	}
    }
    
    public static void main(String[] strings) {
	try {
	    Getopt getopt = new Getopt("Alloy Tester", strings, "v");
	    int i;
	    while ((i = getopt.getopt()) != -1) {
		switch (i) {
		case 118:
		    _verbose = true;
		    Dbg.addDbgMsgListener(0, _infoListener);
		    break;
		case 63:
		case 104:
		    System.out.println
			("Alloy Tester command line options:\n  -v : verbose output");
		    return;
		}
	    }
	    Dbg.defaultInit();
	    for (int i_11_ = getopt.getOptind(); i_11_ < strings.length;
		 i_11_++) {
		try {
		    TestSpecs testspecs = new TestSpecs(strings[i_11_]);
		    System.out.println(testspecs);
		    testspecs.runTests();
		} catch (IOException ioexception) {
		    System.err.println("Unable to open test spec. file "
				       + strings[i_11_]);
		}
	    }
	} catch (RuntimeException runtimeexception) {
	    System.err
		.println("ERROR: Uncaught exception in regression tester.");
	    runtimeexception.printStackTrace();
	    CleanupManager.exit(1);
	}
	CleanupManager.exit(0);
    }
}