refactor SimpleLTL DAG check, remove common/PlainObjectReference.java

There's actually JDK library functionality for a hash map that
uses object identity instead of .equals(), making PlainObjectReference
unnecessary. Use IdentityHashMap instead.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11169 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/common/PlainObjectReference.java

@@ -1,84 +0,0 @@
-//==============================================================================
-//	
-//	Copyright (c) 2015-
-//	Authors:
-//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (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 <T> the type of the underlying class
- */
-public class PlainObjectReference<T>
-{
-	/** 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;
-	}
-}

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<PlainObjectReference<SimpleLTL>> seen = new HashSet<PlainObjectReference<SimpleLTL>>();
+		// use an IdentityHashMap with (formula,formula) pairs indicating that formula
+		// has already been seen (due to lack of IdentityHashSet)
+		IdentityHashMap<SimpleLTL, SimpleLTL> seen = new IdentityHashMap<SimpleLTL, SimpleLTL>();
 		return isTree(seen);
 	}
 
@@ -921,13 +922,12 @@ public class SimpleLTL {
 	 *
 	 * The already seen SimpleLTL subtrees are tracked in {@code seen}.
 	 */
-	private boolean isTree(HashSet<PlainObjectReference<SimpleLTL>> seen)
+	private boolean isTree(IdentityHashMap<SimpleLTL,SimpleLTL> seen)
 	{
-		PlainObjectReference<SimpleLTL> ref = new PlainObjectReference<SimpleLTL>(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<PlainObjectReference<SimpleLTL>, String> map = new HashMap<PlainObjectReference<SimpleLTL>, String>();
+		IdentityHashMap<SimpleLTL, String> map = new IdentityHashMap<SimpleLTL, String>();
 
 		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<PlainObjectReference<SimpleLTL>, String> seen)
+	private String toDot(PrintStream out, IdentityHashMap<SimpleLTL, String> seen)
 	{
-		PlainObjectReference<SimpleLTL> ref = new PlainObjectReference<SimpleLTL>(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) {