From 1506d469930d5f50c8da4202fd5e1d9af0815cc6 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 30 Jul 2013 20:09:42 +0000
Subject: [PATCH] Comment.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7195 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/LTLModelChecker.java | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 30e84b46..cc323440 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -806,6 +806,8 @@ public class LTLModelChecker extends PrismComponent
 				JDDNode statesK_i = buildKStatesForRabinPair(draDDRowVars, dra, i);
 				// 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
 				JDD.Ref(model.getTrans01());
 				JDD.Ref(statesLi_not);
 				candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), statesLi_not);