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) {