diff --git a/prism/src/parser/ast/Coalition.java b/prism/src/parser/ast/Coalition.java index c8af0fb1..e4bf911e 100644 --- a/prism/src/parser/ast/Coalition.java +++ b/prism/src/parser/ast/Coalition.java @@ -28,11 +28,14 @@ package parser.ast; import java.util.ArrayList; import java.util.List; +import java.util.Map; import prism.PrismUtils; /** * Class to represent coalition info, e.g., in an ExpressionStrategy object. + * Stored as a list of strings which are either player names (e.g. "controller") + * or player indices (e.g. "2") starting from 1. Alternatively, "*" denotes all players. */ public class Coalition { @@ -67,12 +70,19 @@ public class Coalition // Set methods + /** + * Make this coalition comprise all players (denoted "*") + */ public void setAllPlayers() { allPlayers = true; players = null; } + /** + * Make this coalition comprise these players + * (each string can be a player name or a (1-indexed) player index) + */ public void setPlayers(List players) { allPlayers = false; @@ -82,16 +92,73 @@ public class Coalition // Get methods + /** + * Does this coalition comprise all players? (denoted "*") + */ public boolean isAllPlayers() { return allPlayers; } + /** + * Get a list of strings describing the coalition + * (each string can be a player name or a (1-indexed) player index). + * This will be null is the coalition is "*" (all players). + */ public List getPlayers() { return players; } + // Other methods + + /** + * Check if a given player (specified by its index) is in the coalition. + * Player indices start from 1. A list of player names must be passed in, + * whose size equals the number of players, but in which some names can be null or "". + */ + public boolean isPlayerIndexInCoalition(int index, List playerNames) + { + if (allPlayers) + return true; + int playerIndex; + for (String player : players) { + try { + playerIndex = Integer.parseInt(player); + if (index == playerIndex) + return true; + } catch (NumberFormatException e) { + playerIndex = playerNames.indexOf(player); + if (playerIndex != -1 && index == playerIndex) + return true; + } + } + return false; + } + + /** + * Check if a given player (specified by its index) is in the coalition. + * Player indices start from 1. A mapping from player names to indices is passed in. + */ + public boolean isPlayerIndexInCoalition(int index, Map playerNamesMap) + { + if (allPlayers) + return true; + int playerIndex; + for (String player : players) { + try { + playerIndex = Integer.parseInt(player); + if (index == playerIndex) + return true; + } catch (NumberFormatException e) { + Integer playerIndexI = playerNamesMap.get(player); + if (playerIndexI != null && index == (int) playerIndexI) + return true; + } + } + return false; + } + @Override public String toString() {