/* Anthony Giardullo
 * Danish Lakhani
 * 
 * This file contains the code we used to transform our specially annotated
 * PRISM code into runnable PRISM code.  This code was written quickly for
 * our own use and does not have any error-checking.  Use at your own risk.
 * 
 * Useage:
 *   java prism-helper input-file output-file
 *
 * This program allows you to essentially use for-loops to create many 
 * PRISM rules at once.  This program will modify any line in the input
 * file that starts with "{".  In addition, this program only modifies the
 * line-by-line, so don't break up rules that you want this code to modify
 * into multiple lines except as shown in the examples.
 *
 *
 * EXAMPLES:
 *
 * Running this program on the following expression will produce a rule
 * for every value of i from 1 to 3:
 *
 * {i 1 3} [](x = {i}) -> (y'=var{i});
 *
 * will get changed to:
 *
 * [](x = 1) -> (y'=var1);
 * [](x = 2) -> (y'=var2);
 * [](x = 3) -> (y'=var3);
 *
 *
 * You can also specify the bounds of the loop using constants from the
 * code.  Suppose the constants 'start' and 'end' are defined on an
 * earlier line in the PRISM file.  You can then have i range over all
 * values between these values inclusively as follows:
 *
 * {i start end} [](x = {i}) -> (y'=var{i});
 *
 *
 * This program also supports looping over all possible values of two
 * variables:
 *
 * {i 1 3 j 100 101} [](x = {i}) & (y = {j}) -> (z'={i}*{j});
 *
 * will get changed to:
 *
 * [](x = 1) & (y = 100) -> (z'=1*100);
 * [](x = 1) & (y = 101) -> (z'=1*101);
 * [](x = 2) & (y = 100) -> (z'=2*100);
 * [](x = 2) & (y = 101) -> (z'=2*101);
 * [](x = 3) & (y = 100) -> (z'=3*100);
 * [](x = 3) & (y = 101) -> (z'=3*101);
 *
 *
 * Also, you can loop over two lines at once as follows:
 *
 * 2{i 1 2} [](x = {i}) ->
 * {j 1 3} prob: (y'={j})+
 *
 * will get changed to:
 *
 * [](x = 1) ->
 * prob: (y'=1)+
 * prob: (y'=2)+
 * prob: (y'=3);
 * [](x = 2) ->
 * prob: (y'=1)+
 * prob: (y'=2)+
 * prob: (y'=3);
 *
 * Note that a semicolon is replaced in the last line of each rule.
 *
 * You can use the same syntax above to create just one rule with a
 * variable number of transitions by sticking a dummy variable in the
 * first loop that is not used:
 *
 * 2{z 1 1} [](foo = true) ->
 * {j 1 3} prob: (y'={j})+
 *
 * will get changed to:
 *
 * [](foo = true) ->
 * prob: (y'=1)+
 * prob: (y'=2)+
 * prob: (y'=3);
 *
 *
 * It is worth noting that this program has nothing to do with PRISM other
 * than that it knows when to change a '+' to a ';' as shown above.  So
 * you should be able to use this program with PRISM 2.0 although it has
 * not been tested.
 *
 */

import java.io.*;
import java.lang.*;
import java.util.*;


public class prismHelper{


    private static Hashtable constants = new Hashtable();


    public static void printUseage(){
	System.out.println("preparse in-file out-file ");
			   
    }

    public static void addConstant(String name, int value, PrintStream pStream){
	String line = "const " + name + " = " + value +";";
	pStream.println(line);
	constants.put(name, String.valueOf(value));
    }

    public static void addRate(String name, double value, PrintStream
			       pStream){
	String line = "rate " + name + " = " + value + ";";
	pStream.println(line);
    }


    public static void main(String[] args) throws Exception{
	if(!(args.length == 2)){

	    printUseage();
	    return;
	}
	
	String in = args[0];
	String out = args[1];


	File inFile = new File(in);
	FileInputStream inStream = new FileInputStream(inFile);
	BufferedReader reader = 
	    new BufferedReader(new InputStreamReader(inStream));


	File outFile = new File(out);
	FileOutputStream outStream = new FileOutputStream(outFile);
	PrintStream pStream = new PrintStream(outStream);
	
	String line;
	while((line = reader.readLine()) != null){

	    if(line.trim().startsWith("const ")){
		int index1 = line.indexOf("const ");
		int index2 = line.indexOf("=");
		int index3 = line.indexOf(";");
		String c = line.substring(index1 + 6, index2).trim(); 
		String cval = line.substring(index2 + 1, index3).trim();
		int val = Integer.parseInt(cval);

		constants.put(c, cval);
	    }

	    
	    if(line.trim().startsWith("{")){
		line = line.trim();
		doScript(line, pStream, null);
	    }
	    else if(line.trim().startsWith("2{")){
		line = line.trim().substring(1);

		doScript(line, pStream, reader.readLine().trim());
	    }
	    else{
		pStream.println(line);
	    }
	    

	}
	

    }

    private static void doScript(String line, PrintStream pStream, String line2) {

	String dec = line.substring(1, line.indexOf("}"));
	line = line.substring(line.indexOf("}")+1);
	
	StringTokenizer tok = new StringTokenizer(dec, " ");
	
	int numVars = tok.countTokens() / 3;
	String[] vars = new String[numVars];
	int[] varStarts = new int[numVars];
	int[] varEnds = new int[numVars];
	
	for(int i = 0; tok.hasMoreTokens(); i++){
	    vars[i] = tok.nextToken();
	    
	    String token = tok.nextToken();
	    Object cval = constants.get(token);
	    if(cval != null)
		varStarts[i] = Integer.parseInt((String)cval);
	    else
		varStarts[i] = Integer.parseInt(token);
	    
	    token = tok.nextToken();
	    cval = constants.get(token);
	    if(cval != null)
		varEnds[i] = Integer.parseInt((String)cval);
	    else
		varEnds[i] = Integer.parseInt(token);
	}
	
	
	//only for 2 vars for now
	for(int i = varStarts[0]; i <= varEnds[0]; i++){
	    
	    String temp = 
		replaceSubstring(line, "{"+vars[0]+"}",String.valueOf(i));
	    String line2temp = 
		replaceSubstring(line2,"{"+vars[0]+"}", String.valueOf(i));
	    
	    if(numVars > 1){
		for(int j = varStarts[1]; j <= varEnds[1]; j++){
		    
		    String temp2 = 
			replaceSubstring(temp, "{"+vars[1]+"}", String.valueOf(j));
		    String line2temp2 = 
			replaceSubstring(line2temp, "{"+vars[1]+"}", String.valueOf(j));
    
		    if(i == varEnds[0] && j == varEnds[1])
			temp2 = replacePlusWithSemi(temp2);
		    
		    pStream.println(temp2);
		    if(line2 != null)
			doScript(line2temp2, pStream, null);
		    
		}
	    }else{
		
		if(i == varEnds[0])
		    temp = replacePlusWithSemi(temp);
		
		pStream.println(temp);
		if(line2 != null){
		   
		    doScript(line2temp, pStream, null);
		}
	    }
	    
	}
		    
    }


    private static String replacePlusWithSemi(String line){
	if(line.trim().endsWith("+"))	{
	    int index = line.lastIndexOf("+");

	    return line.substring(0, index) + ";";
	}
	else{
	    return line;
	}
    }


    private static String replaceSubstring(String s, String old, String replace)
    {
	String result = "";
	
	if(s == null)
	    return null;

	int position;
	while((position = s.indexOf(old)) >= 0){
	    result += s.substring(0, position);
	    result += replace;

	    s = s.substring(position + old.length());

	}

	result += s;

	return result;
    }
}