diff --git a/prism/src/prism/LTSFromDA.java b/prism/src/prism/LTSFromDA.java index e2601b28..7eb3011e 100644 --- a/prism/src/prism/LTSFromDA.java +++ b/prism/src/prism/LTSFromDA.java @@ -1,9 +1,35 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + package prism; -import java.util.ArrayList; import java.util.BitSet; +import java.util.HashSet; import java.util.Iterator; -import java.util.List; +import java.util.Set; import strat.MDStrategy; import explicit.LTS; @@ -30,7 +56,7 @@ public class LTSFromDA extends ModelExplicit implements LTS @Override public Iterator getSuccessorsIterator(int s) { - List succs = new ArrayList(); + Set succs = new HashSet(); int n = da.getNumEdges(s); for (int i = 0; i < n; i++) { succs.add(da.getEdgeDest(s, i)); @@ -185,7 +211,7 @@ public class LTSFromDA extends ModelExplicit implements LTS @Override public Iterator getSuccessorsIterator(int s, int i) { - List succs = new ArrayList(); + Set succs = new HashSet(); succs.add(da.getEdgeDest(s, i)); return succs.iterator(); }