//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

// This is a very stripped down version of the PRISM version 3.x parser
// used to generate valid code for post-3.x versions of PRISM.

// It fixes 3 things:
// * appends semicolons to properties in properties files
// * ensures that updates are parenthesised
// * replaces the defunct range operator with an equivalent expression

options {
	LOOKAHEAD = 2147483647; // max possible lookahead
}

PARSER_BEGIN(Prism3To4)

package parser;

import java.io.*;

@SuppressWarnings({"unused", "static-access", "serial"})
public class Prism3To4
{
	public static void main(String[] args) throws ParseException
	{
		try {
			Prism3To4 p;
			if (args.length > 0) { p = new Prism3To4(new FileInputStream(args[0])); }
			else { p = new Prism3To4(System.in); }
			p.ModulesFileOrPropertiesFile();
		}
		catch (TokenMgrError e) {
			System.err.println("Syntax error"+(args.length > 0?" in "+args[0]:"")+": " + e.getMessage()); System.exit(1);
		}
		catch (ParseException e) {
			System.err.println("Error"+(args.length > 0?" in "+args[0]:"")+": " + e.getMessage()); System.exit(1);
		}
		catch (FileNotFoundException e) {
			System.err.println(e); System.exit(1);
		}
	}
	
	private static void insertTokenBeforeNext(Token t, String s)
	{
		Token tNew=new Token(); tNew.image=s; tNew.specialToken=t.next.specialToken; t.next.specialToken=null; tNew.next=t.next; t.next=tNew;
	} 
}

//-----------------------------------------------------------------------------------

PARSER_END(Prism3To4)

// skip (but store) all other white space

SPECIAL_TOKEN :
{
	<WHITESPACE: (" "|"\t"|"\n"|"\r")>
}

// skip (but store) comments

SPECIAL_TOKEN :
{
	<COMMENT: "//" (~["\n","\r"])* ("\n"|"\r"|"\r\n")>
}

// tokens

TOKEN :
{
	// keywords
	< BOOL:				"bool" >
|	< CONST:			"const" >
|	< CEIL:				"ceil" >
|	< CTMC:				"ctmc" >
|	< CUMUL:			"C" >
|	< DOUBLE:			"double" >
|	< DTMC:				"dtmc" >
|	< ENDINIT:			"endinit" >
|	< ENDMODULE:		"endmodule" >
|	< ENDREWARDS:		"endrewards" >
|	< ENDSYSTEM:		"endsystem" >
|	< FALSE:			"false" >
|	< FLOOR:			"floor" >
|	< FORMULA:			"formula" >
|	< FUNC:				"func" >
|	< FUTURE:			"F" >
|	< GLOBAL:			"global" >
|	< GLOB:				"G" >
|	< INIT:				"init" >
|	< INST:				"I" >
|	< INT:				"int" >
|	< LABEL:			"label" >
|	< MAX:				"max" >
|	< MDP:				"mdp" >
|	< MIN:				"min" >
|	< MODULE:			"module" >
|	< NEXT:				"X" >
|	< NONDETERMINISTIC:	"nondeterministic" >
|	< PMAX:				"Pmax" >
|	< PMIN:				"Pmin" >
|	< P:				"P" >
|	< PROBABILISTIC:	"probabilistic" >
|	< PROB:				"prob" >
|	< RATE:				"rate" >
|	< REWARDS:			"rewards" >
|	< RMAX:				"Rmax" >
|	< RMIN:				"Rmin" >
|	< R:				"R" >
|	< S:				"S" >
|	< STOCHASTIC:		"stochastic" >
|	< SYSTEM:			"system" >
|	< TRUE:				"true" >
|	< UNTIL:			"U" >
	// punctuation, etc.
	// note that "NOT" must be the first item of punctuation in this list
	// (PrismSyntaxHighlighter relies on this fact)
|	< NOT:			"!" >
|	< AND:			"&" >
|	< OR:			"|" >
|	< IMPLIES:		"=>" >
|	< RARROW:		"->" >
|	< COLON:		":" >
|	< SEMICOLON:	";" >
|	< COMMA:		"," >
|	< DOTS:			".." >
|	< LPARENTH:		"(" >
|	< RPARENTH:		")" >
|	< LBRACKET: 	"[" >
|	< RBRACKET:		"]" >
|	< LBRACE:		"{" >
|	< RBRACE:		"}" >
|	< EQ:			"=" >
|	< NE:			"!=" >
|	< LT:			"<" >
|	< GT:			">" >
|	< LE:			"<=" >
|	< GE:			">=" >
|	< PLUS:			"+" >
|	< MINUS:		"-" >
|	< TIMES:		"*" >
|	< DIVIDE:		"/" >
|	< PRIME:		"'" >
|	< RENAME:		"<-" >
|	< QMARK:		"?" >
|	< DQUOTE:		"\"" >
	// regular expressions
|	< REG_INT:			(["1"-"9"](["0"-"9"])*)|("0") >
//|	< REG_DOUBLE:		<REG_INT>"."(["0"-"9"])+ >
|	< REG_DOUBLE:		(["0"-"9"])*(".")?(["0"-"9"])+(["e","E"](["-","+"])?(["0"-"9"])+)? >
|	< REG_IDENTPRIME:	["_","a"-"z","A"-"Z"](["_","a"-"z","A"-"Z","0"-"9"])*"'" >
|	< REG_IDENT:		["_","a"-"z","A"-"Z"](["_","a"-"z","A"-"Z","0"-"9"])* >
|	< PREPROC:			"#"(~["#"])*"#" >
}

//-----------------------------------------------------------------------------------
// top-level stuff
//-----------------------------------------------------------------------------------

void ModulesFileOrPropertiesFile() :
{
	Token t = null, ptr, ptr2;
}
{
	{ t = getToken(1); }
	( ModulesFile() | PropertiesFile() )
	{
		ptr = t;
		while (ptr != null) {
			if (ptr.specialToken != null) {
				ptr2 = ptr;
				while (ptr2.specialToken != null) ptr2 = ptr2.specialToken;
				while (ptr2 != null) { System.out.print(ptr2.image); ptr2 = ptr2.next; }
			}
			System.out.print(ptr.image);
			ptr = ptr.next;
		}
	}
}

// modules file

void ModulesFile() : {}
{
	( ( ( ModulesFileType() ) | FormulaDef() | LabelDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )* <EOF> )
}

// properties file

void PropertiesFile() : {}
{
	( ( /*FormulaDef() |*/ LabelDef() | ConstantDef() | PCTLFormula() { getToken(0).image += ";"; } 
 )* <EOF> )
}

// a single expression

void SingleExpression() : {}
{
	( Expression() <EOF> )
}

//-----------------------------------------------------------------------------------
// modules file stuff
//-----------------------------------------------------------------------------------

// keyword denoting module type (nondeterministic, probabilistic, ...)

void ModulesFileType() : {}
{
	( <PROBABILISTIC> | <NONDETERMINISTIC> | <STOCHASTIC> | <DTMC> | <MDP> | <CTMC> )
}

// formula definition

void FormulaDef() : {}
{
	( <FORMULA> Identifier() <EQ> Expression() <SEMICOLON> )
}

// label definition

void LabelDef() : {}
{
	( <LABEL> <DQUOTE> Identifier() <DQUOTE> <EQ> Expression() <SEMICOLON> )
}

// constant definition

void ConstantDef() : {}
{
	( <CONST> <INT> Identifier() (<EQ> Expression())? <SEMICOLON> )
	| ( <CONST> <DOUBLE> Identifier() (<EQ> Expression())? <SEMICOLON> )
	| ( <CONST> <BOOL> Identifier() (<EQ> Expression())? <SEMICOLON> )
	| ( <CONST> Identifier() (<EQ> Expression())? <SEMICOLON> )
	| ( ( <RATE> | <PROB> ) Identifier() (<EQ> Expression())? <SEMICOLON> )
}

// global variable declaration

void GlobalDecl() : {}
{
	( <GLOBAL> Declaration() )
}

// module definition

void Module() : {}
{
	( <MODULE> Identifier() ( Declaration() )* ( Command() )* <ENDMODULE> )
}

// variable declaration

void Declaration() : {}
{
	( Identifier() <COLON> <LBRACKET> Expression() <DOTS> Expression() <RBRACKET>
	( <INIT> Expression() )? <SEMICOLON> ) | ( Identifier() <COLON> <BOOL> ( <INIT> Expression() )? <SEMICOLON> )
}

// command definition

void Command() : {}
{
	( <LBRACKET> ( Identifier() )? <RBRACKET> Expression() <RARROW> Updates() <SEMICOLON> )
}

void Updates() : {}
{
	( Update() ) | ( ProbUpdate() ( <PLUS> ProbUpdate() )* )
}

void ProbUpdate() : {}
{
	( Expression() <COLON> Update() )
}

void Update() : {}
{
	( UpdateElement() ( <AND> UpdateElement() )* ) | ( <TRUE> )
}

void UpdateElement() :
{
	Token t1, t2;
}
{
	( <LPARENTH> IdentifierPrime() <EQ> Expression() <RPARENTH> ) | ( { t1=getToken(0); } IdentifierPrime() <EQ> Expression() { t2=getToken(0); } )
	{ insertTokenBeforeNext(t1, "("); t2.image += ")"; } 
}

// module definition (by renaming)

void RenamedModule() : {}
{
	( <MODULE> Identifier() <EQ> Identifier() <LBRACKET> Renames() <RBRACKET> <ENDMODULE> )
}

void Renames() : {}
{
	( Rename() ( <COMMA> Rename() )* )
}

void Rename() : {}
{
	((( Identifier() ) | ( <MIN> ) | ( <MAX> ) | ( <FLOOR> ) | ( <CEIL> ))
	<EQ>
	(( Identifier() ) | ( <MIN> ) | ( <MAX> ) | ( <FLOOR> ) | ( <CEIL> )))
}

// system composition definition

void SystemComp() : {}
{
	( <SYSTEM> SystemParallels() <ENDSYSTEM> )
}

// system definition component

void SystemParallels() : {}
{
	( SystemFullParallel() ) | ( SystemInterleaved() ) | ( SystemParallel() ) | ( SystemHideRename() )
}

// system definition component (full parallel)

void SystemFullParallel() : {}
{
	( SystemHideRename() ( <OR> <OR> SystemHideRename() )+ )
}

// system definition component (interleaved parallel)

void SystemInterleaved() : {}
{
	( SystemHideRename() ( <OR> <OR> <OR> SystemHideRename() )+ )
}

// system definition component (parallel over set of actions)

void SystemParallel() : {}
{
	( SystemHideRename() <OR> <LBRACKET> ( SystemAction() ( <COMMA> SystemAction() )* ) <RBRACKET> <OR> SystemHideRename() )
}

// system definition component (hiding and renaming)

void SystemHideRename() : {}
{
	( SystemAtomic() ( ( ( <DIVIDE> <LBRACE> ( SystemAction() ( <COMMA> SystemAction() )* ) <RBRACE> ) |
	( <LBRACE> SystemAction() <RENAME> SystemAction() ( <COMMA> SystemAction() <RENAME> SystemAction() )* <RBRACE> ) ) )* )
}

// system definition component (bottom level)

void SystemAtomic() : {}
{
	( SystemModule() ) | ( SystemBrackets() )
}

// system definition component (action identifier)

void SystemAction() : {}
{
	( Identifier() )
}

// system definition component (module identifier)

void SystemModule() : {}
{
	( Identifier() )
}

// system definition component (brackets)

void SystemBrackets() : {}
{
	( <LPARENTH> SystemParallels() <RPARENTH> )
}

// reward structure

void RewardStruct() : {}
{
	( ( <REWARDS> (<DQUOTE> Identifier() <DQUOTE>)? ( RewardStructItem() )* <ENDREWARDS> ) )
}

// single line (item) of state-based rewards structure

void RewardStructItem() : {}
{
	( ( <LBRACKET> ( Identifier() )? <RBRACKET> )? Expression() <COLON> Expression() <SEMICOLON> )
}

// multiple initial states

void Init() : {}
{
	( ( <INIT> Expression() <ENDINIT> ) )
}

//-----------------------------------------------------------------------------------
// properties file stuff
//-----------------------------------------------------------------------------------

// pctl formula

void PCTLFormula() : {}
{
	( PCTLImplies() )
}

void PCTLImplies() : {}
{
	( PCTLOr() ( <IMPLIES> PCTLOr() )? )
}

void PCTLOr() : {}
{
	( PCTLAnd() ( <OR> PCTLAnd() )* )
}

void PCTLAnd() : {}
{
	( PCTLNot() ( <AND> PCTLNot() )* )
}

void PCTLNot() : {}
{
	( (<NOT>)? PCTLProb() )
}

// pctl prob operator

void PCTLProb() : {}
{
	( (
	( <P> LtGt() Expression() ) |
	( <P> <EQ> <QMARK> ) |
	( <P> <MIN> <EQ> <QMARK> ) |
	( <P> <MAX> <EQ> <QMARK> ) |
	( <PMIN> <EQ> <QMARK> ) |
	( <PMAX> <EQ> <QMARK> ) )
	<LBRACKET>
	( PCTLProbNext() | PCTLProbBoundedUntil() | PCTLProbUntil() | PCTLProbBoundedFutureGlobal() | PCTLProbFutureGlobal() )
	( <LBRACE> PCTLFormula() <RBRACE>
	(( <LBRACE> <MIN> <RBRACE> ) | ( <LBRACE> <MAX> <RBRACE> ))*
	)? <RBRACKET> )
	| ( PCTLSS() )
}

// pctl next

void PCTLProbNext() : {}
{
	( <NEXT> PCTLFormula() )
}

// pctl bounded until

void PCTLProbBoundedUntil() : {}
{
	( PCTLFormula() <UNTIL> ((<LE> Expression()) | (<GE> Expression()) | (<LBRACKET> Expression() <COMMA> Expression() <RBRACKET>)) PCTLFormula() )
}

// pctl until (unbounded)

void PCTLProbUntil() : {}
{
	( PCTLFormula() <UNTIL> PCTLFormula() )
}

// pctl bounded future (eventually) or global

void PCTLProbBoundedFutureGlobal() : {}
{
	( (<FUTURE>|<GLOB>) ((<LE> Expression()) | (<GE> Expression()) | (<LBRACKET> Expression() <COMMA> Expression() <RBRACKET>)) PCTLFormula() )
}

// pctl future (eventually) or globally

void PCTLProbFutureGlobal() : {}
{
	( (<FUTURE>|<GLOB>) PCTLFormula() )
}

// pctl steady state (actually only csl - not pctl at all)

void PCTLSS() : {}
{
	( ( ( ( <S> LtGt() Expression() ) | ( <S> <EQ> <QMARK> ) ) <LBRACKET> PCTLFormula() ( <LBRACE> PCTLFormula() <RBRACE> )? <RBRACKET> ) ) | ( PCTLReward() )
}

// pctl reward operator

void PCTLReward() : {}
{
	( ( ( <R>
	( <LBRACE> ((<DQUOTE> Identifier() <DQUOTE>) | (Expression())) <RBRACE> )?
	(( LtGt() Expression() ) |
	( <EQ> <QMARK> ) |
	( <MIN> <EQ> <QMARK> ) |
	( <MAX> <EQ> <QMARK> ))) |
	( <RMIN> <EQ> <QMARK> ) |
	( <RMAX> <EQ> <QMARK> ) )
	<LBRACKET>
	( PCTLRewardCumul() | PCTLRewardInst() | PCTLRewardReach() | PCTLRewardSS() )
	( <LBRACE> PCTLFormula() <RBRACE>
	(( <LBRACE> <MIN> <RBRACE> ) | ( <LBRACE> <MAX> <RBRACE> ))*
	)? <RBRACKET> )
	| ( PCTLInit() )
}

// cumulative reward

void PCTLRewardCumul() : {}
{
	( <CUMUL> <LE> Expression() )
}

// instantaneous reward

void PCTLRewardInst() : {}
{
	( <INST> <EQ> Expression() )
}

// reach reward

void PCTLRewardReach() : {}
{
	( <FUTURE> PCTLFormula() )
}

// steady-state reward

void PCTLRewardSS() : {}
{
	( <S> )
}

// init

void PCTLInit() : {}
{
	( <DQUOTE> <INIT> <DQUOTE> ) | ( PCTLLabel() )
}

// label

void PCTLLabel() : {}
{
	( <DQUOTE> Identifier() <DQUOTE> ) | ( PCTLBrackets() )
}

// brackets

void PCTLBrackets() : {}
{
	( <LPARENTH> PCTLFormula() <RPARENTH> ) | ( PCTLExpression() )
}

// pctl expression

void PCTLExpression() : {}
{
	( ExpressionRelOpRange() )
}

//-----------------------------------------------------------------------------------
// expression stuff
//-----------------------------------------------------------------------------------

// expression

void Expression() : {}
{
	( ExpressionITE() )
}

// expression (if-then-else)

void ExpressionITE() : {}
{
	( ExpressionOr() <QMARK> ExpressionOr() <COLON> ExpressionITE() ) | ( ExpressionOr() )
}

// expression (or)

void ExpressionOr() : {}
{
	( ExpressionAnd() ( <OR> ExpressionOr() )? )
}

// expression (and)

void ExpressionAnd() : {}
{
	( ExpressionNot() ( <AND> ExpressionNot() )* )
}

// expression (not)

void ExpressionNot() : {}
{
	( (<NOT>)? ExpressionRelOpRange() )
}

// expression: relational operators/ranges

void ExpressionRelOpRange() :
{
	Token t0, t1, t2, ptr;
	String relOp = null;
	boolean up, thisIsARange = false;
	String lhs = null, s1 = null, s2 = null, newExpr = "";
}
{
	( ExpressionPlusMinus() relOp=LtGt() ExpressionPlusMinus() ) | (
	{ t0=getToken(0); t1=getToken(1); }
	ExpressionPlusMinus()
	{ t2=getToken(1); ptr = t1; lhs = ""; while (ptr != t2) { lhs += ptr.image; ptr = ptr.next; } }
	relOp=EqNeq() (
	{ newExpr = (relOp.equals("!="))?"!(":"("; }
	{ t1=getToken(1); }
	ExpressionPlusMinus()
	{ t2=getToken(1); ptr = t1; s1 = ""; while (ptr != t2) { s1 += ptr.image; ptr = ptr.next; } up = false; }
	( <DOTS>
	{ thisIsARange = true; t1=getToken(1); }
	ExpressionPlusMinus()
	{ t2=getToken(1); ptr = t1; s2 = ""; while (ptr != t2) { s2 += ptr.image; ptr = ptr.next; } up = true; }
	)?
	{ if (up) newExpr += "("+lhs+")>=("+s1+")&("+lhs+")<=("+s2+")"; else newExpr += "("+lhs+")=("+s1+")"; }
	) ( ( <COMMA>
	{ thisIsARange = true; t1=getToken(1); }
	ExpressionPlusMinus()
	{ t2=getToken(1); ptr = t1; s1 = ""; while (ptr != t2) { s1 += ptr.image; ptr = ptr.next; } up = false; }
	( <DOTS>
	{ t1=getToken(1); }
	ExpressionPlusMinus()
	{ t2=getToken(1); ptr = t1; s2 = ""; while (ptr != t2) { s2 += ptr.image; ptr = ptr.next; } up = true; }
	)?
	{ if (up) newExpr += "|("+lhs+")>=("+s1+")&("+lhs+")<=("+s2+")"; else newExpr += "|("+lhs+")=("+s1+")"; }
	) )*
	{ newExpr += ")"; if (thisIsARange) { t0.next = getToken(1); insertTokenBeforeNext(t0, newExpr); } }
	) | ( ExpressionPlusMinus() )
}

// expression: plus/minus - binary, left associative

void ExpressionPlusMinus() : {}
{
	( ExpressionTimesDivide() ( ( <PLUS> | <MINUS> ) ExpressionTimesDivide() )* )
}

// expression: times/divide - binary, left associative

void ExpressionTimesDivide() : {}
{
	( ExpressionUnaryMinus() ( ( <TIMES> | <DIVIDE> ) ExpressionUnaryMinus() )* )
}

// expression: unary minus (right associative)

void ExpressionUnaryMinus() : {}
{
	( <MINUS> ExpressionFunc() ) | ( ExpressionFunc() )
}

// expression (function)

void ExpressionFunc() : {}
{
	((((( <MIN> ) | ( <MAX> ) | ( <FLOOR> ) | ( <CEIL> )) <LPARENTH> ) | ( <FUNC> <LPARENTH> (( Identifier() ) | ( <MIN> ) | ( <MAX> ) | ( <FLOOR> ) | ( <CEIL> )) <COMMA> )) Expression() ( <COMMA> Expression() )* <RPARENTH> ) | ( ExpressionIdent() )
}

// expression (identifier)

void ExpressionIdent() : {}
{
	( Identifier() ) | ( ExpressionLiteral() )
}

// expression (literal)

void ExpressionLiteral() : {}
{
	( Int() ) | ( Double() ) | ( <TRUE> ) | ( <FALSE> ) | ( ExpressionBrackets() )
}

// expression (brackets)

void ExpressionBrackets() : {}
{
	( <LPARENTH> Expression() <RPARENTH> )
}

//-----------------------------------------------------------------------------------
// miscellaneous stuff
//-----------------------------------------------------------------------------------

// identifier

String Identifier() :
{
}
{
	<REG_IDENT>
	{
		return token.image;
	}
}

// identifier with a prime

String IdentifierPrime() :
{
}
{
	<REG_IDENTPRIME>
	{
		// remove prime and return
		String s = token.image;
		s = s.substring(0, s.length()-1);
		return s;
	}
}

// one of the relational operators: =, !=

String EqNeq() :
{
}
{
	( <EQ> | <NE> )
	{
		return token.image;
	}
}

// one of the relational operators: >, <, >=, <=

String LtGt() :
{
}
{
	( <GT> | <LT> | <GE> | <LE> )
	{
		return token.image;
	}
}

// integer

int Int() :
{
	int i;
}
{
	// basic int
	<REG_INT>
	{
		i = Integer.parseInt(token.image);
		return i;
	}
}

// double

String Double() :
{
}
{
	<REG_DOUBLE>
	{
		//return Double.valueOf(token.image).doubleValue();
		return token.image;
	}
}

//------------------------------------------------------------------------------