s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Added iff (<=>) to PRISM model/properties language. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3175 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
2dfc151b8a
commit
3c8ca8495d
10 changed files with 801 additions and 697 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1136
      prism/src/parser/PrismParser.java
  2. 16
      prism/src/parser/PrismParser.jj
  3. 65
      prism/src/parser/PrismParserConstants.java
  4. 216
      prism/src/parser/PrismParserTokenManager.java
  5. 11
      prism/src/parser/ast/Expression.java
  6. 31
      prism/src/parser/ast/ExpressionBinaryOp.java
  7. 3
      prism/src/parser/visitor/ConvertForJltl2ba.java
  8. 16
      prism/src/parser/visitor/Simplify.java
  9. 1
      prism/src/parser/visitor/TypeCheck.java
  10. 3
      prism/src/prism/StateModelChecker.java

1136
prism/src/parser/PrismParser.java
File diff suppressed because it is too large
View File

16
prism/src/parser/PrismParser.jj
View File

@ -411,6 +411,7 @@ TOKEN :
| < AND: "&" >
| < OR: "|" >
| < IMPLIES: "=>" >
| < IFF: "<=>" >
| < RARROW: "->" >
| < COLON: ":" >
| < SEMICOLON: ";" >
@ -1120,9 +1121,22 @@ Expression ExpressionImplies(boolean prop, boolean pathprop) :
Expression ret, expr;
Token begin = null;
}
{
{ begin = getToken(1); } ret = ExpressionIff(prop, pathprop)
( <IMPLIES> expr = ExpressionIff(prop, pathprop) { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0)); } )*
{ return ret; }
}
// Expression: if-and-only-iff
Expression ExpressionIff(boolean prop, boolean pathprop) :
{
Expression ret, expr;
Token begin = null;
}
{
{ begin = getToken(1); } ret = ExpressionOr(prop, pathprop)
( <IMPLIES> expr = ExpressionOr(prop, pathprop) { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0)); } )*
( <IFF> expr = ExpressionOr(prop, pathprop) { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IFF, ret, expr); ret.setPosition(begin, getToken(0)); } )*
{ return ret; }
}

65
prism/src/parser/PrismParserConstants.java
View File

@ -121,67 +121,69 @@ public interface PrismParserConstants {
/** RegularExpression Id. */
int IMPLIES = 55;
/** RegularExpression Id. */
int RARROW = 56;
int IFF = 56;
/** RegularExpression Id. */
int COLON = 57;
int RARROW = 57;
/** RegularExpression Id. */
int SEMICOLON = 58;
int COLON = 58;
/** RegularExpression Id. */
int COMMA = 59;
int SEMICOLON = 59;
/** RegularExpression Id. */
int DOTS = 60;
int COMMA = 60;
/** RegularExpression Id. */
int LPARENTH = 61;
int DOTS = 61;
/** RegularExpression Id. */
int RPARENTH = 62;
int LPARENTH = 62;
/** RegularExpression Id. */
int LBRACKET = 63;
int RPARENTH = 63;
/** RegularExpression Id. */
int RBRACKET = 64;
int LBRACKET = 64;
/** RegularExpression Id. */
int LBRACE = 65;
int RBRACKET = 65;
/** RegularExpression Id. */
int RBRACE = 66;
int LBRACE = 66;
/** RegularExpression Id. */
int EQ = 67;
int RBRACE = 67;
/** RegularExpression Id. */
int NE = 68;
int EQ = 68;
/** RegularExpression Id. */
int LT = 69;
int NE = 69;
/** RegularExpression Id. */
int GT = 70;
int LT = 70;
/** RegularExpression Id. */
int LE = 71;
int GT = 71;
/** RegularExpression Id. */
int GE = 72;
int LE = 72;
/** RegularExpression Id. */
int PLUS = 73;
int GE = 73;
/** RegularExpression Id. */
int MINUS = 74;
int PLUS = 74;
/** RegularExpression Id. */
int TIMES = 75;
int MINUS = 75;
/** RegularExpression Id. */
int DIVIDE = 76;
int TIMES = 76;
/** RegularExpression Id. */
int PRIME = 77;
int DIVIDE = 77;
/** RegularExpression Id. */
int RENAME = 78;
int PRIME = 78;
/** RegularExpression Id. */
int QMARK = 79;
int RENAME = 79;
/** RegularExpression Id. */
int DQUOTE = 80;
int QMARK = 80;
/** RegularExpression Id. */
int REG_INT = 81;
int DQUOTE = 81;
/** RegularExpression Id. */
int REG_DOUBLE = 82;
int REG_INT = 82;
/** RegularExpression Id. */
int REG_IDENTPRIME = 83;
int REG_DOUBLE = 83;
/** RegularExpression Id. */
int REG_IDENT = 84;
int REG_IDENTPRIME = 84;
/** RegularExpression Id. */
int PREPROC = 85;
int REG_IDENT = 85;
/** RegularExpression Id. */
int LEXICAL_ERROR = 86;
int PREPROC = 86;
/** RegularExpression Id. */
int LEXICAL_ERROR = 87;
/** Lexical state. */
int DEFAULT = 0;
@ -244,6 +246,7 @@ public interface PrismParserConstants {
"\"&\"",
"\"|\"",
"\"=>\"",
"\"<=>\"",
"\"->\"",
"\":\"",
"\";\"",

216
prism/src/parser/PrismParserTokenManager.java
View File

@ -23,33 +23,36 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 0:
if ((active0 & 0xc783a04a00908L) != 0L)
return 23;
if ((active1 & 0x1000L) != 0L)
if ((active1 & 0x2000L) != 0L)
return 1;
if ((active0 & 0x1000000000000000L) != 0L)
if ((active0 & 0x2000000000000000L) != 0L)
return 11;
if ((active0 & 0x387c5fb5ff6f0L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
return 23;
}
return -1;
case 1:
if ((active0 & 0x39fddfb5ff6f0L) != 0L)
{
jjmatchedKind = 84;
jjmatchedPos = 1;
if (jjmatchedPos != 1)
{
jjmatchedKind = 85;
jjmatchedPos = 1;
}
return 23;
}
return -1;
case 2:
if ((active0 & 0x100e8000000L) != 0L)
return 23;
if ((active0 & 0x39edd135ff6f0L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 2;
return 23;
}
if ((active0 & 0x100e8000000L) != 0L)
return 23;
return -1;
case 3:
if ((active0 & 0x21ad801100490L) != 0L)
@ -58,66 +61,66 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
{
if (jjmatchedPos != 3)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 3;
}
return 23;
}
return -1;
case 4:
if ((active0 & 0x10020060L) != 0L)
return 23;
if ((active0 & 0x18445024df200L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 4;
return 23;
}
if ((active0 & 0x10020060L) != 0L)
return 23;
return -1;
case 5:
if ((active0 & 0x1000100480200L) != 0L)
return 23;
if ((active0 & 0x84440205f000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 5;
return 23;
}
return -1;
case 6:
if ((active0 & 0x40000041000L) != 0L)
return 23;
if ((active0 & 0x80440201e000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 6;
return 23;
}
if ((active0 & 0x40000041000L) != 0L)
return 23;
return -1;
case 7:
if ((active0 & 0x80440201e000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 7;
return 23;
}
return -1;
case 8:
if ((active0 & 0x2014000L) != 0L)
return 23;
if ((active0 & 0x80440000a000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 8;
return 23;
}
if ((active0 & 0x2014000L) != 0L)
return 23;
return -1;
case 9:
if ((active0 & 0x800000008000L) != 0L)
return 23;
if ((active0 & 0x4400002000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 9;
return 23;
}
@ -125,7 +128,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 10:
if ((active0 & 0x4400002000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 10;
return 23;
}
@ -135,7 +138,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x4400000000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 11;
return 23;
}
@ -145,7 +148,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x400000000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 12;
return 23;
}
@ -153,7 +156,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 13:
if ((active0 & 0x400000000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 13;
return 23;
}
@ -161,7 +164,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 14:
if ((active0 & 0x400000000L) != 0L)
{
jjmatchedKind = 84;
jjmatchedKind = 85;
jjmatchedPos = 14;
return 23;
}
@ -186,45 +189,45 @@ static private int jjMoveStringLiteralDfa0_0()
{
case 33:
jjmatchedKind = 52;
return jjMoveStringLiteralDfa1_0(0x0L, 0x10L);
return jjMoveStringLiteralDfa1_0(0x0L, 0x20L);
case 34:
return jjStopAtPos(0, 80);
return jjStopAtPos(0, 81);
case 38:
return jjStopAtPos(0, 53);
case 39:
return jjStopAtPos(0, 77);
return jjStopAtPos(0, 78);
case 40:
return jjStopAtPos(0, 61);
case 41:
return jjStopAtPos(0, 62);
case 41:
return jjStopAtPos(0, 63);
case 42:
return jjStopAtPos(0, 75);
return jjStopAtPos(0, 76);
case 43:
return jjStopAtPos(0, 73);
return jjStopAtPos(0, 74);
case 44:
return jjStopAtPos(0, 59);
return jjStopAtPos(0, 60);
case 45:
jjmatchedKind = 74;
return jjMoveStringLiteralDfa1_0(0x100000000000000L, 0x0L);
jjmatchedKind = 75;
return jjMoveStringLiteralDfa1_0(0x200000000000000L, 0x0L);
case 46:
return jjMoveStringLiteralDfa1_0(0x1000000000000000L, 0x0L);
return jjMoveStringLiteralDfa1_0(0x2000000000000000L, 0x0L);
case 47:
return jjStartNfaWithStates_0(0, 76, 1);
return jjStartNfaWithStates_0(0, 77, 1);
case 58:
return jjStopAtPos(0, 57);
case 59:
return jjStopAtPos(0, 58);
case 59:
return jjStopAtPos(0, 59);
case 60:
jjmatchedKind = 69;
return jjMoveStringLiteralDfa1_0(0x0L, 0x4080L);
jjmatchedKind = 70;
return jjMoveStringLiteralDfa1_0(0x100000000000000L, 0x8100L);
case 61:
jjmatchedKind = 67;
jjmatchedKind = 68;
return jjMoveStringLiteralDfa1_0(0x80000000000000L, 0x0L);
case 62:
jjmatchedKind = 70;
return jjMoveStringLiteralDfa1_0(0x0L, 0x100L);
jjmatchedKind = 71;
return jjMoveStringLiteralDfa1_0(0x0L, 0x200L);
case 63:
return jjStopAtPos(0, 79);
return jjStopAtPos(0, 80);
case 65:
return jjStartNfaWithStates_0(0, 3, 23);
case 67:
@ -252,9 +255,9 @@ static private int jjMoveStringLiteralDfa0_0()
case 88:
return jjStartNfaWithStates_0(0, 33, 23);
case 91:
return jjStopAtPos(0, 63);
case 93:
return jjStopAtPos(0, 64);
case 93:
return jjStopAtPos(0, 65);
case 98:
return jjMoveStringLiteralDfa1_0(0x10L, 0x0L);
case 99:
@ -284,11 +287,11 @@ static private int jjMoveStringLiteralDfa0_0()
case 116:
return jjMoveStringLiteralDfa1_0(0x2000000000000L, 0x0L);
case 123:
return jjStopAtPos(0, 65);
return jjStopAtPos(0, 66);
case 124:
return jjStopAtPos(0, 54);
case 125:
return jjStopAtPos(0, 66);
return jjStopAtPos(0, 67);
default :
return jjMoveNfa_0(0, 0);
}
@ -303,26 +306,29 @@ static private int jjMoveStringLiteralDfa1_0(long active0, long active1)
switch(curChar)
{
case 45:
if ((active1 & 0x4000L) != 0L)
return jjStopAtPos(1, 78);
if ((active1 & 0x8000L) != 0L)
return jjStopAtPos(1, 79);
break;
case 46:
if ((active0 & 0x1000000000000000L) != 0L)
return jjStopAtPos(1, 60);
if ((active0 & 0x2000000000000000L) != 0L)
return jjStopAtPos(1, 61);
break;
case 61:
if ((active1 & 0x10L) != 0L)
return jjStopAtPos(1, 68);
else if ((active1 & 0x80L) != 0L)
return jjStopAtPos(1, 71);
if ((active1 & 0x20L) != 0L)
return jjStopAtPos(1, 69);
else if ((active1 & 0x100L) != 0L)
return jjStopAtPos(1, 72);
break;
{
jjmatchedKind = 72;
jjmatchedPos = 1;
}
else if ((active1 & 0x200L) != 0L)
return jjStopAtPos(1, 73);
return jjMoveStringLiteralDfa2_0(active0, 0x100000000000000L, active1, 0L);
case 62:
if ((active0 & 0x80000000000000L) != 0L)
return jjStopAtPos(1, 55);
else if ((active0 & 0x100000000000000L) != 0L)
return jjStopAtPos(1, 56);
else if ((active0 & 0x200000000000000L) != 0L)
return jjStopAtPos(1, 57);
break;
case 97:
return jjMoveStringLiteralDfa2_0(active0, 0x20030020000L, active1, 0L);
@ -364,6 +370,10 @@ static private int jjMoveStringLiteralDfa2_0(long old0, long active0, long old1,
}
switch(curChar)
{
case 62:
if ((active0 & 0x100000000000000L) != 0L)
return jjStopAtPos(2, 56);
break;
case 97:
if ((active0 & 0x10000000000L) != 0L)
return jjStartNfaWithStates_0(2, 40, 23);
@ -853,14 +863,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 23:
if ((0x3ff000000000000L & l) != 0L)
{
if (kind > 84)
kind = 84;
if (kind > 85)
kind = 85;
jjCheckNAdd(22);
}
else if (curChar == 39)
{
if (kind > 83)
kind = 83;
if (kind > 84)
kind = 84;
}
if ((0x3ff000000000000L & l) != 0L)
jjCheckNAddTwoStates(20, 21);
@ -868,8 +878,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 0:
if ((0x3ff000000000000L & l) != 0L)
{
if (kind > 82)
kind = 82;
if (kind > 83)
kind = 83;
jjCheckNAddStates(0, 3);
}
else if ((0x100002600L & l) != 0L)
@ -885,14 +895,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
jjstateSet[jjnewStateCnt++] = 1;
if ((0x3fe000000000000L & l) != 0L)
{
if (kind > 81)
kind = 81;
if (kind > 82)
kind = 82;
jjCheckNAdd(8);
}
else if (curChar == 48)
{
if (kind > 81)
kind = 81;
if (kind > 82)
kind = 82;
}
break;
case 1:
@ -922,20 +932,20 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 7:
if ((0x3fe000000000000L & l) == 0L)
break;
if (kind > 81)
kind = 81;
if (kind > 82)
kind = 82;
jjCheckNAdd(8);
break;
case 8:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 81)
kind = 81;
if (kind > 82)
kind = 82;
jjCheckNAdd(8);
break;
case 9:
if (curChar == 48 && kind > 81)
kind = 81;
if (curChar == 48 && kind > 82)
kind = 82;
break;
case 10:
if (curChar == 46)
@ -944,8 +954,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 11:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 82)
kind = 82;
if (kind > 83)
kind = 83;
jjCheckNAddTwoStates(11, 12);
break;
case 13:
@ -955,8 +965,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 14:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 82)
kind = 82;
if (kind > 83)
kind = 83;
jjCheckNAdd(14);
break;
case 15:
@ -968,14 +978,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
jjCheckNAddTwoStates(16, 17);
break;
case 17:
if (curChar == 35 && kind > 85)
kind = 85;
if (curChar == 35 && kind > 86)
kind = 86;
break;
case 18:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 82)
kind = 82;
if (kind > 83)
kind = 83;
jjCheckNAddStates(0, 3);
break;
case 20:
@ -983,14 +993,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
jjCheckNAddTwoStates(20, 21);
break;
case 21:
if (curChar == 39 && kind > 83)
kind = 83;
if (curChar == 39 && kind > 84)
kind = 84;
break;
case 22:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 84)
kind = 84;
if (kind > 85)
kind = 85;
jjCheckNAdd(22);
break;
default : break;
@ -1007,8 +1017,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 23:
if ((0x7fffffe87fffffeL & l) != 0L)
{
if (kind > 84)
kind = 84;
if (kind > 85)
kind = 85;
jjCheckNAdd(22);
}
if ((0x7fffffe87fffffeL & l) != 0L)
@ -1017,8 +1027,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 0:
if ((0x7fffffe87fffffeL & l) == 0L)
break;
if (kind > 84)
kind = 84;
if (kind > 85)
kind = 85;
jjCheckNAddStates(7, 9);
break;
case 2:
@ -1038,8 +1048,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
case 22:
if ((0x7fffffe87fffffeL & l) == 0L)
break;
if (kind > 84)
kind = 84;
if (kind > 85)
kind = 85;
jjCheckNAdd(22);
break;
default : break;
@ -1113,17 +1123,17 @@ public static final String[] jjstrLiteralImages = {
"\160\162\157\142\141\142\151\154\151\163\164\151\143", "\160\162\157\142", "\160\164\141", "\162\141\164\145",
"\162\145\167\141\162\144\163", "\122\155\141\170", "\122\155\151\156", "\122", "\123",
"\163\164\157\143\150\141\163\164\151\143", "\163\171\163\164\145\155", "\164\162\165\145", "\125", "\127", "\41", "\46",
"\174", "\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", "\133",
"\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53",
"\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null, null,
null, };
"\174", "\75\76", "\74\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51",
"\133", "\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75",
"\53", "\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null,
null, null, };
/** Lexer state names. */
public static final String[] lexStateNames = {
"DEFAULT",
};
static final long[] jjtoToken = {
0xfffffffffffffff9L, 0x7fffffL,
0xfffffffffffffff9L, 0xffffffL,
};
static final long[] jjtoSkip = {
0x6L, 0x0L,
@ -1236,9 +1246,9 @@ public static Token getNextToken()
jjmatchedKind = 0x7fffffff;
jjmatchedPos = 0;
curPos = jjMoveStringLiteralDfa0_0();
if (jjmatchedPos == 0 && jjmatchedKind > 86)
if (jjmatchedPos == 0 && jjmatchedKind > 87)
{
jjmatchedKind = 86;
jjmatchedKind = 87;
}
if (jjmatchedKind != 0x7fffffff)
{

11
prism/src/parser/ast/Expression.java
View File

@ -369,6 +369,11 @@ public abstract class Expression extends ASTElement
return new ExpressionBinaryOp(ExpressionBinaryOp.OR, expr1, expr2);
}
public static Expression Iff(Expression expr1, Expression expr2)
{
return new ExpressionBinaryOp(ExpressionBinaryOp.IFF, expr1, expr2);
}
public static Expression Implies(Expression expr1, Expression expr2)
{
return new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, expr1, expr2);
@ -437,6 +442,12 @@ public abstract class Expression extends ASTElement
return expr instanceof ExpressionBinaryOp && ((ExpressionBinaryOp) expr).getOperator() == ExpressionBinaryOp.OR;
}
public static boolean isIff(Expression expr)
{
return expr instanceof ExpressionBinaryOp
&& ((ExpressionBinaryOp) expr).getOperator() == ExpressionBinaryOp.IFF;
}
public static boolean isImplies(Expression expr)
{
return expr instanceof ExpressionBinaryOp

31
prism/src/parser/ast/ExpressionBinaryOp.java
View File

@ -35,22 +35,23 @@ public class ExpressionBinaryOp extends Expression
{
// Operator constants
public static final int IMPLIES = 1;
public static final int OR = 2;
public static final int AND = 3;
public static final int EQ = 4;
public static final int NE = 5;
public static final int GT = 6;
public static final int GE = 7;
public static final int LT = 8;
public static final int LE = 9;
public static final int PLUS = 10;
public static final int MINUS = 11;
public static final int TIMES = 12;
public static final int DIVIDE = 13;
public static final int IFF = 2;
public static final int OR = 3;
public static final int AND = 4;
public static final int EQ = 5;
public static final int NE = 6;
public static final int GT = 7;
public static final int GE = 8;
public static final int LT = 9;
public static final int LE = 10;
public static final int PLUS = 11;
public static final int MINUS = 12;
public static final int TIMES = 13;
public static final int DIVIDE = 14;
// Operator symbols
public static final String opSymbols[] = { "", "=>", "|", "&", "=", "!=", ">", ">=", "<", "<=", "+", "-", "*", "/" };
public static final String opSymbols[] = { "", "=>", "<=>", "|", "&", "=", "!=", ">", ">=", "<", "<=", "+", "-", "*", "/" };
// Operator type testers
public static boolean isLogical(int op) { return op==IMPLIES || op==OR || op==AND; }
public static boolean isLogical(int op) { return op==IMPLIES || op==IFF || op==OR || op==AND; }
public static boolean isRelOp(int op) { return op==EQ || op==NE || op==GT || op==GE || op==LT || op==LE; }
public static boolean isArithmetic(int op) { return op==PLUS || op==MINUS || op==TIMES || op==DIVIDE; }
@ -131,6 +132,8 @@ public class ExpressionBinaryOp extends Expression
switch (op) {
case IMPLIES:
return new Boolean(!operand1.evaluateBoolean(ec) || operand2.evaluateBoolean(ec));
case IFF:
return new Boolean(operand1.evaluateBoolean(ec) == operand2.evaluateBoolean(ec));
case OR:
return new Boolean(operand1.evaluateBoolean(ec) || operand2.evaluateBoolean(ec));
case AND:

3
prism/src/parser/visitor/ConvertForJltl2ba.java
View File

@ -96,6 +96,9 @@ public class ConvertForJltl2ba extends ASTTraverseModify
case ExpressionBinaryOp.IMPLIES:
res = new SimpleLTL(SimpleLTL.LTLType.IMPLIES, ltl1, ltl2);
break;
case ExpressionBinaryOp.IFF:
res = new SimpleLTL(SimpleLTL.LTLType.EQUIV, ltl1, ltl2);
break;
case ExpressionBinaryOp.OR:
res = new SimpleLTL(SimpleLTL.LTLType.OR, ltl1, ltl2);
break;

16
prism/src/parser/visitor/Simplify.java
View File

@ -54,6 +54,22 @@ public class Simplify extends ASTTraverseModify
if (Expression.isTrue(e.getOperand1()))
return e.getOperand2();
break;
case ExpressionBinaryOp.IFF:
if (Expression.isFalse(e.getOperand1())) {
if (Expression.isFalse(e.getOperand2())) {
return Expression.True();
} else if (Expression.isTrue(e.getOperand2())) {
return Expression.False();
}
}
if (Expression.isTrue(e.getOperand1())) {
if (Expression.isFalse(e.getOperand2())) {
return Expression.False();
} else if (Expression.isTrue(e.getOperand2())) {
return Expression.True();
}
}
break;
case ExpressionBinaryOp.OR:
if (Expression.isTrue(e.getOperand1()) || Expression.isTrue(e.getOperand2()))
return Expression.True();

1
prism/src/parser/visitor/TypeCheck.java
View File

@ -246,6 +246,7 @@ public class TypeCheck extends ASTTraverse
switch (e.getOperator()) {
case ExpressionBinaryOp.IMPLIES:
case ExpressionBinaryOp.IFF:
case ExpressionBinaryOp.OR:
case ExpressionBinaryOp.AND:
if (!(t1 instanceof TypeBool) && !(t1 instanceof TypePathBool)) {

3
prism/src/prism/StateModelChecker.java
View File

@ -401,6 +401,9 @@ public class StateModelChecker implements ModelChecker
case ExpressionBinaryOp.IMPLIES:
dd = JDD.Or(JDD.Not(dd1), dd2);
break;
case ExpressionBinaryOp.IFF:
dd = JDD.Not(JDD.Xor(dd1, dd2));
break;
case ExpressionBinaryOp.OR:
dd = JDD.Or(dd1, dd2);
break;

Write Preview
Loading…
Cancel
Save