From 896048bf379d94ad78cc60f4080de02e996ba188 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 19 Dec 2013 01:06:16 +0000 Subject: [PATCH] Bugfix: allow trivial LTL formulae that are just propositions (accidentally disabled a little while back by previous over-zealous type checking). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7723 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/visitor/TypeCheck.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 9162dd61..7f8b251c 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -478,7 +478,8 @@ public class TypeCheck extends ASTTraverse } } // Check path operator - if (!(e.getExpression().getType() instanceof TypePathBool)) { + // Note: need to allow (non-path) Boolean types too, since propositional formulae are also LTL + if (!(e.getExpression().getType() instanceof TypePathBool || e.getExpression().getType() instanceof TypeBool)) { throw new PrismLangException("Type error: Contents of P operator is not a path formula", e.getExpression()); } // Set type