Bugfix: Some state reward struct items misidentified as transition rewards.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1565 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/PrismParser.java

@@ -1150,11 +1150,11 @@ public class PrismParser implements PrismParserConstants {
         jj_la1[26] = jj_gen;
         break label_11;
       }
-            begin2 = getToken(1);
+            begin2 = getToken(1); s = null;
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case LBRACKET:
         jj_consume_token(LBRACKET);
-                                                   s = "";
+                                                             s = "";
         switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
         case REG_IDENT:
           s = Identifier();

prism/src/parser/PrismParser.jj

@@ -835,7 +835,7 @@ RewardStruct RewardStruct() :
 	// (which would not be allowed to appear here anyway)
 	( LOOKAHEAD(<DQUOTE>) <DQUOTE> name = Identifier() <DQUOTE> { rs.setName(name); } )?
 	// Reward structure items
-	( { begin2 = getToken(1); } ( <LBRACKET> { s = ""; } ( s=Identifier() )? <RBRACKET> )?
+	( { begin2 = getToken(1); s = null; } ( <LBRACKET> { s = ""; } ( s=Identifier() )? <RBRACKET> )?
 	guard = Expression(false, false) <COLON> value = Expression(false, false) <SEMICOLON>
 	{ rsi = new RewardStructItem(s, guard, value); rsi.setPosition(begin2, getToken(0)); rs.addItem(rsi); } )*
 	<ENDREWARDS>

prism/src/parser/ast/RewardStructItem.java

@@ -31,8 +31,14 @@ import prism.PrismLangException;
 
 public class RewardStructItem extends ASTElement
 {
+	// Synchronising action:
+	// * null = none (i.e. state reward)
+	// * "" = empty/tau/asynchronous action (i.e. transition reward)
+	// * "act" = "act"-labelled action (i.e. transition reward)
 	private String synch;
+	// Guard expression
 	private Expression states;
+	// Reward expression
 	private Expression reward;
 	
 	// constructor