diff --git a/prism/src/common/PlainObjectReference.java b/prism/src/common/PlainObjectReference.java deleted file mode 100644 index eafdb349..00000000 --- a/prism/src/common/PlainObjectReference.java +++ /dev/null @@ -1,84 +0,0 @@ -//============================================================================== -// -// 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 common; - -/** - * Helper class that wraps some other object and strips away - * custom implementations of {@code hashCode} and {@code equals}. - * - * This is useful for storing objects that have such custom implementations - * in a HashSet or HashMap when the goal is to maintain the distinction - * between different Java objects, even though they might test equal via - * {@code equals}. - * - * A PlainObjectReference wraps another object and provides {@code hashCode} - * via {@code System.identityHashCode} and {@code equals} via equality checking - * with the {@code ==} operator, i.e., what would happen using the - * default implementation of {@code Object}. - * - * @param the type of the underlying class - */ -public class PlainObjectReference -{ - /** The object that is referenced */ - private T object; - - /** Constructor, take reference to object */ - public PlainObjectReference(T object) - { - this.object = object; - } - - /** Get the referenced object */ - public T getObject() - { - return object; - } - - @Override - public int hashCode() - { - // return the identityHashCode of the referenced object, - // just as it would happen if there were no {@code hashCode} - // method in the object - return System.identityHashCode(object); - } - - @Override - public boolean equals(Object obj) - { - if (this == obj) - return true; - if (obj == null) - return false; - if (!(obj instanceof PlainObjectReference)) - return false; - PlainObjectReference other = (PlainObjectReference) obj; - // test for equality via == - return other.object == object; - } -} diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java index 6a7ac837..67ab5c06 100644 --- a/prism/src/jltl2ba/SimpleLTL.java +++ b/prism/src/jltl2ba/SimpleLTL.java @@ -30,11 +30,10 @@ package jltl2ba; import java.io.PrintStream; import java.util.ArrayList; import java.util.HashMap; -import java.util.HashSet; +import java.util.IdentityHashMap; import java.util.List; import java.util.Map; -import common.PlainObjectReference; import jltl2dstar.APMonom; import jltl2dstar.NBA; import prism.PrismException; @@ -911,7 +910,9 @@ public class SimpleLTL { */ public boolean isTree() { - HashSet> seen = new HashSet>(); + // use an IdentityHashMap with (formula,formula) pairs indicating that formula + // has already been seen (due to lack of IdentityHashSet) + IdentityHashMap seen = new IdentityHashMap(); return isTree(seen); } @@ -921,13 +922,12 @@ public class SimpleLTL { * * The already seen SimpleLTL subtrees are tracked in {@code seen}. */ - private boolean isTree(HashSet> seen) + private boolean isTree(IdentityHashMap seen) { - PlainObjectReference ref = new PlainObjectReference(this); - if (seen.contains(ref)) { + if (seen.containsKey(this)) { return false; } - seen.add(ref); + seen.put(this, this); if (left != null && !left.isTree(seen)) { // left child exists and is not a tree @@ -1355,7 +1355,7 @@ public class SimpleLTL { /** Print a DOT representation of the syntax tree of this SimpleLTL formula */ public void toDot(PrintStream out) { - HashMap, String> map = new HashMap, String>(); + IdentityHashMap map = new IdentityHashMap(); out.println("digraph {"); toDot(out, map); @@ -1368,15 +1368,15 @@ public class SimpleLTL { * @param out the output print stream * @param seen a map storing an identifier for each subformula that has already been seen / printed */ - private String toDot(PrintStream out, HashMap, String> seen) + private String toDot(PrintStream out, IdentityHashMap seen) { - PlainObjectReference ref = new PlainObjectReference(this); - if (seen.containsKey(ref)) { - return seen.get(ref); + String id = seen.get(this); + if (id != null) { + return id; } - String id = Integer.toString(seen.size()); - seen.put(ref, id); + id = Integer.toString(seen.size()); + seen.put(this, id); out.println(id + " [label=\""+toStringLBT()+"\"]"); switch (kind) {