Allow <<>> operator for MDPs (but not checked properly yet).

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

prism/src/parser/visitor/CheckValid.java

@@ -118,5 +118,10 @@ public class CheckValid extends ASTTraverse
 	{
 		if (!modelType.nondeterministic())
 			throw new PrismLangException("The " + e.getOperatorString() + " operator is only meaningful for models with nondeterminism");
+		// Currently (for non-games), <<>> or [[]] can only contain "*" or "" 
+		Coalition coalition = e.getCoalition();
+		if (!(coalition.isAllPlayers() || coalition.isEmpty())) {
+			throw new PrismLangException("The " + e.getOperatorString() + " operator must contain either \"*\" or be empty for an " + modelType);
+		}
 	}
 }