You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
1603 lines
42 KiB
1603 lines
42 KiB
//==============================================================================
|
|
//
|
|
// 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
|
|
//
|
|
//==============================================================================
|
|
|
|
options {
|
|
LOOKAHEAD = 1;
|
|
}
|
|
|
|
PARSER_BEGIN(PrismParser)
|
|
|
|
package parser;
|
|
|
|
import java.io.*;
|
|
import java.util.ArrayList;
|
|
|
|
import parser.ast.*;
|
|
import prism.PrismLangException;
|
|
|
|
public class PrismParser
|
|
{
|
|
// The modules file associated with properties file being parsed
|
|
private static ModulesFile modulesFile;
|
|
|
|
// List of keyword strings
|
|
private static ArrayList<String> keywordList = new ArrayList<String>();
|
|
|
|
// Flag indicating whether we are parsing a PRISM property (or just a PRISM expression);
|
|
private static boolean parsingProperty = false;
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Main method for testing purposes
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
public static void main(String[] args)
|
|
{
|
|
PrismParser p = null;
|
|
InputStream str = null;
|
|
String src = null;
|
|
|
|
try {
|
|
if (args.length == 0) {
|
|
System.out.println("Usage: java parser.PrismParser <switch> [<file>]");
|
|
System.out.println("Where: <switch> = -modulesfile or -mf");
|
|
System.out.println(" -propertiesfile or -pf");
|
|
System.out.println(" -expression or -e");
|
|
System.exit(1);
|
|
}
|
|
|
|
p = new PrismParser();
|
|
str = (args.length > 1) ? new FileInputStream(args[1]) : System.in;
|
|
src = (args.length > 1) ? "file "+args[1] : "stdin";
|
|
System.out.println("Reading from "+src+"...\n");
|
|
|
|
if (args[0].equals("-modulesfile") || args[0].equals("-mf")) {
|
|
ModulesFile mf = p.parseModulesFile(str);
|
|
System.out.print("Modules file:\n=============\n\n" + mf);
|
|
System.out.print("\nTree:\n=====\n" + mf.toTreeString());
|
|
mf.tidyUp();
|
|
System.out.print("\nAnd after expansion:\n====================\n\n" +mf);
|
|
}
|
|
else if (args[0].equals("-propertiesfile") || args[0].equals("-pf")) {
|
|
PropertiesFile pf = p.parsePropertiesFile(new ModulesFile(), str);
|
|
System.out.print("Properties file:\n================\n\n" + pf);
|
|
System.out.print("\nTree:\n=====\n" + pf.toTreeString());
|
|
pf.tidyUp();
|
|
System.out.print("\nAnd after expansion:\n====================\n\n" + pf);
|
|
}
|
|
else if (args[0].equals("-expression") || args[0].equals("-e")) {
|
|
Expression expr = p.parseSingleExpression(str);
|
|
System.out.println("Expression: " + expr.toString());
|
|
System.out.print("Tree:\n=====\n" + expr.toTreeString());
|
|
expr.typeCheck();
|
|
expr.semanticCheck();
|
|
System.out.println("Type: " + Expression.getTypeString(expr.getType()));
|
|
System.out.println("Eval: " + expr.evaluate(null, null));
|
|
} else {
|
|
System.out.println("Unknown switch"); System.exit(1);
|
|
}
|
|
}
|
|
catch (PrismLangException e) {
|
|
System.out.println("Error in "+src+": " + e.getMessage()+"."); System.exit(1);
|
|
}
|
|
catch (FileNotFoundException e) {
|
|
System.out.println(e); System.exit(1);
|
|
}
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Methods called by Prism
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Constructor
|
|
|
|
public PrismParser()
|
|
{
|
|
// Call default constructor
|
|
this(System.in);
|
|
// Build a list of strings for keywords
|
|
keywordList.clear();
|
|
for (int i = PrismParserConstants.COMMENT+1; i < PrismParserConstants.NOT; i++) {
|
|
keywordList.add(PrismParserConstants.tokenImage[i].replaceAll("\"", ""));
|
|
}
|
|
}
|
|
|
|
// Parse modules file
|
|
|
|
public ModulesFile parseModulesFile(InputStream str) throws PrismLangException { return parseModulesFile(str, 0); }
|
|
|
|
public ModulesFile parseModulesFile(InputStream str, int typeOverride) throws PrismLangException
|
|
{
|
|
ModulesFile mf = null;
|
|
|
|
// (Re)start parser
|
|
ReInit(str);
|
|
// Parse
|
|
try {
|
|
mf = ModulesFile();
|
|
}
|
|
catch (ParseException e) {
|
|
ExpressionIdent tmp = new ExpressionIdent(e.currentToken.next.image);
|
|
tmp.setPosition(e.currentToken.next);
|
|
throw new PrismLangException("Syntax error", tmp);
|
|
}
|
|
// Override type of model if requested
|
|
if (typeOverride != 0) {
|
|
mf.setType(typeOverride);
|
|
}
|
|
|
|
return mf;
|
|
}
|
|
|
|
// Parse properties file (pass ModulesFile in to get at its constants)
|
|
|
|
public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str) throws PrismLangException
|
|
{ return parsePropertiesFile(mf, str, false); }
|
|
|
|
public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str, boolean strict) throws PrismLangException
|
|
{
|
|
PropertiesFile pf = null;
|
|
|
|
// (Re)start parser
|
|
ReInit(str);
|
|
modulesFile = mf;
|
|
// Parse
|
|
try {
|
|
pf = strict ? PropertiesFile() : PropertiesFileSemicolonless();
|
|
}
|
|
catch (ParseException e) {
|
|
ExpressionIdent tmp = new ExpressionIdent(e.currentToken.next.image);
|
|
tmp.setPosition(e.currentToken.next);
|
|
throw new PrismLangException("Syntax error", tmp);
|
|
}
|
|
|
|
return pf;
|
|
}
|
|
|
|
// Parse a single expression
|
|
|
|
public Expression parseSingleExpression(InputStream str) throws PrismLangException
|
|
{
|
|
Expression expr = null;
|
|
|
|
// (Re)start parser
|
|
ReInit(str);
|
|
// Parse
|
|
try {
|
|
expr = SingleExpression();
|
|
}
|
|
catch (ParseException e) {
|
|
ExpressionIdent tmp = new ExpressionIdent(e.currentToken.next.image);
|
|
tmp.setPosition(e.currentToken.next);
|
|
throw new PrismLangException("Syntax error", tmp);
|
|
}
|
|
return expr;
|
|
}
|
|
|
|
// Parse a for loop
|
|
|
|
public ForLoop parseForLoop(InputStream str) throws PrismLangException
|
|
{
|
|
ForLoop fl = null;
|
|
|
|
// (Re)start parser
|
|
ReInit(str);
|
|
// Parse
|
|
try {
|
|
fl = ForLoop();
|
|
}
|
|
catch (ParseException e) {
|
|
ExpressionIdent tmp = new ExpressionIdent(e.currentToken.next.image);
|
|
tmp.setPosition(e.currentToken.next);
|
|
throw new PrismLangException("Syntax error", tmp);
|
|
}
|
|
return fl;
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Some utility methods
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Get comment block (including white space)
|
|
// preceding a token and remove "//" characters
|
|
|
|
public static String getPrecedingCommentBlock(Token firstToken)
|
|
{
|
|
String comment = "", s;
|
|
Token t = firstToken;
|
|
|
|
// extract any comment from the previous lines of the file
|
|
if (t.specialToken != null) {
|
|
// trace back thru special tokens
|
|
t = t.specialToken;
|
|
while (t.specialToken != null) t = t.specialToken;
|
|
// ignore initial white space
|
|
while (t != null && t.kind == PrismParserConstants.WHITESPACE) t = t.next;
|
|
// concatenate special tokens
|
|
while (t != null) {
|
|
s = t.image;
|
|
// strip any nasty carriage returns
|
|
s = s.replaceAll("\r", "");
|
|
// remove "//" and preceding/subsequent spaces/tabs from comments
|
|
if (t.kind == PrismParserConstants.COMMENT) {
|
|
while (comment.length() > 0 && (""+comment.charAt(comment.length()-1)).matches("[ \t]"))
|
|
comment = comment.substring(0,comment.length()-1);
|
|
s = s.substring(2);
|
|
s = s.replaceFirst("[ \t]*", "");
|
|
}
|
|
comment += s;
|
|
t = t.next;
|
|
}
|
|
}
|
|
// remove final new line (if present)
|
|
if (comment.length() > 0 && (comment.charAt(comment.length()-1) == '\n'))
|
|
comment = comment.substring(0,comment.length()-1);
|
|
|
|
return comment;
|
|
}
|
|
|
|
// Add "//"s into comment block
|
|
|
|
public static String slashCommentBlock(String comment)
|
|
{
|
|
int i;
|
|
String s, res = "";
|
|
// break into lines
|
|
while ((i = comment.indexOf("\n")) != -1) {
|
|
s = comment.substring(0, i);
|
|
comment = comment.substring(i+1);
|
|
// add "//" to non-empty lines
|
|
if (s.trim().length()>0) res += "// " + s;
|
|
res += "\n";
|
|
}
|
|
// deal with any trailing characters (with no new line ending them)
|
|
if (comment.trim().length()>0) res += "// " + comment + "\n";
|
|
return res;
|
|
}
|
|
|
|
// Test a string to see if it is a PRISM language keyword
|
|
|
|
public static boolean isKeyword(String s)
|
|
{
|
|
return keywordList.contains(s);
|
|
}
|
|
|
|
/**
|
|
* Set the tab size used by the lexer/parser.
|
|
*/
|
|
public void setTabSize(int size)
|
|
{
|
|
SimpleCharStream.setTabSize(size);
|
|
}
|
|
|
|
/**
|
|
* Get the tab size used by the lexer/parser.
|
|
*/
|
|
public int getTabSize() {
|
|
return SimpleCharStream.getTabSize(0);
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// A few classes for temporary storage of bits of the AST
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
static class TimeBound { public Expression lBound = null; public Expression uBound = null; }
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
PARSER_END(PrismParser)
|
|
|
|
// Token definitions follow
|
|
// Note that PrismSyntaxHighlighter makes assumptions about the ordering of these
|
|
|
|
// 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" >
|
|
| < CTMC: "ctmc" >
|
|
| < C: "C" >
|
|
| < DOUBLE: "double" >
|
|
| < DTMC: "dtmc" >
|
|
| < ENDINIT: "endinit" >
|
|
| < ENDMODULE: "endmodule" >
|
|
| < ENDREWARDS: "endrewards" >
|
|
| < ENDSYSTEM: "endsystem" >
|
|
| < FALSE: "false" >
|
|
| < FORMULA: "formula" >
|
|
| < FUNC: "func" >
|
|
| < F: "F" >
|
|
| < GLOBAL: "global" >
|
|
| < G: "G" >
|
|
| < INIT: "init" >
|
|
| < I: "I" >
|
|
| < INT: "int" >
|
|
| < LABEL: "label" >
|
|
| < MAX: "max" >
|
|
| < MDP: "mdp" >
|
|
| < MIN: "min" >
|
|
| < MODULE: "module" >
|
|
| < X: "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" >
|
|
| < U: "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: (["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: "#"(~["#"])*"#" >
|
|
// Special catch-all token for lexical errors
|
|
// (this allows us to throw our usual exceptions in this case)
|
|
| < LEXICAL_ERROR: ~[] >
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Top-level productions
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Modules file
|
|
|
|
ModulesFile ModulesFile() throws PrismLangException :
|
|
{
|
|
int type = 0;
|
|
int typeCount = 0;
|
|
Token typeDupe = null;
|
|
Declaration global;
|
|
Module m = null;
|
|
RenamedModule rm = null;
|
|
RewardStruct rs = null;
|
|
Expression init = null;
|
|
int initCount = 0;
|
|
Expression initDupe = null;
|
|
SystemDefn sys = null;
|
|
int sysCount = 0;
|
|
SystemDefn sysDupe = null;
|
|
ModulesFile mf = new ModulesFile();
|
|
Token begin = null;
|
|
parsingProperty = false;
|
|
}
|
|
{
|
|
( { begin = getToken(1); }
|
|
// Model type
|
|
( type=ModulesFileType() { typeCount++; if (typeCount == 2) typeDupe = getToken(0); } ) |
|
|
// Formula/label/constant definition
|
|
FormulaDef(mf.getFormulaList()) | LabelDef(mf.getLabelList()) | ConstantDef(mf.getConstantList()) |
|
|
// Global variable
|
|
global = GlobalDecl() { mf.addGlobal(global); } |
|
|
// Renamed module
|
|
LOOKAHEAD(<MODULE> Identifier() <EQ>) rm = RenamedModule() { mf.addRenamedModule(rm); } |
|
|
// Module
|
|
m = Module() { mf.addModule(m); } |
|
|
// Reward structure
|
|
rs = RewardStruct() { mf.addRewardStruct(rs); } |
|
|
// Initial states ("init...endinit" construct)
|
|
init = Init() { mf.setInitialStates(init); initCount++; if (initCount == 2) initDupe = init; } |
|
|
// System definition ("system...endsystem" construct)
|
|
sys = SystemEndsystem() { mf.setSystemDefn(sys); sysCount++; if (sysCount == 2) sysDupe = sys; }
|
|
)* <EOF>
|
|
{
|
|
// Check for multiple instances of some items
|
|
if (typeDupe != null) {
|
|
ExpressionIdent tmp = new ExpressionIdent(typeDupe.image);
|
|
tmp.setPosition(typeDupe);
|
|
throw new PrismLangException("There were multiple model type declarations", tmp);
|
|
}
|
|
if (initDupe != null) {
|
|
throw new PrismLangException("There were multiple init...endinit constructs", initDupe);
|
|
}
|
|
if (sysDupe != null) {
|
|
throw new PrismLangException("There were multiple system...endsystem constructs", sysDupe);
|
|
}
|
|
|
|
// Set type (default is MDP)
|
|
switch (type) {
|
|
case PROBABILISTIC:
|
|
case DTMC:
|
|
mf.setType(ModulesFile.PROBABILISTIC); break;
|
|
case NONDETERMINISTIC:
|
|
case MDP:
|
|
mf.setType(ModulesFile.NONDETERMINISTIC); break;
|
|
case STOCHASTIC:
|
|
case CTMC:
|
|
mf.setType(ModulesFile.STOCHASTIC); break;
|
|
default : mf.setType(ModulesFile.NONDETERMINISTIC); break;
|
|
}
|
|
|
|
// Return completed ModulesFile object
|
|
mf.setPosition(begin != null? begin: getToken(0), getToken(0));
|
|
return mf;
|
|
}
|
|
}
|
|
|
|
// Properties file
|
|
|
|
PropertiesFile PropertiesFile() throws PrismLangException :
|
|
{
|
|
PropertiesFile pf = new PropertiesFile(modulesFile);
|
|
Expression expr;
|
|
Token begin = null, t = null;
|
|
parsingProperty = false;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
(
|
|
// Semi-colon terminated property
|
|
( { t = getToken(1); } expr = Property() { pf.addProperty(expr, getPrecedingCommentBlock(t)); } (<SEMICOLON>)+ )
|
|
|
|
|
// Label/constant definition
|
|
( LabelDef(pf.getLabelList()) ) | ( ConstantDef(pf.getConstantList()) )
|
|
)* <EOF>
|
|
{ pf.setPosition(begin, getToken(0)); return pf; }
|
|
}
|
|
|
|
// Properties file with optional semicolons - beware of potential ambiguities
|
|
|
|
PropertiesFile PropertiesFileSemicolonless() throws PrismLangException :
|
|
{
|
|
PropertiesFile pf = new PropertiesFile(modulesFile);
|
|
Expression expr;
|
|
Token begin = null, t = null;
|
|
parsingProperty = false;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
(
|
|
// Semi-colon terminated property
|
|
( { t = getToken(1); } expr = Property() (<SEMICOLON>)* { pf.addProperty(expr, getPrecedingCommentBlock(t)); } )
|
|
|
|
|
// Label/constant definition
|
|
( LabelDef(pf.getLabelList()) ) | ( ConstantDef(pf.getConstantList()) )
|
|
)* <EOF>
|
|
{ pf.setPosition(begin, getToken(0)); return pf; }
|
|
}
|
|
|
|
// Property expression (used above)
|
|
|
|
Expression Property() :
|
|
{
|
|
Expression expr;
|
|
parsingProperty = true;
|
|
}
|
|
{
|
|
expr = Expression()
|
|
{
|
|
parsingProperty = false;
|
|
return expr;
|
|
}
|
|
}
|
|
|
|
// A single expression
|
|
|
|
Expression SingleExpression() :
|
|
{
|
|
Expression ret;
|
|
parsingProperty = false;
|
|
}
|
|
{
|
|
( ret = Expression() <EOF> ) { return ret; }
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Modules file stuff (a few bits of which are reused for property files)
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Keyword denoting model type
|
|
|
|
int ModulesFileType() :
|
|
{
|
|
}
|
|
{
|
|
( <DTMC>|<PROBABILISTIC> | <MDP>|<NONDETERMINISTIC> | <CTMC>|<STOCHASTIC> )
|
|
{ return getToken(0).kind; }
|
|
}
|
|
|
|
// Formula definition
|
|
|
|
void FormulaDef(FormulaList formulaList) :
|
|
{
|
|
Expression name = null, expr = null;
|
|
}
|
|
{
|
|
( <FORMULA> name = ExpressionIdent() <EQ> expr = Expression() <SEMICOLON> )
|
|
{ formulaList.addFormula((ExpressionIdent)name, expr); }
|
|
}
|
|
|
|
// Label definition
|
|
|
|
void LabelDef(LabelList labelList) throws PrismLangException :
|
|
{
|
|
Expression name = null, expr = null;
|
|
}
|
|
{
|
|
LOOKAHEAD(<LABEL> <DQUOTE>) <LABEL> ( <DQUOTE> name = ExpressionIdent() <DQUOTE> <EQ> expr = Expression() <SEMICOLON> )
|
|
{ labelList.addLabel((ExpressionIdent)name, expr); }
|
|
// Error handling
|
|
| LOOKAHEAD(<LABEL>) ( <LABEL> name = ExpressionIdent() ) { throw new PrismLangException("Label names must be enclosed in double-quotes", name); }
|
|
}
|
|
|
|
// Constant definition
|
|
|
|
void ConstantDef(ConstantList constantList) :
|
|
{
|
|
int type = Expression.INT;
|
|
Expression name = null, expr = null;
|
|
}
|
|
{
|
|
// Constant (allow omission of "int" and use of "rate"/"prob" for backwards compatability)
|
|
(( <CONST> ( <INT> { type=Expression.INT; } | <DOUBLE> { type=Expression.DOUBLE; } | <BOOL> { type=Expression.BOOLEAN; } )? )
|
|
| (<RATE> | <PROB> ) { type=Expression.DOUBLE; } )
|
|
// Name and (optional) initial value
|
|
name = ExpressionIdent()
|
|
( <EQ> expr = Expression() )? <SEMICOLON>
|
|
{ constantList.addConstant((ExpressionIdent)name, expr, type); }
|
|
}
|
|
|
|
// Global variable declaration
|
|
|
|
Declaration GlobalDecl() :
|
|
{
|
|
Declaration decl = null;
|
|
}
|
|
{
|
|
( <GLOBAL> decl = Declaration() )
|
|
{ return decl; }
|
|
}
|
|
|
|
// Variable declaration
|
|
|
|
Declaration Declaration() :
|
|
{
|
|
String name = null;
|
|
Expression low = null, high = null, init = null;
|
|
Declaration decl;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
( { begin = getToken(1);} name = Identifier() <COLON>
|
|
// Integer-range variable declaration
|
|
(( <LBRACKET> low = Expression() <DOTS> high = Expression() <RBRACKET> ( <INIT> init = Expression() )? <SEMICOLON>
|
|
{ decl = new Declaration(name, low, high, init); } )
|
|
// Boolean variable declaration
|
|
| ( <BOOL> ( <INIT> init = Expression() )? <SEMICOLON> { return new Declaration(name, init); } )))
|
|
{ decl.setPosition(begin, getToken(0)); return decl; }
|
|
}
|
|
|
|
// Module
|
|
|
|
Module Module() :
|
|
{
|
|
String name = null;
|
|
Declaration var = null;
|
|
Command comm = null;
|
|
Module module = null;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
begin = <MODULE> name = Identifier() { module = new Module(name); }
|
|
( var = Declaration() { module.addDeclaration(var); } )*
|
|
( comm = Command() { module.addCommand(comm); } )*
|
|
<ENDMODULE>
|
|
{ module.setPosition(begin, getToken(0)); return module; }
|
|
}
|
|
|
|
// Command
|
|
|
|
Command Command() :
|
|
{
|
|
String synch = null;
|
|
Expression guard = null;
|
|
Updates updates = null;
|
|
Command comm = new Command();
|
|
Token begin = null;
|
|
}
|
|
{
|
|
// Synchronisation action-label
|
|
begin = <LBRACKET> ( synch = Identifier() { comm.setSynch(synch); } )? <RBRACKET>
|
|
// Guard/updates
|
|
guard = Expression() { comm.setGuard(guard); } <RARROW> updates = Updates() { comm.setUpdates(updates); } <SEMICOLON>
|
|
{ comm.setPosition(begin, getToken(0)); return comm; }
|
|
}
|
|
|
|
// Updates
|
|
|
|
Updates Updates() :
|
|
{
|
|
Expression prob;
|
|
Update update;
|
|
Updates updates = new Updates();
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
(
|
|
// Single update with probability 1
|
|
LOOKAHEAD(Update()) update = Update()
|
|
{ updates.addUpdate(null, update); }
|
|
|
|
|
// Several probabilistic updates
|
|
( prob = Expression() <COLON> update = Update() { updates.addUpdate(prob, update); }
|
|
( <PLUS> prob = Expression() <COLON> update = Update() { updates.addUpdate(prob, update); } )* )
|
|
)
|
|
{ updates.setPosition(begin, getToken(0)); return updates; }
|
|
}
|
|
|
|
Update Update() :
|
|
{
|
|
Update update = new Update();
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
// Conjunction of update elements
|
|
(( UpdateElement(update) ( <AND> UpdateElement(update) )* )
|
|
// Empty conjunction: true
|
|
| <TRUE> )
|
|
{ update.setPosition(begin, getToken(0)); return update; }
|
|
}
|
|
|
|
void UpdateElement(Update update) :
|
|
{
|
|
ExpressionIdent var = null;
|
|
Expression expr = null;
|
|
}
|
|
{
|
|
<LPARENTH> var = IdentifierPrime() <EQ> expr = Expression() <RPARENTH> { update.addElement(var, expr); }
|
|
}
|
|
|
|
// Module renaming
|
|
|
|
RenamedModule RenamedModule() :
|
|
{
|
|
String name = null, base = null;
|
|
RenamedModule rm = null;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
begin = <MODULE> name = Identifier() <EQ> base = Identifier() { rm = new RenamedModule(name, base); }
|
|
<LBRACKET> Rename(rm) ( <COMMA> Rename(rm) )* <RBRACKET> <ENDMODULE>
|
|
{ rm.setPosition(begin, getToken(0)); return rm; }
|
|
}
|
|
|
|
void Rename(RenamedModule rm) :
|
|
{
|
|
String id1 = null, id2 = null;
|
|
}
|
|
{
|
|
// NB: have to explicitly include keywords for functions because they can be renamed
|
|
(( id1=Identifier() | <MIN> { id1="min"; } | <MAX> { id1="max"; } )
|
|
<EQ>
|
|
( id2=Identifier() | <MIN> { id2="min"; } | <MAX> { id2="max"; } ))
|
|
{
|
|
rm.addRename(id1, id2);
|
|
}
|
|
}
|
|
|
|
// Reward structure
|
|
|
|
RewardStruct RewardStruct() :
|
|
{
|
|
String name = null, s = null;
|
|
Expression guard = null, value = null;
|
|
RewardStruct rs = new RewardStruct();
|
|
RewardStructItem rsi;
|
|
Token begin = null, begin2 = null;
|
|
}
|
|
{
|
|
begin = <REWARDS>
|
|
// Optional name (lookahead required so not misdetected as an ExpressionLabel)
|
|
( LOOKAHEAD(<DQUOTE>) <DQUOTE> name = Identifier() <DQUOTE> { rs.setName(name); } )?
|
|
// Reward structure items
|
|
( { begin2 = getToken(1); } ( <LBRACKET> { s = ""; } ( s=Identifier() )? <RBRACKET> )? guard = Expression() <COLON> value = Expression() <SEMICOLON>
|
|
{ rsi = new RewardStructItem(s, guard, value); rsi.setPosition(begin2, getToken(0)); rs.addItem(rsi); } )*
|
|
<ENDREWARDS>
|
|
{ rs.setPosition(begin, getToken(0)); return rs; }
|
|
}
|
|
|
|
// Initial states ("init...endinit" construct)
|
|
|
|
Expression Init() :
|
|
{
|
|
Expression expr = null;
|
|
}
|
|
{
|
|
<INIT> expr = Expression() <ENDINIT> { return expr; }
|
|
}
|
|
|
|
// System definition ("system...endsystem" construct)
|
|
|
|
SystemDefn SystemEndsystem() :
|
|
{
|
|
SystemDefn ret;
|
|
}
|
|
{
|
|
<SYSTEM> ( ret = SystemDefn() ) <ENDSYSTEM>
|
|
{ return ret; }
|
|
}
|
|
|
|
// System definition component
|
|
|
|
SystemDefn SystemDefn() :
|
|
{
|
|
SystemDefn ret;
|
|
}
|
|
{
|
|
ret = SystemFullParallel()
|
|
{ return ret; }
|
|
}
|
|
|
|
// System definition component (full parallel)
|
|
|
|
SystemDefn SystemFullParallel() :
|
|
{
|
|
SystemDefn sys1 = null, sys2 = null;
|
|
SystemFullParallel par = null;
|
|
Token begin;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
sys1 = SystemInterleaved()
|
|
( { par = new SystemFullParallel(); par.addOperand(sys1); } ( LOOKAHEAD(<OR> <OR>) <OR> <OR> sys2 = SystemParallel() { par.addOperand(sys2); } )* )
|
|
{
|
|
if (par==null) {
|
|
return sys1;
|
|
}
|
|
else {
|
|
par.setPosition(begin, getToken(0));
|
|
return par;
|
|
}
|
|
}
|
|
}
|
|
|
|
// System definition component (interleaved parallel)
|
|
|
|
SystemDefn SystemInterleaved() :
|
|
{
|
|
SystemDefn sys1 = null, sys2 = null;
|
|
SystemInterleaved par = null;
|
|
Token begin;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
sys1 = SystemParallel()
|
|
( { par = new SystemInterleaved(); par.addOperand(sys1); } ( LOOKAHEAD(<OR> <OR> <OR>) <OR> <OR> <OR> sys2 = SystemFullParallel() { par.addOperand(sys2); } )* )
|
|
{
|
|
if (par==null) {
|
|
return sys1;
|
|
}
|
|
else {
|
|
par.setPosition(begin, getToken(0));
|
|
return par;
|
|
}
|
|
}
|
|
}
|
|
|
|
// System definition component (parallel over set of actions)
|
|
|
|
SystemDefn SystemParallel() :
|
|
{
|
|
SystemDefn sys1 = null, sys2 = null;
|
|
SystemParallel par = null;
|
|
String s;
|
|
Token begin;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
sys1 = SystemHideRename()
|
|
( LOOKAHEAD(<OR> <LBRACKET>) { par = new SystemParallel(); par.setOperand1(sys1); } <OR>
|
|
<LBRACKET> ( s = Identifier() { par.addAction(s); } ( <COMMA> s = Identifier() { par.addAction(s); } )* ) <RBRACKET>
|
|
<OR> sys2 = SystemHideRename() { par.setOperand2(sys2); }
|
|
)?
|
|
{
|
|
if (par==null) {
|
|
return sys1;
|
|
}
|
|
else {
|
|
par.setPosition(begin, getToken(0));
|
|
return par;
|
|
}
|
|
}
|
|
}
|
|
|
|
// System definition component (hiding and renaming)
|
|
|
|
SystemDefn SystemHideRename() :
|
|
{
|
|
SystemDefn sys = null;
|
|
SystemHide hide = null;
|
|
SystemRename rename = null;
|
|
String s1 = null, s2 = null;
|
|
Token begin;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
( sys = SystemAtomic() (
|
|
// Hiding
|
|
(
|
|
{ hide = new SystemHide(sys); }
|
|
<DIVIDE> <LBRACE> ( s1 = Identifier() { hide.addAction(s1); } ( <COMMA> s1 = Identifier() { hide.addAction(s1); } )* ) <RBRACE>
|
|
{ sys = hide; }
|
|
)
|
|
// Renaming
|
|
| (
|
|
{ rename = new SystemRename(sys); }
|
|
<LBRACE> s1 = Identifier() <RENAME> s2 = Identifier() { rename.addRename(s1, s2); }
|
|
( <COMMA> s1 = Identifier() <RENAME> s2 = Identifier() { rename.addRename(s1, s2); } )* <RBRACE>
|
|
{ sys = rename; }
|
|
)
|
|
)* )
|
|
{ sys.setPosition(begin, getToken(0)); return sys; }
|
|
}
|
|
|
|
// System definition component (bottom level)
|
|
|
|
SystemDefn SystemAtomic() :
|
|
{
|
|
String name = null;
|
|
SystemDefn sys = null;
|
|
Token begin;
|
|
}
|
|
{
|
|
{ begin = getToken(1); }
|
|
// Module name
|
|
(( name = Identifier() { sys = new SystemModule(name); } )
|
|
// Parentheses
|
|
|( <LPARENTH> sys = SystemDefn() <RPARENTH> { sys = new SystemBrackets(sys); } ))
|
|
{ sys.setPosition(begin, getToken(0)); return sys; }
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Expressions - including PRISM properties (depending on "parsingProperty" flag)
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Expression
|
|
|
|
Expression Expression() :
|
|
{
|
|
Expression ret;
|
|
}
|
|
{
|
|
ret = ExpressionITE()
|
|
{ return ret; }
|
|
}
|
|
|
|
|
|
// Expression: if-then-else, i.e. "cond ? then : else"
|
|
|
|
Expression ExpressionITE() :
|
|
{
|
|
Expression ret, left, right;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionImplies()
|
|
[ <QMARK> left = ExpressionImplies() <COLON> right = ExpressionITE() { ret = new ExpressionITE(ret, left, right); ret.setPosition(begin, getToken(0)); } ]
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: implies
|
|
|
|
Expression ExpressionImplies() :
|
|
{
|
|
Expression ret, expr;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionOr()
|
|
( <IMPLIES> expr = ExpressionOr() { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0)); } )*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: or
|
|
|
|
Expression ExpressionOr() :
|
|
{
|
|
Expression ret, expr;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionAnd()
|
|
( <OR> expr = ExpressionAnd() { ret = new ExpressionBinaryOp(ExpressionBinaryOp.OR, ret, expr); ret.setPosition(begin, getToken(0)); } )*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: and
|
|
|
|
Expression ExpressionAnd() :
|
|
{
|
|
Expression ret, expr;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionNot()
|
|
( <AND> expr = ExpressionNot() { ret = new ExpressionBinaryOp(ExpressionBinaryOp.AND, ret, expr); ret.setPosition(begin, getToken(0)); } )*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: not
|
|
|
|
Expression ExpressionNot() :
|
|
{
|
|
Expression ret, expr;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
(
|
|
begin = <NOT> expr = ExpressionNot() { ret = new ExpressionUnaryOp(ExpressionUnaryOp.NOT, expr); ret.setPosition(begin, getToken(0)); }
|
|
|
|
|
ret = ExpressionEquality()
|
|
)
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: equality operators: =, !=
|
|
|
|
Expression ExpressionEquality() :
|
|
{
|
|
Expression ret, expr;
|
|
int op;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionRelop()
|
|
( op = EqNeq() expr = ExpressionRelop() { ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0)); } )*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: relational operators: >, <, >=, <=
|
|
|
|
Expression ExpressionRelop() :
|
|
{
|
|
Expression ret, expr;
|
|
int op;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionPlusMinus()
|
|
( op = LtGt() expr = ExpressionPlusMinus() { ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0)); } )*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: plus/minus
|
|
|
|
// JavaCC warns about lookahead for this function. This is because in a few places
|
|
// (bounded temporal operators and semicolon-less properties files)
|
|
// (see the relevant productions for details)
|
|
// we allow two or more successive expressions resulting in potential ambiguities
|
|
// e.g. "-a-b" = "(-a)-b" = "-a" "-b"
|
|
// Ignoring the warning results in the largest match being taken.
|
|
|
|
Expression ExpressionPlusMinus() :
|
|
{
|
|
Expression ret, expr;
|
|
int op;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionTimesDivide()
|
|
(
|
|
( <PLUS> { op = ExpressionBinaryOp.PLUS; } | <MINUS> { op = ExpressionBinaryOp.MINUS; } )
|
|
expr = ExpressionTimesDivide() { ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0)); }
|
|
)*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: times/divide
|
|
|
|
Expression ExpressionTimesDivide() :
|
|
{
|
|
Expression ret, expr;
|
|
int op;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
{ begin = getToken(1); } ret = ExpressionUnaryMinus()
|
|
(
|
|
( <TIMES> { op = ExpressionBinaryOp.TIMES; } | <DIVIDE> { op = ExpressionBinaryOp.DIVIDE; } )
|
|
expr = ExpressionUnaryMinus() { ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0)); }
|
|
)*
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: unary minus
|
|
|
|
Expression ExpressionUnaryMinus() :
|
|
{
|
|
Expression ret, expr;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
(
|
|
begin = <MINUS> expr = ExpressionUnaryMinus()
|
|
{ ret = new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, expr); ret.setPosition(begin, getToken(0)); }
|
|
|
|
|
ret = ExpressionBasic()
|
|
)
|
|
{ return ret; }
|
|
}
|
|
|
|
// Basic expression (top of operator precedence ordering)
|
|
|
|
Expression ExpressionBasic() :
|
|
{
|
|
Expression ret;
|
|
}
|
|
{
|
|
(
|
|
ret = ExpressionLiteral()
|
|
|
|
|
ret = ExpressionFuncOrIdent()
|
|
|
|
|
ret = ExpressionFuncMinMax()
|
|
|
|
|
ret = ExpressionFuncOldStyle()
|
|
|
|
|
ret = ExpressionParenth()
|
|
|
|
|
// Remaining options are only applicable for properties
|
|
ret = ExpressionBasicProperties()
|
|
)
|
|
{ return ret; }
|
|
}
|
|
|
|
// Expression: function or identifier
|
|
|
|
// JavaCC warns about lookahead for this function. This is because in a few places
|
|
// (bounded temporal operators and semicolon-less properties files)
|
|
// (see the relevant productions for details)
|
|
// we allow two or more successive expressions resulting in potential ambiguities
|
|
// e.g. "a(b)" = "a" "(b)"
|
|
// Ignoring the warning results in the largest match being taken.
|
|
|
|
Expression ExpressionFuncOrIdent() :
|
|
{
|
|
String s = null;
|
|
Expression ret = null;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
// If there is no "(...)", this is an identifier
|
|
s = Identifier() { ret = new ExpressionIdent(s); begin = getToken(0); }
|
|
// If there is, it's a function
|
|
( <LPARENTH> { ret = new ExpressionFunc(s); } ExpressionFuncArgs((ExpressionFunc)ret) <RPARENTH> )?
|
|
{ ret.setPosition(begin, getToken(0)); return ret; }
|
|
}
|
|
|
|
// Expression: min/max function (treated differently because min/max are keywords)
|
|
|
|
Expression ExpressionFuncMinMax() :
|
|
{
|
|
String s = null;
|
|
ExpressionFunc func = null;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
( begin = <MIN> { s = "min"; } | begin = <MAX> { s = "max"; } )
|
|
{ func = new ExpressionFunc(s); } <LPARENTH> ExpressionFuncArgs(func) <RPARENTH>
|
|
{ func.setPosition(begin, getToken(0)); return func; }
|
|
}
|
|
|
|
// Expression: old-style function, i.e. "func(name, ...)"
|
|
|
|
Expression ExpressionFuncOldStyle() :
|
|
{
|
|
String s = null;
|
|
ExpressionFunc func = null;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
begin = <FUNC> <LPARENTH> ( <MIN> { s = "min"; } | <MAX> { s = "max"; } | s = Identifier() )
|
|
<COMMA> { func = new ExpressionFunc(s); func.setOldStyle(true); } ExpressionFuncArgs(func) <RPARENTH>
|
|
{ func.setPosition(begin, getToken(0)); return func; }
|
|
}
|
|
|
|
// Arguments for a function in an expression
|
|
|
|
void ExpressionFuncArgs(ExpressionFunc func) :
|
|
{
|
|
Expression expr;
|
|
}
|
|
{
|
|
expr = Expression() { func.addOperand(expr); } ( <COMMA> expr = Expression() { func.addOperand(expr); })*
|
|
}
|
|
|
|
// Expression: identifier
|
|
|
|
Expression ExpressionIdent() :
|
|
{
|
|
String ident;
|
|
Expression ret;
|
|
}
|
|
{
|
|
ident = Identifier()
|
|
{ ret = new ExpressionIdent(ident); ret.setPosition(getToken(0)); return ret; }
|
|
}
|
|
|
|
// Expression: literal
|
|
|
|
Expression ExpressionLiteral() :
|
|
{
|
|
Expression ret;
|
|
}
|
|
{
|
|
(
|
|
<REG_INT> { ret = new ExpressionLiteral(Expression.INT, new Integer(getToken(0).image)); }
|
|
|
|
|
<REG_DOUBLE> { ret = new ExpressionLiteral(Expression.DOUBLE, new Double(getToken(0).image), getToken(0).image); }
|
|
|
|
|
<TRUE> { ret = new ExpressionLiteral(Expression.BOOLEAN, new Boolean(true)); }
|
|
|
|
|
<FALSE> { ret = new ExpressionLiteral(Expression.BOOLEAN, new Boolean(false)); }
|
|
)
|
|
{ ret.setPosition(getToken(0)); return ret; }
|
|
}
|
|
|
|
// Expression: parentheses
|
|
|
|
Expression ExpressionParenth() :
|
|
{
|
|
Expression expr, ret;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
begin = <LPARENTH> expr = Expression() <RPARENTH>
|
|
{ ret = new ExpressionUnaryOp(ExpressionUnaryOp.PARENTH, expr); ret.setPosition(begin, getToken(0)); return ret;}
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Property stuff
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Extra basic expressions allowed in properties
|
|
|
|
Expression ExpressionBasicProperties() :
|
|
{
|
|
Expression ret;
|
|
}
|
|
{
|
|
// These productions are only allowed in expressions if the "parsingProperty" flag is set
|
|
{ if (!parsingProperty) throw generateParseException(); }
|
|
(
|
|
ret = ExpressionProb()
|
|
|
|
|
ret = ExpressionSS()
|
|
|
|
|
ret = ExpressionReward()
|
|
|
|
|
ret = ExpressionLabel()
|
|
)
|
|
{ return ret; }
|
|
}
|
|
|
|
// (Property) expression: probabilistic operator P
|
|
|
|
Expression ExpressionProb() :
|
|
{
|
|
int r;
|
|
String relOp = null;
|
|
Expression prob = null;
|
|
PathExpression pe;
|
|
Filter filter = null;
|
|
ExpressionProb ret = new ExpressionProb();
|
|
Token begin = null;
|
|
}
|
|
{
|
|
// Various options for "P" keyword and attached symbols
|
|
(( begin = <P> (( r = LtGt() prob = Expression() { relOp = ExpressionBinaryOp.opSymbols[r]; } )
|
|
|( <EQ> <QMARK> { relOp = "="; } )
|
|
|( <MIN> <EQ> <QMARK> { relOp = "min="; } )
|
|
|( <MAX> <EQ> <QMARK> { relOp = "max="; } )))
|
|
// These two are dupes of above but allow space to be omitted
|
|
|( begin = <PMIN> <EQ> <QMARK> { relOp = "min="; } )
|
|
|( begin = <PMAX> <EQ> <QMARK> { relOp = "max="; } ))
|
|
// Path formula, optional filter
|
|
<LBRACKET> pe = ExpressionProbContents() (filter = Filter())? <RBRACKET>
|
|
{
|
|
ret.setRelOp(relOp);
|
|
ret.setProb(prob);
|
|
ret.setPathExpression(pe);
|
|
ret.setFilter(filter);
|
|
ret.setPosition(begin, getToken(0));
|
|
return ret;
|
|
}
|
|
}
|
|
|
|
// Filter for a P/S/R operator
|
|
|
|
Filter Filter() :
|
|
{
|
|
Filter filter;
|
|
Expression expr;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
begin = <LBRACE> expr = Expression() { filter = new Filter(expr); } <RBRACE>
|
|
( <LBRACE>
|
|
( <MIN> { filter.setMinRequested(true); }
|
|
| <MAX> { filter.setMaxRequested(true); } )
|
|
<RBRACE> )*
|
|
{ filter.setPosition(begin, getToken(0)); return filter; }
|
|
}
|
|
|
|
// Path formulas which can go in a P operator
|
|
|
|
PathExpression ExpressionProbContents() :
|
|
{
|
|
PathExpression pe;
|
|
}
|
|
{
|
|
( pe = PathExpressionTemporal() )
|
|
{ return pe; }
|
|
}
|
|
|
|
// Temporal operarors (X, U, F, G)
|
|
|
|
PathExpression PathExpressionTemporal() :
|
|
{
|
|
PathExpressionTemporal pe = new PathExpressionTemporal();
|
|
Expression expr1 = null, expr2 = null;
|
|
TimeBound tb = null;
|
|
Token begin = null;
|
|
}
|
|
{
|
|
(
|
|
{ begin = getToken(0); }
|
|
(
|
|
<X> { pe.setOperator(PathExpressionTemporal.P_X); }
|
|
| expr1 = Expression() <U> { pe.setOperator(PathExpressionTemporal.P_U); }
|
|
| <F> { pe.setOperator(PathExpressionTemporal.P_F); }
|
|
| <G> { pe.setOperator(PathExpressionTemporal.P_G); }
|
|
)
|
|
( tb = TimeBound() )?
|
|
( expr2 = Expression() )?
|
|
)
|
|
{
|
|
if (tb != null) pe.setLowerBound(tb.lBound);
|
|
if (tb != null) pe.setUpperBound(tb.uBound);
|
|
if (expr1 != null) {
|
|
PathExpressionExpr pe1 = new PathExpressionExpr(expr1);
|
|
pe1.setPosition(expr1);
|
|
pe.setOperand1(pe1);
|
|
}
|
|
if (expr2 != null) {
|
|
PathExpressionExpr pe2 = new PathExpressionExpr(expr2);
|
|
pe2.setPosition(expr2);
|
|
pe.setOperand2(pe2);
|
|
}
|
|
|
|
// This is the usual case.
|
|
if (expr2 != null) {
|
|
pe.setPosition(begin, getToken(0));
|
|
return pe;
|
|
}
|
|
// And this is a bit of inelegant jiggery-pokery.
|
|
// The problem is that bounded path formulas sometimes need
|
|
// two successive expressions with no separator, e.g. t and b in "F<=t b".
|
|
// Parsing two successive expressions is tricky because:
|
|
// 1. e.g. "t (b)" gets parsed a as single expression: function "t(b)"
|
|
// 2. e.g. "-a -b" gets parsed as a single expression: subtraction "(-a)-b"
|
|
// These are the only two problem cases. The cunning plan is to make the second
|
|
// expression optional and then check if it is missing afterwards.
|
|
// Note that case 2 is genuinely ambiguous (e.g. where to split "-a-b-c"?).
|
|
// Fortunately this does not type check (the expression should be Boolean)
|
|
// so we don't really care.
|
|
else {
|
|
if (tb != null) {
|
|
if (tb.lBound == null) {
|
|
if (tb.uBound instanceof ExpressionFunc && ((ExpressionFunc)tb.uBound).getNumOperands() == 1) {
|
|
Expression actualBound = new ExpressionIdent(((ExpressionFunc)tb.uBound).getName());
|
|
actualBound.setPosition(tb.uBound);
|
|
actualBound.setEndColumn(actualBound.getBeginColumn()+((ExpressionFunc)tb.uBound).getName().length()-1);
|
|
pe.setUpperBound(actualBound);
|
|
Expression actualOperand2 = ((ExpressionFunc)tb.uBound).getOperand(0);
|
|
actualOperand2 = Expression.Parenth(actualOperand2);
|
|
actualOperand2.setPosition(((ExpressionFunc)tb.uBound).getOperand(0));
|
|
PathExpressionExpr pe2 = new PathExpressionExpr(actualOperand2);
|
|
pe2.setPosition(actualOperand2);
|
|
pe.setOperand2(pe2);
|
|
pe.setPosition(begin, getToken(0));
|
|
return pe;
|
|
}
|
|
}
|
|
if (tb.uBound == null) {
|
|
if (tb.lBound instanceof ExpressionFunc && ((ExpressionFunc)tb.lBound).getNumOperands() == 1) {
|
|
Expression actualBound = new ExpressionIdent(((ExpressionFunc)tb.lBound).getName());
|
|
actualBound.setPosition(tb.lBound);
|
|
actualBound.setEndColumn(actualBound.getBeginColumn()+((ExpressionFunc)tb.lBound).getName().length()-1);
|
|
pe.setLowerBound(actualBound);
|
|
Expression actualOperand2 = ((ExpressionFunc)tb.lBound).getOperand(0);
|
|
actualOperand2 = Expression.Parenth(actualOperand2);
|
|
actualOperand2.setPosition(((ExpressionFunc)tb.uBound).getOperand(0));
|
|
PathExpressionExpr pe2 = new PathExpressionExpr(actualOperand2);
|
|
pe2.setPosition(actualOperand2);
|
|
pe.setOperand2(pe2);
|
|
pe.setPosition(begin, getToken(0));
|
|
return pe;
|
|
}
|
|
}
|
|
}
|
|
throw generateParseException();
|
|
}
|
|
}
|
|
}
|
|
|
|
// Time bound for temporal operators
|
|
|
|
TimeBound TimeBound() :
|
|
{
|
|
TimeBound tb = new TimeBound();
|
|
}
|
|
{
|
|
( <LE> tb.uBound = Expression()
|
|
| <GE> tb.lBound = Expression()
|
|
| <LBRACKET> tb.lBound = Expression() <COMMA> tb.uBound = Expression() <RBRACKET> )
|
|
{ return tb; }
|
|
}
|
|
|
|
// (Property) expression: steady-state operator S
|
|
|
|
Expression ExpressionSS() :
|
|
{
|
|
int r;
|
|
String relOp = null;
|
|
Expression prob = null;
|
|
Expression expr;
|
|
Filter filter = null;
|
|
ExpressionSS ret = new ExpressionSS();
|
|
Token begin;
|
|
}
|
|
{
|
|
// Various options for "S" keyword and attached symbols
|
|
begin = <S> (
|
|
( r = LtGt() prob = Expression() { relOp = ExpressionBinaryOp.opSymbols[r]; } ) |
|
|
( <EQ> <QMARK> { relOp = "="; } )
|
|
)
|
|
// Expression, optional filter
|
|
<LBRACKET> expr = Expression() (filter = Filter())? <RBRACKET>
|
|
{
|
|
ret.setRelOp(relOp);
|
|
ret.setProb(prob);
|
|
ret.setExpression(expr);
|
|
ret.setFilter(filter);
|
|
ret.setPosition(begin, getToken(0));
|
|
return ret;
|
|
}
|
|
}
|
|
|
|
// (Property) expression: expected reward operator R
|
|
|
|
Expression ExpressionReward() :
|
|
{
|
|
int r;
|
|
Object index = null;
|
|
String relOp = null;
|
|
Expression rew = null;
|
|
PathExpression pe;
|
|
Filter filter = null;
|
|
ExpressionReward ret = new ExpressionReward();
|
|
Token begin;
|
|
}
|
|
{
|
|
// Various options for "R" keyword and attached symbols
|
|
(( begin = <R> (index = RewardIndex())?
|
|
(( r = LtGt() rew = Expression() { relOp = ExpressionBinaryOp.opSymbols[r]; } )
|
|
|( <EQ> <QMARK> { relOp = "="; } )
|
|
|( <MIN> <EQ> <QMARK> { relOp = "min="; } )
|
|
|( <MAX> <EQ> <QMARK> { relOp = "max="; } )))
|
|
// These two are dupes of above but allow space to be omitted
|
|
|( begin = <RMIN> <EQ> <QMARK> { relOp = "min="; } )
|
|
|( begin = <RMAX> <EQ> <QMARK> { relOp = "max="; } ))
|
|
// Path formula, optional filter
|
|
<LBRACKET> pe = ExpressionRewardContents() (filter = Filter())? <RBRACKET>
|
|
{
|
|
ret.setRewardStructIndex(index);
|
|
ret.setRelOp(relOp);
|
|
ret.setReward(rew);
|
|
ret.setPathExpression(pe);
|
|
ret.setFilter(filter);
|
|
ret.setPosition(begin, getToken(0));
|
|
return ret;
|
|
}
|
|
}
|
|
|
|
// Reward struct index for R operator
|
|
|
|
Object RewardIndex() :
|
|
{
|
|
Object index;
|
|
}
|
|
{
|
|
// Lookahead here is to ensure that "id" is not misdetected as an ExpressionLabel
|
|
( <LBRACE> ( LOOKAHEAD(<DQUOTE>) ( <DQUOTE> index = Identifier() <DQUOTE> ) | index = Expression() ) <RBRACE> )
|
|
{ return index; }
|
|
}
|
|
|
|
// Contents of an R operator
|
|
|
|
PathExpression ExpressionRewardContents() :
|
|
{
|
|
Expression expr = null;
|
|
PathExpressionTemporal pe = null;
|
|
Token begin;
|
|
}
|
|
{
|
|
( begin = <C> <LE> expr = Expression() { pe = new PathExpressionTemporal(PathExpressionTemporal.R_C, null, null); pe.setUpperBound(expr); }
|
|
| begin = <I> <EQ> expr = Expression() { pe = new PathExpressionTemporal(PathExpressionTemporal.R_I, null, null); pe.setUpperBound(expr); }
|
|
| begin = <F> expr = Expression() { pe = new PathExpressionTemporal(PathExpressionTemporal.R_F, null, new PathExpressionExpr(expr)); }
|
|
| begin = <S> { pe = new PathExpressionTemporal(PathExpressionTemporal.R_S, null, null); } )
|
|
{ pe.setPosition(begin, getToken(0)); return pe; }
|
|
}
|
|
|
|
// (Property) expression: label (including "init")
|
|
|
|
Expression ExpressionLabel() :
|
|
{
|
|
String s;
|
|
ExpressionLabel ret = null;
|
|
Token begin;
|
|
}
|
|
{
|
|
// Label can be arbitary string or the "init" keyword
|
|
( begin = <DQUOTE> ( s=Identifier() | <INIT> { s = "init"; } ) <DQUOTE> )
|
|
{ ret = new ExpressionLabel(s); ret.setPosition(begin, getToken(0)); return ret; }
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------------
|
|
// Miscellaneous stuff
|
|
//-----------------------------------------------------------------------------------
|
|
|
|
// Identifier
|
|
|
|
String Identifier() :
|
|
{
|
|
}
|
|
{
|
|
<REG_IDENT> { return getToken(0).image; }
|
|
}
|
|
|
|
// Primed identifier
|
|
|
|
ExpressionIdent IdentifierPrime() :
|
|
{
|
|
}
|
|
{
|
|
<REG_IDENTPRIME>
|
|
{
|
|
// Remove prime, create new ident and return
|
|
String s = getToken(0).image;
|
|
s = s.substring(0, s.length()-1);
|
|
ExpressionIdent expr = new ExpressionIdent(s);
|
|
expr.setPosition(token);
|
|
expr.setEndColumn(expr.getEndColumn() - 1);
|
|
return expr;
|
|
}
|
|
}
|
|
|
|
// Equality operators: =, !=
|
|
|
|
int EqNeq() :
|
|
{
|
|
}
|
|
{
|
|
<EQ> {return ExpressionBinaryOp.EQ; } |
|
|
<NE> {return ExpressionBinaryOp.NE; }
|
|
}
|
|
|
|
// Relational operators: >, <, >=, <=
|
|
|
|
int LtGt() :
|
|
{
|
|
}
|
|
{
|
|
<GT> {return ExpressionBinaryOp.GT; } |
|
|
<LT> {return ExpressionBinaryOp.LT; } |
|
|
<GE> {return ExpressionBinaryOp.GE; }|
|
|
<LE> {return ExpressionBinaryOp.LE; }
|
|
}
|
|
|
|
// For loop
|
|
|
|
ForLoop ForLoop() :
|
|
{
|
|
String s;
|
|
Expression from = null, to = null, step = null;
|
|
ForLoop fl = new ForLoop();
|
|
Token begin;
|
|
}
|
|
{
|
|
( { begin = getToken(1); } s=Identifier() <EQ> from = Expression() <COLON> to = Expression() ( <COLON> step = Expression() )? <EOF> )
|
|
{
|
|
fl.setLHS(s);
|
|
fl.setFrom(from);
|
|
fl.setTo(to);
|
|
if (step != null) fl.setStep(step);
|
|
fl.setPosition(begin, getToken(0));
|
|
return fl;
|
|
}
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|