Push coalition info into a separate class (including option for * = all players).

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

prism/src/explicit/ProbModelChecker.java

@@ -27,8 +27,8 @@
 package explicit;
 
 import java.util.BitSet;
-import java.util.List;
 
+import parser.ast.Coalition;
 import parser.ast.Expression;
 import parser.ast.ExpressionProb;
 import parser.ast.ExpressionReward;
@@ -483,7 +483,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			throw new PrismException("The " + expr.getOperatorString() + " operator is only supported for MDPs currently");
 
 		// Extract coalition info
-		List<String> coalition = expr.getCoalition();
+		Coalition coalition = expr.getCoalition();
 		// Strip any parentheses (they might have been needless wrapped around a single P or R)
 		Expression exprSub = expr.getExpression();
 		while (Expression.isParenth(exprSub))
@@ -520,7 +520,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
 	 * @param coalition If relevant, info about which set of players this P operator refers to
 	 */
-	protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, List<String> coalition) throws PrismException
+	protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, Coalition coalition) throws PrismException
 	{
 		Expression pb; // Probability bound (expression)
 		double p = 0; // Probability bound (actual value)
@@ -760,7 +760,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	/**
 	 * Model check an R operator expression and return the values for all states.
 	 */
-	protected StateValues checkExpressionReward(Model model, ExpressionReward expr, boolean forAll, List<String> coalition) throws PrismException
+	protected StateValues checkExpressionReward(Model model, ExpressionReward expr, boolean forAll, Coalition coalition) throws PrismException
 	{
 		Expression rb; // Reward bound (expression)
 		double r = 0; // Reward bound (actual value)

prism/src/parser/ast/Coalition.java

@@ -0,0 +1,100 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package parser.ast;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import prism.PrismUtils;
+
+/**
+ * Class to represent coalition info, e.g., in an ExpressionStrategy object.
+ */
+public class Coalition
+{
+	/** Is coalition all players? (denoted by *) */
+	protected boolean allPlayers;
+	
+	/** Coalition: list of player names */
+	protected List<String> players; 
+	
+	// Constructors
+
+	/**
+	 * Default constructor: empty player list
+	 */
+	public Coalition()
+	{
+		// Default" empty list of players
+		allPlayers = false;
+		players = new ArrayList<String>();
+	}
+
+	/**
+	 * Copy constructor
+	 */
+	public Coalition(Coalition c)
+	{
+		if (c.isAllPlayers())
+			allPlayers = true;
+		else
+			players = new ArrayList<String>(c.getPlayers());
+	}
+
+	// Set methods
+
+	public void setAllPlayers()
+	{
+		allPlayers = true;
+		players = null;
+	}
+
+	public void setPlayers(List<String> players)
+	{
+		allPlayers = false;
+		this.players.clear();
+		this.players.addAll(players);
+	}
+
+	// Get methods
+
+	public boolean isAllPlayers()
+	{
+		return allPlayers;
+	}
+	
+	public List<String> getPlayers()
+	{
+		return players;
+	}
+	
+	@Override
+	public String toString()
+	{
+		return allPlayers ? "*" : PrismUtils.joinString(players, ",");
+	}
+}

prism/src/parser/ast/ExpressionStrategy.java

@@ -26,13 +26,11 @@
 
 package parser.ast;
 
-import java.util.ArrayList;
 import java.util.List;
 
 import parser.EvaluateContext;
 import parser.visitor.ASTVisitor;
 import prism.PrismLangException;
-import prism.PrismUtils;
 
 /**
  * Class to represent ATL <<.>> and [[.]] operators, i.e. quantification over strategies
@@ -43,9 +41,8 @@ public class ExpressionStrategy extends Expression
 	/** "There exists a strategy" (true) or "for all strategies" (false) */
 	protected boolean thereExists = false;
 	
-	// Coalition info (for game models)
-	/** Coalition: list of player names */
-	protected List<String> coalition = null; 
+	/** Coalition info (for game models) */
+	protected Coalition coalition = new Coalition(); 
 	
 	/** Child expression */
 	protected Expression expression = null;
@@ -54,7 +51,6 @@ public class ExpressionStrategy extends Expression
 
 	public ExpressionStrategy()
 	{
-
 	}
 
 	public ExpressionStrategy(boolean thereExists)
@@ -75,9 +71,14 @@ public class ExpressionStrategy extends Expression
 		this.thereExists = thereExists;
 	}
 	
+	public void setCoalitionAllPlayers()
+	{
+		this.coalition.setAllPlayers();
+	}
+
 	public void setCoalition(List<String> coalition)
 	{
-		this.coalition = coalition;
+		this.coalition.setPlayers(coalition);
 	}
 
 	public void setExpression(Expression expression)
@@ -100,11 +101,21 @@ public class ExpressionStrategy extends Expression
 		return thereExists ? "<<>>" : "[[]]";
 	}
 
-	public List<String> getCoalition()
+	public Coalition getCoalition()
 	{
 		return coalition;
 	}
 	
+	public boolean coalitionIsAllPlayers()
+	{
+		return coalition.isAllPlayers();
+	}
+	
+	public List<String> getCoalitionPlayers()
+	{
+		return coalition.getPlayers();
+	}
+	
 	public Expression getExpression()
 	{
 		return expression;
@@ -155,7 +166,7 @@ public class ExpressionStrategy extends Expression
 	{
 		String s = "";
 		s += (thereExists ? "<<" : "[[");
-		s += PrismUtils.joinString(coalition, ",");
+		s += coalition;
 		s += (thereExists ? ">>" : "]]");
 		s += " " + expression.toString();
 		return s;
@@ -166,7 +177,7 @@ public class ExpressionStrategy extends Expression
 	{
 		ExpressionStrategy expr = new ExpressionStrategy();
 		expr.setThereExists(isThereExists());
-		expr.setCoalition(new ArrayList<String>(coalition));
+		expr.coalition = new Coalition(coalition);
 		expr.setExpression(expression == null ? null : expression.deepCopy());
 		expr.setType(type);
 		expr.setPosition(this);