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