From b71b56460b30d1a98a5de0a028bacad30dfe7bba Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 18 Nov 2009 20:47:21 +0000
Subject: [PATCH] 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          | 4 ++--
 prism/src/parser/PrismParser.jj            | 2 +-
 prism/src/parser/ast/RewardStructItem.java | 6 ++++++
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java
index e6d5f1e0..6818abee 100644
--- a/prism/src/parser/PrismParser.java
+++ b/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();
diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj
index 486d846a..f9e2a382 100644
--- a/prism/src/parser/PrismParser.jj
+++ b/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>
diff --git a/prism/src/parser/ast/RewardStructItem.java b/prism/src/parser/ast/RewardStructItem.java
index 6aaf2b00..3e3dbada 100644
--- a/prism/src/parser/ast/RewardStructItem.java
+++ b/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