From 25eebecd10f8bfa9810e73f4efdc5b0be4a305a2 Mon Sep 17 00:00:00 2001
From: Elliott Baron <ebaron@fedoraproject.org>
Date: Sun, 1 Nov 2009 00:02:17 -0400
Subject: 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.
---
 .../codan/extension/QuineMcCluskeySimplifier.java  | 114 +++++++++++++++++++++
 1 file changed, 114 insertions(+)
 create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java

(limited to 'org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/QuineMcCluskeySimplifier.java')

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;
+	}
+
+}
-- 
cgit