From 1cbbcbc0a4195244724081fb13349dd5e9817514 Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:01 +0200 Subject: [PATCH 1/7] adjusting parser + adding cyclic dependency check to support labels inside labels --- prism/src/parser/ParseException.java | 6 +- prism/src/parser/PrismParser.java | 352 +++++++++++------------ prism/src/parser/PrismParser.jj | 8 +- prism/src/parser/ast/LabelList.java | 34 ++- prism/src/parser/ast/ModulesFile.java | 4 + prism/src/parser/ast/PropertiesFile.java | 4 + 6 files changed, 222 insertions(+), 186 deletions(-) diff --git a/prism/src/parser/ParseException.java b/prism/src/parser/ParseException.java index 839bcc2939..1d220a5f93 100644 --- a/prism/src/parser/ParseException.java +++ b/prism/src/parser/ParseException.java @@ -122,9 +122,7 @@ private static String initialise(Token currentToken, retval += " \""; tok = tok.next; } - if (currentToken.next != null) { - retval += "\" at line " + currentToken.next.beginLine + ", column " + currentToken.next.beginColumn; - } + retval += "\" at line " + currentToken.next.beginLine + ", column " + currentToken.next.beginColumn; retval += "." + EOL; @@ -192,4 +190,4 @@ static String add_escapes(String str) { } } -/* JavaCC - OriginalChecksum=8dbcceed9d408427f9932dcf43e59aaa (do not edit this line) */ +/* JavaCC - OriginalChecksum=498e95145a190935df56665f42563744 (do not edit this line) */ diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 3caebbf460..be28778cb8 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -2626,6 +2626,10 @@ static class ExpressionPair { public Expression expr1 = null; public Expression ret = ExpressionParenth(prop, pathprop); break; } + case DQUOTE:{ + ret = ExpressionLabel(prop, pathprop); + break; + } case PMAXMAX: case PMAXMIN: case PMAX: @@ -2664,10 +2668,6 @@ static class ExpressionPair { public Expression expr1 = null; public Expression ret = ExpressionStrategy(prop, pathprop); break; } - case DQUOTE:{ - ret = ExpressionLabel(prop, pathprop); - break; - } case FILTER:{ ret = ExpressionFilter(prop, pathprop); break; @@ -3837,8 +3837,8 @@ static class ExpressionPair { public Expression expr1 = null; public Expression Expression ExpressionLabel(boolean prop, boolean pathprop) throws ParseException {String s; ExpressionLabel ret = null; Token begin; -if (!prop) {if (true) throw generateParseException();} - begin = jj_consume_token(DQUOTE); + // Label can be arbitary string or the "init" keyword + begin = jj_consume_token(DQUOTE); switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { case REG_IDENT:{ s = Identifier(); @@ -4215,7 +4215,7 @@ static private boolean jj_2_18(int xla) finally { jj_save(17, xla); } } - static private boolean jj_3R_ExpressionStrategy_1897_11_186() + static private boolean jj_3R_ExpressionStrategy_1897_11_188() { if (jj_3R_ExpressionParenth_1577_9_147()) return true; return false; @@ -4224,9 +4224,9 @@ static private boolean jj_3R_ExpressionStrategy_1897_11_186() static private boolean jj_3R_SystemHideRename_1130_11_82() { if (jj_scan_token(LBRACE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(RENAME)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -4266,7 +4266,7 @@ static private boolean jj_3R_ExpressionFuncOldStyle_1515_9_146() static private boolean jj_3R_ExpressionStrategy_1895_11_223() { - if (jj_3R_ExpressionProb_1618_9_148()) return true; + if (jj_3R_ExpressionProb_1618_9_149()) return true; return false; } @@ -4276,7 +4276,7 @@ static private boolean jj_3_4() return false; } - static private boolean jj_3R_ExpressionStrategy_1895_9_185() + static private boolean jj_3R_ExpressionStrategy_1895_9_187() { Token xsp; xsp = jj_scanpos; @@ -4287,7 +4287,7 @@ static private boolean jj_3R_ExpressionStrategy_1895_9_185() return false; } - static private boolean jj_3R_ExpressionStrategy_1892_11_184() + static private boolean jj_3R_ExpressionStrategy_1892_11_186() { if (jj_scan_token(DLBRACKET)) return true; if (jj_3R_ExpressionStrategyCoalition_1914_9_222()) return true; @@ -4301,7 +4301,7 @@ static private boolean jj_3R_RewardIndex_1800_101_245() return false; } - static private boolean jj_3R_ExpressionStrategy_1891_10_183() + static private boolean jj_3R_ExpressionStrategy_1891_10_185() { if (jj_scan_token(DLT)) return true; if (jj_3R_ExpressionStrategyCoalition_1914_9_222()) return true; @@ -4320,7 +4320,7 @@ static private boolean jj_3R_SystemHideRename_1124_9_81() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -4341,18 +4341,18 @@ static private boolean jj_3R_SystemHideRename_1124_9_70() return false; } - static private boolean jj_3R_ExpressionStrategy_1888_9_152() + static private boolean jj_3R_ExpressionStrategy_1888_9_153() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionStrategy_1891_10_183()) { + if (jj_3R_ExpressionStrategy_1891_10_185()) { jj_scanpos = xsp; - if (jj_3R_ExpressionStrategy_1892_11_184()) return true; + if (jj_3R_ExpressionStrategy_1892_11_186()) return true; } xsp = jj_scanpos; - if (jj_3R_ExpressionStrategy_1895_9_185()) { + if (jj_3R_ExpressionStrategy_1895_9_187()) { jj_scanpos = xsp; - if (jj_3R_ExpressionStrategy_1897_11_186()) return true; + if (jj_3R_ExpressionStrategy_1897_11_188()) return true; } return false; } @@ -4426,14 +4426,14 @@ static private boolean jj_3_10() static private boolean jj_3R_ExpressionFuncOrIdent_1486_9_144() { - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; Token xsp; xsp = jj_scanpos; if (jj_3R_ExpressionFuncOrIdent_1488_11_159()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_ExpressionForAll_1869_9_151() + static private boolean jj_3R_ExpressionForAll_1869_9_152() { if (jj_scan_token(A)) return true; if (jj_scan_token(LBRACKET)) return true; @@ -4446,7 +4446,7 @@ static private boolean jj_3R_SystemParallel_1095_11_60() { if (jj_scan_token(OR)) return true; if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -4469,23 +4469,23 @@ static private boolean jj_3R_SystemParallel_1093_9_50() static private boolean jj_3R_ExpressionBasic_1464_17_142() { - if (jj_3R_ExpressionFilter_1960_9_154()) return true; + if (jj_3R_ExpressionFilter_1958_9_154()) return true; return false; } static private boolean jj_3R_ExpressionBasic_1462_17_141() { - if (jj_3R_ExpressionLabel_1942_9_153()) return true; + if (jj_3R_ExpressionStrategy_1888_9_153()) return true; return false; } static private boolean jj_3R_ExpressionBasic_1460_17_140() { - if (jj_3R_ExpressionStrategy_1888_9_152()) return true; + if (jj_3R_ExpressionForAll_1869_9_152()) return true; return false; } - static private boolean jj_3R_ExpressionExists_1850_9_150() + static private boolean jj_3R_ExpressionExists_1850_9_151() { if (jj_scan_token(E)) return true; if (jj_scan_token(LBRACKET)) return true; @@ -4496,13 +4496,13 @@ static private boolean jj_3R_ExpressionExists_1850_9_150() static private boolean jj_3R_ExpressionBasic_1458_17_139() { - if (jj_3R_ExpressionForAll_1869_9_151()) return true; + if (jj_3R_ExpressionExists_1850_9_151()) return true; return false; } static private boolean jj_3R_ExpressionBasic_1456_17_138() { - if (jj_3R_ExpressionExists_1850_9_150()) return true; + if (jj_3R_ExpressionReward_1741_9_150()) return true; return false; } @@ -4514,13 +4514,13 @@ static private boolean jj_3R_ExpressionTimesDivide_1408_64_128() static private boolean jj_3R_ExpressionBasic_1454_17_137() { - if (jj_3R_ExpressionReward_1741_9_149()) return true; + if (jj_3R_ExpressionSS_1697_9_34()) return true; return false; } static private boolean jj_3R_ExpressionBasic_1452_17_136() { - if (jj_3R_ExpressionSS_1697_9_34()) return true; + if (jj_3R_ExpressionProb_1618_9_149()) return true; return false; } @@ -4531,9 +4531,9 @@ static private boolean jj_3_18() return false; } - static private boolean jj_3R_ExpressionBasic_1450_17_135() + static private boolean jj_3R_ExpressionBasic_1449_17_135() { - if (jj_3R_ExpressionProb_1618_9_148()) return true; + if (jj_3R_ExpressionLabel_1942_9_148()) return true; return false; } @@ -4624,7 +4624,7 @@ static private boolean jj_3R_ExpressionRewardContents_1827_11_217() return false; } - static private boolean jj_3R_ExpressionReward_1769_69_182() + static private boolean jj_3R_ExpressionReward_1769_69_184() { if (jj_3R_Filter_1673_9_48()) return true; return false; @@ -4645,7 +4645,7 @@ static private boolean jj_3R_ExpressionRewardContents_1826_9_216() static private boolean jj_3_2() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; if (jj_scan_token(COLON)) return true; return false; @@ -4654,12 +4654,12 @@ static private boolean jj_3_2() static private boolean jj_3R_RewardIndex_1800_33_244() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_ExpressionRewardContents_1823_9_181() + static private boolean jj_3R_ExpressionRewardContents_1823_9_183() { Token xsp; xsp = jj_scanpos; @@ -4696,7 +4696,7 @@ static private boolean jj_3R_ExpressionBasic_1438_9_129() jj_scanpos = xsp; if (jj_3R_ExpressionBasic_1447_17_134()) { jj_scanpos = xsp; - if (jj_3R_ExpressionBasic_1450_17_135()) { + if (jj_3R_ExpressionBasic_1449_17_135()) { jj_scanpos = xsp; if (jj_3R_ExpressionBasic_1452_17_136()) { jj_scanpos = xsp; @@ -4759,7 +4759,7 @@ static private boolean jj_3R_SystemFullParallel_1046_9_36() static private boolean jj_3R_RewardIndex_1798_22_240() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } @@ -4831,7 +4831,7 @@ static private boolean jj_3R_RewardIndex_1798_9_231() static private boolean jj_3_7() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; if (jj_3R_SystemDefn_1033_9_32()) return true; return false; @@ -4900,7 +4900,7 @@ static private boolean jj_3R_ExpressionReward_1752_26_235() return false; } - static private boolean jj_3R_ExpressionReward_1767_10_180() + static private boolean jj_3R_ExpressionReward_1767_10_182() { if (jj_scan_token(RMAXMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -4924,7 +4924,7 @@ static private boolean jj_3R_ExpressionReward_1759_17_215() return false; } - static private boolean jj_3R_ExpressionReward_1766_10_179() + static private boolean jj_3R_ExpressionReward_1766_10_181() { if (jj_scan_token(RMAXMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -4948,7 +4948,7 @@ static private boolean jj_3R_ExpressionReward_1758_17_214() return false; } - static private boolean jj_3R_ExpressionReward_1765_10_178() + static private boolean jj_3R_ExpressionReward_1765_10_180() { if (jj_scan_token(RMINMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -4971,7 +4971,7 @@ static private boolean jj_3R_ExpressionReward_1757_17_213() return false; } - static private boolean jj_3R_ExpressionReward_1764_10_177() + static private boolean jj_3R_ExpressionReward_1764_10_179() { if (jj_scan_token(RMINMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -4987,7 +4987,7 @@ static private boolean jj_3R_ExpressionReward_1756_17_212() return false; } - static private boolean jj_3R_ExpressionReward_1763_10_176() + static private boolean jj_3R_ExpressionReward_1763_10_178() { if (jj_scan_token(RMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -4995,7 +4995,7 @@ static private boolean jj_3R_ExpressionReward_1763_10_176() return false; } - static private boolean jj_3R_ExpressionReward_1762_10_175() + static private boolean jj_3R_ExpressionReward_1762_10_177() { if (jj_scan_token(RMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5042,7 +5042,7 @@ static private boolean jj_3R_ExpressionReward_1747_17_209() static private boolean jj_3R_ExpressionReward_1746_18_208() { - if (jj_3R_LtGt_2048_9_46()) return true; + if (jj_3R_LtGt_2046_9_46()) return true; if (jj_3R_Expression_1176_9_39()) return true; return false; } @@ -5056,14 +5056,14 @@ static private boolean jj_3R_ExpressionReward_1745_18_207() static private boolean jj_3R_ExpressionReward_1744_19_206() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } static private boolean jj_3R_ExpressionRelop_1369_11_115() { - if (jj_3R_LtGt_2048_9_46()) return true; + if (jj_3R_LtGt_2046_9_46()) return true; if (jj_3R_ExpressionPlusMinus_1389_9_114()) return true; return false; } @@ -5085,7 +5085,7 @@ static private boolean jj_3R_ExpressionSS_1705_55_40() return false; } - static private boolean jj_3R_ExpressionReward_1743_10_174() + static private boolean jj_3R_ExpressionReward_1743_10_176() { if (jj_scan_token(R)) return true; Token xsp; @@ -5119,23 +5119,23 @@ static private boolean jj_3R_ExpressionReward_1743_10_174() return false; } - static private boolean jj_3R_ExpressionReward_1741_9_149() + static private boolean jj_3R_ExpressionReward_1741_9_150() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionReward_1743_10_174()) { + if (jj_3R_ExpressionReward_1743_10_176()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1762_10_175()) { + if (jj_3R_ExpressionReward_1762_10_177()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1763_10_176()) { + if (jj_3R_ExpressionReward_1763_10_178()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1764_10_177()) { + if (jj_3R_ExpressionReward_1764_10_179()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1765_10_178()) { + if (jj_3R_ExpressionReward_1765_10_180()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1766_10_179()) { + if (jj_3R_ExpressionReward_1766_10_181()) { jj_scanpos = xsp; - if (jj_3R_ExpressionReward_1767_10_180()) return true; + if (jj_3R_ExpressionReward_1767_10_182()) return true; } } } @@ -5143,16 +5143,16 @@ static private boolean jj_3R_ExpressionReward_1741_9_149() } } if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_ExpressionRewardContents_1823_9_181()) return true; + if (jj_3R_ExpressionRewardContents_1823_9_183()) return true; xsp = jj_scanpos; - if (jj_3R_ExpressionReward_1769_69_182()) jj_scanpos = xsp; + if (jj_3R_ExpressionReward_1769_69_184()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } static private boolean jj_3R_ExpressionEquality_1355_11_113() { - if (jj_3R_EqNeq_2038_9_116()) return true; + if (jj_3R_EqNeq_2036_9_116()) return true; if (jj_3R_ExpressionRelop_1368_9_112()) return true; return false; } @@ -5171,7 +5171,7 @@ static private boolean jj_3R_ExpressionEquality_1354_9_111() static private boolean jj_3_1() { if (jj_scan_token(MODULE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(EQ)) return true; return false; } @@ -5240,7 +5240,7 @@ static private boolean jj_3R_ExpressionSS_1702_17_38() static private boolean jj_3R_ExpressionSS_1700_19_45() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -5257,7 +5257,7 @@ static private boolean jj_3R_ExpressionSS_1700_17_37() Token xsp; xsp = jj_scanpos; if (jj_3R_ExpressionSS_1700_19_45()) jj_scanpos = xsp; - if (jj_3R_LtGt_2048_9_46()) return true; + if (jj_3R_LtGt_2046_9_46()) return true; if (jj_3R_Expression_1176_9_39()) return true; return false; } @@ -5315,7 +5315,7 @@ static private boolean jj_3R_Update_896_36_42() return false; } - static private boolean jj_3R_ExpressionProb_1644_51_173() + static private boolean jj_3R_ExpressionProb_1644_51_175() { if (jj_3R_Filter_1673_9_48()) return true; return false; @@ -5367,7 +5367,7 @@ static private boolean jj_3R_Filter_1674_11_58() static private boolean jj_3R_UpdateElement_909_9_41() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierPrime_2020_9_49()) return true; + if (jj_3R_IdentifierPrime_2018_9_49()) return true; if (jj_scan_token(EQ)) return true; if (jj_3R_Expression_1176_9_39()) return true; if (jj_scan_token(RPARENTH)) return true; @@ -5405,58 +5405,58 @@ static private boolean jj_3R_ExpressionImplies_1285_9_83() return false; } - static private boolean jj_3R_LtGt_2051_9_55() + static private boolean jj_3R_LtGt_2049_9_55() { if (jj_scan_token(LE)) return true; return false; } - static private boolean jj_3R_LtGt_2050_9_54() + static private boolean jj_3R_LtGt_2048_9_54() { if (jj_scan_token(GE)) return true; return false; } - static private boolean jj_3R_LtGt_2049_9_53() + static private boolean jj_3R_LtGt_2047_9_53() { if (jj_scan_token(LT)) return true; return false; } - static private boolean jj_3R_LtGt_2048_9_52() + static private boolean jj_3R_Update_896_10_35() + { + if (jj_3R_UpdateElement_909_9_41()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_Update_896_36_42()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_LtGt_2046_9_52() { if (jj_scan_token(GT)) return true; return false; } - static private boolean jj_3R_LtGt_2048_9_46() + static private boolean jj_3R_LtGt_2046_9_46() { Token xsp; xsp = jj_scanpos; - if (jj_3R_LtGt_2048_9_52()) { + if (jj_3R_LtGt_2046_9_52()) { jj_scanpos = xsp; - if (jj_3R_LtGt_2049_9_53()) { + if (jj_3R_LtGt_2047_9_53()) { jj_scanpos = xsp; - if (jj_3R_LtGt_2050_9_54()) { + if (jj_3R_LtGt_2048_9_54()) { jj_scanpos = xsp; - if (jj_3R_LtGt_2051_9_55()) return true; + if (jj_3R_LtGt_2049_9_55()) return true; } } } return false; } - static private boolean jj_3R_Update_896_10_35() - { - if (jj_3R_UpdateElement_909_9_41()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_Update_896_36_42()) { jj_scanpos = xsp; break; } - } - return false; - } - static private boolean jj_3R_ExpressionITE_1271_17_84() { if (jj_scan_token(QMARK)) return true; @@ -5479,61 +5479,61 @@ static private boolean jj_3R_Update_894_9_31() static private boolean jj_3_14() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_13() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_12() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } static private boolean jj_3_11() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3R_EqNeq_2039_9_120() + static private boolean jj_3R_EqNeq_2037_9_120() { if (jj_scan_token(NE)) return true; return false; } - static private boolean jj_3R_EqNeq_2038_9_116() + static private boolean jj_3_5() + { + if (jj_3R_Update_894_9_31()) return true; + return false; + } + + static private boolean jj_3R_EqNeq_2036_9_116() { Token xsp; xsp = jj_scanpos; - if (jj_3R_EqNeq_2038_9_119()) { + if (jj_3R_EqNeq_2036_9_119()) { jj_scanpos = xsp; - if (jj_3R_EqNeq_2039_9_120()) return true; + if (jj_3R_EqNeq_2037_9_120()) return true; } return false; } - static private boolean jj_3R_EqNeq_2038_9_119() + static private boolean jj_3R_EqNeq_2036_9_119() { if (jj_scan_token(EQ)) return true; return false; } - static private boolean jj_3_5() - { - if (jj_3R_Update_894_9_31()) return true; - return false; - } - static private boolean jj_3R_ExpressionITE_1269_9_76() { if (jj_3R_ExpressionImplies_1285_9_83()) return true; @@ -5545,19 +5545,19 @@ static private boolean jj_3R_ExpressionITE_1269_9_76() static private boolean jj_3R_TimeBound_1255_20_101() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; return false; } static private boolean jj_3R_TimeBound_1254_20_99() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; return false; } static private boolean jj_3R_TimeBound_1253_20_97() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; return false; } @@ -5571,7 +5571,7 @@ static private boolean jj_3R_ExpressionProb_1629_26_230() static private boolean jj_3R_TimeBound_1252_20_95() { - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; return false; } @@ -5590,7 +5590,7 @@ static private boolean jj_3R_ExpressionProb_1627_26_228() return false; } - static private boolean jj_3R_ExpressionProb_1642_10_172() + static private boolean jj_3R_ExpressionProb_1642_10_174() { if (jj_scan_token(PMAXMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -5614,7 +5614,7 @@ static private boolean jj_3R_ExpressionProb_1634_17_205() return false; } - static private boolean jj_3R_ExpressionProb_1641_10_171() + static private boolean jj_3R_ExpressionProb_1641_10_173() { if (jj_scan_token(PMAXMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5645,7 +5645,7 @@ static private boolean jj_3R_ExpressionProb_1633_17_204() return false; } - static private boolean jj_3R_ExpressionProb_1640_10_170() + static private boolean jj_3R_ExpressionProb_1640_10_172() { if (jj_scan_token(PMINMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -5678,7 +5678,7 @@ static private boolean jj_3R_ExpressionProb_1632_17_203() return false; } - static private boolean jj_3R_ExpressionProb_1639_10_169() + static private boolean jj_3R_ExpressionProb_1639_10_171() { if (jj_scan_token(PMINMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5706,7 +5706,7 @@ static private boolean jj_3R_ExpressionProb_1631_17_202() return false; } - static private boolean jj_3R_ExpressionProb_1638_10_168() + static private boolean jj_3R_ExpressionProb_1638_10_170() { if (jj_scan_token(PMAX)) return true; if (jj_scan_token(EQ)) return true; @@ -5726,7 +5726,7 @@ static private boolean jj_3R_TimeBound_1254_11_87() return false; } - static private boolean jj_3R_ExpressionProb_1637_10_167() + static private boolean jj_3R_ExpressionProb_1637_10_169() { if (jj_scan_token(PMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -5748,7 +5748,7 @@ static private boolean jj_3R_TimeBound_1253_11_86() static private boolean jj_3R_ExpressionProb_1621_25_198() { - if (jj_3R_LtGt_2048_9_46()) return true; + if (jj_3R_LtGt_2046_9_46()) return true; if (jj_3R_Expression_1176_9_39()) return true; return false; } @@ -5756,7 +5756,7 @@ static private boolean jj_3R_ExpressionProb_1621_25_198() static private boolean jj_3R_ExpressionProb_1620_26_197() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_IdentifierExpression_1998_9_33()) return true; + if (jj_3R_IdentifierExpression_1996_9_33()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -5773,12 +5773,6 @@ static private boolean jj_3R_TimeBound_1252_11_85() return false; } - static private boolean jj_3R_IdentifierPrime_2020_9_49() - { - if (jj_scan_token(REG_IDENTPRIME)) return true; - return false; - } - static private boolean jj_3R_ExpressionProb_1627_17_201() { if (jj_scan_token(MAX)) return true; @@ -5817,6 +5811,12 @@ static private boolean jj_3R_TimeBound_1252_9_77() return false; } + static private boolean jj_3R_IdentifierPrime_2018_9_49() + { + if (jj_scan_token(REG_IDENTPRIME)) return true; + return false; + } + static private boolean jj_3R_ExpressionProb_1623_17_200() { if (jj_scan_token(MIN)) return true; @@ -5839,15 +5839,15 @@ static private boolean jj_3R_ExpressionProb_1622_17_199() return false; } - static private boolean jj_3R_ExpressionFilter_1966_56_193() + static private boolean jj_3R_ExpressionTemporalUnary_1239_17_62() { - if (jj_scan_token(OR)) return true; + if (jj_3R_ExpressionITE_1269_9_76()) return true; return false; } - static private boolean jj_3R_ExpressionTemporalUnary_1239_17_62() + static private boolean jj_3R_ExpressionFilter_1964_56_193() { - if (jj_3R_ExpressionITE_1269_9_76()) return true; + if (jj_scan_token(OR)) return true; return false; } @@ -5875,7 +5875,7 @@ static private boolean jj_3R_ExpressionTemporalUnary_1232_19_72() return false; } - static private boolean jj_3R_ExpressionProb_1620_10_166() + static private boolean jj_3R_ExpressionProb_1620_10_168() { if (jj_scan_token(P)) return true; Token xsp; @@ -5924,23 +5924,23 @@ static private boolean jj_3R_ExpressionTemporalUnary_1230_17_61() return false; } - static private boolean jj_3R_ExpressionProb_1618_9_148() + static private boolean jj_3R_ExpressionProb_1618_9_149() { Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionProb_1620_10_166()) { + if (jj_3R_ExpressionProb_1620_10_168()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1637_10_167()) { + if (jj_3R_ExpressionProb_1637_10_169()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1638_10_168()) { + if (jj_3R_ExpressionProb_1638_10_170()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1639_10_169()) { + if (jj_3R_ExpressionProb_1639_10_171()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1640_10_170()) { + if (jj_3R_ExpressionProb_1640_10_172()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1641_10_171()) { + if (jj_3R_ExpressionProb_1641_10_173()) { jj_scanpos = xsp; - if (jj_3R_ExpressionProb_1642_10_172()) return true; + if (jj_3R_ExpressionProb_1642_10_174()) return true; } } } @@ -5950,14 +5950,14 @@ static private boolean jj_3R_ExpressionProb_1618_9_148() if (jj_scan_token(LBRACKET)) return true; if (jj_3R_Expression_1176_9_39()) return true; xsp = jj_scanpos; - if (jj_3R_ExpressionProb_1644_51_173()) jj_scanpos = xsp; + if (jj_3R_ExpressionProb_1644_51_175()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_IdentifierExpression_1998_9_33() + static private boolean jj_3R_IdentifierExpression_1996_9_33() { - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; return false; } @@ -5972,21 +5972,21 @@ static private boolean jj_3R_ExpressionTemporalUnary_1228_9_56() return false; } - static private boolean jj_3R_ExpressionFilter_1966_34_192() + static private boolean jj_3R_ExpressionTemporalBinary_1214_19_66() { - if (jj_scan_token(AND)) return true; + if (jj_3R_TimeBound_1252_9_77()) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1965_35_190() + static private boolean jj_3R_ExpressionFilter_1964_34_192() { - if (jj_scan_token(MAX)) return true; + if (jj_scan_token(AND)) return true; return false; } - static private boolean jj_3R_ExpressionTemporalBinary_1214_19_66() + static private boolean jj_3R_ExpressionFilter_1963_35_190() { - if (jj_3R_TimeBound_1252_9_77()) return true; + if (jj_scan_token(MAX)) return true; return false; } @@ -6008,7 +6008,7 @@ static private boolean jj_3R_ExpressionTemporalBinary_1211_19_63() return false; } - static private boolean jj_3R_Identifier_1987_9_30() + static private boolean jj_3R_Identifier_1985_9_30() { if (jj_scan_token(REG_IDENT)) return true; return false; @@ -6031,7 +6031,7 @@ static private boolean jj_3R_ExpressionTemporalBinary_1209_17_57() return false; } - static private boolean jj_3R_ExpressionLabel_1944_47_188() + static private boolean jj_3R_ExpressionLabel_1942_45_167() { if (jj_scan_token(INIT)) return true; return false; @@ -6044,16 +6044,9 @@ static private boolean jj_3R_ExpressionFuncArgs_1527_72_196() return false; } - static private boolean jj_3R_ExpressionFilter_1971_11_195() - { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_Expression_1176_9_39()) return true; - return false; - } - static private boolean jj_3R_ExpressionFuncOldStyle_1515_83_165() { - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; return false; } @@ -6066,34 +6059,41 @@ static private boolean jj_3R_ExpressionTemporalBinary_1206_9_47() return false; } - static private boolean jj_3R_ExpressionFilter_1967_11_194() + static private boolean jj_3R_ExpressionFilter_1969_11_195() { - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_Expression_1176_9_39()) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1966_11_191() + static private boolean jj_3R_ExpressionFilter_1965_11_194() { - if (jj_scan_token(PLUS)) return true; + if (jj_3R_Identifier_1985_9_30()) return true; return false; } - static private boolean jj_3R_ExpressionFilter_1965_11_189() + static private boolean jj_3R_ExpressionFilter_1964_11_191() { - if (jj_scan_token(MIN)) return true; + if (jj_scan_token(PLUS)) return true; return false; } - static private boolean jj_3R_ExpressionLabel_1944_30_187() + static private boolean jj_3R_ExpressionFilter_1963_11_189() { - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_scan_token(MIN)) return true; return false; } static private boolean jj_3R_SystemHideRename_1126_81_91() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; + return false; + } + + static private boolean jj_3R_ExpressionLabel_1942_28_166() + { + if (jj_3R_Identifier_1985_9_30()) return true; return false; } @@ -6105,23 +6105,23 @@ static private boolean jj_3R_ExpressionParenth_1577_9_147() return false; } - static private boolean jj_3R_ExpressionFilter_1960_9_154() + static private boolean jj_3R_ExpressionFilter_1958_9_154() { if (jj_scan_token(FILTER)) return true; if (jj_scan_token(LPARENTH)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionFilter_1965_11_189()) { + if (jj_3R_ExpressionFilter_1963_11_189()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1965_35_190()) { + if (jj_3R_ExpressionFilter_1963_35_190()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1966_11_191()) { + if (jj_3R_ExpressionFilter_1964_11_191()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1966_34_192()) { + if (jj_3R_ExpressionFilter_1964_34_192()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1966_56_193()) { + if (jj_3R_ExpressionFilter_1964_56_193()) { jj_scanpos = xsp; - if (jj_3R_ExpressionFilter_1967_11_194()) return true; + if (jj_3R_ExpressionFilter_1965_11_194()) return true; } } } @@ -6130,7 +6130,7 @@ static private boolean jj_3R_ExpressionFilter_1960_9_154() if (jj_scan_token(COMMA)) return true; if (jj_3R_Expression_1176_9_39()) return true; xsp = jj_scanpos; - if (jj_3R_ExpressionFilter_1971_11_195()) jj_scanpos = xsp; + if (jj_3R_ExpressionFilter_1969_11_195()) jj_scanpos = xsp; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -6159,14 +6159,14 @@ static private boolean jj_3R_Expression_1176_9_39() return false; } - static private boolean jj_3R_ExpressionLabel_1942_9_153() + static private boolean jj_3R_ExpressionLabel_1942_9_148() { if (jj_scan_token(DQUOTE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_ExpressionLabel_1944_30_187()) { + if (jj_3R_ExpressionLabel_1942_28_166()) { jj_scanpos = xsp; - if (jj_3R_ExpressionLabel_1944_47_188()) return true; + if (jj_3R_ExpressionLabel_1942_45_167()) return true; } if (jj_scan_token(DQUOTE)) return true; return false; @@ -6174,7 +6174,7 @@ static private boolean jj_3R_ExpressionLabel_1942_9_153() static private boolean jj_3R_ExpressionStrategy_1895_51_224() { - if (jj_3R_ExpressionReward_1741_9_149()) return true; + if (jj_3R_ExpressionReward_1741_9_150()) return true; return false; } @@ -6218,7 +6218,7 @@ static private boolean jj_3R_ExpressionLiteral_1538_9_155() static private boolean jj_3R_SystemAtomic_1154_10_79() { if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } @@ -6260,14 +6260,14 @@ static private boolean jj_3R_ExpressionStrategyCoalition_1916_11_243() static private boolean jj_3R_SystemAtomic_1152_9_78() { - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; return false; } static private boolean jj_3R_SystemParallel_1096_65_71() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; return false; } @@ -6330,9 +6330,9 @@ static private boolean jj_3R_ExpressionFuncArgs_1527_9_162() static private boolean jj_3R_SystemHideRename_1133_19_92() { if (jj_scan_token(COMMA)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; if (jj_scan_token(RENAME)) return true; - if (jj_3R_Identifier_1987_9_30()) return true; + if (jj_3R_Identifier_1985_9_30()) return true; return false; } diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index d80d828f0d..90e047cb70 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -1445,6 +1445,8 @@ Expression ExpressionBasic(boolean prop, boolean pathprop) : ret = ExpressionFuncOldStyle(prop, pathprop) | ret = ExpressionParenth(prop, pathprop) + | + ret = ExpressionLabel(prop, pathprop) | // Remaining options are only applicable for properties ret = ExpressionProb(prop, pathprop) @@ -1458,8 +1460,6 @@ Expression ExpressionBasic(boolean prop, boolean pathprop) : ret = ExpressionForAll(prop, pathprop) | ret = ExpressionStrategy(prop, pathprop) - | - ret = ExpressionLabel(prop, pathprop) | ret = ExpressionFilter(prop, pathprop) ) @@ -1938,10 +1938,8 @@ Expression ExpressionLabel(boolean prop, boolean pathprop) : Token begin; } { - // This production is only allowed in expressions if the "prop" parameter is true - { if (!prop) throw generateParseException(); } // Label can be arbitary string or the "init" keyword - ( begin = ( s=Identifier() | { s = "init"; } ) ) + begin = ( s=Identifier() | { s = "init"; } ) { ret = new ExpressionLabel(s); ret.setPosition(begin, getToken(0)); return ret; } } diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java index b242192742..12392e3b97 100644 --- a/prism/src/parser/ast/LabelList.java +++ b/prism/src/parser/ast/LabelList.java @@ -32,6 +32,7 @@ import parser.visitor.ASTVisitor; import parser.visitor.DeepCopy; import prism.PrismLangException; +import prism.PrismUtils; // class to store list of labels @@ -52,7 +53,38 @@ public LabelList() labels = new ArrayList<>(); nameIdents = new ArrayList<>(); } - + + /** + * Checking all labels for cyclic dependencies.
+ * Note: This method does not take formulas into account. Therefore, to prevent + * cycles completely, it is necessary to expand formulas beforehand. + * + * @throws PrismLangException In case a cyclic dependency was found. + */ + public void findCycles() throws PrismLangException + { + // Create boolean matrix of dependencies + // (matrix[i][j] is true if label i contains label j) + int n = size(); + int j; + boolean[][] matrix = new boolean[n][n]; + for (int i = 0; i < n; i++) { + List iLabels = labels.get(i).getAllLabels(); + for (j = 0; j < n; j++) { + if (iLabels.contains(names.get(j))) { + // label i contains j + matrix[i][j] = true; + } + } + } + // Check for and report dependencies + int firstCycle = PrismUtils.findCycle(matrix); + if (firstCycle != -1) { + String s = "Cyclic dependency in definition of label \"" + names.get(firstCycle) + "\""; + throw new PrismLangException(s, labels.get(firstCycle)); + } + } + // Set methods public void addLabel(ExpressionIdent n, Expression l) diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 147cdb538f..3f6944dc90 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -894,6 +894,10 @@ public void tidyUp() throws PrismLangException // Check label identifiers checkLabelIdents(); + // Check labels for cyclic dependencies + // should be done after formulas were expanded + labelList.findCycles(); + // Check module names checkModuleNames(); diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 4cccaecb58..bf9b0184df 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -322,6 +322,10 @@ public void tidyUp() throws PrismLangException // Check label identifiers checkLabelIdents(); + // Check label for cyclic dependencies + // should be done after formulas were expanded + combinedLabelList.findCycles(); + // Check constant identifiers checkConstantIdents(); // Find all instances of constants (i.e. locate idents which are constants). From 847bfc8cb01b01233a80c042c517e373c171d627 Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:28 +0200 Subject: [PATCH 2/7] label inside label and guard evaluation for explicit --- prism/src/explicit/ConstructModel.java | 29 +++++----- prism/src/parser/EvaluateContextState.java | 26 ++++++++- prism/src/parser/ast/Expression.java | 15 ++++++ prism/src/parser/ast/ExpressionLabel.java | 5 +- prism/src/parser/ast/LabelList.java | 54 +++++++++++++++++-- prism/src/prism/ModelGenerator.java | 26 +++------ prism/src/prism/ModelGenerator2MTBDD.java | 6 ++- prism/src/prism/TestModelGenerator.java | 10 ---- .../simulator/ModulesFileModelGenerator.java | 10 ++-- prism/src/simulator/Updater.java | 8 +-- 10 files changed, 130 insertions(+), 59 deletions(-) diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 22795ac98c..6870c832fa 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -32,6 +32,7 @@ import java.util.BitSet; import java.util.LinkedList; import java.util.List; +import java.util.Map; import common.Interval; import parser.State; @@ -456,9 +457,10 @@ public Model constructModel(ModelGenerator modelGen, boole // Discard permutation permut = null; - if (!justReach && attachLabels) + if (!justReach && attachLabels) { attachLabels(modelGen, model); - + } + return model; } @@ -485,29 +487,32 @@ private void setStateObservation(ModelGenerator modelGen, POMDPSi private void attachLabels(ModelGenerator modelGen, ModelExplicit model) throws PrismException { - // Get state info - List statesList = model.getStatesList(); - int numStates = statesList.size(); + int i,j; // Create storage for labels int numLabels = modelGen.getNumLabels(); // No need to continue unless this ModelGenerator uses labels if (numLabels == 0) return; - BitSet bitsets[] = new BitSet[numLabels]; - for (int j = 0; j < numLabels; j++) { + BitSet[] bitsets = new BitSet[numLabels]; + for (j = 0; j < numLabels; j++) { bitsets[j] = new BitSet(); } + + // Get state info + List statesList = model.getStatesList(); + int numStates = statesList.size(); + // Construct bitsets for labels - for (int i = 0; i < numStates; i++) { + for (i = 0; i < numStates; i++) { State state = statesList.get(i); - modelGen.exploreState(state); - for (int j = 0; j < numLabels; j++) { - if (modelGen.isLabelTrue(j)) { + Map labelValues = modelGen.getLabelValues(state); + for (j = 0; j < numLabels; j++) { + if (labelValues.get(modelGen.getLabelName(j))) { bitsets[j].set(i); } } } // Attach labels/bitsets - for (int j = 0; j < numLabels; j++) { + for (j = 0; j < numLabels; j++) { model.addLabel(modelGen.getLabelName(j), bitsets[j]); } } diff --git a/prism/src/parser/EvaluateContextState.java b/prism/src/parser/EvaluateContextState.java index e9022d42dc..7a37ab58e1 100644 --- a/prism/src/parser/EvaluateContextState.java +++ b/prism/src/parser/EvaluateContextState.java @@ -26,6 +26,8 @@ package parser; +import java.util.Map; + /** * Information required to evaluate an expression, * where the values for variables are stored in a State object. @@ -40,15 +42,24 @@ public class EvaluateContextState extends EvaluateContext */ private Object[] varValues; + /** values of all labels in this state */ + protected Map labelValues; + public EvaluateContextState(State state) { - setState(state); + this(null, state); } public EvaluateContextState(Values constantValues, State state) { - setConstantValues(constantValues); + this(constantValues, null, state); + } + + public EvaluateContextState(Values constantValues, Map labelValues, State state) + { setState(state); + setConstantValues(constantValues); + setLabelValues(labelValues); } /** @@ -68,4 +79,15 @@ public Object getVarValue(String name, int index) // so use index if provided; otherwise unknown return index == -1 ? null : varValues[index]; } + + public EvaluateContextState setLabelValues(Map labelValues) + { + this.labelValues = labelValues; + return this; + } + + public Boolean getLabelValue(String name) + { + return labelValues.get(name); + } } diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 0f71f64789..321fb527ed 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -50,6 +50,8 @@ import prism.PrismException; import prism.PrismLangException; +import java.util.Map; + // Abstract class for PRISM language expressions public abstract class Expression extends ASTElement @@ -576,6 +578,19 @@ public boolean evaluateBoolean(Values constantValues, State state) throws PrismL return evaluateBoolean(new EvaluateContextState(constantValues, state)); } + /** + * Evaluate this expression as a boolean, based on values for labels/variables. + * Any typing issues cause an exception. + * Constant values are supplied as a Values object. + * Label values are supplied as a Map. + * Variable values are supplied as a State object, i.e. array of variable values. + * Note: assumes that type checking has been done. + */ + public boolean evaluateBoolean(Values constantValues, Map labelValues, State state) throws PrismLangException + { + return evaluateBoolean(new EvaluateContextState(constantValues, labelValues, state)); + } + /** * Evaluate this expression as a boolean, based on values for some variables (but not constants). * Basically casts the result to a boolean, checking for any type errors. diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java index b390d6ca41..15cd9c627d 100644 --- a/prism/src/parser/ast/ExpressionLabel.java +++ b/prism/src/parser/ast/ExpressionLabel.java @@ -83,7 +83,10 @@ public boolean isProposition() @Override public Object evaluate(EvaluateContext ec) throws PrismLangException { - throw new PrismLangException("Cannot evaluate labels", this); + Object value = ec.getLabelValue(this.name); + if (value == null) + throw new PrismLangException("Failed to evaluate label", this); + return value; } @Override diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java index 12392e3b97..06cbef73c8 100644 --- a/prism/src/parser/ast/LabelList.java +++ b/prism/src/parser/ast/LabelList.java @@ -28,7 +28,10 @@ import java.util.ArrayList; import java.util.List; +import java.util.HashMap; +import java.util.Map; +import parser.State; import parser.visitor.ASTVisitor; import parser.visitor.DeepCopy; import prism.PrismLangException; @@ -39,11 +42,11 @@ public class LabelList extends ASTElement { // Name/expression pairs to define labels - private ArrayList names; - private ArrayList labels; + protected ArrayList names; + protected ArrayList labels; // We also store an ExpressionIdent to match each name. // This is to just to provide positional info. - private ArrayList nameIdents; + protected ArrayList nameIdents; // Constructor @@ -85,8 +88,51 @@ public void findCycles() throws PrismLangException } } + /** + * Evaluates all label with the given state.
+ * + * @param currentState The state to evaluate the labels in. + * @return A map of the values. + * @throws PrismLangException In case an evaluation fails. + */ + public Map getLabelValues(State currentState) throws PrismLangException + { + Map labelValues = new HashMap<>(labels.size()); + + for (String label : names) { + evaluateLabel(label, labelValues, currentState); + } + + return labelValues; + } + + /** + * Helper function to recursively evaluate label values. The value will be stored inside the given map. + * + * @param name The name of the label. + * @param labelValues The already known values of all labels. + */ + private void evaluateLabel(String name, Map labelValues, State state) throws PrismLangException + { + // check if value is already known + if (labelValues.containsKey(name)) { + return; + } + // get expression + Expression label = labels.get(names.indexOf(name)); + // check if all the (other) label dependencies are evaluated + for (String dependency : label.getAllLabels()){ + if (!labelValues.containsKey(dependency)){ + // evaluate other label first + evaluateLabel(dependency, labelValues, state); + } + } + // all dependencies are fulfilled + labelValues.put(name, label.evaluateBoolean(null, labelValues, state)); + } + + // Set methods - public void addLabel(ExpressionIdent n, Expression l) { names.add(n.getName()); diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java index 95cd919289..6f7ec88c46 100644 --- a/prism/src/prism/ModelGenerator.java +++ b/prism/src/prism/ModelGenerator.java @@ -33,6 +33,7 @@ import common.Interval; import parser.State; import parser.ast.Expression; +import java.util.Map; /** * Interface for classes that generate a probabilistic model: @@ -420,21 +421,6 @@ public default String getTransitionUpdateStringFull(int i, int offset) throws Pr */ public State computeTransitionTarget(int i, int offset) throws PrismException; - /** - * Is label {@code label} true in the state currently being explored? - * @param label The name of the label to check - */ - public default boolean isLabelTrue(String label) throws PrismException - { - // Default implementation: Look up label and then check by index - int i = getLabelIndex(label); - if (i == -1) { - throw new PrismException("Label \"" + label + "\" not defined"); - } else { - return isLabelTrue(i); - } - } - /** * For real-time models, get the clock invariant for the current state, * i.e., an expression over clock variables which must remain true. @@ -448,13 +434,15 @@ public default Expression getClockInvariant() throws PrismException } /** - * Is the {@code i}th label of the model true in the state currently being explored? - * @param i The index of the label to check + * Create a Map of label names and values for the given state + * + * @param state Context state for evaluation. + * @throws PrismLangException If evaluation of a label fails. */ - public default boolean isLabelTrue(int i) throws PrismException + default Map getLabelValues(State state) throws PrismException { // No labels by default - throw new PrismException("Label number \"" + i + "\" not defined"); + throw new PrismException("Labels not defined"); } /** diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index cc43316ffa..cc1e4e4c80 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -27,6 +27,7 @@ package prism; import java.util.LinkedList; +import java.util.Map; import java.util.Vector; import jdd.JDD; @@ -511,9 +512,10 @@ private void buildTransAndRewards() throws PrismException // Print some progress info occasionally // TODO progress.updateIfReady(src + 1); } - + + Map labelValues = modelGen.getLabelValues(state); for (int l = 0; l < numLabels; l++) { - if (modelGen.isLabelTrue(l)) { + if (labelValues.get(modelGen.getLabelName(l))) { labelsArray[l] = JDD.Or(labelsArray[l], ddState.copy()); } } diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index 3c65f63e00..83cf4285f6 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/prism/src/prism/TestModelGenerator.java @@ -134,16 +134,6 @@ public State computeTransitionTarget(int i, int offset) throws PrismException } return s; } - - @Override - public boolean isLabelTrue(int i) throws PrismException - { - if (i == 0) { - return x == n; - } else { - throw new PrismException("Label number \"" + i + "\" not defined"); - } - } public static void main(String args[]) { diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 063eafda39..ff187f53af 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -2,6 +2,7 @@ import java.util.ArrayList; import java.util.List; +import java.util.Map; import common.Interval; import param.BigRational; @@ -603,10 +604,9 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio } @Override - public boolean isLabelTrue(int i) throws PrismException + public Map getLabelValues(State state) throws PrismLangException { - Expression expr = labelList.getLabel(i); - return expr.evaluateBoolean(ec.setState(exploreState)); + return labelList.getLabelValues(state); } @Override @@ -756,7 +756,7 @@ private TransitionList getTransitionListScalars() throws PrismException } // Compute the current transition list, if required if (!transitionListBuilt) { - updater.calculateTransitions(exploreState, transitionList); + updater.calculateTransitions(exploreState, getLabelValues(exploreState) ,transitionList); transitionListBuilt = true; } return transitionList; @@ -772,7 +772,7 @@ private TransitionList> getTransitionListIntervals() throws Pris } // Compute the current transition list, if required if (!transitionListBuilt) { - updaterInt.calculateTransitions(exploreState, transitionListInt); + updaterInt.calculateTransitions(exploreState, getLabelValues(exploreState),transitionListInt); transitionListIntBuilt = true; } return transitionListInt; diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index f5ef9ef0b0..e9be42dfd8 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -165,7 +165,7 @@ public Updater(ModulesFile modulesFile, VarList varList, Evaluator eval, * @param state State from which to explore * @param transitionList TransitionList object in which to store result */ - public void calculateTransitions(State state, TransitionList transitionList) throws PrismException + public void calculateTransitions(State state, Map labelValues, TransitionList transitionList) throws PrismException { List> chs; int i, j, k, l, n, count; @@ -186,7 +186,7 @@ public void calculateTransitions(State state, TransitionList transitionLi // Calculate the available updates for each module/action // (update information in updateLists, clockGuards, enabledSynchs and enabledModules) for (i = 0; i < numModules; i++) { - calculateUpdatesForModule(i, state); + calculateUpdatesForModule(i, state, labelValues); } //System.out.println("updateLists: " + updateLists); @@ -284,7 +284,7 @@ public void calculateTransitions(State state, TransitionList transitionLi * @param m The module index * @param state State from which to explore */ - protected void calculateUpdatesForModule(int m, State state) throws PrismLangException + protected void calculateUpdatesForModule(int m, State state, Map labelValues) throws PrismLangException { Module module = modulesFile.getModule(m); int n = module.getNumCommands(); @@ -305,7 +305,7 @@ protected void calculateUpdatesForModule(int m, State state) throws PrismLangExc guardSat = true; } } else { - guardSat = command.getGuard().evaluateBoolean(ec.setState(state)); + guardSat = command.getGuard().evaluateBoolean(ec.setLabelValues(labelValues).setState(state)); } // If the command is enabled, update stored info if (guardSat) { From 805bc42dbe74b4f1ea1501f7d89bd5bbe56f8021 Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:33 +0200 Subject: [PATCH 3/7] label inside guard evaluation for hybrid --- prism/src/parser/EvaluateContext.java | 9 +++++++++ prism/src/parser/EvaluateContextState.java | 1 + prism/src/prism/Modules2MTBDD.java | 2 +- prism/src/prism/StateModelChecker.java | 8 ++++++-- 4 files changed, 17 insertions(+), 3 deletions(-) diff --git a/prism/src/parser/EvaluateContext.java b/prism/src/parser/EvaluateContext.java index 5eadbfe99a..83fab146c0 100644 --- a/prism/src/parser/EvaluateContext.java +++ b/prism/src/parser/EvaluateContext.java @@ -128,6 +128,15 @@ public Object getConstantValue(String name) */ public abstract Object getVarValue(String name, int index); + /** + * Return the value for a label; null if unknown. + */ + public Boolean getLabelValue(String name) + { + // no labels defined by default + return null; + } + /** * Return the value for an observable (by name or index); null if unknown. */ diff --git a/prism/src/parser/EvaluateContextState.java b/prism/src/parser/EvaluateContextState.java index 7a37ab58e1..2c451c1a6a 100644 --- a/prism/src/parser/EvaluateContextState.java +++ b/prism/src/parser/EvaluateContextState.java @@ -86,6 +86,7 @@ public EvaluateContextState setLabelValues(Map labelValues) return this; } + @Override public Boolean getLabelValue(String name) { return labelValues.get(name); diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 9ecacb8d34..783e8c071d 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -272,7 +272,7 @@ public Model translate() throws PrismException sortRanges(); // create stripped-down StateModelChecker for expression to MTBDD conversions - expr2mtbdd = new StateModelChecker(prism, varList, allDDRowVars, varDDRowVars, constantValues); + expr2mtbdd = new StateModelChecker(prism, varList, modulesFile.getLabelList(), allDDRowVars, varDDRowVars, constantValues); // translate modules file into dd translateModules(); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 531615a8b3..1f21ed5179 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -57,6 +57,9 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // Constant values protected Values constantValues; + // Label list of Modules file + protected LabelList modulLabelList; + // Model info protected Model model; protected VarList varList; @@ -135,7 +138,7 @@ public StateModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismEx * {@code clearDummyModel()} later. *
[ REFS: none, DEREFS: none ] */ - public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException + public StateModelChecker(Prism prism, VarList varList, LabelList modulLabelList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException { // Initialise PrismComponent super(prism); @@ -146,6 +149,7 @@ public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDD this.allDDRowVars = allDDRowVars; this.varDDRowVars = varDDRowVars; this.constantValues = constantValues; + this.modulLabelList = modulLabelList; // Create dummy model reach = null; model = new ProbModel(JDD.Constant(0), // trans @@ -1614,7 +1618,7 @@ public LabelList getLabelList() if (propertiesFile != null) { return propertiesFile.getCombinedLabelList(); // combined list from properties and modules file } else { - return null; + return modulLabelList; // (if available) labelList of modules file only } } From d64a49fd29224be62d8bea685bea81054542d136 Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:35 +0200 Subject: [PATCH 4/7] label inside guard evaluation for exact --- prism/src/parser/ast/Expression.java | 19 +++++++++++++++++++ prism/src/parser/ast/ExpressionLabel.java | 10 ++++++++++ 2 files changed, 29 insertions(+) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 321fb527ed..c407109b1f 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -105,6 +105,12 @@ public Object getConstantValue(String name) { return ec.getConstantValue(name); } + + @Override + public Boolean getLabelValue(String name) + { + return ec.getLabelValue(name); + } })); } @@ -674,6 +680,19 @@ public BigRational evaluateExact(Values constantValues, State state) throws Pris return evaluateExact(new EvaluateContextState(constantValues, state)); } + /** + * Evaluate this expression exactly to a BigRational, based on values for constants, variables and labels. + * This is regardless of the type (e.g. ints, booleans are also converted). + * Constant values are supplied as a Values object. + * Variable values are supplied as a State object, i.e. array of variable values. + * Labels are supplied as a Map from label names to booleans. + * Note: assumes that type checking has been done. + */ + public BigRational evaluateExact(Values constantValues, Map labelValues, State state) throws PrismLangException + { + return evaluateExact(new EvaluateContextState(constantValues, labelValues, state)); + } + /** * Evaluate this expression exactly to a BigRational, based on values for some variables (but not constants). * This is regardless of the type (e.g. ints, booleans are also converted). diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java index 15cd9c627d..4bcf29f6be 100644 --- a/prism/src/parser/ast/ExpressionLabel.java +++ b/prism/src/parser/ast/ExpressionLabel.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.EvaluateContext; import parser.visitor.ASTVisitor; import parser.visitor.DeepCopy; @@ -89,6 +90,15 @@ public Object evaluate(EvaluateContext ec) throws PrismLangException return value; } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + Boolean value = ec.getLabelValue(this.name); + if (value == null) + throw new PrismLangException("Failed to evaluate label", this); + return BigRational.from(value); + } + @Override public boolean returnsSingleValue() { From 3de9ce4021ffb05069584df8a253f0a8200d9232 Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:40 +0200 Subject: [PATCH 5/7] moving label-evalution and -caching to LabelEvaluator - Fix evaluation order of labels instead repetitive recursion --- prism/src/explicit/ConstructModel.java | 38 +--- prism/src/parser/EvaluateContextState.java | 10 +- prism/src/parser/ast/Expression.java | 5 +- prism/src/parser/ast/ExpressionLabel.java | 4 +- prism/src/parser/ast/LabelList.java | 94 +++------ prism/src/prism/ModelGenerator.java | 20 +- prism/src/prism/ModelGenerator2MTBDD.java | 6 +- prism/src/simulator/LabelEvaluator.java | 193 ++++++++++++++++++ .../simulator/ModulesFileModelGenerator.java | 22 +- prism/src/simulator/Updater.java | 5 +- prism/unit-tests/parser/ast/LabelTest.java | 122 +++++++++++ 11 files changed, 399 insertions(+), 120 deletions(-) create mode 100644 prism/src/simulator/LabelEvaluator.java create mode 100644 prism/unit-tests/parser/ast/LabelTest.java diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 6870c832fa..e3f928dd61 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -458,7 +458,11 @@ public Model constructModel(ModelGenerator modelGen, boole permut = null; if (!justReach && attachLabels) { - attachLabels(modelGen, model); + // Attach labels/bitsets + List statesList = model.getStatesList(); + for (String label : model.getLabels()){ + model.addLabel(label, modelGen.getLabel(label, statesList)); + } } return model; @@ -484,38 +488,6 @@ private void setStateObservation(ModelGenerator modelGen, POMDPSi // Set observation/unobservation pomdp.setObservation(s, sObs, sUnobs, modelGen.getObservableNames()); } - - private void attachLabels(ModelGenerator modelGen, ModelExplicit model) throws PrismException - { - int i,j; - // Create storage for labels - int numLabels = modelGen.getNumLabels(); - // No need to continue unless this ModelGenerator uses labels - if (numLabels == 0) return; - BitSet[] bitsets = new BitSet[numLabels]; - for (j = 0; j < numLabels; j++) { - bitsets[j] = new BitSet(); - } - - // Get state info - List statesList = model.getStatesList(); - int numStates = statesList.size(); - - // Construct bitsets for labels - for (i = 0; i < numStates; i++) { - State state = statesList.get(i); - Map labelValues = modelGen.getLabelValues(state); - for (j = 0; j < numLabels; j++) { - if (labelValues.get(modelGen.getLabelName(j))) { - bitsets[j].set(i); - } - } - } - // Attach labels/bitsets - for (j = 0; j < numLabels; j++) { - model.addLabel(modelGen.getLabelName(j), bitsets[j]); - } - } /** * Test method. diff --git a/prism/src/parser/EvaluateContextState.java b/prism/src/parser/EvaluateContextState.java index 2c451c1a6a..2149340613 100644 --- a/prism/src/parser/EvaluateContextState.java +++ b/prism/src/parser/EvaluateContextState.java @@ -26,7 +26,7 @@ package parser; -import java.util.Map; +import java.util.function.Predicate; /** * Information required to evaluate an expression, @@ -43,7 +43,7 @@ public class EvaluateContextState extends EvaluateContext private Object[] varValues; /** values of all labels in this state */ - protected Map labelValues; + protected Predicate labelValues; public EvaluateContextState(State state) { @@ -55,7 +55,7 @@ public EvaluateContextState(Values constantValues, State state) this(constantValues, null, state); } - public EvaluateContextState(Values constantValues, Map labelValues, State state) + public EvaluateContextState(Values constantValues, Predicate labelValues, State state) { setState(state); setConstantValues(constantValues); @@ -80,7 +80,7 @@ public Object getVarValue(String name, int index) return index == -1 ? null : varValues[index]; } - public EvaluateContextState setLabelValues(Map labelValues) + public EvaluateContextState setLabelValues(Predicate labelValues) { this.labelValues = labelValues; return this; @@ -89,6 +89,6 @@ public EvaluateContextState setLabelValues(Map labelValues) @Override public Boolean getLabelValue(String name) { - return labelValues.get(name); + return labelValues.test(name); } } diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index c407109b1f..c0330e86d3 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -51,6 +51,7 @@ import prism.PrismLangException; import java.util.Map; +import java.util.function.Predicate; // Abstract class for PRISM language expressions @@ -592,7 +593,7 @@ public boolean evaluateBoolean(Values constantValues, State state) throws PrismL * Variable values are supplied as a State object, i.e. array of variable values. * Note: assumes that type checking has been done. */ - public boolean evaluateBoolean(Values constantValues, Map labelValues, State state) throws PrismLangException + public boolean evaluateBoolean(Values constantValues, Predicate labelValues, State state) throws PrismLangException { return evaluateBoolean(new EvaluateContextState(constantValues, labelValues, state)); } @@ -688,7 +689,7 @@ public BigRational evaluateExact(Values constantValues, State state) throws Pris * Labels are supplied as a Map from label names to booleans. * Note: assumes that type checking has been done. */ - public BigRational evaluateExact(Values constantValues, Map labelValues, State state) throws PrismLangException + public BigRational evaluateExact(Values constantValues, Predicate labelValues, State state) throws PrismLangException { return evaluateExact(new EvaluateContextState(constantValues, labelValues, state)); } diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java index 4bcf29f6be..644e5bd0e9 100644 --- a/prism/src/parser/ast/ExpressionLabel.java +++ b/prism/src/parser/ast/ExpressionLabel.java @@ -82,9 +82,9 @@ public boolean isProposition() } @Override - public Object evaluate(EvaluateContext ec) throws PrismLangException + public Boolean evaluate(EvaluateContext ec) throws PrismLangException { - Object value = ec.getLabelValue(this.name); + Boolean value = ec.getLabelValue(this.name); if (value == null) throw new PrismLangException("Failed to evaluate label", this); return value; diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java index 06cbef73c8..44fd139b0b 100644 --- a/prism/src/parser/ast/LabelList.java +++ b/prism/src/parser/ast/LabelList.java @@ -28,10 +28,7 @@ import java.util.ArrayList; import java.util.List; -import java.util.HashMap; -import java.util.Map; -import parser.State; import parser.visitor.ASTVisitor; import parser.visitor.DeepCopy; import prism.PrismLangException; @@ -49,7 +46,7 @@ public class LabelList extends ASTElement protected ArrayList nameIdents; // Constructor - + public LabelList() { names = new ArrayList<>(); @@ -66,20 +63,7 @@ public LabelList() */ public void findCycles() throws PrismLangException { - // Create boolean matrix of dependencies - // (matrix[i][j] is true if label i contains label j) - int n = size(); - int j; - boolean[][] matrix = new boolean[n][n]; - for (int i = 0; i < n; i++) { - List iLabels = labels.get(i).getAllLabels(); - for (j = 0; j < n; j++) { - if (iLabels.contains(names.get(j))) { - // label i contains j - matrix[i][j] = true; - } - } - } + boolean[][] matrix = getLabelDependencies(); // Check for and report dependencies int firstCycle = PrismUtils.findCycle(matrix); if (firstCycle != -1) { @@ -89,49 +73,29 @@ public void findCycles() throws PrismLangException } /** - * Evaluates all label with the given state.
+ * Create a boolean matrix of dependencies between labels. * - * @param currentState The state to evaluate the labels in. - * @return A map of the values. - * @throws PrismLangException In case an evaluation fails. + * @return a matrix m such that label i depends on label j iff m[i][j] + * @throws PrismLangException */ - public Map getLabelValues(State currentState) throws PrismLangException + public boolean[][] getLabelDependencies() throws PrismLangException { - Map labelValues = new HashMap<>(labels.size()); - - for (String label : names) { - evaluateLabel(label, labelValues, currentState); - } - - return labelValues; - } - - /** - * Helper function to recursively evaluate label values. The value will be stored inside the given map. - * - * @param name The name of the label. - * @param labelValues The already known values of all labels. - */ - private void evaluateLabel(String name, Map labelValues, State state) throws PrismLangException - { - // check if value is already known - if (labelValues.containsKey(name)) { - return; - } - // get expression - Expression label = labels.get(names.indexOf(name)); - // check if all the (other) label dependencies are evaluated - for (String dependency : label.getAllLabels()){ - if (!labelValues.containsKey(dependency)){ - // evaluate other label first - evaluateLabel(dependency, labelValues, state); + // (matrix[i][j] is true if label i contains label j) + int n = size(); + int j; + boolean[][] matrix = new boolean[n][n]; + for (int i = 0; i < n; i++) { + List iLabels = labels.get(i).getAllLabels(); + for (j = 0; j < n; j++) { + if (iLabels.contains(names.get(j))) { + // label i contains j + matrix[i][j] = true; + } } } - // all dependencies are fulfilled - labelValues.put(name, label.evaluateBoolean(null, labelValues, state)); + return matrix; } - // Set methods public void addLabel(ExpressionIdent n, Expression l) { @@ -139,18 +103,18 @@ public void addLabel(ExpressionIdent n, Expression l) labels.add(l); nameIdents.add(n); } - + public void setLabelName(int i , ExpressionIdent n) { names.set(i, n.getName()); nameIdents.set(i, n); } - + public void setLabel(int i , Expression l) { labels.set(i, l); } - + // Get methods public int size() @@ -162,17 +126,17 @@ public String getLabelName(int i) { return names.get(i); } - + public List getLabelNames() { return names; } - + public Expression getLabel(int i) { return labels.get(i); } - + public ExpressionIdent getLabelNameIdent(int i) { return nameIdents.get(i); @@ -187,7 +151,7 @@ public int getLabelIndex(String s) } // Methods required for ASTElement: - + /** * Visitor method. */ @@ -195,7 +159,7 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + /** * Convert to string. */ @@ -203,16 +167,16 @@ public String toString() { String s = ""; int i, n; - + n = size(); for (i = 0; i < n; i++) { s += "label \"" + getLabelName(i); s += "\" = " + getLabel(i) + ";\n"; } - + return s; } - + @Override public LabelList deepCopy(DeepCopy copier) throws PrismLangException { diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java index 6f7ec88c46..cf378e9452 100644 --- a/prism/src/prism/ModelGenerator.java +++ b/prism/src/prism/ModelGenerator.java @@ -29,11 +29,12 @@ import java.util.Collections; import java.util.List; +import java.util.BitSet; +import java.util.function.Predicate; import common.Interval; import parser.State; import parser.ast.Expression; -import java.util.Map; /** * Interface for classes that generate a probabilistic model: @@ -434,18 +435,31 @@ public default Expression getClockInvariant() throws PrismException } /** - * Create a Map of label names and values for the given state + * Create a {@link Predicate} of all labels in the current state. * * @param state Context state for evaluation. * @throws PrismLangException If evaluation of a label fails. */ - default Map getLabelValues(State state) throws PrismException + default Predicate getLabelValues(State state) throws PrismException { // No labels by default throw new PrismException("Labels not defined"); } /** + * This method creates a BitSet for the given label-name containing all values in the + * order of the given statesList. + * @param name The name of the Label. + * @param statesList The List of states in right order. + * @return a {@link BitSet} of all values from the given label. + * @throws PrismException If the label values aren't cached or not all states have been evaluated + */ + default BitSet getLabel(String name, List statesList) throws PrismException + { + throw new PrismException("Labels are not cached"); + } + + /** * Get the observation when entering state {@code state}. * This is represented as a {@link parser.State} object, with one value per observable. * For models that are not partially observable, null can be returned. diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index cc1e4e4c80..38ba6cb9d5 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -27,8 +27,8 @@ package prism; import java.util.LinkedList; -import java.util.Map; import java.util.Vector; +import java.util.function.Predicate; import jdd.JDD; import jdd.JDDNode; @@ -513,9 +513,9 @@ private void buildTransAndRewards() throws PrismException // TODO progress.updateIfReady(src + 1); } - Map labelValues = modelGen.getLabelValues(state); + Predicate labelValues = modelGen.getLabelValues(state); for (int l = 0; l < numLabels; l++) { - if (labelValues.get(modelGen.getLabelName(l))) { + if (labelValues.test(modelGen.getLabelName(l))) { labelsArray[l] = JDD.Or(labelsArray[l], ddState.copy()); } } diff --git a/prism/src/simulator/LabelEvaluator.java b/prism/src/simulator/LabelEvaluator.java new file mode 100644 index 0000000000..861c81a24f --- /dev/null +++ b/prism/src/simulator/LabelEvaluator.java @@ -0,0 +1,193 @@ +package simulator; + + +import parser.State; +import parser.ast.Expression; +import parser.ast.LabelList; +import prism.PrismException; +import prism.PrismLangException; +import prism.PrismUtils; + +import java.util.BitSet; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.NoSuchElementException; +import java.util.function.Predicate; + +/** + * This class will evaluate labels. Therefore, it's wrapped around a {@link LabelList}. + *
+ * It also caches the results. + */ +public class LabelEvaluator +{ + /** Map of each evaluated state and a bitset containing the label-values ordered as in labelList */ + Map stateValues = new HashMap<>(); + /** The labelList that will be evaluated */ + LabelList labelList; + int[] evaluationOrder; + + /** + * Creates new object that will evaluate and cache the given {@link LabelList}. + */ + public LabelEvaluator(LabelList labelList) throws PrismLangException + { + this.labelList = labelList; + this.evaluationOrder = fixEvaluationOrder(labelList); + } + + /** + * Fix an order on the labels such that l1 < l2 if l2 depends on l1. + * + * @param labels a {@link LabelList} of labels to be evaluated + * @return an int array of the label indices in ascending order + * @throws PrismLangException In case a label dependencies could not be computed. + */ + private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException + { + boolean[][] deps = labels.getLabelDependencies(); + assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cylce"; + + int numLabels = labels.size(); + BitSet done = new BitSet(numLabels); + int[] order = new int[numLabels]; + for (int l = done.nextClearBit(0); l < numLabels; l = done.nextClearBit(l)) { + traverseDfs(deps, l, order, -1, done); + } + return order; + } + + /** + * Do a depth-first search in a graph given by an adjacency matrix starting at a given node. + * + * @param adj an adjacency matrix with adj[i][j] iff i->j + * @param start a start node + * @param trace an int array to record the trace, will be modified + * @param last index of last element of the trace + * @param done a {@link BitSet} of already visited nodes, will be modified + * @return the index of the last element of the extended trace, i.e., of the start node + */ + private int traverseDfs(boolean[][] adj, int start, int[] trace, int last, BitSet done) + { + if (!done.get(start)) { + boolean[] isSuccessor = adj[start]; + for (int node = isSuccessor.length - 1; node >= 0; node--) { + if (isSuccessor[node]) { + last = traverseDfs(adj, node, trace, last, done); + } + } + trace[++last] = start; + done.set(start); + } + return last; + } + + /** + * Returns the value of a specific label in a specific state. + * + * @param state The state to evaluate in. + * @param label The label that will be evaluated. + * @return The value of the Label. + * @throws PrismLangException In case a label couldn't be evaluated. + */ + public boolean getLabelValue(State state, String label) throws PrismLangException + { + return getStateValues(state).get(labelList.getLabelIndex(label)); + } + + /** + * This method provides all label values concerning a given state.
+ * It will evaluate all the Labels if necessary. + * + * @param state The state to evaluate in. + * @return Returns a {@link Map} containing all label-values for the given state, indexed by their name. + * @throws PrismLangException In case a label couldn't be evaluated. + */ + public Predicate getLabelValues(State state) throws PrismLangException + { + return asPredicate(getStateValues(state)); + } + + /** + * This method provides all values of a certain label. They will be ordered by the given statesList.
+ * States will be evaluated if necessary. + * + * @param label The name of the label. + * @param statesList The states to evaluate against in correct order. + * @return All values of the label. + * @throws PrismException In case a label evaluation fails. + */ + public BitSet getLabel(String label, List statesList) throws PrismException + { + int statesNum = statesList.size(); + int labelIndex = labelList.getLabelIndex(label); + BitSet labelValues = new BitSet(); + for (int i = statesNum - 1; i >= 0; i--) { + State state = statesList.get(i); + BitSet valuesOfState = getStateValues(state); + labelValues.set(i, valuesOfState.get(labelIndex)); + } + return labelValues; + } + + /** + * This method provides all label values of a certain state as a {@link BitSet}. + * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList} + * + * @param state The state to evaluate in. + * @return Always returns a BitSet with the label values. + * @throws PrismLangException In case a label evaluation fails. + */ + protected BitSet getStateValues(State state) throws PrismLangException + { + BitSet values = stateValues.get(state); + if (values == null) { + values = evaluateState(state); + stateValues.put(state, values); + } + return values; + } + + /** + * Evaluates all label with the given state.
+ * + * @param state The state to evaluate the labels in. + * @return A {@link BitSet} of all label values in this state. + * @throws PrismLangException In case a label evaluation fails. + */ + private BitSet evaluateState(State state) throws PrismLangException + { + BitSet values = new BitSet(); + Predicate labelValues = asPredicate(values); + for (int i : evaluationOrder) { + Expression label = labelList.getLabel(i); + boolean labelValue = label.evaluateBoolean(null, labelValues, state); + values.set(i, labelValue); + } + stateValues.put(state, values); + return values; + } + + /** + * Convert the label values for a state to a predicate on the label names. + * + * @param values the label values for some state + * @return a Predicate evaluating to {@code true} for a label name if the Bit at the corresponding index in {@code values} is set + */ + public Predicate asPredicate(BitSet values) + { + return new Predicate() + { + @Override + public boolean test(String name) + { + int index = labelList.getLabelIndex(name); + if (index == -1) { + throw new NoSuchElementException("Unknown label \"" + name + "\""); + } + return values.get(index); + } + }; + } +} diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index ff187f53af..3f5c55967f 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -1,8 +1,9 @@ package simulator; import java.util.ArrayList; +import java.util.BitSet; import java.util.List; -import java.util.Map; +import java.util.function.Predicate; import common.Interval; import param.BigRational; @@ -78,6 +79,8 @@ public class ModulesFileModelGenerator implements ModelGenerator, // Global clock invariant (conjunction of per-module invariants) protected Expression invariant; + // label value cache + protected LabelEvaluator labelsCache; /** * Build a ModulesFileModelGenerator for a particular PRISM model, represented by a {@link ModulesFile} instance. @@ -191,7 +194,7 @@ public ModulesFileModelGenerator(ModulesFile modulesFile, Evaluator eval, if (modulesFile.getSystemDefn() != null) { throw new PrismException("The system...endsystem construct is not currently supported"); } - + // Store basic model info this.modulesFile = modulesFile; this.originalModulesFile = modulesFile; @@ -253,6 +256,9 @@ public Object visit(ExpressionConstant e) throws PrismLangException labelList = modulesFile.getLabelList(); labelNames = labelList.getLabelNames(); + // create label-cache + labelsCache = new LabelEvaluator(labelList); + // Create data structures for exploring model if (!modelType.uncertain()) { updater = new Updater(modulesFile, varList, eval, parent); @@ -604,11 +610,17 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio } @Override - public Map getLabelValues(State state) throws PrismLangException + public Predicate getLabelValues(State state) throws PrismLangException { - return labelList.getLabelValues(state); + return labelsCache.getLabelValues(state); } - + + @Override + public BitSet getLabel(String name, List statesList) throws PrismException + { + return labelsCache.getLabel(name, statesList); + } + @Override public Expression getClockInvariant() throws PrismException { diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index e9be42dfd8..be41ad5a4b 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -32,6 +32,7 @@ import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.function.Predicate; import parser.EvaluateContextState; import parser.State; @@ -165,7 +166,7 @@ public Updater(ModulesFile modulesFile, VarList varList, Evaluator eval, * @param state State from which to explore * @param transitionList TransitionList object in which to store result */ - public void calculateTransitions(State state, Map labelValues, TransitionList transitionList) throws PrismException + public void calculateTransitions(State state, Predicate labelValues, TransitionList transitionList) throws PrismException { List> chs; int i, j, k, l, n, count; @@ -284,7 +285,7 @@ public void calculateTransitions(State state, Map labelValues, * @param m The module index * @param state State from which to explore */ - protected void calculateUpdatesForModule(int m, State state, Map labelValues) throws PrismLangException + protected void calculateUpdatesForModule(int m, State state, Predicate labelValues) throws PrismLangException { Module module = modulesFile.getModule(m); int n = module.getNumCommands(); diff --git a/prism/unit-tests/parser/ast/LabelTest.java b/prism/unit-tests/parser/ast/LabelTest.java new file mode 100644 index 0000000000..f512a90ddf --- /dev/null +++ b/prism/unit-tests/parser/ast/LabelTest.java @@ -0,0 +1,122 @@ +package parser.ast; + +import org.junit.jupiter.api.Nested; +import org.junit.jupiter.api.Test; +import parser.State; +import parser.type.TypeInt; +import prism.PrismLangException; +import simulator.LabelEvaluator; + +import java.util.function.Predicate; + +import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertThrows; + +public class LabelTest +{ + @Nested + class LabelListTest + { + @Test + public void testFindCycles_emptyList() + { + LabelList ll = new LabelList(); + assertDoesNotThrow(ll::findCycles); + } + + @Test + public void testFindCycles_1LabelCycle() + { + LabelList ll = createLabelListWith1LabelCycle(); + assertThrows(PrismLangException.class, ll::findCycles); + } + + @Test + public void testFindCycles_2LabelCycle() + { + LabelList ll = createLabelListWith2LabelCycle(); + assertThrows(PrismLangException.class, ll::findCycles); + } + + @Test + public void testFindCycles_noCycle() + { + LabelList ll = createLabelListWithoutCycle(); + assertDoesNotThrow(ll::findCycles); + } + } + + @Nested + class LabelEvaluterTest + { + @Test + public void testGetLabelValues() throws PrismLangException + { + /* + d is part of the state and will go from [0..5] + + label "l1" = "l2" | d=5 + label "l2" = d<=3 + */ + LabelList ll = createLabelListWithoutCycle(); + LabelEvaluator labelEvaluator = new LabelEvaluator(ll); + + // loop through all states and check label values + for (int i = 0; i <= 5; i++) { + // create the new state with 1 variable + State state = new State(1); + // set d to [0..5] + state.setValue(0, i); // index of d is 0 + + // expected labelValues + boolean l2 = i <= 3; + boolean l1 = l2 || i == 5; + + // compare + Predicate actualValues = labelEvaluator.getLabelValues(state); + assertEquals(l1, actualValues.test("l1")); + assertEquals(l2, actualValues.test("l2")); + } + } + } + + private LabelList createLabelListWithoutCycle() + { + /* + label "l1" = "l2" | d=5 + label "l2" = d<=3 + */ + LabelList ll = new LabelList(); + ExpressionVar dVar = new ExpressionVar("d", TypeInt.getInstance()); + dVar.setIndex(0); // index of d is 0 + ll.addLabel(new ExpressionIdent("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, + new ExpressionLabel("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, + dVar, new ExpressionLiteral(TypeInt.getInstance(), 5)))); + ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.LE, + dVar, new ExpressionLiteral(TypeInt.getInstance(), 3))); + return ll; + } + + private LabelList createLabelListWith1LabelCycle() + { + LabelList ll = new LabelList(); + /* label "l1" = "l1" */ + ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l1")); + return ll; + } + + private LabelList createLabelListWith2LabelCycle() + { + LabelList ll = new LabelList(); + /* + label "l1" = "l2" + label "l2" = "l1" | d=5 + */ + ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2")); + ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, + new ExpressionLabel("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, + new ExpressionVar("d", TypeInt.getInstance()), new ExpressionLiteral(TypeInt.getInstance(), 5)))); + return ll; + } +} From 1d56c7996b442886dfc98ea5394ecdf8f1a48a7b Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:46 +0200 Subject: [PATCH 6/7] prism-tests for labels inside labels and guards --- .../language/labels-inside-guards.lab | 4 + .../language/labels-inside-guards.prism | 16 +++ .../language/labels-inside-guards.prism.props | 3 + .../labels-inside-guards.prism.props.args | 5 + .../language/labels-inside-guards.sta | 4 + .../language/labels-inside-guards.tra | 8 ++ .../language/labels-inside-labels.lab | 13 +++ .../language/labels-inside-labels.prism | 33 ++++++ .../language/labels-inside-labels.prism.props | 10 ++ .../labels-inside-labels.prism.props.args | 5 + .../unit-tests/parser/ast/LabelListTest.java | 109 ++++++++++++++++++ 11 files changed, 210 insertions(+) create mode 100644 prism-tests/functionality/language/labels-inside-guards.lab create mode 100644 prism-tests/functionality/language/labels-inside-guards.prism create mode 100644 prism-tests/functionality/language/labels-inside-guards.prism.props create mode 100644 prism-tests/functionality/language/labels-inside-guards.prism.props.args create mode 100644 prism-tests/functionality/language/labels-inside-guards.sta create mode 100644 prism-tests/functionality/language/labels-inside-guards.tra create mode 100644 prism-tests/functionality/language/labels-inside-labels.lab create mode 100644 prism-tests/functionality/language/labels-inside-labels.prism create mode 100644 prism-tests/functionality/language/labels-inside-labels.prism.props create mode 100644 prism-tests/functionality/language/labels-inside-labels.prism.props.args create mode 100644 prism/unit-tests/parser/ast/LabelListTest.java diff --git a/prism-tests/functionality/language/labels-inside-guards.lab b/prism-tests/functionality/language/labels-inside-guards.lab new file mode 100644 index 0000000000..56c23fc1d5 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-guards.lab @@ -0,0 +1,4 @@ +0="init" 1="deadlock" 2="foo" +0: 0 +1: 2 +2: 2 diff --git a/prism-tests/functionality/language/labels-inside-guards.prism b/prism-tests/functionality/language/labels-inside-guards.prism new file mode 100644 index 0000000000..b588cdbe72 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-guards.prism @@ -0,0 +1,16 @@ +dtmc + +// 1. labels should not be expanded like formulas +// 2. label should be evaluated correctly so that +// (s1 = true & s2 = true) is unreachable + +module m1 + s1: bool init false; + + [] !"foo" -> (s1'=true); + [] true -> (s1'=false); +endmodule + +module m2=m1[s1=s2] endmodule + +label "foo" = s1 | s2; diff --git a/prism-tests/functionality/language/labels-inside-guards.prism.props b/prism-tests/functionality/language/labels-inside-guards.prism.props new file mode 100644 index 0000000000..9e8ae13014 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-guards.prism.props @@ -0,0 +1,3 @@ +// RESULT: 0 +P=? [ s1=true & s2=true ] + diff --git a/prism-tests/functionality/language/labels-inside-guards.prism.props.args b/prism-tests/functionality/language/labels-inside-guards.prism.props.args new file mode 100644 index 0000000000..c46b784845 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-guards.prism.props.args @@ -0,0 +1,5 @@ +-explicit -exportmodel labels-inside-guards.tra,sta,lab +-mtbdd -exportmodel labels-inside-guards.tra,sta,lab +-hybrid -exportmodel labels-inside-guards.tra,sta,lab +-sparse -exportmodel labels-inside-guards.tra,sta,lab +-exact diff --git a/prism-tests/functionality/language/labels-inside-guards.sta b/prism-tests/functionality/language/labels-inside-guards.sta new file mode 100644 index 0000000000..ebdc013c3a --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-guards.sta @@ -0,0 +1,4 @@ +(s1,s2) +0:(false,false) +1:(false,true) +2:(true,false) diff --git a/prism-tests/functionality/language/labels-inside-guards.tra b/prism-tests/functionality/language/labels-inside-guards.tra new file mode 100644 index 0000000000..651193bea4 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-guards.tra @@ -0,0 +1,8 @@ +3 7 +0 0 0.5 +0 1 0.25 +0 2 0.25 +1 0 0.5 +1 1 0.5 +2 0 0.5 +2 2 0.5 diff --git a/prism-tests/functionality/language/labels-inside-labels.lab b/prism-tests/functionality/language/labels-inside-labels.lab new file mode 100644 index 0000000000..f984265305 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-labels.lab @@ -0,0 +1,13 @@ +0="init" 1="deadlock" 2="l1" 3="l2" 4="l3" 5="l4" 6="l5" +0: 0 3 5 6 +1: 3 5 6 +2: 3 5 6 +3: 3 5 6 +4: 3 5 6 +5: 3 5 6 +6: 3 5 6 +7: 3 5 6 +8: 2 3 5 6 +9: 3 4 5 6 +10: 3 4 5 6 +11: 3 4 5 6 diff --git a/prism-tests/functionality/language/labels-inside-labels.prism b/prism-tests/functionality/language/labels-inside-labels.prism new file mode 100644 index 0000000000..5c73486b91 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-labels.prism @@ -0,0 +1,33 @@ +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the die + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> (s'=7); + +endmodule + +// l1 = ((d>=3 & d<=5) | d<=5) & d=2 +label "l1" = "l2" & d=2; +// l2 = (d>=3 & d<=5) | d<=5 +label "l2" = "l3" | "l4"; +// l3 = d>=3 & d<=5 +label "l3" = f2 & "l4"; +// l4 = d<=5 +label "l4" = f1; +// l5 = d<=5 +label "l5" = d<=5; + +formula f1 = "l5"; +formula f2 = d>=3; diff --git a/prism-tests/functionality/language/labels-inside-labels.prism.props b/prism-tests/functionality/language/labels-inside-labels.prism.props new file mode 100644 index 0000000000..a25a196ae3 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-labels.prism.props @@ -0,0 +1,10 @@ +// RESULT: 1/6 +P=? [ F s=7 & "l1" ] +// RESULT: 5/6 +P=? [ F s=7 & "l2" ] +// RESULT: 3/6 +P=? [ F s=7 & "l3" ] +// RESULT: 5/6 +P=? [ F s=7 & "l4" ] +// RESULT: 5/6 +P=? [ F s=7 & "l5" ] diff --git a/prism-tests/functionality/language/labels-inside-labels.prism.props.args b/prism-tests/functionality/language/labels-inside-labels.prism.props.args new file mode 100644 index 0000000000..cee1b246c9 --- /dev/null +++ b/prism-tests/functionality/language/labels-inside-labels.prism.props.args @@ -0,0 +1,5 @@ +-explicit -exportlabels labels-inside-labels.lab +-mtbdd -exportlabels labels-inside-labels.lab +-hybrid -exportlabels labels-inside-labels.lab +-sparse -exportlabels labels-inside-labels.lab +-exact diff --git a/prism/unit-tests/parser/ast/LabelListTest.java b/prism/unit-tests/parser/ast/LabelListTest.java new file mode 100644 index 0000000000..c562028696 --- /dev/null +++ b/prism/unit-tests/parser/ast/LabelListTest.java @@ -0,0 +1,109 @@ +package parser.ast; + +import org.junit.jupiter.api.Test; +import parser.State; +import parser.type.TypeInt; +import prism.PrismLangException; + +import java.util.Map; + +import static org.junit.jupiter.api.Assertions.*; + +public class LabelListTest +{ + @Test + public void testFindCycles_emptyList() + { + LabelList ll = new LabelList(); + assertDoesNotThrow(ll::findCycles); + } + + @Test + public void testFindCycles_1LabelCycle() + { + LabelList ll = createLabelListWith1LabelCycle(); + assertThrows(PrismLangException.class, ll::findCycles); + } + + @Test + public void testFindCycles_2LabelCycle() + { + LabelList ll = createLabelListWith2LabelCycle(); + assertThrows(PrismLangException.class, ll::findCycles); + } + + @Test + public void testFindCycles_noCycle() + { + LabelList ll = createLabelListWithoutCycle(); + assertDoesNotThrow(ll::findCycles); + } + + @Test + public void testGetLabelValues() throws PrismLangException + { + /* + d is part of the state and will go from [0..5] + + label "l1" = "l2" | d=5 + label "l2" = d<=3 + */ + LabelList ll = createLabelListWithoutCycle(); + + // loop through all states and check label values + for (int i = 0; i <= 5; i++) { + // create the new state with 1 variable + State state = new State(1); + // set d to [0..5] + state.setValue(0, i); // index of d is 0 + + // expected labelValues + boolean l2 = i <= 3; + boolean l1 = l2 || i == 5; + + // compare + Map actualValues = ll.getLabelValues(state); + assertEquals(l1, actualValues.get("l1")); + assertEquals(l2, actualValues.get("l2")); + } + } + + private LabelList createLabelListWithoutCycle() + { + /* + label "l1" = "l2" | d=5 + label "l2" = d<=3 + */ + LabelList ll = new LabelList(); + ExpressionVar dVar = new ExpressionVar("d", TypeInt.getInstance()); + dVar.setIndex(0); // index of d is 0 + ll.addLabel(new ExpressionIdent("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, + new ExpressionLabel("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, + dVar, new ExpressionLiteral(TypeInt.getInstance(), 5)))); + ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.LE, + dVar, new ExpressionLiteral(TypeInt.getInstance(), 3))); + return ll; + } + + private LabelList createLabelListWith1LabelCycle() + { + LabelList ll = new LabelList(); + /* label "l1" = "l1" */ + ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l1")); + return ll; + } + + private LabelList createLabelListWith2LabelCycle() + { + LabelList ll = new LabelList(); + /* + label "l1" = "l2" + label "l2" = "l1" | d=5 + */ + ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2")); + ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, + new ExpressionLabel("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, + new ExpressionVar("d", TypeInt.getInstance()), new ExpressionLiteral(TypeInt.getInstance(), 5)))); + return ll; + } +} From ed6f0c4161eb7d97383bfe525397b02540365729 Mon Sep 17 00:00:00 2001 From: Max Kurze Date: Mon, 3 Apr 2023 21:06:54 +0200 Subject: [PATCH 7/7] unittests for labels inside labels and guards --- prism/src/simulator/LabelEvaluator.java | 25 ++- .../parser/ast/LabelEvaluatorTest.java | 133 +++++++++++++++ .../unit-tests/parser/ast/LabelListTest.java | 109 ------------- prism/unit-tests/parser/ast/LabelTest.java | 151 +++++++++--------- 4 files changed, 220 insertions(+), 198 deletions(-) create mode 100644 prism/unit-tests/parser/ast/LabelEvaluatorTest.java delete mode 100644 prism/unit-tests/parser/ast/LabelListTest.java diff --git a/prism/src/simulator/LabelEvaluator.java b/prism/src/simulator/LabelEvaluator.java index 861c81a24f..99b06adfc1 100644 --- a/prism/src/simulator/LabelEvaluator.java +++ b/prism/src/simulator/LabelEvaluator.java @@ -34,26 +34,25 @@ public class LabelEvaluator public LabelEvaluator(LabelList labelList) throws PrismLangException { this.labelList = labelList; - this.evaluationOrder = fixEvaluationOrder(labelList); + this.evaluationOrder = fixEvaluationOrder(labelList.getLabelDependencies()); } /** * Fix an order on the labels such that l1 < l2 if l2 depends on l1. * - * @param labels a {@link LabelList} of labels to be evaluated + * @param deps an adjacency matrix with adj[i][j] iff i->j * @return an int array of the label indices in ascending order - * @throws PrismLangException In case a label dependencies could not be computed. */ - private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException + public int[] fixEvaluationOrder(boolean[][] deps) { - boolean[][] deps = labels.getLabelDependencies(); - assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cylce"; + assert deps.length == 0 || deps.length == deps[0].length : "dependency matrix must be square"; + assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cycle"; - int numLabels = labels.size(); + int numLabels = deps.length; BitSet done = new BitSet(numLabels); int[] order = new int[numLabels]; - for (int l = done.nextClearBit(0); l < numLabels; l = done.nextClearBit(l)) { - traverseDfs(deps, l, order, -1, done); + for (int l = done.nextClearBit(0), last = -1; l < numLabels; l = done.nextClearBit(l)) { + last = traverseDfs(deps, l, order, last, done); } return order; } @@ -113,7 +112,7 @@ public Predicate getLabelValues(State state) throws PrismLangException * This method provides all values of a certain label. They will be ordered by the given statesList.
* States will be evaluated if necessary. * - * @param label The name of the label. + * @param label The name of the label. * @param statesList The states to evaluate against in correct order. * @return All values of the label. * @throws PrismException In case a label evaluation fails. @@ -133,7 +132,7 @@ public BitSet getLabel(String label, List statesList) throws PrismExcepti /** * This method provides all label values of a certain state as a {@link BitSet}. - * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList} + * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList}. * * @param state The state to evaluate in. * @return Always returns a BitSet with the label values. @@ -150,7 +149,7 @@ protected BitSet getStateValues(State state) throws PrismLangException } /** - * Evaluates all label with the given state.
+ * Evaluates all label with the given state. * * @param state The state to evaluate the labels in. * @return A {@link BitSet} of all label values in this state. @@ -173,7 +172,7 @@ private BitSet evaluateState(State state) throws PrismLangException * Convert the label values for a state to a predicate on the label names. * * @param values the label values for some state - * @return a Predicate evaluating to {@code true} for a label name if the Bit at the corresponding index in {@code values} is set + * @return a Predicate evaluating to {@code true} for a label name iff the Bit at the corresponding index in {@code values} is set */ public Predicate asPredicate(BitSet values) { diff --git a/prism/unit-tests/parser/ast/LabelEvaluatorTest.java b/prism/unit-tests/parser/ast/LabelEvaluatorTest.java new file mode 100644 index 0000000000..2748245cee --- /dev/null +++ b/prism/unit-tests/parser/ast/LabelEvaluatorTest.java @@ -0,0 +1,133 @@ +package parser.ast; + +import org.junit.jupiter.api.Test; +import parser.State; +import prism.PrismLangException; +import simulator.LabelEvaluator; + +import java.util.Arrays; +import java.util.List; +import java.util.function.Predicate; +import java.util.stream.Collectors; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; +import static parser.ast.LabelTest.createLabelListWithDependencyChain; +import static parser.ast.LabelTest.createLabelListWithoutCycle; + +public class LabelEvaluatorTest +{ + @Test + public void testGetLabelValues() throws PrismLangException + { + /* + creating LabelList with + + label "l2" = d<=3; + label "l1" = "l2" | d=5; + + and checking for [0..5] of int d + */ + LabelList ll = createLabelListWithoutCycle(); + LabelEvaluator labelEvaluator = new LabelEvaluator(ll); + + // loop through all states and check label values + for (int i = 0; i <= 5; i++) { + // create the new state with 1 variable + State state = new State(1); + // set d to [0..5] + state.setValue(0, i); // index of d is 0 + + // expected labelValues + boolean l2 = i <= 3; + boolean l1 = l2 || i == 5; + + // compare + Predicate actualValues = labelEvaluator.getLabelValues(state); + assertEquals(l1, actualValues.test("l1")); + assertEquals(l2, actualValues.test("l2")); + } + } + + @Test + public void testLabelChainEvaluation() throws PrismLangException + { + LabelList ll = createLabelListWithDependencyChain(); + LabelEvaluator labelEvaluator = new LabelEvaluator(ll); + + State state = new State(0); + assertTrue(labelEvaluator.getLabelValue(state, "l1")); + assertTrue(labelEvaluator.getLabelValue(state, "l2")); + assertTrue(labelEvaluator.getLabelValue(state, "l3")); + } + + @Test + public void testLabelDFS_chain() throws PrismLangException + { + /* + * label "l0" = "l2" + * label "l2" = "l4" + * label "l4" = "l3" + * label "l3" = "l1" + */ + boolean[][] dependencies = new boolean[5][5]; + dependencies[0][2] = true; + dependencies[2][4] = true; + dependencies[4][3] = true; + dependencies[3][1] = true; + + List order = getEvaluationOrder(dependencies); + + assertTrue(order.indexOf(2) < order.indexOf(0)); + assertTrue(order.indexOf(4) < order.indexOf(2)); + assertTrue(order.indexOf(3) < order.indexOf(4)); + assertTrue(order.indexOf(1) < order.indexOf(3)); + } + + @Test + public void testLabelDFS_unrelatedLabels() throws PrismLangException + { + // all false -- no dependencies + boolean[][] dependencies = new boolean[5][5]; + + List order = getEvaluationOrder(dependencies); + + assertEquals(5, order.size()); + } + + @Test + public void testLabelDFS_multipleCorrelationComponents() throws PrismLangException + { + /* + * label "l0" = "l1" & "l3" + * label "l3" = "l1" + * + * label "l4" = "l2" & "l5" + * label "l2" = "l6" + */ + boolean[][] dependencies = new boolean[7][7]; + dependencies[0][1] = dependencies[0][3] = true; + dependencies[3][1] = true; + dependencies[4][2] = dependencies[4][5] = true; + dependencies[2][6] = true; + + List order = getEvaluationOrder(dependencies); + + assertTrue(order.indexOf(1) < order.indexOf(0)); + assertTrue(order.indexOf(3) < order.indexOf(0)); + + assertTrue(order.indexOf(1) < order.indexOf(3)); + + assertTrue(order.indexOf(2) < order.indexOf(4)); + assertTrue(order.indexOf(5) < order.indexOf(4)); + + assertTrue(order.indexOf(6) < order.indexOf(2)); + } + + private List getEvaluationOrder(boolean[][] deps) throws PrismLangException + { + LabelEvaluator labelEvaluator = new LabelEvaluator(new LabelList()); + return Arrays.stream(labelEvaluator.fixEvaluationOrder(deps)).boxed().collect(Collectors.toList()); + } + +} diff --git a/prism/unit-tests/parser/ast/LabelListTest.java b/prism/unit-tests/parser/ast/LabelListTest.java deleted file mode 100644 index c562028696..0000000000 --- a/prism/unit-tests/parser/ast/LabelListTest.java +++ /dev/null @@ -1,109 +0,0 @@ -package parser.ast; - -import org.junit.jupiter.api.Test; -import parser.State; -import parser.type.TypeInt; -import prism.PrismLangException; - -import java.util.Map; - -import static org.junit.jupiter.api.Assertions.*; - -public class LabelListTest -{ - @Test - public void testFindCycles_emptyList() - { - LabelList ll = new LabelList(); - assertDoesNotThrow(ll::findCycles); - } - - @Test - public void testFindCycles_1LabelCycle() - { - LabelList ll = createLabelListWith1LabelCycle(); - assertThrows(PrismLangException.class, ll::findCycles); - } - - @Test - public void testFindCycles_2LabelCycle() - { - LabelList ll = createLabelListWith2LabelCycle(); - assertThrows(PrismLangException.class, ll::findCycles); - } - - @Test - public void testFindCycles_noCycle() - { - LabelList ll = createLabelListWithoutCycle(); - assertDoesNotThrow(ll::findCycles); - } - - @Test - public void testGetLabelValues() throws PrismLangException - { - /* - d is part of the state and will go from [0..5] - - label "l1" = "l2" | d=5 - label "l2" = d<=3 - */ - LabelList ll = createLabelListWithoutCycle(); - - // loop through all states and check label values - for (int i = 0; i <= 5; i++) { - // create the new state with 1 variable - State state = new State(1); - // set d to [0..5] - state.setValue(0, i); // index of d is 0 - - // expected labelValues - boolean l2 = i <= 3; - boolean l1 = l2 || i == 5; - - // compare - Map actualValues = ll.getLabelValues(state); - assertEquals(l1, actualValues.get("l1")); - assertEquals(l2, actualValues.get("l2")); - } - } - - private LabelList createLabelListWithoutCycle() - { - /* - label "l1" = "l2" | d=5 - label "l2" = d<=3 - */ - LabelList ll = new LabelList(); - ExpressionVar dVar = new ExpressionVar("d", TypeInt.getInstance()); - dVar.setIndex(0); // index of d is 0 - ll.addLabel(new ExpressionIdent("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, - new ExpressionLabel("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, - dVar, new ExpressionLiteral(TypeInt.getInstance(), 5)))); - ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.LE, - dVar, new ExpressionLiteral(TypeInt.getInstance(), 3))); - return ll; - } - - private LabelList createLabelListWith1LabelCycle() - { - LabelList ll = new LabelList(); - /* label "l1" = "l1" */ - ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l1")); - return ll; - } - - private LabelList createLabelListWith2LabelCycle() - { - LabelList ll = new LabelList(); - /* - label "l1" = "l2" - label "l2" = "l1" | d=5 - */ - ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2")); - ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, - new ExpressionLabel("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, - new ExpressionVar("d", TypeInt.getInstance()), new ExpressionLiteral(TypeInt.getInstance(), 5)))); - return ll; - } -} diff --git a/prism/unit-tests/parser/ast/LabelTest.java b/prism/unit-tests/parser/ast/LabelTest.java index f512a90ddf..a00785cdb2 100644 --- a/prism/unit-tests/parser/ast/LabelTest.java +++ b/prism/unit-tests/parser/ast/LabelTest.java @@ -1,92 +1,57 @@ package parser.ast; -import org.junit.jupiter.api.Nested; import org.junit.jupiter.api.Test; -import parser.State; +import parser.type.TypeBool; import parser.type.TypeInt; import prism.PrismLangException; -import simulator.LabelEvaluator; - -import java.util.function.Predicate; import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; -import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertThrows; public class LabelTest { - @Nested - class LabelListTest + @Test + public void testFindCycles_emptyList() { - @Test - public void testFindCycles_emptyList() - { - LabelList ll = new LabelList(); - assertDoesNotThrow(ll::findCycles); - } - - @Test - public void testFindCycles_1LabelCycle() - { - LabelList ll = createLabelListWith1LabelCycle(); - assertThrows(PrismLangException.class, ll::findCycles); - } - - @Test - public void testFindCycles_2LabelCycle() - { - LabelList ll = createLabelListWith2LabelCycle(); - assertThrows(PrismLangException.class, ll::findCycles); - } - - @Test - public void testFindCycles_noCycle() - { - LabelList ll = createLabelListWithoutCycle(); - assertDoesNotThrow(ll::findCycles); - } + LabelList ll = new LabelList(); + assertDoesNotThrow(ll::findCycles); } - @Nested - class LabelEvaluterTest + @Test + public void testFindCycles_1LabelCycle() { - @Test - public void testGetLabelValues() throws PrismLangException - { - /* - d is part of the state and will go from [0..5] - - label "l1" = "l2" | d=5 - label "l2" = d<=3 - */ - LabelList ll = createLabelListWithoutCycle(); - LabelEvaluator labelEvaluator = new LabelEvaluator(ll); - - // loop through all states and check label values - for (int i = 0; i <= 5; i++) { - // create the new state with 1 variable - State state = new State(1); - // set d to [0..5] - state.setValue(0, i); // index of d is 0 + LabelList ll = createLabelListWith1LabelCycle(); + assertThrows(PrismLangException.class, ll::findCycles); + } - // expected labelValues - boolean l2 = i <= 3; - boolean l1 = l2 || i == 5; + @Test + public void testFindCycles_2LabelCycle() + { + LabelList ll = createLabelListWith2LabelCycle(); + assertThrows(PrismLangException.class, ll::findCycles); + } - // compare - Predicate actualValues = labelEvaluator.getLabelValues(state); - assertEquals(l1, actualValues.test("l1")); - assertEquals(l2, actualValues.test("l2")); - } - } + @Test + public void testFindCycles_noCycle() + { + LabelList ll = createLabelListWithoutCycle(); + assertDoesNotThrow(ll::findCycles); } - private LabelList createLabelListWithoutCycle() + /** + *

+ * Helper method that will create a {@link LabelList} with the following Labels: + *

+ *
    + *
  • label "l2" = d<=3;
    • + *
  • label "l1" = "l2" | d=5;
    • + *
+ *

+ * Note: d is the only variable (index 0) and has {@link TypeInt} + *

+ */ + protected static LabelList createLabelListWithoutCycle() { - /* - label "l1" = "l2" | d=5 - label "l2" = d<=3 - */ LabelList ll = new LabelList(); ExpressionVar dVar = new ExpressionVar("d", TypeInt.getInstance()); dVar.setIndex(0); // index of d is 0 @@ -98,25 +63,59 @@ private LabelList createLabelListWithoutCycle() return ll; } - private LabelList createLabelListWith1LabelCycle() + /** + *

+ * Helper method that will create a {@link LabelList} with the following Labels: + *

+ *
    + *
  • label "l1" = "l1";
    • + *
+ */ + protected static LabelList createLabelListWith1LabelCycle() { LabelList ll = new LabelList(); - /* label "l1" = "l1" */ ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l1")); return ll; } - private LabelList createLabelListWith2LabelCycle() + /** + *

+ * Helper method that will create a {@link LabelList} with the following Labels: + *

+ *
    + *
  • label "l1" = "l2";
    • + *
  • label "l2" = "l1" | d=5;
    • + *
+ *

+ * Note: d is the only variable (index 0) and has {@link TypeInt} + *

+ */ + protected static LabelList createLabelListWith2LabelCycle() { LabelList ll = new LabelList(); - /* - label "l1" = "l2" - label "l2" = "l1" | d=5 - */ ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2")); ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.OR, new ExpressionLabel("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ, new ExpressionVar("d", TypeInt.getInstance()), new ExpressionLiteral(TypeInt.getInstance(), 5)))); return ll; } + + /** + *

+ * Helper method that will create a {@link LabelList} with the following Labels: + *

+ *
    + *
  • label "l1" = "l2";
    • + *
  • label "l2" = "l3";
    • + *
  • label "l3" = true;
    • + *
+ */ + protected static LabelList createLabelListWithDependencyChain() + { + LabelList ll = new LabelList(); + ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2")); + ll.addLabel(new ExpressionIdent("l2"), new ExpressionLabel("l3")); + ll.addLabel(new ExpressionIdent("l3"), new ExpressionLiteral(TypeBool.getInstance(), true)); + return ll; + } }