From 33c6025033927bf99f05b626b328079432ab74e1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 17 Apr 2011 21:44:47 +0000 Subject: [PATCH] PTA fix: disallowing diagonal clock constraints for digital clocks engine (for; until we can find a fix). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2780 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/DigitalClocks.java | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 191a417a..ae868c03 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -112,10 +112,14 @@ public class DigitalClocks varList = modulesFile.createVarList(); // Check that model does not contain any closed clock constraints - // (don't need to check for diagonal-free-ness) ast = findAStrictClockConstraint(modulesFile); if (ast != null) throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", ast); + // Check that model does not contain any diagonal clock constraints + // (for now; should be able to relax this later) + ast = findADiagonalClockConstraint(modulesFile); + if (ast != null) + throw new PrismLangException("Diagonal clock constraints are not allowed when using the digital clocks method", ast); // ACheck for any references to clocks in rewards structures - not allowed. for (RewardStruct rs : modulesFile.getRewardStructs()) { @@ -321,11 +325,16 @@ public class DigitalClocks } // Check for presence of strict clock constraints - // TODO: also need to look in any required properties file labels - // (currently, these cannot even contain clocks so not an issue) ast = findAStrictClockConstraint(propertyToCheck); if (ast != null) throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", ast); + // Check for presence of diagonal clock constraints + // (for now; should be able to relax this later) + ast = findADiagonalClockConstraint(modulesFile); + if (ast != null) + throw new PrismLangException("Diagonal clock constraints are not allowed when using the digital clocks method", ast); + // TODO: also need to look in any required properties file labels + // (currently, these cannot even contain clocks so not an issue) } /**