From 8465fdeb071a7b901e3620198d162f6b95e9759c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Jun 2011 20:54:34 +0000 Subject: [PATCH] Property names parsed (but not used) and -test switch added (but no property/verify blocks yet). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3096 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 235 +++++++++-------- prism/src/parser/PrismParser.jj | 44 ++-- prism/src/parser/ast/PropertiesFile.java | 164 ++++++++++-- prism/src/parser/ast/Property.java | 245 ++++++++++++++++++ prism/src/parser/visitor/ASTTraverse.java | 12 +- .../src/parser/visitor/ASTTraverseModify.java | 23 +- prism/src/parser/visitor/ASTVisitor.java | 1 + prism/src/parser/visitor/TypeCheck.java | 5 + prism/src/prism/PrismCL.java | 62 +++-- 9 files changed, 624 insertions(+), 167 deletions(-) create mode 100644 prism/src/parser/ast/Property.java diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index a41baaf3..56f8b499 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -180,22 +180,21 @@ public class PrismParser implements PrismParserConstants { // Some utility methods //----------------------------------------------------------------------------------- - // Get comment block (including white space) - // preceding a token and remove "//" characters - + /** + * Get comment block directly 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 + if (t.specialToken != null && !(t.specialToken.kind == PrismParserConstants.WHITESPACE && t.specialToken.image.matches("[\u005c\u005cn\u005c\u005cr]*"))) { + // trace back thru special tokens that are comments 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.specialToken != null && !(t.specialToken.kind == PrismParserConstants.WHITESPACE && t.specialToken.image.matches("[\u005c\u005cn\u005c\u005cr]*"))) + t = t.specialToken; + // concatenate comment special tokens while (t != null) { s = t.image; // strip any nasty carriage returns @@ -430,8 +429,8 @@ public class PrismParser implements PrismParserConstants { // Properties file static final public PropertiesFile PropertiesFile() throws ParseException, PrismLangException { PropertiesFile pf = new PropertiesFile(modulesFile); - Expression expr; - Token begin = null, t = null; + Property prop; + Token begin = null; begin = getToken(1); label_2: while (true) { @@ -491,9 +490,8 @@ public class PrismParser implements PrismParserConstants { case REG_INT: case REG_DOUBLE: case REG_IDENT: - t = getToken(1); - expr = Property(); - pf.addProperty(expr, getPrecedingCommentBlock(t)); + prop = Property(); + pf.addProperty(prop); label_3: while (true) { jj_consume_token(SEMICOLON); @@ -529,8 +527,8 @@ public class PrismParser implements PrismParserConstants { // Properties file with optional semicolons - beware of potential ambiguities static final public PropertiesFile PropertiesFileSemicolonless() throws ParseException, PrismLangException { PropertiesFile pf = new PropertiesFile(modulesFile); - Expression expr; - Token begin = null, t = null; + Property prop; + Token begin = null; begin = getToken(1); label_4: while (true) { @@ -590,8 +588,7 @@ public class PrismParser implements PrismParserConstants { case REG_INT: case REG_DOUBLE: case REG_IDENT: - t = getToken(1); - expr = Property(); + prop = Property(); label_5: while (true) { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -604,7 +601,7 @@ public class PrismParser implements PrismParserConstants { } jj_consume_token(SEMICOLON); } - pf.addProperty(expr, getPrecedingCommentBlock(t)); + pf.addProperty(prop); break; case LABEL: LabelDef(pf.getLabelList()); @@ -625,14 +622,24 @@ public class PrismParser implements PrismParserConstants { throw new Error("Missing return statement in function"); } -// Property expression (used above) - static final public Expression Property() throws ParseException { +// Property - expression, with optional name/comment + static final public Property Property() throws ParseException { + String name = null; Expression expr; - // Note that we jump in a few levels down in the Expression hierarchy - // (more precisely, we skip the temporal operators, which can't occur at the top-level) - // (this avoids some common parsing errors for semicolon-less files) - expr = ExpressionITE(true, false); - {if (true) return expr;} + Property prop; + Token begin = null; + begin = getToken(1); + if (jj_2_2(2147483647)) { + jj_consume_token(DQUOTE); + name = Identifier(); + jj_consume_token(DQUOTE); + jj_consume_token(COLON); + } else { + ; + } + expr = ExpressionITE(true, false); + prop = new Property(expr, name, getPrecedingCommentBlock(begin)); + prop.setPosition(begin, getToken(0)); {if (true) return prop;} throw new Error("Missing return statement in function"); } @@ -730,7 +737,7 @@ public class PrismParser implements PrismParserConstants { static final public void LabelDef(LabelList labelList) throws ParseException, PrismLangException { ExpressionIdent name = null; Expression expr = null; - if (jj_2_2(2147483647)) { + if (jj_2_3(2147483647)) { jj_consume_token(LABEL); jj_consume_token(DQUOTE); name = IdentifierExpression(); @@ -739,7 +746,7 @@ public class PrismParser implements PrismParserConstants { expr = Expression(false, false); jj_consume_token(SEMICOLON); labelList.addLabel(name, expr); - } else if (jj_2_3(2147483647)) { + } else if (jj_2_4(2147483647)) { jj_consume_token(LABEL); name = IdentifierExpression(); {if (true) throw new PrismLangException("Label names must be enclosed in double-quotes", name);} @@ -979,7 +986,7 @@ public class PrismParser implements PrismParserConstants { Updates updates = new Updates(); Token begin = null; begin = getToken(1); - if (jj_2_4(2147483647)) { + if (jj_2_5(2147483647)) { update = Update(); updates.addUpdate(null, update); } else { @@ -1132,7 +1139,7 @@ public class PrismParser implements PrismParserConstants { RewardStructItem rsi; Token begin = null, begin2 = null; begin = jj_consume_token(REWARDS); - if (jj_2_5(2147483647)) { + if (jj_2_6(2147483647)) { jj_consume_token(DQUOTE); name = Identifier(); jj_consume_token(DQUOTE); @@ -1243,7 +1250,7 @@ public class PrismParser implements PrismParserConstants { par = new SystemFullParallel(); par.addOperand(sys1); label_12: while (true) { - if (jj_2_6(2147483647)) { + if (jj_2_7(2147483647)) { ; } else { break label_12; @@ -1273,7 +1280,7 @@ public class PrismParser implements PrismParserConstants { par = new SystemInterleaved(); par.addOperand(sys1); label_13: while (true) { - if (jj_2_7(2147483647)) { + if (jj_2_8(2147483647)) { ; } else { break label_13; @@ -1302,7 +1309,7 @@ public class PrismParser implements PrismParserConstants { Token begin; begin = getToken(1); sys1 = SystemHideRename(); - if (jj_2_8(2147483647)) { + if (jj_2_9(2147483647)) { par = new SystemParallel(); par.setOperand1(sys1); jj_consume_token(OR); jj_consume_token(LBRACKET); @@ -1619,7 +1626,7 @@ public class PrismParser implements PrismParserConstants { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { case LE: jj_consume_token(LE); - if (jj_2_9(2147483647)) { + if (jj_2_10(2147483647)) { tb.uBound = IdentifierExpression(); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -1660,7 +1667,7 @@ public class PrismParser implements PrismParserConstants { case LT: jj_consume_token(LT); tb.uBoundStrict=true; - if (jj_2_10(2147483647)) { + if (jj_2_11(2147483647)) { tb.uBound = IdentifierExpression(); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -1700,7 +1707,7 @@ public class PrismParser implements PrismParserConstants { break; case GE: jj_consume_token(GE); - if (jj_2_11(2147483647)) { + if (jj_2_12(2147483647)) { tb.lBound = IdentifierExpression(); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -1741,7 +1748,7 @@ public class PrismParser implements PrismParserConstants { case GT: jj_consume_token(GT); tb.lBoundStrict=true; - if (jj_2_12(2147483647)) { + if (jj_2_13(2147483647)) { tb.lBound = IdentifierExpression(); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -2633,7 +2640,7 @@ public class PrismParser implements PrismParserConstants { static final public Object RewardIndex() throws ParseException { Object index; jj_consume_token(LBRACE); - if (jj_2_13(2147483647)) { + if (jj_2_14(2147483647)) { jj_consume_token(DQUOTE); index = Identifier(); jj_consume_token(DQUOTE); @@ -3052,56 +3059,14 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(12, xla); } } - static private boolean jj_3R_160() { - if (jj_3R_81()) return true; - if (jj_3R_34()) return true; - return false; - } - - static private boolean jj_3R_139() { - if (jj_scan_token(R)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_159()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3R_160()) { - jj_scanpos = xsp; - if (jj_3R_161()) { - jj_scanpos = xsp; - if (jj_3R_162()) { - jj_scanpos = xsp; - if (jj_3R_163()) return true; - } - } - } - return false; - } - - static private boolean jj_3R_68() { - if (jj_scan_token(OR)) return true; - if (jj_3R_67()) return true; - return false; - } - - static private boolean jj_3R_116() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_139()) { - jj_scanpos = xsp; - if (jj_3R_140()) { - jj_scanpos = xsp; - if (jj_3R_141()) return true; - } - } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_142()) return true; - xsp = jj_scanpos; - if (jj_3R_143()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; - return false; + static private boolean jj_2_14(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_14(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(13, xla); } } - static private boolean jj_3_12() { + static private boolean jj_3_13() { if (jj_3R_29()) return true; if (jj_scan_token(LPARENTH)) return true; return false; @@ -3117,7 +3082,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_10() { + static private boolean jj_3_11() { if (jj_3R_29()) return true; if (jj_scan_token(LPARENTH)) return true; return false; @@ -3157,13 +3122,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_11() { + static private boolean jj_3_12() { if (jj_3R_29()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3_9() { + static private boolean jj_3_10() { if (jj_3R_29()) return true; if (jj_scan_token(LPARENTH)) return true; return false; @@ -3507,12 +3472,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_3() { + static private boolean jj_3_4() { if (jj_scan_token(LABEL)) return true; return false; } - static private boolean jj_3_2() { + static private boolean jj_3_3() { if (jj_scan_token(LABEL)) return true; if (jj_scan_token(DQUOTE)) return true; return false; @@ -3550,7 +3515,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_7() { + static private boolean jj_3_8() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; @@ -3634,7 +3599,15 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_6() { + static private boolean jj_3_2() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_27()) return true; + if (jj_scan_token(DQUOTE)) return true; + if (jj_scan_token(COLON)) return true; + return false; + } + + static private boolean jj_3_7() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; return false; @@ -3678,7 +3651,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_8() { + static private boolean jj_3_9() { if (jj_scan_token(OR)) return true; if (jj_scan_token(LBRACKET)) return true; return false; @@ -3848,13 +3821,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_1() { - if (jj_scan_token(MODULE)) return true; - if (jj_3R_27()) return true; - if (jj_scan_token(EQ)) return true; - return false; - } - static private boolean jj_3R_120() { if (jj_scan_token(FILTER)) return true; if (jj_scan_token(LPARENTH)) return true; @@ -3929,6 +3895,13 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3_1() { + if (jj_scan_token(MODULE)) return true; + if (jj_3R_27()) return true; + if (jj_scan_token(EQ)) return true; + return false; + } + static private boolean jj_3R_173() { if (jj_3R_34()) return true; return false; @@ -3978,7 +3951,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_5() { + static private boolean jj_3_6() { if (jj_scan_token(DQUOTE)) return true; return false; } @@ -4050,7 +4023,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_13() { + static private boolean jj_3_14() { if (jj_scan_token(DQUOTE)) return true; return false; } @@ -4193,7 +4166,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_4() { + static private boolean jj_3_5() { if (jj_3R_28()) return true; return false; } @@ -4278,6 +4251,55 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_160() { + if (jj_3R_81()) return true; + if (jj_3R_34()) return true; + return false; + } + + static private boolean jj_3R_139() { + if (jj_scan_token(R)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_159()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_160()) { + jj_scanpos = xsp; + if (jj_3R_161()) { + jj_scanpos = xsp; + if (jj_3R_162()) { + jj_scanpos = xsp; + if (jj_3R_163()) return true; + } + } + } + return false; + } + + static private boolean jj_3R_68() { + if (jj_scan_token(OR)) return true; + if (jj_3R_67()) return true; + return false; + } + + static private boolean jj_3R_116() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_139()) { + jj_scanpos = xsp; + if (jj_3R_140()) { + jj_scanpos = xsp; + if (jj_3R_141()) return true; + } + } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_142()) return true; + xsp = jj_scanpos; + if (jj_3R_143()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; + return false; + } + static private boolean jj_initialized_once = false; /** Generated Token Manager. */ static public PrismParserTokenManager token_source; @@ -4308,7 +4330,7 @@ public class PrismParser implements PrismParserConstants { private static void jj_la1_init_2() { jj_la1_2 = new int[] {0x0,0x0,0x0,0x170400,0x0,0x170400,0x170400,0x0,0x170400,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x8,0x0,0x0,0x100000,0x0,0x0,0x100000,0x200,0x170400,0x0,0x0,0x0,0x170400,0x100000,0x0,0x0,0x1002,0x0,0x0,0x1002,0x100000,0x0,0x1e0,0x0,0x0,0x1e0,0x170400,0x170400,0x170400,0x170400,0x170400,0x1e0,0x8000,0x0,0x0,0x0,0x170400,0x18,0x1e0,0x600,0x600,0x1800,0x1800,0x170400,0x170000,0x0,0x0,0x100000,0x0,0x60000,0x1e8,0x0,0x2,0x2,0x0,0x1e8,0x2,0x2,0x1e8,0x0,0x2,0x170400,0x0,0x100000,0x100200,0x0,0x100000,0x18,0x1e0,0x0,}; } - static final private JJCalls[] jj_2_rtns = new JJCalls[13]; + static final private JJCalls[] jj_2_rtns = new JJCalls[14]; static private boolean jj_rescan = false; static private int jj_gc = 0; @@ -4560,7 +4582,7 @@ public class PrismParser implements PrismParserConstants { static private void jj_rescan_token() { jj_rescan = true; - for (int i = 0; i < 13; i++) { + for (int i = 0; i < 14; i++) { try { JJCalls p = jj_2_rtns[i]; do { @@ -4580,6 +4602,7 @@ public class PrismParser implements PrismParserConstants { case 10: jj_3_11(); break; case 11: jj_3_12(); break; case 12: jj_3_13(); break; + case 13: jj_3_14(); break; } } p = p.next; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 24d90625..cbe54082 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -213,22 +213,21 @@ public class PrismParser // Some utility methods //----------------------------------------------------------------------------------- - // Get comment block (including white space) - // preceding a token and remove "//" characters - + /** + * Get comment block directly 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 + if (t.specialToken != null && !(t.specialToken.kind == PrismParserConstants.WHITESPACE && t.specialToken.image.matches("[\\n\\r]*"))) { + // trace back thru special tokens that are comments 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.specialToken != null && !(t.specialToken.kind == PrismParserConstants.WHITESPACE && t.specialToken.image.matches("[\\n\\r]*"))) + t = t.specialToken; + // concatenate comment special tokens while (t != null) { s = t.image; // strip any nasty carriage returns @@ -519,14 +518,14 @@ ModulesFile ModulesFile() throws PrismLangException : PropertiesFile PropertiesFile() throws PrismLangException : { PropertiesFile pf = new PropertiesFile(modulesFile); - Expression expr; - Token begin = null, t = null; + Property prop; + Token begin = null; } { { begin = getToken(1); } ( // Semi-colon terminated property - ( { t = getToken(1); } expr = Property() { pf.addProperty(expr, getPrecedingCommentBlock(t)); } ()+ ) + ( prop = Property() { pf.addProperty(prop); } ()+ ) | // Label/constant definition ( LabelDef(pf.getLabelList()) ) | ( ConstantDef(pf.getConstantList()) ) @@ -539,14 +538,14 @@ PropertiesFile PropertiesFile() throws PrismLangException : PropertiesFile PropertiesFileSemicolonless() throws PrismLangException : { PropertiesFile pf = new PropertiesFile(modulesFile); - Expression expr; - Token begin = null, t = null; + Property prop; + Token begin = null; } { { begin = getToken(1); } ( // Semi-colon terminated property - ( { t = getToken(1); } expr = Property() ()* { pf.addProperty(expr, getPrecedingCommentBlock(t)); } ) + ( prop = Property() ()* { pf.addProperty(prop); } ) | // Label/constant definition ( LabelDef(pf.getLabelList()) ) | ( ConstantDef(pf.getConstantList()) ) @@ -554,17 +553,26 @@ PropertiesFile PropertiesFileSemicolonless() throws PrismLangException : { pf.setPosition(begin, getToken(0)); return pf; } } -// Property expression (used above) +// Property - expression, with optional name/comment -Expression Property() : +Property Property() : { + String name = null; Expression expr; + Property prop; + Token begin = null; } { // Note that we jump in a few levels down in the Expression hierarchy // (more precisely, we skip the temporal operators, which can't occur at the top-level) // (this avoids some common parsing errors for semicolon-less files) - expr = ExpressionITE(true, false) { return expr; } + // Note also use of lookahead (to colon) to distinguish (optional) name from label reference + ( { begin = getToken(1); } + ( LOOKAHEAD( Identifier() ) name = Identifier() )? + expr = ExpressionITE(true, false) + { prop = new Property(expr, name, getPrecedingCommentBlock(begin)); } + ) + { prop.setPosition(begin, getToken(0)); return prop; } } // A single expression diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 78cef5a1..03fae5aa 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -44,11 +44,10 @@ public class PropertiesFile extends ASTElement private LabelList labelList; private LabelList combinedLabelList; // Labels from both model/here private ConstantList constantList; - private Vector properties; // Properties - private Vector comments; // Property comments + private Vector properties; // Properties // list of all identifiers used - private List allIdentsUsed; + private Vector allIdentsUsed; // actual values of constants private Values constantValues; @@ -57,32 +56,72 @@ public class PropertiesFile extends ASTElement public PropertiesFile(ModulesFile mf) { - modulesFile = mf; + setModulesFile(mf); formulaList = new FormulaList(); labelList = new LabelList(); combinedLabelList = new LabelList(); constantList = new ConstantList(); - properties = new Vector(); - comments = new Vector(); + properties = new Vector(); allIdentsUsed = new Vector(); constantValues = null; } // Set methods + /** Attach to a ModulesFile (so can access labels/constants etc.) */ + public void setModulesFile(ModulesFile mf) { this.modulesFile = mf; } + public void setFormulaList(FormulaList fl) { formulaList = fl; } public void setLabelList(LabelList ll) { labelList = ll; } public void setConstantList(ConstantList cl) { constantList = cl; } + public void addProperty(Property prop) + { + properties.add(prop); + } + public void addProperty(Expression p, String c) { - properties.addElement(p); - comments.addElement(c); + properties.addElement(new Property(p, null, c)); } - public void setProperty(int i, Expression p) { properties.setElementAt(p, i); } + public void setPropertyObject(int i, Property prop) { properties.set(i, prop); } + + public void setPropertyExpression(int i, Expression p) { properties.get(i).setExpression(p); } + + /** + * Insert the contents of another PropertiesFile (just a shallow copy). + */ + public void insertPropertiesFile(PropertiesFile pf) throws PrismLangException + { + FormulaList fl; + LabelList ll; + ConstantList cl; + int i, n; + fl = pf.formulaList; + n = fl.size(); + for (i = 0; i < n; i++) { + formulaList.addFormula(fl.getFormulaNameIdent(i), fl.getFormula(i)); + } + ll = pf.labelList; + n = ll.size(); + for (i = 0; i < n; i++) { + labelList.addLabel(ll.getLabelNameIdent(i), ll.getLabel(i)); + } + cl = pf.constantList; + n = cl.size(); + for (i = 0; i < n; i++) { + constantList.addConstant(cl.getConstantNameIdent(i), cl.getConstant(i), cl.getConstantType(i)); + } + n = pf.properties.size(); + for (i = 0; i < n; i++) { + properties.add(pf.properties.get(i)); + } + // Need to re-tidy (some checks should be re-done, some new info created) + tidyUp(); + } // Get methods @@ -96,9 +135,39 @@ public class PropertiesFile extends ASTElement public int getNumProperties() { return properties.size(); } - public Expression getProperty(int i) { return properties.elementAt(i); } + public Property getPropertyObject(int i) { return properties.get(i); } + + public Expression getProperty(int i) { return properties.get(i).getExpression(); } + + public String getPropertyName(int i) { return properties.get(i).getName(); } + + public String getPropertyComment(int i) { return properties.get(i).getComment(); } + + /** + * Look up a property by name from those listed in this properties file. + * (Use {@link #lookUpPropertyObjectByName} to search model file too) + * Returns null if not found. + */ + public Property getPropertyObjectByName(String name) + { + int i, n; + n = getNumProperties(); + for (i = 0; i < n; i++) { + if (name.equals(getPropertyName(i))) { + return getPropertyObject(i); + } + } + return null; + } - public String getPropertyComment(int i) { return comments.elementAt(i); } + /** + * Look up a property by name, currently just locally like {@link #getPropertyObjectByName}. + * Returns null if not found. + */ + public Property lookUpPropertyObjectByName(String name) + { + return getPropertyObjectByName(name); + } /** * Check if an identifier is used by this properties file @@ -119,7 +188,7 @@ public class PropertiesFile extends ASTElement // check for any cyclic dependencies in the formula list and then expand all formulas. // Note: We have to look for formulas defined both here and in the model. // Note also that we opt not to do actual replacement of formulas in calls to exandFormulas - // (to improve legebility of properties) + // (to improve legibility of properties) findAllFormulas(modulesFile.getFormulaList()); findAllFormulas(formulaList); formulaList.findCycles(); @@ -139,6 +208,9 @@ public class PropertiesFile extends ASTElement // check constants for cyclic dependencies constantList.findCycles(); + // Check property names + checkPropertyNames(); + // Find all instances of variables (i.e. locate idents which are variables). findAllVars(modulesFile.getVarNames(), modulesFile.getVarTypes()); @@ -234,6 +306,44 @@ public class PropertiesFile extends ASTElement } } + /** + * Check for any duplicate property names (or clashes with labels). + */ + private void checkPropertyNames() throws PrismLangException + { + int i, n; + String s; + Vector propNames; + LabelList mfLabels; + + // get label list from model file + mfLabels = modulesFile.getLabelList(); + // Go thru properties + n = properties.size(); + propNames = new Vector(); + for (i = 0; i < n; i++) { + s = properties.get(i).getName(); + if (s == null) + continue; + // see if ident has been used already for a label in model file + if (mfLabels.getLabelIndex(s) != -1) { + throw new PrismLangException("Property name \"" + s + "\" clashes with label in model file", getPropertyObject(i)); + } + // see if ident has been used already for a label in properties file + if (labelList.getLabelIndex(s) != -1) { + throw new PrismLangException("Property name \"" + s + "\" clashes with label", getPropertyObject(i)); + } + // see if ident has been used already for a property name + if (propNames.contains(s)) { + throw new PrismLangException("Duplicated property name \"" + s + "\"", getPropertyObject(i)); + } + // store identifier + else { + propNames.addElement(s); + } + } + } + // get undefined constants public Vector getUndefinedConstants() @@ -290,14 +400,7 @@ public class PropertiesFile extends ASTElement n = getNumProperties(); for (i = 0; i < n; i++) { - // add comment (if any) - tmp = getPropertyComment(i); - if (tmp != null) { - if (tmp.length() > 0) { - s += PrismParser.slashCommentBlock(tmp); - } - } - s += getProperty(i) + "\n"; + s += getPropertyObject(i) + ";\n"; if (i < n-1) s += "\n"; } @@ -307,10 +410,27 @@ public class PropertiesFile extends ASTElement /** * Perform a deep copy. */ + @SuppressWarnings("unchecked") public ASTElement deepCopy() { - // Deep copy not required for whole properties file - return null; + int i, n; + PropertiesFile ret = new PropertiesFile(modulesFile); + // Copy ASTElement stuff + ret.setPosition(this); + // Deep copy main components + ret.setFormulaList((FormulaList) formulaList.deepCopy()); + ret.setLabelList((LabelList) labelList.deepCopy()); + ret.combinedLabelList = (LabelList) combinedLabelList.deepCopy(); + ret.setConstantList((ConstantList) constantList.deepCopy()); + n = getNumProperties(); + for (i = 0; i < n; i++) { + ret.addProperty((Property) getPropertyObject(i).deepCopy()); + } + // Copy other (generated) info + ret.allIdentsUsed = (allIdentsUsed == null) ? null : (Vector)allIdentsUsed.clone(); + ret.constantValues = (constantValues == null) ? null : new Values(constantValues); + + return ret; } } diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java new file mode 100644 index 00000000..1ec99da4 --- /dev/null +++ b/prism/src/parser/ast/Property.java @@ -0,0 +1,245 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// 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 +// +//============================================================================== + +package parser.ast; + +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import parser.type.*; +import parser.visitor.*; +import prism.PrismException; +import prism.PrismLangException; +import prism.PrismUtils; + +/** + * PRISM property, i.e. a PRISM expression plus other (optional info) such as name, comment, etc. + */ +public class Property extends ASTElement +{ + /** PRISM expression representing property */ + private Expression expr; + /** Optional name for property (null if absent); */ + private String name; + /** Optional comment for property (null if absent); */ + private String comment; + + // Constructors + + public Property(Expression expr) + { + this(expr, null, null); + } + + public Property(Expression expr, String name) + { + this(expr, name, null); + } + + public Property(Expression expr, String name, String comment) + { + this.expr = expr; + this.name = name; + this.comment = comment; + } + + // Mutators + + public void setExpression(Expression expr) + { + this.expr = expr; + } + + public void setName(String name) + { + this.name = name; + } + + public void setComment(String comment) + { + this.comment = comment; + } + + // Accessors + + public Expression getExpression() + { + return expr; + } + + public String getName() + { + return name; + } + + public String getComment() + { + return comment; + } + + /** + * Tests a result (specified as an object of the appropriate type: Boolean, Double, etc.) + * against the expected result for this Property, specified by an embedded "RESULT: xxx" + * string in the accompanying comment (immediately preceding it in the property specification). + * If the test fails or something else goes wrong, an explanatory PrismException is thrown. + * Otherwise, the method successfully exits, returning a boolean value that indicates + * whether or not a check was actually applied (i.e. if the result specification is of the + * form "RESULT: ?") then false is returned; otherwise true. + * @param result The actual result + * @return Whether or not the check was performed + */ + public boolean checkAgainstExpectedResult(Object result) throws PrismException + { + String strExpected = null; + Type type; + + // Extract expected result from comment + if (comment != null) { + Pattern p = Pattern.compile("RESULT:[ \t]*([^ \t\n\r]+)"); + Matcher matcher = p.matcher(comment); + if (matcher.find()) + strExpected = matcher.group(1); + if (matcher.find()) + throw new PrismException("Multiple RESULT specificiations for test"); + } + if (strExpected == null) { + throw new PrismException("Did not find RESULT specification to test against"); + } + + // Check for special "don't case" case + if (strExpected.equals("?")) { + return false; + } + + // Check expected/actual result + type = expr.getType(); + + // Boolean-valued properties + if (type instanceof TypeBool) { + // Parse expected result + boolean boolExp; + strExpected = strExpected.toLowerCase(); + if (strExpected.equals("true")) + boolExp = true; + else if (strExpected.equals("false")) + boolExp = false; + else + throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for boolean-valued property"); + // Parse actual result + boolean boolRes; + if (!(result instanceof Boolean)) + throw new PrismException("Result is wrong type for (boolean-valued) property"); + boolRes = ((Boolean) result).booleanValue(); + if (boolRes != boolExp) + throw new PrismException("Wrong result (expected " + boolExp + ")"); + } + + // Integer-valued properties + else if (type instanceof TypeInt) { + // Parse expected result + int intExp; + try { + intExp = Integer.parseInt(strExpected); + } catch (NumberFormatException e) { + throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for integer-valued property"); + } + // Parse actual result + int intRes; + if (!(result instanceof Integer)) + throw new PrismException("Result is wrong type for (integer-valued) property"); + intRes = ((Integer) result).intValue(); + if (intRes != intExp) + throw new PrismException("Wrong result (expected " + intExp + ")"); + } + + // Double-valued properties + else if (type instanceof TypeDouble) { + // Parse expected result + double doubleExp; + try { + // See if it's a fraction + if (strExpected.matches("[0-9]+/[0-9]+")) { + int numer = Integer.parseInt(strExpected.substring(0, strExpected.indexOf('/'))); + int denom = Integer.parseInt(strExpected.substring(strExpected.indexOf('/') + 1)); + doubleExp = ((double) numer) / denom; + } + // Otherwise, just a double + else { + doubleExp = Double.parseDouble(strExpected); + } + } catch (NumberFormatException e) { + throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for double-valued property"); + } + // Parse actual result + double doubleRes; + if (!(result instanceof Double)) + throw new PrismException("Result is wrong type for (double-valued) property"); + doubleRes = ((Double) result).doubleValue(); + if (!PrismUtils.doublesAreCloseRel(doubleRes, doubleExp, 1e-5)) + throw new PrismException("Wrong result (expected " + doubleExp + ")"); + } + + // Unknown type + else { + throw new PrismException("Don't know how to test properties of type " + type); + } + + return true; + } + + // Methods required for ASTElement: + + /** + * Visitor method. + */ + public Object accept(ASTVisitor v) throws PrismLangException + { + return v.visit(this); + } + + @Override + public String toString() + { + // Note: don't print comment + String s = ""; + //if (comment != null) + //s += PrismParser.slashCommentBlock(comment); + if (name != null) + s += "\"" + name + "\": "; + s += expr; + return s; + } + + @Override + public Property deepCopy() + { + Property prop = new Property(expr, name, comment); + prop.setPosition(this); + return prop; + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 811ea2c3..08eba4a2 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -76,13 +76,23 @@ public class ASTTraverse implements ASTVisitor if (e.getConstantList() != null) e.getConstantList().accept(this); n = e.getNumProperties(); for (i = 0; i < n; i++) { - if (e.getProperty(i) != null) e.getProperty(i).accept(this); + if (e.getPropertyObject(i) != null) e.getPropertyObject(i).accept(this); } visitPost(e); return null; } public void visitPost(PropertiesFile e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(Property e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(Property e) throws PrismLangException + { + visitPre(e); + if (e.getExpression() != null) e.getExpression().accept(this); + visitPost(e); + return null; + } + public void visitPost(Property e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(FormulaList e) throws PrismLangException { defaultVisitPre(e); } public Object visit(FormulaList e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index ed940797..17b319cd 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -77,12 +77,33 @@ public class ASTTraverseModify implements ASTVisitor if (e.getConstantList() != null) e.setConstantList((ConstantList)(e.getConstantList().accept(this))); n = e.getNumProperties(); for (i = 0; i < n; i++) { - if (e.getProperty(i) != null) e.setProperty(i, (Expression)(e.getProperty(i).accept(this))); + if (e.getPropertyObject(i) != null) e.setPropertyObject(i, (Property)(e.getPropertyObject(i).accept(this))); } visitPost(e); return e; } public void visitPost(PropertiesFile e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- + + public void visitPre(Property e) throws PrismLangException + { + defaultVisitPre(e); + } + + public Object visit(Property e) throws PrismLangException + { + visitPre(e); + if (e.getExpression() != null) + e.setExpression((Expression) e.getExpression().accept(this)); + visitPost(e); + return e; + } + + public void visitPost(Property e) throws PrismLangException + { + defaultVisitPost(e); + } + // ----------------------------------------------------------------------------------- public void visitPre(FormulaList e) throws PrismLangException { defaultVisitPre(e); } public Object visit(FormulaList e) throws PrismLangException diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index 0f6fe0e3..c833454c 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/prism/src/parser/visitor/ASTVisitor.java @@ -34,6 +34,7 @@ public interface ASTVisitor // ASTElement classes (model/properties file) public Object visit(ModulesFile e) throws PrismLangException; public Object visit(PropertiesFile e) throws PrismLangException; + public Object visit(Property e) throws PrismLangException; public Object visit(FormulaList e) throws PrismLangException; public Object visit(LabelList e) throws PrismLangException; public Object visit(ConstantList e) throws PrismLangException; diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 61103478..4a76f88f 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -46,6 +46,11 @@ public class TypeCheck extends ASTTraverse } } + public void visitPost(Property e) throws PrismLangException + { + e.setType(e.getExpression().getType()); + } + public void visitPost(FormulaList e) throws PrismLangException { // Formulas are defined at the text level and are type checked after diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 69e16426..d25919a9 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -73,6 +73,7 @@ public class PrismCL private boolean explicitbuild = false; private boolean explicitbuildtest = false; private boolean nobuild = false; + private boolean test = false; // property info private int propertyToCheck = -1; @@ -122,7 +123,7 @@ public class PrismCL // info about which properties to model check private int numPropertiesToCheck = 0; - private Expression propertiesToCheck[] = null; + private List propertiesToCheck = null; // info about undefined constants private UndefinedConstants undefinedConstants; @@ -197,7 +198,7 @@ public class PrismCL // initialise storage for results results = new ResultsCollection[numPropertiesToCheck]; for (i = 0; i < numPropertiesToCheck; i++) { - results[i] = new ResultsCollection(undefinedConstants, propertiesToCheck[i].getResultName()); + results[i] = new ResultsCollection(undefinedConstants, propertiesToCheck.get(i).getExpression().getResultName()); } // iterate through as many models as necessary @@ -328,13 +329,13 @@ public class PrismCL if (simulate && undefinedConstants.getNumPropertyIterations() > 1) { try { mainLog.println("\n-------------------------------------------"); - mainLog.println("\nSimulating: " + propertiesToCheck[j]); + mainLog.println("\nSimulating: " + propertiesToCheck.get(j)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString()); - simMethod = processSimulationOptions(propertiesToCheck[j]); - prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results[j], propertiesToCheck[j], null, + simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); + prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results[j], propertiesToCheck.get(j).getExpression(), null, simMaxPath, simMethod); } catch (PrismException e) { // in case of (overall) error, report it, store as result for property, and proceed @@ -363,7 +364,7 @@ public class PrismCL // log output mainLog.println("\n-------------------------------------------"); - mainLog.println("\n" + (simulate ? "Simulating" : "Model checking") + ": " + propertiesToCheck[j]); + mainLog.println("\n" + (simulate ? "Simulating" : "Model checking") + ": " + propertiesToCheck.get(j)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); @@ -375,7 +376,7 @@ public class PrismCL if (modulesFile.getModelType() == ModelType.PTA && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { DigitalClocks dc = new DigitalClocks(prism); - dc.translate(modulesFile, propertiesFile, propertiesToCheck[j]); + dc.translate(modulesFile, propertiesFile, propertiesToCheck.get(j).getExpression()); modulesFileToCheck = dc.getNewModulesFile(); modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); doPrismLangExports(modulesFileToCheck); @@ -388,21 +389,21 @@ public class PrismCL if (!simulate) { // PTA model checking if (modulesFileToCheck.getModelType() == ModelType.PTA) { - res = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertiesToCheck[j]); + res = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertiesToCheck.get(j).getExpression()); } // Non-PTA model checking else { if (!explicit) { - res = prism.modelCheck(model, propertiesFile, propertiesToCheck[j]); + res = prism.modelCheck(model, propertiesFile, propertiesToCheck.get(j).getExpression()); } else { - res = prismExpl.modelCheck(modelExpl, modulesFileToCheck, propertiesFile, propertiesToCheck[j]); + res = prismExpl.modelCheck(modelExpl, modulesFileToCheck, propertiesFile, propertiesToCheck.get(j).getExpression()); } } } // approximate (simulation-based) model checking else { - simMethod = processSimulationOptions(propertiesToCheck[j]); - res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertiesToCheck[j], null, simMaxPath, simMethod); + simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); + res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertiesToCheck.get(j).getExpression(), null, simMaxPath, simMethod); simMethod.reset(); } } catch (PrismException e) { @@ -422,6 +423,20 @@ public class PrismCL error("Problem storing results"); } + // if required, check result against expected value + if (test) { + try { + if (propertiesToCheck.get(j).checkAgainstExpectedResult(res.getResult())) { + mainLog.println("Testing result: PASS"); + } else { + mainLog.println("Testing result: NOT TESTED"); + } + } catch (PrismException e) { + mainLog.println("Testing result: FAIL: " + e.getMessage()); + errorAndExit("Testing failed"); + } + } + // iterate to next property undefinedConstants.iterateProperty(); } @@ -452,7 +467,7 @@ public class PrismCL for (i = 0; i < numPropertiesToCheck; i++) { if (i > 0) tmpLog.println(); - tmpLog.print(propertiesToCheck[i] + ":\n" + results[i].toString(false, " ", " ")); + tmpLog.print(propertiesToCheck.get(i) + ":\n" + results[i].toString(false, " ", " ")); } tmpLog.close(); } @@ -565,25 +580,24 @@ public class PrismCL { int i; + propertiesToCheck = new ArrayList(); + // no properties to check if (propertiesFile == null) { numPropertiesToCheck = 0; - propertiesToCheck = null; } // unless specified, verify all properties else if (propertyToCheck == -1) { numPropertiesToCheck = propertiesFile.getNumProperties(); - propertiesToCheck = new Expression[numPropertiesToCheck]; for (i = 0; i < numPropertiesToCheck; i++) { - propertiesToCheck[i] = propertiesFile.getProperty(i); + propertiesToCheck.add(propertiesFile.getPropertyObject(i)); } } // otherwise just verify the relevant property else { if (propertyToCheck > 0 && propertyToCheck <= propertiesFile.getNumProperties()) { numPropertiesToCheck = 1; - propertiesToCheck = new Expression[1]; - propertiesToCheck[0] = propertiesFile.getProperty(propertyToCheck - 1); + propertiesToCheck.add(propertiesFile.getPropertyObject(propertyToCheck - 1)); } else { errorAndExit("There is not a property " + propertyToCheck + " to verify"); } @@ -1065,6 +1079,10 @@ public class PrismCL else if (sw.equals("nobuild")) { nobuild = true; } + // enable "testing" mode + else if (sw.equals("test")) { + test = true; + } // IMPORT OPTIONS: @@ -1754,6 +1772,7 @@ public class PrismCL mainLog.println("-transient (or -tr ) .... Compute transient probabilities for time (D/CTMCs only)"); mainLog.println("-simpath ....... Generate a random path with the simulator"); mainLog.println("-nobuild ....................... Skip model construction (just do parse/export)"); + mainLog.println("-test .......................... Enable \"test\" mode"); mainLog.println(); mainLog.println("IMPORT OPTIONS:"); mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language"); @@ -1827,6 +1846,11 @@ public class PrismCL private void error(String s) { + // If (and only if) we are in "test" mode, treat any error as fatal + if (test) { + errorAndExit(s); + } + // Normal case: just display error message, but don't exit mainLog.println("\nError: " + s + "."); } @@ -1835,7 +1859,7 @@ public class PrismCL private void errorAndExit(String s) { prism.closeDown(false); - error(s); + mainLog.println("\nError: " + s + "."); System.exit(1); }