From faabdef716636fb8db3786bbb9cc321d1dba1794 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 14 Jul 2019 00:12:30 +0100 Subject: [PATCH] Error message fix (PTAs). --- prism/src/pta/DigitalClocks.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 6eff8fe0..f3636f1f 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -351,7 +351,7 @@ public class DigitalClocks // Check that there are no nested probabilistic operators if (propertyToCheck.computeProbNesting() > 1) { - throw new PrismLangException("Nested P operators are not allowed when using the digital clocks method", propertyToCheck); + throw new PrismLangException("Nested P/R operators are not allowed when using the digital clocks method", propertyToCheck); } // Check for presence of strict clock constraints