From a6003f8216e641dbad2c70378ad9f62facb8504c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 27 Jul 2015 07:11:35 +0000 Subject: [PATCH] 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 | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 403abcdb..9e3babb6 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/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); + } } }