Graph Class

src/main/java/proof/data/Graph.java

@@ -0,0 +1,114 @@
+package proof.data;
+
+/**
+ * Maintains a graph.
+ * 
+ * Represents a graph by an adjacency matrix. Requires nodes to be indexed continuously.
+ * 
+ * @author Tilo Wiedera
+ *
+ */
+public class Graph {
+
+  private int[][] edgeIndices;
+  private double[] costs;
+
+  public final static int NO_EDGE = -1;
+  public final static double NO_EDGE_COST = Double.MAX_VALUE;
+
+  /**
+   * Creates a new graph with the exact number of nodes and edges.
+   * 
+   * @param numberOfNodes The number of nodes
+   * 
+   * @param numberOfEdges The number of edges
+   */
+  public Graph(int numberOfNodes, int numberOfEdges) {
+    costs = new double[numberOfEdges];
+    edgeIndices = new int[numberOfNodes][numberOfNodes];
+
+    for (int i = 0; i < numberOfEdges; i++) {
+      costs[i] = NO_EDGE_COST;
+    }
+
+    for (int i = 0; i < numberOfNodes; i++) {
+      for (int ii = 0; ii < numberOfNodes; ii++) {
+        edgeIndices[i][ii] = NO_EDGE;
+      }
+    }
+  }
+
+  /**
+   * Checks whether a single edge exists (or its directed counterpart).
+   * 
+   * @param source The index of the first node
+   * @param target The index of the second node
+   * 
+   * @return {@code true} iff the edge exist
+   */
+  public boolean edgeExists(int source, int target) {
+    if (source < 0 || source >= edgeIndices.length) {
+      throw new IllegalArgumentException("source node out of range: " + source);
+    }
+    if (target < 0 || target >= edgeIndices.length) {
+      throw new IllegalArgumentException("target node out of range: " + source);
+    }
+
+    return edgeIndices[source][target] != NO_EDGE;
+  }
+
+  /**
+   * Returns the id of any single edge.
+   * 
+   * @param source The index of the first node
+   * @param target The index of the second node
+   * 
+   * @return The index of the edge
+   */
+  int getEdgeId(int source, int target) {
+    if (!edgeExists(source, target)) {
+      throw new IllegalArgumentException("Edge does not exist!");
+    }
+
+    return edgeIndices[source][target];
+  }
+
+  /**
+   * Returns the cost of a single edge
+   * 
+   * @param source The index of the first node
+   * @param target The index of the second node
+   * 
+   * @return The cost
+   */
+  public double getEdgeCost(int source, int target) {
+    return costs[getEdgeId(source, target)];
+  }
+
+  /**
+   * Creates a new edge.
+   * 
+   * Will fail if the index is already in use or the edge already exists.
+   * 
+   * @param edgeId The edge index to be used
+   * @param source The index of the first node
+   * @param target The index of the second node
+   * @param cost The cost of the edge
+   */
+  public void addEdge(int edgeId, int source, int target, double cost) {
+    if (edgeExists(source, target)) {
+      throw new IllegalArgumentException("Can not override existing edge!");
+    }
+
+    if (edgeId < 0 || edgeId >= costs.length) {
+      throw new IllegalArgumentException("Edge index out of bounds: " + edgeId);
+    }
+
+    if (costs[edgeId] != NO_EDGE_COST) {
+      throw new IllegalArgumentException("Edge ID already exists!");
+    }
+
+    costs[edgeId] = cost;
+    edgeIndices[source][target] = edgeIndices[target][source] = edgeId;
+  }
+}

src/main/java/proof/data/reader/GraphReader.java

@@ -0,0 +1,36 @@
+package proof.data.reader;
+
+import org.json.JSONArray;
+import org.json.JSONException;
+import org.json.JSONObject;
+
+import proof.data.Graph;
+import proof.exception.InvalidGraphException;
+
+public class GraphReader implements ObjectReader {
+
+  @Override
+  public Graph read(JSONObject input) {
+    try {
+      int numberOfNodes = input.getInt("numberOfNodes");
+
+      JSONArray edges = input.getJSONArray("edges");
+
+      Graph result = new Graph(numberOfNodes, edges.length());
+
+      for (int i = 0; i < edges.length(); i++) {
+        JSONObject edge = edges.getJSONObject(i);
+
+        result.addEdge(edge.getInt("id"), edge.getInt("source"), edge.getInt("target"),
+            edge.getDouble("cost"));
+      }
+
+      return result;
+
+    } catch (IllegalArgumentException | JSONException e) {
+      InvalidGraphException exception = new InvalidGraphException("Could not parse JSON");
+      exception.initCause(e);
+      throw exception;
+    }
+  }
+}

src/main/java/proof/exception/InvalidGraphException.java

@@ -0,0 +1,9 @@
+package proof.exception;
+
+public class InvalidGraphException extends RuntimeException {
+
+  public InvalidGraphException(String description) {
+    super(description);
+  }
+
+}

src/main/java/proof/validator/ConstraintValidator.java

@@ -15,7 +15,7 @@
  * Validates a single Kuratwoski Constraint.
  *
  * The only type of constraints included in the log are Kuratwoski constraints. These constrains
- * will be validated by proving the repective paths do form a Kuratowski-Subdivision. Valid
+ * will be validated by proving the respective paths do form a Kuratowski-subdivision. Valid
  * Kuratowski subdivisions are the K3,3 and the K5.
  *
  * @author Tilo Wiedera
@@ -45,16 +45,49 @@ public void validate(JSONObject object) throws InvalidProofException {
 
     JSONArray paths = object.getJSONArray("paths");
 
-    boolean isK33 = paths.length() == 9;
-    boolean isK5 = paths.length() == 10;
+    validatePaths(vars, paths);
 
-    if (!isK33 && !isK5) {
+    if (paths.length() == 9) {
+      validateK33(vars, paths);
+    } else if (paths.length() == 10) {
+      validateK5(vars, paths);
+    } else {
       throw new InvalidConstraintException(
           "Invalid number of Kuratowski-Paths for single Constraint: " + paths.length());
     }
+  }
 
+  /**
+   * For each path, we have to validate the required crossings are realized.
+   *
+   * @param vars
+   * @param paths
+   */
+  private void validatePaths(Map<CrossingIndex, Boolean> vars, JSONArray paths) {
     for (int i = 0; i < paths.length(); i++) {
+      JSONArray path = paths.getJSONArray(i);
+
 
     }
   }
+
+  /**
+   * Asserts that all five nodes are connected to one another.
+   *
+   * @param vars
+   * @param paths
+   */
+  private void validateK5(Map<CrossingIndex, Boolean> vars, JSONArray paths) {
+    // TODO
+  }
+
+  /**
+   * Asserts a valid K33, i.e. a bipartit Graph with 3 nodes in each of the two subsets.
+   *
+   * @param vars
+   * @param paths
+   */
+  private void validateK33(Map<CrossingIndex, Boolean> vars, JSONArray paths) {
+    // TODO
+  }
 }

src/test/java/proof/validator/ResourceBasedTest.java → src/test/java/proof/ResourceBasedTest.java

@@ -1,4 +1,4 @@
-package proof.validator;
+package proof;
 
 import static org.junit.Assert.fail;
 

src/test/java/proof/data/reader/GraphReaderTest.java

@@ -0,0 +1,84 @@
+package proof.data.reader;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+import static org.junit.Assert.fail;
+
+import java.io.IOException;
+
+import org.junit.Test;
+
+import proof.ResourceBasedTest;
+import proof.data.Graph;
+import proof.exception.InvalidGraphException;
+
+/**
+ * Tests for {@link GraphReader}.
+ * 
+ * @author Tilo Wiedera
+ *
+ */
+public class GraphReaderTest extends ResourceBasedTest {
+
+  @Override
+  protected String getResourceSubdir() {
+    return "graph-reader";
+  }
+
+  private final GraphReader graphReader = new GraphReader();
+
+
+  @Test(expected = InvalidGraphException.class)
+  public void testRead_empty() throws IOException {
+    graphReader.read(loadJSON("invalid/empty"));
+  }
+
+  @Test(expected = InvalidGraphException.class)
+  public void testRead_ambiguous() throws IOException {
+    graphReader.read(loadJSON("invalid/ambiguous-edge-ids"));
+  }
+
+  @Test(expected = InvalidGraphException.class)
+  public void testRead_nodeOutOfRange() throws IOException {
+    graphReader.read(loadJSON("invalid/node-out-of-range"));
+  }
+
+  @Test(expected = InvalidGraphException.class)
+  public void testRead_multiEdge() throws IOException {
+    graphReader.read(loadJSON("invalid/multi-edge"));
+  }
+
+  @Test(expected = InvalidGraphException.class)
+  public void testRead_multiEdgeDirected() throws IOException {
+    graphReader.read(loadJSON("invalid/multi-edge-directed"));
+  }
+
+  @Test(expected = InvalidGraphException.class)
+  public void testRead_edgeOutOfRange() throws IOException {
+    graphReader.read(loadJSON("invalid/edge-out-of-range"));
+  }
+
+  @Test
+  public void testRead_simple() throws IOException {
+    Graph graph = graphReader.read(loadJSON("valid/simple"));
+
+    assertFalse(graph.edgeExists(0, 3));
+    assertFalse(graph.edgeExists(1, 3));
+    assertFalse(graph.edgeExists(2, 3));
+
+    assertTrue(graph.edgeExists(0, 1));
+    assertTrue(graph.edgeExists(0, 2));
+    assertTrue(graph.edgeExists(1, 2));
+
+    assertEquals(30, (int) graph.getEdgeCost(0, 2));
+    assertEquals(30, (int) graph.getEdgeCost(2, 0));
+    assertEquals(78, (int) graph.getEdgeCost(1, 2));
+
+    try {
+      graph.getEdgeCost(0, 3);
+      fail("getEdgeCost for invalid edge should throw an exception");
+    } catch (IllegalArgumentException expected) {
+    }
+  }
+}

src/test/java/proof/validator/BranchCoverageValidatorTest.java

@@ -4,6 +4,7 @@
 
 import org.junit.Test;
 
+import proof.ResourceBasedTest;
 import proof.exception.InvalidCoverageException;
 
 public class BranchCoverageValidatorTest extends ResourceBasedTest {

src/test/resources/graph-reader/invalid/ambiguous-edge-ids.json

@@ -0,0 +1,23 @@
+{
+	"numberOfNodes": 3,
+	"edges": [ 
+		{
+			"id": 0,
+			"source": 0,
+			"target": 2,
+			"cost": 30.123
+		},
+		{
+			"id": 1,
+			"cost": 78,
+			"source": 1,
+			"target": 2
+		},
+		{
+			"source": 1,
+			"id": 1,
+			"cost": 0.42,
+			"target": 0
+		}
+	]
+}

src/test/resources/graph-reader/invalid/edge-out-of-range.json

@@ -0,0 +1,17 @@
+{
+	"numberOfNodes": 3,
+	"edges": [ 
+		{
+			"id": 0,
+			"source": 0,
+			"target": 2,
+			"cost": 30.123
+		},
+		{
+			"id": 2,
+			"cost": 78,
+			"source": 1,
+			"target": 2
+		}
+	]
+}

src/test/resources/graph-reader/invalid/empty.json

@@ -0,0 +1,3 @@
+{
+	"test": true
+}

src/test/resources/graph-reader/invalid/multi-edge-directed.json

@@ -0,0 +1,23 @@
+{
+	"numberOfNodes": 3,
+	"edges": [ 
+		{
+			"id": 0,
+			"source": 0,
+			"target": 2,
+			"cost": 30.123
+		},
+		{
+			"id": 2,
+			"cost": 78,
+			"source": 1,
+			"target": 2
+		},
+		{
+			"source": 2,
+			"id": 1,
+			"cost": 0.42,
+			"target": 1
+		}
+	]
+}