From 9611929efc6b7722ee7052ff445441167e4750f0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 9 Mar 2016 12:42:57 +0000 Subject: [PATCH] prism/LTLModelChecker: add remark to TODO For the non-fair case, the restriction is indeed done by the ECComputer, but for the fair case, the restriction of candidateStates to states_Li_not is required. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11243 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 3a789301..d4323754 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -872,7 +872,9 @@ public class LTLModelChecker extends PrismComponent // Find states in the model for which there are no transitions leaving !L_i // (this will allow us to reduce the problem to finding MECs, not ECs) // TODO: I don't think this next step is needed, - // since the ECComputer restricts the model in this way anyway + // since the ECComputer restricts the model in this way anyway. + // However, for fairness, the restriction of the candidateStates + // to statesLi_not has to happen for correctness. JDD.Ref(model.getTrans01()); JDD.Ref(statesLi_not); candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), statesLi_not);