Implemented Quine-McCluskey algorithm to join execution states. Property simulation working!

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: Join execution states.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: Implement equals and hashCode.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java: Use PropSim.

8 files changed, 492 insertions, 52 deletions

diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java
new file mode 100644
index 0000000..3b62b87
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESSimplifier.java
@@ -0,0 +1,72 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import org.eclipse.cdt.codan.extension.Minterm.Value;
+import org.eclipse.cdt.core.dom.ast.IVariable;
+
+public class ESSimplifier extends QuineMcCluskeySimplifier<IVariable> {
+
+	public ESSimplifier(ITruthTable<IVariable> tt) {
+		super(tt);
+	}
+
+	public Set<ExecutionState> getExecutionStateCover() {
+		Set<ExecutionState> ret = new HashSet<ExecutionState>();
+		List<Minterm<IVariable>> implicantCover = getImplicantCover();
+		for (Minterm<IVariable> term : implicantCover) {
+			ExecutionState es = new ExecutionState();
+			for (IVariable var : variables) {
+				Value val = term.getValue(var);
+				if (val == Value.TRUE) {
+					es.addClause(new ExecutionStateClause(var, true));
+				}
+				else if (val == Value.FALSE) {
+					es.addClause(new ExecutionStateClause(var, false));
+				}
+				// Don't care about Don't cares
+			}
+			ret.add(es);
+		}
+		return ret;
+	}
+	
+	@Override
+	public String toString() {
+		StringBuffer buf = new StringBuffer();
+		for (IVariable var : variables) {
+			buf.append(var.getName());
+			buf.append(" ");
+		}
+		buf.append("\n");
+		for (Minterm<IVariable> term : minterms) {
+			for (IVariable var : variables) {
+				switch (term.getValue(var)) {
+				case TRUE:
+					buf.append("1");
+					break;
+				case FALSE:
+					buf.append("0");
+					break;
+				default:
+					buf.append("-");
+				}
+				buf.append(" ");
+			}
+			buf.append("\n");
+		}
+		return buf.toString();
+	}
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java
new file mode 100644
index 0000000..94e7574
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java
@@ -0,0 +1,86 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import org.eclipse.cdt.codan.extension.Minterm.Value;
+import org.eclipse.cdt.core.dom.ast.IVariable;
+
+public class ESTruthTable implements ITruthTable<IVariable> {
+	private List<Minterm<IVariable>> minterms;
+	private List<IVariable> variables;
+	
+	public ESTruthTable(Set<ExecutionState> es) {
+		minterms = new ArrayList<Minterm<IVariable>>();
+		variables = new ArrayList<IVariable>();
+		
+		for (ExecutionState e : es) {
+			for (ExecutionStateClause c : e.getClauses()) {
+				IVariable var = c.getVariable();
+				if (!variables.contains(var)) {
+					variables.add(var);
+				}
+			}
+		}
+		
+		// Initialize with Don't Cares
+		for (int i = 0; i < es.size(); i++) {
+			Map<IVariable, Value> values = new HashMap<IVariable, Value>();
+			for (IVariable var : variables) {
+				values.put(var, Value.DONTCARE);
+			}
+			minterms.add(new Minterm<IVariable>(values));
+		}
+		
+		// Set actual truth values
+		Iterator<ExecutionState> it = es.iterator();
+		for (int i = 0; i < es.size(); i++) {
+			Minterm<IVariable> term = minterms.get(i);
+			ExecutionState e = it.next();
+			for (ExecutionStateClause c : e.getClauses()) {
+				term.setValue(c.getVariable(), c.isTrue() ? Value.TRUE : Value.FALSE);
+			}
+		}		
+	}
+	
+	public List<Minterm<IVariable>> getMinterms() {
+		return minterms;
+	}
+	
+	public List<IVariable> getVariables() {
+		return variables;
+	}
+	
+	@Override
+	public String toString() {
+		StringBuffer buf = new StringBuffer();
+		for (IVariable var : variables) {
+			buf.append(var.getName());
+			buf.append(" ");
+		}
+		buf.append("\n");
+		for (Minterm<IVariable> term : minterms) {
+			for (IVariable var : variables) {
+				buf.append(term.getValue(var));
+				buf.append(" ");
+			}
+			buf.append("\n");
+		}
+		return buf.toString();
+	}
+
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
index 208f9f0..c19970e 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
@@ -10,26 +10,26 @@
  *******************************************************************************/
 package org.eclipse.cdt.codan.extension;
 
-import java.util.ArrayList;
 import java.util.HashMap;
-import java.util.List;
+import java.util.HashSet;
 import java.util.Map;
+import java.util.Set;
 
 import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ExecutionState {
-	private List<ExecutionStateClause> clauses;
+	private Set<ExecutionStateClause> clauses;
 	private Map<IVariable, Boolean> truthAssignments;
 	private boolean top;
 	private boolean bottom;
 
 	public ExecutionState() {
 		truthAssignments = new HashMap<IVariable, Boolean>();
-		clauses = new ArrayList<ExecutionStateClause>();
+		clauses = new HashSet<ExecutionStateClause>();
 		top = true;
 		bottom = false;
 	}
-	
+
 	public void addClause(ExecutionStateClause clause) {
 		// Cannot get out of bottom, do not add duplicate clauses
 		if (!bottom && !clauses.contains(clause)) {
@@ -37,110 +37,126 @@ public class ExecutionState {
 			if (clauses.contains(clause.getNegation())) {
 				clauses.clear();
 				bottom = true; // x AND NOT x = F
-			}
-			else {
+			} else {
 				clauses.add(clause);
 			}
 		}
 	}
-	
+
 	public void removeClause(ExecutionStateClause node) {
 		clauses.remove(node);
 		if (clauses.size() == 0) {
 			setTop();
 		}
 	}
-	
+
 	public void addTruthAssignment(IVariable var, boolean value) {
 		truthAssignments.put(var, value);
 	}
-	
+
 	public Map<IVariable, Boolean> getTruthAssignments() {
 		return truthAssignments;
 	}
-	
+
 	public void setTruthAssignments(Map<IVariable, Boolean> truthAssignments) {
 		this.truthAssignments = truthAssignments;
 	}
-	
+
 	public void bindTruthAssignments() {
 		boolean unsatisfiable = false;
-		List<ExecutionStateClause> clausesCopy = new ArrayList<ExecutionStateClause>(clauses);
+		Set<ExecutionStateClause> clausesCopy = new HashSet<ExecutionStateClause>(
+				clauses);
 		for (ExecutionStateClause c : clausesCopy) {
 			Boolean truth = truthAssignments.get(c.getVariable());
 			if (truth != null) {
-				if (truth == c.isTrue()) { // does truth value of clause match truth assignment?
+				if (truth == c.isTrue()) { // does truth value of clause match
+											// truth assignment?
 					removeClause(c);
-				}
-				else {
+				} else {
 					unsatisfiable = true;
 				}
 			}
 		}
-		
+
 		if (unsatisfiable) {
 			setBottom();
 		}
 	}
-	
-	//FIXME
-	public ExecutionState join(ExecutionState other) {
-		// Add clauses from other, canceling out negating clauses
-		for (ExecutionStateClause clause : other.getClauses()) {
-			ExecutionStateClause negation = clause.getNegation();
-			if (clauses.contains(negation)) {
-				removeClause(negation);
-				other.removeClause(clause);
-			}
-		}
-		return this;
+
+	public static Set<ExecutionState> join(Set<ExecutionState> es) {
+		ESTruthTable tt = new ESTruthTable(es);
+		ESSimplifier simp = new ESSimplifier(tt);
+		return simp.getExecutionStateCover();
 	}
-	
-	public ExecutionStateClause[] getClauses() {
-		return clauses.toArray(new ExecutionStateClause[clauses.size()]);
+
+	public Set<ExecutionStateClause> getClauses() {
+		return clauses;
 	}
-	
+
 	public boolean isTop() {
 		return top;
 	}
-	
+
 	public boolean isBottom() {
 		return bottom;
 	}
-	
+
 	public void setTop() {
 		top = true;
 		bottom = false;
 		clauses.clear();
 	}
-	
+
 	public void setBottom() {
 		bottom = true;
 		top = false;
 		clauses.clear();
 	}
-	
+
 	@Override
 	public String toString() {
 		String ret;
 		if (top) {
 			ret = "[TOP]";
-		}
-		else if (bottom) {
+		} else if (bottom) {
 			ret = "[BOTTOM]";
-		}
-		else {
+		} else {
 			StringBuffer buf = new StringBuffer();
 			if (clauses.size() > 0) {
 				for (ExecutionStateClause c : clauses) {
 					buf.append(c);
 					buf.append(" AND ");
 				}
-				buf.delete(buf.length() - 5 /* " AND ".length() */, buf.length());
+				buf.delete(buf.length() - 5 /* " AND ".length() */, buf
+						.length());
 			}
 			ret = buf.toString();
 		}
 		return ret;
 	}
 
+	public ExecutionState copy() {
+		ExecutionState ret = new ExecutionState();
+		for (ExecutionStateClause cl : clauses) {
+			ret.addClause(cl);
+		}
+		return ret;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof ExecutionState) {
+			ExecutionState other = (ExecutionState) obj;
+			return clauses.equals(other.getClauses())
+					&& truthAssignments.equals(other.getTruthAssignments())
+					&& top == other.isTop() && bottom == other.isBottom();
+		}
+		return false;
+	}
+	
+	@Override
+	public int hashCode() {
+		return clauses.hashCode() + truthAssignments.hashCode() + (top ? 1 : 0) + (bottom ? 1 : 0);
+	}
+
 }
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java
new file mode 100644
index 0000000..dd15f2d
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ITruthTable.java
@@ -0,0 +1,21 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.List;
+
+public interface ITruthTable<E> {
+
+	List<Minterm<E>> getMinterms();
+	
+	List<E> getVariables();
+	
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java
new file mode 100644
index 0000000..1aeb0a2
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Minterm.java
@@ -0,0 +1,117 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class Minterm<E> {
+	private Map<E, Value> values;
+
+	public enum Value {
+		TRUE,
+		FALSE,
+		DONTCARE
+	}
+
+	public Minterm(Map<E, Value> values) {
+		this.values = values;
+	}
+
+	public void setValue(E var, Value val) {
+		values.put(var, val);
+	}
+
+	public Value getValue(E var) {
+		return values.get(var);
+	}
+
+	public int length() {
+		return values.size();
+	}
+
+	public Minterm<E> copy() {
+		return new Minterm<E>(new HashMap<E, Value>(values));
+	}
+
+	public Minterm<E> combineTerms(Minterm<E> other) {
+		Minterm<E> ret = null;
+		E diff = null;
+		for (E var : values.keySet()) {
+			if (!values.get(var).equals(other.getValue(var))) {
+				if (diff != null) {
+					// More than one difference
+					diff = null;
+					break;
+				}
+				diff = var;
+			}
+		}
+		
+		// One difference, combine
+		if (diff != null) {
+			ret = copy();
+			// Set the differing value to don't care
+			ret.setValue(diff, Value.DONTCARE);
+		}
+		
+		return ret;
+	}
+	
+	public boolean implies(Minterm<E> other) {
+		boolean result = true;
+		for (E var : values.keySet()) {
+			Value value = values.get(var);
+			if (value != Value.DONTCARE && value != other.getValue(var)) {
+				result = false;
+			}
+		}
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof Minterm<?>) {
+			Minterm<?> other = (Minterm<?>) obj;
+			return values.equals(other.values);
+		}
+		return false;
+	}
+	
+	@Override
+	public int hashCode() {
+		return values.hashCode();
+	}
+	
+	@Override
+	public String toString() {
+		StringBuffer buf = new StringBuffer();
+		for (E k : values.keySet()) {
+			buf.append(k);
+			buf.append(" ");
+		}
+		buf.append("\n");
+		for (Value v : values.values()) {
+			switch (v) {
+			case TRUE:
+				buf.append("1");
+				break;
+			case FALSE:
+				buf.append("0");
+				break;
+			default:
+				buf.append("-");
+			}
+			buf.append(" ");
+		}
+		return buf.toString();	
+	}
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java
new file mode 100644
index 0000000..d363028
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java
@@ -0,0 +1,114 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map;
+import java.util.Queue;
+
+public class QuineMcCluskeySimplifier<E> {
+	protected List<Minterm<E>> minterms;
+	protected List<E> variables;
+	protected List<Minterm<E>> implicantCover;
+	
+	public QuineMcCluskeySimplifier(ITruthTable<E> tt) {
+		minterms = tt.getMinterms();
+		variables = tt.getVariables();
+		List<Minterm<E>> inputMinterms = new ArrayList<Minterm<E>>(minterms);
+		List<Minterm<E>> primeImplicants = new ArrayList<Minterm<E>>(minterms);
+				
+		boolean change = true;
+		while (change && minterms.size() > 1) { // Iterate until we achieve a steady state
+			change = false;
+			Queue<Minterm<E>> primary = new LinkedList<Minterm<E>>();
+			primary.addAll(minterms);			
+			while (!primary.isEmpty()) { // Iterate through all combinations
+				Minterm<E> one = primary.remove();			
+				Queue<Minterm<E>> secondary = new LinkedList<Minterm<E>>();
+				secondary.addAll(minterms);
+				while (!secondary.isEmpty()) {
+					Minterm<E> two = secondary.remove();
+					Minterm<E> combined = one.combineTerms(two);
+					if (combined != null) {
+						if (!minterms.contains(combined)) {
+							change = true;
+							minterms.add(combined);
+						}
+						// Combined one and two so neither are prime implicants
+						primeImplicants.remove(one);
+						primeImplicants.remove(two);
+						if (!primeImplicants.contains(combined)) {
+							primeImplicants.add(combined);
+						}
+					}
+				}
+			}
+		}
+		
+		// Determine which prime implicants cover which original minterms
+		Map<Minterm<E>, List<Minterm<E>>> implications = new HashMap<Minterm<E>, List<Minterm<E>>>();
+		for (Minterm<E> implicant : primeImplicants) {
+			implications.put(implicant, new ArrayList<Minterm<E>>());
+			for (Minterm<E> minterm : inputMinterms) {
+				if (implicant.implies(minterm)) {
+					implications.get(implicant).add(minterm);
+				}
+			}
+		}
+		
+		implicantCover = new ArrayList<Minterm<E>>();
+		// remove minterms which are implied by an essential implicant
+		List<Minterm<E>> mintermsCopy = new ArrayList<Minterm<E>>(inputMinterms);
+		for (Minterm<E> minterm : mintermsCopy) {
+			Minterm<E> implicant = null;
+			int numImplications = 0;
+			for (Minterm<E> pi : primeImplicants) {
+				List<Minterm<E>> impl = implications.get(pi);
+				if (impl.contains(minterm)) {
+					implicant = pi;
+					numImplications++;
+				}
+			}
+			// essential implicant
+			if (numImplications == 1) {
+				inputMinterms.removeAll(implications.get(implicant));
+				if (!implicantCover.contains(implicant)) {
+					implicantCover.add(implicant);
+				}
+			}
+		}
+		
+		// Remove essential implicants from our list
+		primeImplicants.removeAll(implicantCover);
+		
+		// find a cover for the remaining minterms
+		while (inputMinterms.size() > 0) {
+			Minterm<E> maxImplicant = null;
+			for (Minterm<E> pi : primeImplicants) {
+				if (maxImplicant == null
+						|| implications.get(pi).size() >= implications.get(maxImplicant).size()) {
+					maxImplicant = pi;
+				}
+			}
+			inputMinterms.removeAll(implications.get(maxImplicant));
+			primeImplicants.remove(maxImplicant);
+			implicantCover.add(maxImplicant);
+		}
+	}
+	
+	public List<Minterm<E>> getImplicantCover() {
+		return implicantCover;
+	}
+
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
index 93bf3be..19dd6b3 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
@@ -45,10 +45,7 @@ public class SymbolicState {
 	
 	public SymbolicState copy() {
 		Set<PropertyState> ps = new HashSet<PropertyState>(propertyStates);
-		ExecutionState es = new ExecutionState();
-		for (ExecutionStateClause cl : executionState.getClauses()) {
-			es.addClause(cl);
-		}
+		ExecutionState es = executionState.copy();
 		Map<IVariable, Boolean> truthAssignments = new HashMap<IVariable, Boolean>(executionState.getTruthAssignments());
 		es.setTruthAssignments(truthAssignments);
 		
@@ -65,4 +62,18 @@ public class SymbolicState {
 		buf.append("]");
 		return buf.toString();
 	}
+	
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof SymbolicState) {
+			SymbolicState other = (SymbolicState) obj;
+			return propertyStates.equals(other.getPropertyStates()) && executionState.equals(other.getExecutionState());
+		}
+		return false;
+	}
+	
+	@Override
+	public int hashCode() {
+		return propertyStates.hashCode() + executionState.hashCode();
+	}
 }
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
index 5ea8e79..491a481 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
@@ -210,7 +210,7 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 	}
 
 	private Set<SymbolicState> group(Set<SymbolicState> ss) {
-		return groupPSA(ss);
+		return groupPropSim(ss);
 	}
 	
 	private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) {
@@ -236,12 +236,15 @@ public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
 		for (PropertyState p : statesPerProperty.keySet()) {
 			Set<PropertyState> ps = new HashSet<PropertyState>();
 			ps.add(p);
-			ExecutionState es = new ExecutionState();
-			for (ExecutionState e : statesPerProperty.get(p)) {
-				es.join(e);
+			Set<ExecutionState> es = statesPerProperty.get(p);
+			if (es.size() > 1) {
+				// Join execution states in this set
+				es = ExecutionState.join(es);
+			}
+			for (ExecutionState e : es) {
+				SymbolicState s = new SymbolicState(ps, e);
+				ret.add(s);
 			}
-			SymbolicState s = new SymbolicState(ps, es);
-			ret.add(s);
 		}		
 		
 		return ret;