From c46611cc94ef89c8acc5a6525f5406fff8f325b9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 23 Jul 2013 23:55:23 +0000 Subject: [PATCH] Refactor symbolic LTL code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7149 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 5f1cf606..7e318cbe 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -1227,16 +1227,10 @@ public class LTLModelChecker extends PrismComponent } /** - * Returns the union of each set in the vector that has nonempty intersection with the filter BDD. - * - * @param sets - * Vector with sets which are dereferenced after calling this function - * @param filter - * filter BDD against which each set is checked for nonempty intersection also dereferenced after calling - * this function - * @return Referenced BDD with the filtered union - * - * modified by Hongyang for testing + * Return the union of sets from {@code sets} which have a non-empty intersection with {@code filter}. + * @param sets List of BDDs representing sets (dereferenced after calling this function) + * @param filter BDD of states to test for intersection (dereferenced after calling) + * @return Referenced BDD representing the filtered union */ private JDDNode filteredUnion(List sets, JDDNode filter) {