From 74c2aa9491d3fb652c3945a58c9993fab7bfcc9c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:46 +0200 Subject: [PATCH] Prism, exact engine: do deadlock check for digital clock conversion of PTA Similar to what is done for models built with the exact engine. --- prism/src/prism/Prism.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 81bdfade..e9be3172 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3165,6 +3165,17 @@ public class Prism extends PrismComponent implements PrismSettingsListener mc.setModelBuilder(builder); mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); + + if (digital) { + // have to do deadlock checks, as we are in digital clock mode for PTA checking, + // cf. doBuildModelDigitalClocksChecks() + if (modelExpl.getNumDeadlockStates() > 0) { + int dl = modelExpl.getFirstDeadlockState(); + String dls = modelExpl.getStatesList().get(dl).toString(currentModelInfo); + throw new PrismException("Timelock in PTA, e.g. in state " + dls); + } + } + Result result = mc.check(modelExpl, prop.getExpression()); // Convert result of parametric model checking to a single value,