From 578d33e7f13600b528b9f26ff5e7e460ab77ce13 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Feb 2016 08:06:12 +0000 Subject: [PATCH] explicit.LTSNBAProduct: take atomic propositions of NBA into account Without formula simplifications, jltl2ba will produce an APSet L0, L1, ... With formula simplifications (upcoming commit), some APs can be missing in the NBA (when irrelevant) or reordered (due to formula simplification). We handle edge label construction as elsewhere in PRISM for DA, to take this into account. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11186 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTSNBAProduct.java | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/prism/src/explicit/LTSNBAProduct.java b/prism/src/explicit/LTSNBAProduct.java index 74ba3533..3957e90d 100644 --- a/prism/src/explicit/LTSNBAProduct.java +++ b/prism/src/explicit/LTSNBAProduct.java @@ -37,6 +37,7 @@ import prism.PrismLog; import common.IterableBitSet; import common.IterableStateSet; import jltl2ba.APElement; +import jltl2ba.APSet; import jltl2dstar.NBA; import jltl2dstar.NBA_State; @@ -213,6 +214,8 @@ public class LTSNBAProduct extends Product acceptingStates.set(id); } } + + final APSet nbaAPSet = nba.getAPSet(); while (!todo.isEmpty()) { int fromId = todo.pop(); @@ -222,13 +225,9 @@ public class LTSNBAProduct extends Product ProductState from = productIdToProductState.get(fromId); // construct edge label from the labeling of the model state - APElement label = new APElement(labelBS.size()); - for (int ap=0; ap < labelBS.size(); ap++) { - if (labelBS.get(ap).get(from.getModelState())) { - label.set(ap); - } else { - label.clear(ap); - } + APElement label = new APElement(nbaAPSet.size()); + for (int k = 0; k < nbaAPSet.size(); k++) { + label.set(k, labelBS.get(Integer.parseInt(nbaAPSet.getAP(k).substring(1))).get(from.getModelState())); } // the current state in the NBA