Update parser to allow proper <<>> or [[]] syntax.

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

prism/src/parser/PrismParser.jj

@@ -1709,8 +1709,8 @@ Expression ExpressionStrategy(boolean prop, boolean pathprop) :
 	{ if (!prop) throw generateParseException(); }
 	(
 	// <<...>> or [[...]]
-	(( begin = <DLT> { ret = new ExpressionStrategy(true); } <DGT> )
-	| (begin = <DLBRACKET> { ret = new ExpressionStrategy(false); } <DRBRACKET> ))
+	(( begin = <DLT> { ret = new ExpressionStrategy(true); } ExpressionStrategyCoalition(ret) <DGT> )
+	| (begin = <DLBRACKET> { ret = new ExpressionStrategy(false); } ExpressionStrategyCoalition(ret) <DRBRACKET> ))
 	// Child expression
 	( expr = ExpressionProb(prop, pathprop) | expr = ExpressionReward(prop, pathprop)
 	| expr = ExpressionParenth(prop, pathprop) | expr = ExpressionFuncOrIdent(prop, pathprop) )
@@ -1722,6 +1722,32 @@ Expression ExpressionStrategy(boolean prop, boolean pathprop) :
 	}
 }
 
+// Coalition (player list) for a strategy (<<>> or [[]]) operator
+
+void ExpressionStrategyCoalition(ExpressionStrategy exprStrat) :
+{
+	List<String> coalition = new ArrayList<String>();
+	String s;
+}
+{
+	( <TIMES> ) { exprStrat.setCoalitionAllPlayers();}
+	|
+	( s = ExpressionStrategyCoalitionPlayer() { coalition.add(s); }
+	( <COMMA> s = ExpressionStrategyCoalitionPlayer()  { coalition.add(s); } )* )?
+	{ exprStrat.setCoalition(coalition); }
+}
+
+// Single player in a coalition for a strategy (<<>> or [[]]) operator
+
+String ExpressionStrategyCoalitionPlayer() :
+{
+	String s;
+}
+{
+	( <REG_INT> | <REG_IDENT> ) { s = getToken(0).image; }
+	{ return s; }
+}
+
 // (Property) expression: label (including "init")
 
 Expression ExpressionLabel(boolean prop, boolean pathprop) :