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

@@ -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