From 7f10ec8b60e9fd1310447222e4ccce36a2ce0dad Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 18 Aug 2014 10:42:29 +0000 Subject: [PATCH] Bug in explicit engine LTL model checking (happens when there are multiple APs in the formula and ordering is different in the DRA). Reported by Manfred Jaeger. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9091 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index c7dedec5..9515c683 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -161,7 +161,7 @@ public class LTLModelChecker extends PrismComponent for (int s_0 = 0; s_0 < dtmc.getNumStates(); s_0++) { // Get BitSet representing APs (labels) satisfied by state s_0 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(k).get(s_0)); + s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_0)); } // Find corresponding initial state in DRA int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels); @@ -188,7 +188,7 @@ public class LTLModelChecker extends PrismComponent double prob = e.getValue(); // Get BitSet representing APs (labels) satisfied by successor state s_2 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(k).get(s_2)); + s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_2)); } // Find corresponding successor in DRA q_2 = dra.getEdgeDestByLabel(q_1, s_labels); @@ -251,7 +251,7 @@ public class LTLModelChecker extends PrismComponent for (int s_0 = 0; s_0 < mdp.getNumStates(); s_0++) { // Get BitSet representing APs (labels) satisfied by state s_0 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(k).get(s_0)); + s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_0)); } // Find corresponding initial state in DRA int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels); @@ -281,7 +281,7 @@ public class LTLModelChecker extends PrismComponent double prob = e.getValue(); // Get BitSet representing APs (labels) satisfied by successor state s_2 for (int k = 0; k < numAPs; k++) { - s_labels.set(k, labelBS.get(k).get(s_2)); + s_labels.set(k, labelBS.get(Integer.parseInt(dra.getAPList().get(k).substring(1))).get(s_2)); } // Find corresponding successor in DRA q_2 = dra.getEdgeDestByLabel(q_1, s_labels);