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

Updates to filters. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1801 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
142f33ca52
commit
726ff06c1b
8 changed files with 635 additions and 456 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. 744
      prism/src/parser/PrismParser.java
  2. 26
      prism/src/parser/PrismParser.jj
  3. 94
      prism/src/parser/PrismParserConstants.java
  4. 176
      prism/src/parser/PrismParserTokenManager.java
  5. 6
      prism/src/parser/ast/ExpressionFilter.java
  6. 20
      prism/src/parser/ast/Filter.java
  7. 23
      prism/src/parser/visitor/TypeCheck.java
  8. 2
      prism/src/prism/StateModelChecker.java

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

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

@ -1425,7 +1425,7 @@ Expression ExpressionProb(boolean prop, boolean pathprop) :
// Filter is actually dealt with by wrapping this expression in
// an (invisible) ExpressionFilter expression
if (filter != null) {
String filterOp = isBool ? "&" : filter.minRequested() ? "min" : "max";
String filterOp = isBool ? "&" : filter.getFilterOpString();
ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression());
ef.setInvisible(true);
return ef;
@ -1462,14 +1462,15 @@ Expression ExpressionSS(boolean prop, boolean pathprop) :
Filter filter = null;
ExpressionSS ret = new ExpressionSS();
Token begin;
boolean isBool;
}
{
// This production is only allowed in expressions if the "prop" parameter is true
{ if (!prop) throw generateParseException(); }
// Various options for "S" keyword and attached symbols
begin = <S> (
( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; } ) |
( <EQ> <QMARK> { relOp = "="; } )
( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) |
( <EQ> <QMARK> { relOp = "="; isBool = false; } )
)
// Expression, optional filter
<LBRACKET> expr = Expression(prop, pathprop) (filter = Filter())? <RBRACKET>
@ -1482,7 +1483,8 @@ Expression ExpressionSS(boolean prop, boolean pathprop) :
// Filter is actually dealt with by wrapping this expression in
// an (invisible) ExpressionFilter expression
if (filter != null) {
ExpressionFilter ef = new ExpressionFilter(filter.minRequested() ? "min" : "max", ret, filter.getExpression());
String filterOp = isBool ? "&" : filter.getFilterOpString();
ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression());
ef.setInvisible(true);
return ef;
}
@ -1502,19 +1504,20 @@ Expression ExpressionReward(boolean prop, boolean pathprop) :
Filter filter = null;
ExpressionReward ret = new ExpressionReward();
Token begin;
boolean isBool;
}
{
// This production is only allowed in expressions if the "prop" parameter is true
{ if (!prop) throw generateParseException(); }
// Various options for "R" keyword and attached symbols
(( begin = <R> (index = RewardIndex())?
(( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; } )
|( <EQ> <QMARK> { relOp = "="; } )
|( <MIN> <EQ> <QMARK> { relOp = "min="; } )
|( <MAX> <EQ> <QMARK> { relOp = "max="; } )))
(( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } )
|( <EQ> <QMARK> { relOp = "="; isBool = false; } )
|( <MIN> <EQ> <QMARK> { relOp = "min="; isBool = false; } )
|( <MAX> <EQ> <QMARK> { relOp = "max="; isBool = false; } )))
// These two are dupes of above but allow space to be omitted
|( begin = <RMIN> <EQ> <QMARK> { relOp = "min="; } )
|( begin = <RMAX> <EQ> <QMARK> { relOp = "max="; } ))
|( begin = <RMIN> <EQ> <QMARK> { relOp = "min="; isBool = false; } )
|( begin = <RMAX> <EQ> <QMARK> { relOp = "max="; isBool = false; } ))
// Path formula, optional filter
<LBRACKET> expr = ExpressionRewardContents(prop, pathprop) (filter = Filter())? <RBRACKET>
{
@ -1527,7 +1530,8 @@ Expression ExpressionReward(boolean prop, boolean pathprop) :
// Filter is actually dealt with by wrapping this expression in
// an (invisible) ExpressionFilter expression
if (filter != null) {
ExpressionFilter ef = new ExpressionFilter(filter.minRequested() ? "min" : "max", ret, filter.getExpression());
String filterOp = isBool ? "&" : filter.getFilterOpString();
ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression());
ef.setInvisible(true);
return ef;
}

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

@ -1,98 +1,192 @@
/* Generated By:JavaCC: Do not edit this line. PrismParserConstants.java */
package parser;
/**
* Token literal values and constants.
* Generated by org.javacc.parser.OtherFilesGen#start()
*/
public interface PrismParserConstants {
/** End of File. */
int EOF = 0;
/** RegularExpression Id. */
int WHITESPACE = 1;
/** RegularExpression Id. */
int COMMENT = 2;
/** RegularExpression Id. */
int A = 3;
/** RegularExpression Id. */
int BOOL = 4;
/** RegularExpression Id. */
int CLOCK = 5;
/** RegularExpression Id. */
int CONST = 6;
/** RegularExpression Id. */
int CTMC = 7;
/** RegularExpression Id. */
int C = 8;
/** RegularExpression Id. */
int DOUBLE = 9;
/** RegularExpression Id. */
int DTMC = 10;
/** RegularExpression Id. */
int E = 11;
/** RegularExpression Id. */
int ENDINIT = 12;
/** RegularExpression Id. */
int ENDINVARIANT = 13;
/** RegularExpression Id. */
int ENDMODULE = 14;
/** RegularExpression Id. */
int ENDREWARDS = 15;
/** RegularExpression Id. */
int ENDSYSTEM = 16;
/** RegularExpression Id. */
int FALSE = 17;
/** RegularExpression Id. */
int FORMULA = 18;
/** RegularExpression Id. */
int FILTER = 19;
/** RegularExpression Id. */
int FUNC = 20;
/** RegularExpression Id. */
int F = 21;
/** RegularExpression Id. */
int GLOBAL = 22;
/** RegularExpression Id. */
int G = 23;
/** RegularExpression Id. */
int INIT = 24;
/** RegularExpression Id. */
int INVARIANT = 25;
/** RegularExpression Id. */
int I = 26;
/** RegularExpression Id. */
int INT = 27;
/** RegularExpression Id. */
int LABEL = 28;
/** RegularExpression Id. */
int MAX = 29;
/** RegularExpression Id. */
int MDP = 30;
/** RegularExpression Id. */
int MIN = 31;
/** RegularExpression Id. */
int MODULE = 32;
/** RegularExpression Id. */
int X = 33;
/** RegularExpression Id. */
int NONDETERMINISTIC = 34;
/** RegularExpression Id. */
int PMAX = 35;
/** RegularExpression Id. */
int PMIN = 36;
/** RegularExpression Id. */
int P = 37;
/** RegularExpression Id. */
int PROBABILISTIC = 38;
/** RegularExpression Id. */
int PROB = 39;
/** RegularExpression Id. */
int PTA = 40;
/** RegularExpression Id. */
int RATE = 41;
/** RegularExpression Id. */
int REWARDS = 42;
/** RegularExpression Id. */
int RMAX = 43;
/** RegularExpression Id. */
int RMIN = 44;
/** RegularExpression Id. */
int R = 45;
/** RegularExpression Id. */
int S = 46;
/** RegularExpression Id. */
int STOCHASTIC = 47;
/** RegularExpression Id. */
int SYSTEM = 48;
/** RegularExpression Id. */
int TRUE = 49;
/** RegularExpression Id. */
int U = 50;
/** RegularExpression Id. */
int W = 51;
/** RegularExpression Id. */
int NOT = 52;
/** RegularExpression Id. */
int AND = 53;
/** RegularExpression Id. */
int OR = 54;
/** RegularExpression Id. */
int IMPLIES = 55;
/** RegularExpression Id. */
int RARROW = 56;
/** RegularExpression Id. */
int COLON = 57;
/** RegularExpression Id. */
int SEMICOLON = 58;
/** RegularExpression Id. */
int COMMA = 59;
/** RegularExpression Id. */
int DOTS = 60;
/** RegularExpression Id. */
int LPARENTH = 61;
/** RegularExpression Id. */
int RPARENTH = 62;
/** RegularExpression Id. */
int LBRACKET = 63;
/** RegularExpression Id. */
int RBRACKET = 64;
/** RegularExpression Id. */
int LBRACE = 65;
/** RegularExpression Id. */
int RBRACE = 66;
/** RegularExpression Id. */
int EQ = 67;
/** RegularExpression Id. */
int NE = 68;
/** RegularExpression Id. */
int LT = 69;
/** RegularExpression Id. */
int GT = 70;
/** RegularExpression Id. */
int LE = 71;
/** RegularExpression Id. */
int GE = 72;
/** RegularExpression Id. */
int PLUS = 73;
/** RegularExpression Id. */
int MINUS = 74;
/** RegularExpression Id. */
int TIMES = 75;
/** RegularExpression Id. */
int DIVIDE = 76;
/** RegularExpression Id. */
int PRIME = 77;
/** RegularExpression Id. */
int RENAME = 78;
/** RegularExpression Id. */
int QMARK = 79;
/** RegularExpression Id. */
int DQUOTE = 80;
/** RegularExpression Id. */
int REG_INT = 81;
/** RegularExpression Id. */
int REG_DOUBLE = 82;
/** RegularExpression Id. */
int REG_IDENTPRIME = 83;
/** RegularExpression Id. */
int REG_IDENT = 84;
/** RegularExpression Id. */
int PREPROC = 85;
/** RegularExpression Id. */
int LEXICAL_ERROR = 86;
/** Lexical state. */
int DEFAULT = 0;
/** Literal token values. */
String[] tokenImage = {
"<EOF>",
"<WHITESPACE>",

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

@ -7,9 +7,13 @@ import parser.type.*;
import prism.ModelType;
import prism.PrismLangException;
/** Token Manager. */
public class PrismParserTokenManager implements PrismParserConstants
{
/** Debug output. */
public static java.io.PrintStream debugStream = System.out;
/** Set debug output. */
public static void setDebugStream(java.io.PrintStream ds) { debugStream = ds; }
private static final int jjStopStringLiteralDfa_0(int pos, long active0, long active1)
{
@ -169,21 +173,13 @@ private static final int jjStartNfa_0(int pos, long active0, long active1)
{
return jjMoveNfa_0(jjStopStringLiteralDfa_0(pos, active0, active1), pos + 1);
}
static private final int jjStopAtPos(int pos, int kind)
static private int jjStopAtPos(int pos, int kind)
{
jjmatchedKind = kind;
jjmatchedPos = pos;
return pos + 1;
}
static private final int jjStartNfaWithStates_0(int pos, int kind, int state)
{
jjmatchedKind = kind;
jjmatchedPos = pos;
try { curChar = input_stream.readChar(); }
catch(java.io.IOException e) { return pos + 1; }
return jjMoveNfa_0(state, pos + 1);
}
static private final int jjMoveStringLiteralDfa0_0()
static private int jjMoveStringLiteralDfa0_0()
{
switch(curChar)
{
@ -296,7 +292,7 @@ static private final int jjMoveStringLiteralDfa0_0()
return jjMoveNfa_0(0, 0);
}
}
static private final int jjMoveStringLiteralDfa1_0(long active0, long active1)
static private int jjMoveStringLiteralDfa1_0(long active0, long active1)
{
try { curChar = input_stream.readChar(); }
catch(java.io.IOException e) {
@ -356,10 +352,10 @@ static private final int jjMoveStringLiteralDfa1_0(long active0, long active1)
}
return jjStartNfa_0(0, active0, active1);
}
static private final int jjMoveStringLiteralDfa2_0(long old0, long active0, long old1, long active1)
static private int jjMoveStringLiteralDfa2_0(long old0, long active0, long old1, long active1)
{
if (((active0 &= old0) | (active1 &= old1)) == 0L)
return jjStartNfa_0(0, old0, old1);
return jjStartNfa_0(0, old0, old1);
try { curChar = input_stream.readChar(); }
catch(java.io.IOException e) {
jjStopStringLiteralDfa_0(1, active0, 0L);
@ -414,7 +410,7 @@ static private final int jjMoveStringLiteralDfa2_0(long old0, long active0, long
}
return jjStartNfa_0(1, active0, 0L);
}
static private final int jjMoveStringLiteralDfa3_0(long old0, long active0)
static private int jjMoveStringLiteralDfa3_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(1, old0, 0L);
@ -485,7 +481,7 @@ static private final int jjMoveStringLiteralDfa3_0(long old0, long active0)
}
return jjStartNfa_0(2, active0, 0L);
}
static private final int jjMoveStringLiteralDfa4_0(long old0, long active0)
static private int jjMoveStringLiteralDfa4_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(2, old0, 0L);
@ -531,7 +527,7 @@ static private final int jjMoveStringLiteralDfa4_0(long old0, long active0)
}
return jjStartNfa_0(3, active0, 0L);
}
static private final int jjMoveStringLiteralDfa5_0(long old0, long active0)
static private int jjMoveStringLiteralDfa5_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(3, old0, 0L);
@ -581,7 +577,7 @@ static private final int jjMoveStringLiteralDfa5_0(long old0, long active0)
}
return jjStartNfa_0(4, active0, 0L);
}
static private final int jjMoveStringLiteralDfa6_0(long old0, long active0)
static private int jjMoveStringLiteralDfa6_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(4, old0, 0L);
@ -615,7 +611,7 @@ static private final int jjMoveStringLiteralDfa6_0(long old0, long active0)
}
return jjStartNfa_0(5, active0, 0L);
}
static private final int jjMoveStringLiteralDfa7_0(long old0, long active0)
static private int jjMoveStringLiteralDfa7_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(5, old0, 0L);
@ -641,7 +637,7 @@ static private final int jjMoveStringLiteralDfa7_0(long old0, long active0)
}
return jjStartNfa_0(6, active0, 0L);
}
static private final int jjMoveStringLiteralDfa8_0(long old0, long active0)
static private int jjMoveStringLiteralDfa8_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(6, old0, 0L);
@ -673,7 +669,7 @@ static private final int jjMoveStringLiteralDfa8_0(long old0, long active0)
}
return jjStartNfa_0(7, active0, 0L);
}
static private final int jjMoveStringLiteralDfa9_0(long old0, long active0)
static private int jjMoveStringLiteralDfa9_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(7, old0, 0L);
@ -701,7 +697,7 @@ static private final int jjMoveStringLiteralDfa9_0(long old0, long active0)
}
return jjStartNfa_0(8, active0, 0L);
}
static private final int jjMoveStringLiteralDfa10_0(long old0, long active0)
static private int jjMoveStringLiteralDfa10_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(8, old0, 0L);
@ -721,7 +717,7 @@ static private final int jjMoveStringLiteralDfa10_0(long old0, long active0)
}
return jjStartNfa_0(9, active0, 0L);
}
static private final int jjMoveStringLiteralDfa11_0(long old0, long active0)
static private int jjMoveStringLiteralDfa11_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(9, old0, 0L);
@ -743,7 +739,7 @@ static private final int jjMoveStringLiteralDfa11_0(long old0, long active0)
}
return jjStartNfa_0(10, active0, 0L);
}
static private final int jjMoveStringLiteralDfa12_0(long old0, long active0)
static private int jjMoveStringLiteralDfa12_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(10, old0, 0L);
@ -765,7 +761,7 @@ static private final int jjMoveStringLiteralDfa12_0(long old0, long active0)
}
return jjStartNfa_0(11, active0, 0L);
}
static private final int jjMoveStringLiteralDfa13_0(long old0, long active0)
static private int jjMoveStringLiteralDfa13_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(11, old0, 0L);
@ -783,7 +779,7 @@ static private final int jjMoveStringLiteralDfa13_0(long old0, long active0)
}
return jjStartNfa_0(12, active0, 0L);
}
static private final int jjMoveStringLiteralDfa14_0(long old0, long active0)
static private int jjMoveStringLiteralDfa14_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(12, old0, 0L);
@ -801,7 +797,7 @@ static private final int jjMoveStringLiteralDfa14_0(long old0, long active0)
}
return jjStartNfa_0(13, active0, 0L);
}
static private final int jjMoveStringLiteralDfa15_0(long old0, long active0)
static private int jjMoveStringLiteralDfa15_0(long old0, long active0)
{
if (((active0 &= old0)) == 0L)
return jjStartNfa_0(13, old0, 0L);
@ -821,47 +817,24 @@ static private final int jjMoveStringLiteralDfa15_0(long old0, long active0)
}
return jjStartNfa_0(14, active0, 0L);
}
static private final void jjCheckNAdd(int state)
{
if (jjrounds[state] != jjround)
{
jjstateSet[jjnewStateCnt++] = state;
jjrounds[state] = jjround;
}
}
static private final void jjAddStates(int start, int end)
static private int jjStartNfaWithStates_0(int pos, int kind, int state)
{
do {
jjstateSet[jjnewStateCnt++] = jjnextStates[start];
} while (start++ != end);
}
static private final void jjCheckNAddTwoStates(int state1, int state2)
{
jjCheckNAdd(state1);
jjCheckNAdd(state2);
}
static private final void jjCheckNAddStates(int start, int end)
{
do {
jjCheckNAdd(jjnextStates[start]);
} while (start++ != end);
}
static private final void jjCheckNAddStates(int start)
{
jjCheckNAdd(jjnextStates[start]);
jjCheckNAdd(jjnextStates[start + 1]);
jjmatchedKind = kind;
jjmatchedPos = pos;
try { curChar = input_stream.readChar(); }
catch(java.io.IOException e) { return pos + 1; }
return jjMoveNfa_0(state, pos + 1);
}
static final long[] jjbitVec0 = {
0x0L, 0x0L, 0xffffffffffffffffL, 0xffffffffffffffffL
};
static private final int jjMoveNfa_0(int startState, int curPos)
static private int jjMoveNfa_0(int startState, int curPos)
{
int[] nextStates;
int startsAt = 0;
jjnewStateCnt = 23;
int i = 1;
jjstateSet[0] = startState;
int j, kind = 0x7fffffff;
int kind = 0x7fffffff;
for (;;)
{
if (++jjround == 0x7fffffff)
@ -869,7 +842,7 @@ static private final int jjMoveNfa_0(int startState, int curPos)
if (curChar < 64)
{
long l = 1L << curChar;
MatchLoop: do
do
{
switch(jjstateSet[--i])
{
@ -1023,7 +996,7 @@ static private final int jjMoveNfa_0(int startState, int curPos)
else if (curChar < 128)
{
long l = 1L << (curChar & 077);
MatchLoop: do
do
{
switch(jjstateSet[--i])
{
@ -1073,7 +1046,7 @@ static private final int jjMoveNfa_0(int startState, int curPos)
{
int i2 = (curChar & 0xff) >> 6;
long l2 = 1L << (curChar & 077);
MatchLoop: do
do
{
switch(jjstateSet[--i])
{
@ -1105,6 +1078,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
static final int[] jjnextStates = {
10, 11, 12, 18, 2, 3, 5, 20, 21, 22, 13, 14, 16, 17,
};
/** Token literal values. */
public static final String[] jjstrLiteralImages = {
"", null, null, "\101", "\142\157\157\154", "\143\154\157\143\153",
"\143\157\156\163\164", "\143\164\155\143", "\103", "\144\157\165\142\154\145", "\144\164\155\143",
@ -1123,8 +1098,10 @@ public static final String[] jjstrLiteralImages = {
"\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",
"DEFAULT",
};
static final long[] jjtoToken = {
0xfffffffffffffff9L, 0x7fffffL,
@ -1139,15 +1116,20 @@ static protected SimpleCharStream input_stream;
static private final int[] jjrounds = new int[23];
static private final int[] jjstateSet = new int[46];
static protected char curChar;
/** Constructor. */
public PrismParserTokenManager(SimpleCharStream stream){
if (input_stream != null)
throw new TokenMgrError("ERROR: Second call to constructor of static lexer. You must use ReInit() to initialize the static variables.", TokenMgrError.STATIC_LEXER_ERROR);
input_stream = stream;
}
/** Constructor. */
public PrismParserTokenManager(SimpleCharStream stream, int lexState){
this(stream);
SwitchTo(lexState);
}
/** Reinitialise parser. */
static public void ReInit(SimpleCharStream stream)
{
jjmatchedPos = jjnewStateCnt = 0;
@ -1155,18 +1137,22 @@ static public void ReInit(SimpleCharStream stream)
input_stream = stream;
ReInitRounds();
}
static private final void ReInitRounds()
static private void ReInitRounds()
{
int i;
jjround = 0x80000001;
for (i = 23; i-- > 0;)
jjrounds[i] = 0x80000000;
}
/** Reinitialise parser. */
static public void ReInit(SimpleCharStream stream, int lexState)
{
ReInit(stream);
SwitchTo(lexState);
}
/** Switch to specified lex state. */
static public void SwitchTo(int lexState)
{
if (lexState >= 1 || lexState < 0)
@ -1177,14 +1163,27 @@ static public void SwitchTo(int lexState)
static protected Token jjFillToken()
{
Token t = Token.newToken(jjmatchedKind);
t.kind = jjmatchedKind;
final Token t;
final String curTokenImage;
final int beginLine;
final int endLine;
final int beginColumn;
final int endColumn;
String im = jjstrLiteralImages[jjmatchedKind];
t.image = (im == null) ? input_stream.GetImage() : im;
t.beginLine = input_stream.getBeginLine();
t.beginColumn = input_stream.getBeginColumn();
t.endLine = input_stream.getEndLine();
t.endColumn = input_stream.getEndColumn();
curTokenImage = (im == null) ? input_stream.GetImage() : im;
beginLine = input_stream.getBeginLine();
beginColumn = input_stream.getBeginColumn();
endLine = input_stream.getEndLine();
endColumn = input_stream.getEndColumn();
t = Token.newToken(jjmatchedKind);
t.kind = jjmatchedKind;
t.image = curTokenImage;
t.beginLine = beginLine;
t.endLine = endLine;
t.beginColumn = beginColumn;
t.endColumn = endColumn;
return t;
}
@ -1195,22 +1194,22 @@ static int jjround;
static int jjmatchedPos;
static int jjmatchedKind;
/** Get the next Token. */
public static Token getNextToken()
{
int kind;
Token specialToken = null;
Token matchedToken;
int curPos = 0;
EOFLoop :
for (;;)
{
try
{
{
try
{
curChar = input_stream.BeginToken();
}
}
catch(java.io.IOException e)
{
{
jjmatchedKind = 0;
matchedToken = jjFillToken();
matchedToken.specialToken = specialToken;
@ -1273,4 +1272,31 @@ public static Token getNextToken()
}
}
static private void jjCheckNAdd(int state)
{
if (jjrounds[state] != jjround)
{
jjstateSet[jjnewStateCnt++] = state;
jjrounds[state] = jjround;
}
}
static private void jjAddStates(int start, int end)
{
do {
jjstateSet[jjnewStateCnt++] = jjnextStates[start];
} while (start++ != end);
}
static private void jjCheckNAddTwoStates(int state1, int state2)
{
jjCheckNAdd(state1);
jjCheckNAdd(state2);
}
static private void jjCheckNAddStates(int start, int end)
{
do {
jjCheckNAdd(jjnextStates[start]);
} while (start++ != end);
}
}

6
prism/src/parser/ast/ExpressionFilter.java
View File

@ -34,7 +34,7 @@ public class ExpressionFilter extends Expression
{
// Enums for types of filter
public enum FilterOperator {
MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, FORALL, EXISTS, PRINT;
MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, RANGE, FORALL, EXISTS, PRINT;
};
// Operator used in filter
@ -87,6 +87,8 @@ public class ExpressionFilter extends Expression
opType = FilterOperator.AVG;
else if (opName.equals("first"))
opType = FilterOperator.FIRST;
else if (opName.equals("range"))
opType = FilterOperator.RANGE;
else if (opName.equals("forall") || opName.equals("&"))
opType = FilterOperator.FORALL;
else if (opName.equals("exists") || opName.equals("|"))
@ -145,7 +147,7 @@ public class ExpressionFilter extends Expression
*/
public boolean isConstant()
{
// Note: In some sense, ExpressionFilters are constant since they return the same
// Note: In some sense, ExpressionFilters are (often) constant since they return the same
// value for every state. But the actual value is model dependent, so they are not
// considered to be constants.
return false;

20
prism/src/parser/ast/Filter.java
View File

@ -35,9 +35,9 @@ import prism.PrismLangException;
public class Filter extends ASTElement
{
private Expression expr = null;
// Either "min" or "max" ("both" no longer supported)
// (and "min" is nominal default)
private boolean minReq = true;
// Either "min" or "max", or neither or both.
// In the latter case, this means "range"
private boolean minReq = false;
private boolean maxReq = false;
// Constructor
@ -83,6 +83,20 @@ public class Filter extends ASTElement
return maxReq;
}
/**
* Get (as a string) the operator for this filter
* (as need to construct an ExpressionFilter object)
* @return
*/
public String getFilterOpString()
{
if (minReq) {
return maxReq ? "range" : "min";
} else {
return maxReq ? "max" : "range";
}
}
// Methods required for ASTElement:
/**

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

@ -473,6 +473,13 @@ public class TypeCheck extends ASTTraverse
throw new PrismLangException("Type error: P operator filter is not a Boolean", e.getFilter()
.getExpression());
}
// Need to to do this type check here because some info has been lost when converted to ExpressionFilter
if (e.getProb() != null && e.getFilter() != null) {
if (e.getFilter().minRequested() || e.getFilter().maxRequested()) {
throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties");
}
}
// Set type
e.setType(e.getProb() == null ? TypeDouble.getInstance() : TypeBool.getInstance());
}
@ -491,6 +498,13 @@ public class TypeCheck extends ASTTraverse
throw new PrismLangException("Type error: R operator filter is not a Boolean", e.getFilter()
.getExpression());
}
// Need to to do this type check here because some info has been lost when converted to ExpressionFilter
if (e.getReward() != null && e.getFilter() != null) {
if (e.getFilter().minRequested() || e.getFilter().maxRequested()) {
throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties");
}
}
// Set type
e.setType(e.getReward() == null ? TypeDouble.getInstance() : TypeBool.getInstance());
}
@ -503,6 +517,13 @@ public class TypeCheck extends ASTTraverse
throw new PrismLangException("Type error: P operator filter is not a Boolean", e.getFilter()
.getExpression());
}
// Need to to do this type check here because some info has been lost when converted to ExpressionFilter
if (e.getProb() != null && e.getFilter() != null) {
if (e.getFilter().minRequested() || e.getFilter().maxRequested()) {
throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties");
}
}
// Set type
e.setType(e.getProb() == null ? TypeDouble.getInstance() : TypeBool.getInstance());
}
@ -539,6 +560,7 @@ public class TypeCheck extends ASTTraverse
case ARGMAX:
case SUM:
case AVG:
case RANGE:
if (t instanceof TypeBool) {
throw new PrismLangException(
"Type error: Boolean argument not allowed as operand for filter of type \""
@ -567,6 +589,7 @@ public class TypeCheck extends ASTTraverse
case MAX:
case SUM:
case FIRST:
case RANGE:
case PRINT:
e.setType(t);
break;

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

@ -1131,6 +1131,8 @@ public class StateModelChecker implements ModelChecker
res = new StateValuesMTBDD(JDD.Constant(d), model);
break;
case FIRST:
case RANGE:
// TODO: Treat ranges properly
if (empty)
throw new PrismException("Can't select the first value from an empty filter");
d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n());

Write Preview
Loading…
Cancel
Save