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.
---
 .../eclipse/cdt/codan/extension/ESTruthTable.java  | 86 ++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100644 org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ESTruthTable.java

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

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