From aba274af8849bb924498b85d9eba4194cf135ddf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 21 Oct 2010 08:46:19 +0000 Subject: [PATCH] Removed diagonal-free restriction for digital clocks. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2177 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/DigitalClocks.java | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index b0d88877..df206676 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -111,19 +111,20 @@ public class DigitalClocks // TODO: need property constants too? varList = modulesFile.createVarList(); - // Check that model (and properties) are closed and diagonal-free + // Check that model (and properties) are closed + // (don't need to check that they are diagonal-free) astt = new ASTTraverse() { // Clock constraints public void visitPost(ExpressionBinaryOp e) throws PrismLangException { if (e.getOperand1().getType() instanceof TypeClock) { - if (e.getOperand2().getType() instanceof TypeClock) { - throw new PrismLangException("Diagonal clock constraints are not allowed when using the digital clocks method", e); - } else { + //if (e.getOperand2().getType() instanceof TypeClock) { + // throw new PrismLangException("Diagonal clock constraints are not allowed when using the digital clocks method", e); + //} else { if (e.getOperator() == ExpressionBinaryOp.GT || e.getOperator() == ExpressionBinaryOp.LT) throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", e); - } + //} } else if (e.getOperand2().getType() instanceof TypeClock) { if (e.getOperator() == ExpressionBinaryOp.GT || e.getOperator() == ExpressionBinaryOp.LT) throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", e);