diff --git a/prism/src/jdd/Clearable.java b/prism/src/jdd/Clearable.java new file mode 100644 index 00000000..fe6fd72d --- /dev/null +++ b/prism/src/jdd/Clearable.java @@ -0,0 +1,6 @@ +package jdd; + +public interface Clearable +{ + public void clear(); +} diff --git a/prism/src/jdd/TemporaryJDDRefs.java b/prism/src/jdd/TemporaryJDDRefs.java new file mode 100644 index 00000000..afc77973 --- /dev/null +++ b/prism/src/jdd/TemporaryJDDRefs.java @@ -0,0 +1,163 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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 jdd; + +import java.util.Iterator; +import java.util.LinkedList; +import java.util.List; + +/** + * AutoClosable container for keeping track of active JDDNode references + * and other Clearable objects. + *
+ * Use scenario: + *
+ * try(TemporaryJDDRefs refs = new TemporaryJDDRefs()) {
+ * refs.register(node);
+ * ...
+ * }
+ *
+ * The node will be dereferenced when leaving the scope, i.e., when exiting + * normally or when exiting due to an exception. + *
+ * Supports tracking and clearing of objects that implement Clearable as well. + */ +public class TemporaryJDDRefs implements AutoCloseable +{ + /** The active JDDNode references */ + private List activeRefs = new LinkedList(); + /** The active Clearable references */ + private List activeClearables = new LinkedList(); + + @Override + public void close() + { + closeNodes(); + closeClearables(); + } + + /** Close (deref) all active node references */ + private void closeNodes() + { + Iterator it = activeRefs.iterator(); + while (it.hasNext()) { + JDDNode node = it.next(); + JDD.Deref(node); + it.remove(); + } + } + + /** Close (clear) all active Clearable references */ + private void closeClearables() + { + Iterator it = activeClearables.iterator(); + while (it.hasNext()) { + Clearable clearable = it.next(); + clearable.clear(); + it.remove(); + } + } + + /** Register a JDDNode reference */ + public void register(JDDNode node) { + if (node == null) return; + activeRefs.add(node); + } + + /** Register a Clearable reference */ + public void register(Clearable clearable) { + if (clearable == null) return; + activeClearables.add(clearable); + } + + /** + * Release multiple JDDNode references. + *
+ * Releasing a JDDNode does not call {@code JDD.Deref}, + * it simply notifies the container that the reference + * is no longer active. + */ + public void release(JDDNode... nodes) + { + for (JDDNode node : nodes) + release(node); + } + + /** + * Release a JDDNode reference. + *
+ * Releasing a JDDNode does not call {@code JDD.Deref}, + * it simply notifies the container that the reference + * is no longer active. + */ + public void release(JDDNode node) + { + Iterator it = activeRefs.iterator(); + while (it.hasNext()) { + if (it.next() == node) { + it.remove(); + return; + } + } + + throw new UnsupportedOperationException("Can not release node that has not been registered: "+node); + } + + /** + * Release multiple Clearable references. + *
+ * Releasing a Clearable does not call {@code clear()}, + * it simply notifies the container that the reference + * is no longer active. + */ + public void release(Clearable... clearables) + { + for (Clearable clearable : clearables) + release(clearable); + } + + /** + * Release a Clearable reference. + *
+ * Releasing a Clearable does not call {@code clear()}, + * it simply notifies the container that the reference + * is no longer active. + */ + public void release(Clearable clearable) + { + Iterator it = activeClearables.iterator(); + while (it.hasNext()) { + if (it.next() == clearable) { + it.remove(); + return; + } + } + + throw new UnsupportedOperationException("Can not release Clearable that has not been registered"); + } + +}