create OBDD solution, add own validator for graph solutions

solutions/RelationalRAGSolution/src/main/jastadd/Analysis.jrag

+aspect Analysis {
+
+  syn Boolean Row.valueFor(Port port) {
+    for (Cell cell : getCellList()) {
+      if (cell.getPort().equals(port)) {
+        return cell.getValue();
+      }
+    }
+    return null;
+  }
+
+  syn Boolean TerminalNode.valueFor(Port port) {
+    for (Assignment assignment : getAssignmentList()) {
+      if (assignment.getPort().equals(port)) {
+        return assignment.getValue();
+      }
+    }
+    return null;
+  }
+}

solutions/RelationalRAGSolution/src/main/jastadd/BDD.relast

@@ -9,8 +9,8 @@ InnerNode:AbstractNode;
 // rel OutputPort.Assignment* <-> Assignment.Port;
 
 rel BDD.Root -> AbstractNode;
-rel InnerNode.GraphForZero? <-> AbstractNode.ParentForZero*;
-rel InnerNode.GraphForOne? <-> AbstractNode.ParentForOne*;
+rel InnerNode.GraphForZero <-> AbstractNode.ParentForZero*;
+rel InnerNode.GraphForOne <-> AbstractNode.ParentForOne*;
 rel InputPort.InnerNode* <-> InnerNode.Port;
 rel BDD.Port* -> Port;
 

solutions/RelationalRAGSolution/src/main/jastadd/CaseBDD.jrag

@@ -42,12 +42,12 @@ aspect SimpleBDD {
       List<Row> rowsForOne = new ArrayList();
       for (Row row: rows) {
         Boolean rowValue = row.valueFor(nextPort);
-        if (rowValue) {
+        if (rowValue == null) {
           rowsForOne.add(row);
-        } else if (!rowValue) {
           rowsForZero.add(row);
-        } else {
+        } else if (rowValue) {
           rowsForOne.add(row);
+        } else {
           rowsForZero.add(row);
         }
       }

solutions/RelationalRAGSolution/src/main/jastadd/CaseBDT.jrag

@@ -41,12 +41,12 @@ aspect SimpleBDT {
       List<Row> rowsForOne = new ArrayList();
       for (Row row: rows) {
         Boolean rowValue = row.valueFor(nextPort);
-        if (rowValue) {
+        if (rowValue == null) {
           rowsForOne.add(row);
-        } else if (!rowValue) {
           rowsForZero.add(row);
-        } else {
+        } else if (rowValue) {
           rowsForOne.add(row);
+        } else {
           rowsForZero.add(row);
         }
       }

solutions/RelationalRAGSolution/src/main/jastadd/Navigation.jrag

@@ -11,6 +11,9 @@ aspect Navigation {
   syn Subtree Tree.asSubtree() = null;
   eq Subtree.asSubtree() = this;
 
+  syn InnerNode AbstractNode.asInnerNode() = null;
+  eq InnerNode.asInnerNode() = this;
+
   // inh TruthTable LocatedElement.containingTruthTable();
   // eq TruthTable.getPort().containingTruthTable() = this;
   // eq TruthTable.getRow().containingTruthTable() = this;
@@ -26,4 +29,32 @@ aspect Navigation {
 
   syn ASTNode TruthTable.root() = this;
   syn ASTNode BDT.root() = this;
+
+  inh TruthTable Port.containingTruthTable();
+  inh TruthTable Row.containingTruthTable();
+  inh TruthTable PortOrder.containingTruthTable();
+  inh TruthTable Cell.containingTruthTable();
+  eq TruthTable.getPort().containingTruthTable() = this;
+  eq TruthTable.getRow().containingTruthTable() = this;
+  eq TruthTable.getPortOrder().containingTruthTable() = this;
+
+  syn List<OutputPort> TruthTable.outputPorts() {
+    List<OutputPort> result = new ArrayList<>();
+    for (Port port: getPortList()) {
+      if (!port.isInput()) {
+        result.add(port.asOutput());
+      }
+    }
+    return Collections.unmodifiableList(result);
+  }
+
+  syn List<InputPort> TruthTable.inputPorts() {
+    List<InputPort> result = new ArrayList<>();
+    for (Port port: getPortList()) {
+      if (port.isInput()) {
+        result.add(port.asInput());
+      }
+    }
+    return Collections.unmodifiableList(result);
+  }
 }

solutions/RelationalRAGSolution/src/main/jastadd/SimpleBDT.jrag

@@ -24,9 +24,14 @@ aspect SimpleBDT {
     for (Row row : getRowList()) {
       row.printDebug();
       Subtree current = firstSubtree;
-      boolean value = row.valueFor(firstSubtree.getPort());
+      Boolean value = row.valueFor(firstSubtree.getPort());
       for (InputPort port : portOrder.subTreePortList()) {
+        if (value!=null) {
           current = current.getOrCreateSubtree(port, value);
+        } else {
+          current.getOrCreateSubtree(port, true);
+          current = current.getOrCreateSubtree(port, false);
+        }
         value = row.valueFor(port);
       }
       // create leaf node
@@ -59,21 +64,25 @@ aspect SimpleBDT {
   syn InputPort PortOrder.leafPort() = getPortList().get(getPortList().size() - 1);
 
   //--- getOrCreateSubtree ---
-  Subtree Subtree.getOrCreateSubtree(InputPort port, boolean value) {
-    Subtree result;
-    Tree tree = value ? getTreeForOne() : getTreeForZero();
-    if (tree == null) {
-      logger.debug("new subtree {} -{}-> {}", getPort().getName(), value ? 1 : 0, port.getName());
-      Subtree subTree = new Subtree();
-      subTree.setPort(port);
-      if (value) {
-        setTreeForOne(subTree);
+  Subtree Subtree.getOrCreateSubtree(InputPort port, Boolean value) {
+    Subtree result = null;
+    if (value == null || value) {
+      if (getTreeForOne() != null) {
+        result = getTreeForOne().asSubtree();
       } else {
-        setTreeForZero(subTree);
+        result = new Subtree();
+        result.setPort(port);
+        setTreeForOne(result);
+      }
     }
-      result = subTree;
+    if (value == null || !value) {
+      if (getTreeForZero() != null) {
+        result = getTreeForZero().asSubtree();
       } else {
-      result = tree.asSubtree();
+        result = new Subtree();
+        result.setPort(port);
+        setTreeForZero(result);
+      }
     }
     return result;
   }
@@ -81,7 +90,6 @@ aspect SimpleBDT {
   //--- createLeafNode ---
   void Subtree.createLeafNode(Port lastPort, Row row) {
     // assumption: treeForOne/Zero is always null at this point, so no need to check first
-    logger.debug("new leaf {} -{}-> leaf", getPort().getName(), row.valueFor(lastPort) ? 1 : 0);
     Leaf leaf = new Leaf();
     for (Cell cell : row.getCellList()) {
       if (!cell.getPort().isInput()) {
@@ -92,7 +100,21 @@ aspect SimpleBDT {
         leaf.addAssignment(assignment);
       }
     }
-    if (row.valueFor(lastPort)) {
+    Boolean value = row.valueFor(lastPort);
+    if (value == null){
+      setTreeForOne(leaf);
+      Leaf leaf2 = new Leaf();
+      for (Cell cell : row.getCellList()) {
+        if (!cell.getPort().isInput()) {
+          // add to list of assignments
+          Assignment assignment = new Assignment();
+          assignment.setPort(cell.getPort().asOutput());
+          assignment.setValue(cell.getValue());
+          leaf2.addAssignment(assignment);
+        }
+      }
+      setTreeForZero(leaf2);
+    } else if (value) {
       setTreeForOne(leaf);
     } else {
       setTreeForZero(leaf);
@@ -113,16 +135,6 @@ aspect SimpleBDT {
     return result;
   }
 
-  // Eval probably in extra aspect
-  syn boolean Row.valueFor(Port port) {
-    for (Cell cell : getCellList()) {
-      if (cell.getPort().equals(port)) {
-        return cell.getValue();
-      }
-    }
-    return false;
-  }
-
   syn PortOrder TruthTable.getPortOrder() {
     // a port order defines the order, in which the input ports are evaluated
     // for the simple case, this order is defined by the list in which the ports are defined

solutions/RelationalRAGSolution/src/main/jastadd/XMIWriter.jadd

@@ -241,14 +241,14 @@ aspect XMIWriter {
     b.append(" port=\"")
       .append(getPort().xmiPath())
       .append("\"");
-    if (hasGraphForZero()) {
+    if (getGraphForZero() != null) {
       b.append(" treeForZero=\"")
         .append(getGraphForZero().xmiPath())
         .append("\"");
     } else {
       logger.warn("GraphForZero is null in {}", xmiPath());
     }
-    if (hasGraphForOne()) {
+    if (getGraphForOne() != null) {
       b.append(" treeForOne=\"")
         .append(getGraphForOne().xmiPath())
         .append("\"");

solutions/RelationalRAGSolution/src/main/jastadd/reductionOBDD.jrag

+aspect ReductionOBDD {
+
+  public BDD TruthTable.reductionOBDD() {
+    BDD bdd = new BDD();
+
+    bdd.setName(getName());
+
+    for (Port port: getPortList()) {
+      bdd.addPort(port);
+    }
+
+    for (TerminalNode terminal: terminalNodeMap().values()) {
+      bdd.addAbstractNode(terminal);
+    }
+
+    PortOrder portOrder = getPortOrder();
+
+    InnerNode root = new InnerNode();
+    root.setPort(portOrder.getPortList().get(0));
+    bdd.addAbstractNode(root);
+    bdd.setRoot(root);
+
+    Port leafPort = portOrder.leafPort();
+    for (Row row : getRowList()) {
+      insertRow(bdd, root, row, 0);
+    }
+
+    return bdd;
+  }
+
+
+  public void TruthTable.insertRow(BDD bdd, InnerNode parent, Row row, int position) {
+
+    InputPort port = getPortOrder().getPortList().get(position);
+    Boolean value = row.valueFor(port);
+
+    if (position < getPortOrder().getPortList().size() - 1) {
+      InputPort nextPort = getPortOrder().getPortList().get(position + 1);
+      if (value == null || value) {
+        InnerNode result;
+        if (parent.getGraphForOne() != null) {
+          result = parent.getGraphForOne().asInnerNode();
+        } else {
+          result = new InnerNode();
+          result.setPort(nextPort);
+          parent.setGraphForOne(result);
+          bdd.addAbstractNode(result);
+        }
+        insertRow(bdd, result, row, position + 1);
+      }
+      if (value == null || !value) {
+        InnerNode result;
+        if (parent.getGraphForZero() != null) {
+          result = parent.getGraphForZero().asInnerNode();
+        } else {
+          result = new InnerNode();
+          result.setPort(nextPort);
+          parent.setGraphForZero(result);
+          bdd.addAbstractNode(result);
+        }
+        insertRow(bdd, result, row, position + 1);
+      }
+    } else {
+      TerminalNode terminal = terminalNodeMap().get(row.outputString());
+      if (value == null) {
+        if (parent.getGraphForOne() != null || parent.getGraphForZero() != null) {
+          throw new RuntimeException();
+        }
+        parent.setGraphForOne(terminal);
+        parent.setGraphForZero(terminal);
+      } else if (value) {
+        if (parent.getGraphForOne() != null) {
+          throw new RuntimeException();
+        }
+        parent.setGraphForOne(terminal);
+      } else {
+        if (parent.getGraphForZero() != null) {
+          throw new RuntimeException();
+        }
+        parent.setGraphForZero(terminal);
+      }
+    }
+  }
+
+  syn String Row.outputString() {
+    StringBuilder b = new StringBuilder();
+    for (OutputPort port: containingTruthTable().outputPorts()) {
+      Boolean value = valueFor(port);
+      b.append(value==null?"-":value);
+    }
+    return b.toString();
+  }
+
+  syn String TruthTable.compactTable() {
+    StringBuffer result = new StringBuffer();
+    for (Row row: getRowList()) {
+      result.append(row.rowString()).append("\n");
+    }
+    return result.toString();
+  }
+
+  syn String Row.rowString() {
+    StringBuilder b = new StringBuilder();
+    for (Port port: containingTruthTable().getPortList()) {
+      Boolean value = valueFor(port);
+      b.append(value==null?"-":(value?"1":"0"));
+    }
+    return b.toString();
+  }
+
+  syn String TerminalNode.assignmentString() {
+    StringBuilder b = new StringBuilder();
+    for (Port port: this.getAssignment(0).getPort().containingTruthTable().getPortList()) {
+      Boolean value = valueFor(port);
+      b.append(value==null?"-":(value?"1":"0"));
+    }
+    return b.toString();
+  }
+
+  syn Map<String, TerminalNode> TruthTable.terminalNodeMap() {
+    Map<String, TerminalNode> result = new HashMap<>(getNumRow());
+    for (Row row: getRowList()) {
+      String outputString = row.outputString();
+      if (!result.containsKey(outputString)) {
+        TerminalNode terminal = new TerminalNode();
+        for (Cell cell: row.getCellList()) {
+          Port cellPort = cell.getPort();
+          if (!cellPort.isInput()) {
+            Assignment a = new Assignment();
+            a.setPort(cellPort.asOutput());
+            a.setValue(cell.getValue());
+            terminal.addAssignment(a);
+          }
+        }
+        result.put(row.outputString(), terminal);
+      }
+    }
+    return result;
+  }
+}

solutions/RelationalRAGSolution/src/test/java/de/tudresden/inf/st/ttc19/JastAddTest.java

@@ -117,7 +117,7 @@ class JastAddTest {
     StringBuilder simpleBuilder = new StringBuilder();
     simpleBDT.writeBDT(simpleBuilder);
 
-    Path outputPath = Files.createTempFile("relrag-test-simple", ".bddmodel");
+    Path outputPath = Files.createTempFile("relrag-test-simpleBDT", ".bddmodel");
     outputPath.toFile().deleteOnExit();
     try (BufferedWriter writer = Files.newBufferedWriter(outputPath)) {
       writer.write(simpleBuilder.toString());
@@ -136,7 +136,7 @@ class JastAddTest {
 
     StringBuilder bddBuilder = new StringBuilder();
     caseBdd.writeBDT(bddBuilder);
-    Path outputPath = Files.createTempFile("relrag-test-case", ".bddmodel");
+    Path outputPath = Files.createTempFile("relrag-test-caseBDT", ".bddmodel");
     outputPath.toFile().deleteOnExit();
     try (BufferedWriter writer = Files.newBufferedWriter(outputPath)) {
       writer.write(bddBuilder.toString());
@@ -155,12 +155,33 @@ class JastAddTest {
 
     StringBuilder bddBuilder = new StringBuilder();
     caseBdd.writeBDD(bddBuilder);
-    Path outputPath = Files.createTempFile("relrag-test-case-bdd", ".bddmodel");
+    Path outputPath = Files.createTempFile("relrag-test-caseBDD", ".bddmodel");
+    // outputPath.toFile().deleteOnExit();
+    try (BufferedWriter writer = Files.newBufferedWriter(outputPath)) {
+      writer.write(bddBuilder.toString());
+    }
+
+    Assertions.assertTrue(new Validator().validate(tt, caseBdd));
+    validate(inputFile.getAbsolutePath(), outputPath.toString());
+  }
+
+  @ParameterizedTest
+  @MethodSource("truthTableFiles")
+  void testReductionOBDD(String pathName) throws IOException {
+    TruthTable tt = loadTruthTable(pathName);
+    File inputFile = new File(pathName);
+
+    BDD caseBdd = tt.reductionOBDD();
+
+    StringBuilder bddBuilder = new StringBuilder();
+    caseBdd.writeBDD(bddBuilder);
+    Path outputPath = Files.createTempFile("relrag-test-reductionOBDD", ".bddmodel");
     outputPath.toFile().deleteOnExit();
     try (BufferedWriter writer = Files.newBufferedWriter(outputPath)) {
       writer.write(bddBuilder.toString());
     }
 
+    Assertions.assertTrue(new Validator().validate(tt, caseBdd));
     validate(inputFile.getAbsolutePath(), outputPath.toString());
   }
 

solutions/RelationalRAGSolution/src/test/java/de/tudresden/inf/st/ttc19/Validator.java

+package de.tudresden.inf.st.ttc19;
+
+
+import de.tudresden.inf.st.ttc19.jastadd.model.*;
+
+import java.util.NoSuchElementException;
+
+public class Validator {
+
+  public boolean validate(TruthTable tt, BDD bdd) {
+    if (tt.getNumPort() != bdd.getPorts().size()) {
+      System.err.println(String.format(
+          "TT and BDD have different number of ports (TT = %d, BDD = %d)",
+          tt.getNumPort(), bdd.getPorts().size()));
+      return false;
+    }
+
+    int iRow = 0;
+    for (Row ttRow : tt.getRows()) {
+      if (!validate(iRow, ttRow, bdd.getRoot())) {
+        return false;
+      }
+      iRow++;
+    }
+    return true;
+  }
+
+  private boolean validate(int iRow, Row ttRow, AbstractNode tree) {
+    final JastAddList<Assignment> assignments = findAssignments(ttRow, tree);
+    if (assignments.getNumChild() == 0) {
+      System.err.println(String.format("Row %d of TT did not produce any assignments in BDD", iRow));
+    }
+
+    for (Assignment a : assignments) {
+      final String oPortName = a.getPort().getName();
+      final boolean expectedResult = getExpectedResult(ttRow, oPortName);
+      if (expectedResult != a.getValue()) {
+        System.err.println(String.format("Row %s of TT produces unexpected result %s in BDD", ttRow.rowString(), a.getValue()));
+        //return false;
+      }
+    }
+
+    // No mismatches found!
+    return true;
+  }
+
+  private boolean getExpectedResult(Row ttRow, String oPortName) {
+    for (Cell c : ttRow.getCells()) {
+      if (c.getPort() instanceof OutputPort && c.getPort().getName().equals(oPortName)) {
+        return c.getValue();
+      }
+    }
+    throw new NoSuchElementException("Could not find output port " + oPortName + " in the cells of the truth table");
+  }
+
+  private JastAddList<Assignment> findAssignments(Row ttRow, AbstractNode tree) {
+    if (tree instanceof TerminalNode) {
+      TerminalNode leaf = (TerminalNode) tree;
+      return leaf.getAssignmentList();
+    } else if (tree instanceof InnerNode) {
+      InnerNode sb = (InnerNode) tree;
+      InputPort sbInputPort = sb.getPort();
+      for (Cell c : ttRow.getCells()) {
+        // Port must be an input and have the same name
+        if (c.getPort() instanceof InputPort && c.getPort().getName().equals(sbInputPort.getName())) {
+          return findAssignments(ttRow, c.getValue() ? sb.getGraphForOne() : sb.getGraphForZero());
+        }
+      }
+
+      /*
+       * (2019-05-23 Artur Boronat) If the row in the table does not require a
+       * specific value for the port checked in this subtree, try both values.
+       */
+      JastAddList<Assignment> zeroList = findAssignments(ttRow, sb.getGraphForZero());
+      if (zeroList.getNumChild() == 0) {
+        return findAssignments(ttRow, sb.getGraphForOne());
+      } else {
+        return zeroList;
+      }
+    } else if (tree == null) {
+      throw new IllegalArgumentException("Tree must not be null");
+    } else {
+      throw new IllegalArgumentException("Tree must be a subtree or a leaf");
+    }
+  }
+
+}