From 881ecfef2f0e2b271e91418923c56a3280da1979 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:26:34 +0200 Subject: [PATCH] imported patch predecessor-LTLMC-use-backward.patch --- prism/src/explicit/LTLModelChecker.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 0ec0d147..c4ac1da4 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -52,6 +52,7 @@ import prism.ModelType; import prism.PrismComponent; import prism.PrismException; import prism.PrismLangException; +import prism.PrismSettings; import prism.PrismNotSupportedException; import prism.PrismPaths; import prism.PrismUtils; @@ -760,6 +761,9 @@ public class LTLModelChecker extends PrismComponent continue; // Compute accepting maximum end components (MECs) in !L_i ECComputer ecComputer = ECComputer.createECComputer(this, model); + if (getSettings().getBoolean(PrismSettings.PRISM_PRE_REL)) { + ecComputer.setPredecessorRelation(model.getPredecessorRelation(this, true)); + } ecComputer.computeMECStates(statesLi_not, acceptance.get(i).getK()); List mecs = ecComputer.getMECStates(); // Union MEC states @@ -789,6 +793,9 @@ public class LTLModelChecker extends PrismComponent Stack todo = new Stack(); ECComputer ecComputer = ECComputer.createECComputer(this, model); + if (getSettings().getBoolean(PrismSettings.PRISM_PRE_REL)) { + ecComputer.setPredecessorRelation(model.getPredecessorRelation(this, true)); + } ecComputer.computeMECStates(); for (BitSet mecs : ecComputer.getMECStates()) { ECandPairs ecp = new ECandPairs(); @@ -825,6 +832,9 @@ public class LTLModelChecker extends PrismComponent // nothing to do } else { ecComputer = ECComputer.createECComputer(this, model); + if (getSettings().getBoolean(PrismSettings.PRISM_PRE_REL)) { + ecComputer.setPredecessorRelation(model.getPredecessorRelation(this, true)); + } ecComputer.computeMECStates(restrict); for (BitSet mecs : ecComputer.getMECStates()) { ECandPairs newEcp = new ECandPairs(); @@ -864,6 +874,9 @@ public class LTLModelChecker extends PrismComponent continue; // Compute maximum end components (MECs) in !L_i ECComputer ecComputer = ECComputer.createECComputer(this, model); + if (getSettings().getBoolean(PrismSettings.PRISM_PRE_REL)) { + ecComputer.setPredecessorRelation(model.getPredecessorRelation(this, true)); + } ecComputer.computeMECStates(statesLi_not); List mecs = ecComputer.getMECStates(); // Check which MECs contain a state from each K_i_j