From 33925f8a238f1a61a27a70aac7cb4ad482fd6448 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Dec 2009 22:26:41 +0000 Subject: [PATCH] CTL cex generation now uses transActions, not transSynch. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1602 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NonProbModelChecker.java | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java index f8690fe5..040cdc9e 100644 --- a/prism/src/prism/NonProbModelChecker.java +++ b/prism/src/prism/NonProbModelChecker.java @@ -245,15 +245,10 @@ public class NonProbModelChecker extends StateModelChecker JDD.Ref(cexDDs.get(i - 1)); tmp3 = JDD.And(tmp3, JDD.PermuteVariables(cexDDs.get(i - 1), allDDRowVars, allDDColVars)); tmp3 = JDD.ThereExists(tmp3, allDDColVars); - int j, n; - JDDNode[] transSynch = ((NondetModel) model).getTransSynch(); - n = transSynch.length; - for (j = 0; j < n; j++) { - if (JDD.AreInterecting(tmp3, transSynch[j])) { - cexActions.add(((NondetModel) model).getSynchs().get(j)); - break; - } - } + JDD.Ref(transActions); + tmp3 = JDD.Apply(JDD.TIMES, tmp3, transActions); + int action = (int)JDD.FindMax(tmp3); + cexActions.add(action > 1 ? model.getSynchs().get(action - 2) : ""); JDD.Deref(tmp3); JDD.Deref(cexDDs.get(i)); }