Bug fix in learner; shallower copy of truth tables to circumvent dese…

…rialization issue for some SMT formulas
rindPHI · Aug 30, 2022 · 82ea310 · 82ea310
1 parent ba517e9
commit 82ea310
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 28 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -19,6 +19,7 @@ RUN pip install --upgrade pip wheel
 
 RUN git clone https://github.com/rindPHI/islearn.git
 WORKDIR /home/islearn/islearn
+RUN git pull
 RUN git checkout v0.2.12
 RUN pip install -e .[dev,test]
 RUN pip install isla-solver==0.10.5

diff --git a/src/islearn/learner.py b/src/islearn/learner.py
@@ -54,6 +54,9 @@ def __init__(
         self.inputs = list(inputs)
         self.eval_results: List[bool] = list(eval_results)
 
+    def __copy__(self):
+        return TruthTableRow(self.formula, self.inputs, self.eval_results)
+
     def evaluate(
             self,
             graph: gg.GrammarGraph,
@@ -153,6 +156,9 @@ def __init__(self, rows: Iterable[TruthTableRow] = ()):
                 self.__row_hashes.add(row_hash)
                 self.__rows.append(row)
 
+    def __deepcopy__(self, memodict=None):
+        return TruthTable([copy.copy(row) for row in self.__rows])
+
     def __repr__(self):
         return f"TruthTable({repr(self.__rows)})"
 

diff --git a/tests/test_learner.py b/tests/test_learner.py
@@ -1019,34 +1019,34 @@ def test_ip_icmp_ping_request(self):
         self.assertIn(icmp_code_constraint, result.keys())
         self.assertIn(length_constraint, result.keys())
 
-    @pytest.mark.flaky(reruns=3, reruns_delay=2)
+    # @pytest.mark.flaky(reruns=3, reruns_delay=2)
     def test_learn_graphviz(self):
-        # urls = [
-        #     "https://raw.githubusercontent.com/ecliptik/qmk_firmware-germ/56ea98a6e5451e102d943a539a6920eb9cba1919/users/dennytom/chording_engine/state_machine.dot",
-        #     "https://raw.githubusercontent.com/Ranjith32/linux-socfpga/30f69d2abfa285ad9138d24d55b82bf4838f56c7/Documentation/blockdev/drbd/disk-states-8.dot",
-        #     # Below one is graph, not digraph
-        #     "https://raw.githubusercontent.com/nathanaelle/wireguard-topology/f0e42d240624ca0aa801d890c1a4d03d5901dbab/examples/3-networks/topology.dot"
-        # ]
-        #
-        # positive_trees = []
-        # for url in urls:
-        #     with urllib.request.urlopen(url) as f:
-        #         dot_code = (re.sub(r"(^|\n)\s*//.*?(\n|$)", "", f.read().decode('utf-8'))
-        #                     .replace("\\n", "\n")
-        #                     .replace("\r\n", "\n")
-        #                     .strip())
-        #     positive_trees.append(
-        #         language.DerivationTree.from_parse_tree(list(PEGParser(DOT_GRAMMAR).parse(dot_code))[0]))
-
-        positive_inputs = [
-            "digraph { a -> b }",
-            "graph gg { c -- x }",
-            "graph { a; y; a -- y }",
-            "digraph { a; b; c; d; c -> d; a -> c; }",
+        urls = [
+            "https://raw.githubusercontent.com/ecliptik/qmk_firmware-germ/56ea98a6e5451e102d943a539a6920eb9cba1919/users/dennytom/chording_engine/state_machine.dot",
+            "https://raw.githubusercontent.com/Ranjith32/linux-socfpga/30f69d2abfa285ad9138d24d55b82bf4838f56c7/Documentation/blockdev/drbd/disk-states-8.dot",
+            # Below one is graph, not digraph
+            "https://raw.githubusercontent.com/nathanaelle/wireguard-topology/f0e42d240624ca0aa801d890c1a4d03d5901dbab/examples/3-networks/topology.dot"
         ]
-        positive_trees = [
-            language.DerivationTree.from_parse_tree(list(PEGParser(DOT_GRAMMAR).parse(inp))[0])
-            for inp in positive_inputs]
+
+        positive_trees = []
+        for url in urls:
+            with urllib.request.urlopen(url) as f:
+                dot_code = (re.sub(r"(^|\n)\s*//.*?(\n|$)", "", f.read().decode('utf-8'))
+                            .replace("\\n", "\n")
+                            .replace("\r\n", "\n")
+                            .strip())
+            positive_trees.append(
+                language.DerivationTree.from_parse_tree(list(PEGParser(DOT_GRAMMAR).parse(dot_code))[0]))
+
+        # positive_inputs = [
+        #     "digraph { a -> b }",
+        #     "graph gg { c -- x }",
+        #     "graph { a; y; a -- y }",
+        #     "digraph { a; b; c; d; c -> d; a -> c; }",
+        # ]
+        # positive_trees = [
+        #     language.DerivationTree.from_parse_tree(list(PEGParser(DOT_GRAMMAR).parse(inp))[0])
+        #     for inp in positive_inputs]
 
         negative_inputs = [
             "digraph { a -- b }",
@@ -1085,7 +1085,6 @@ def prop(tree: language.DerivationTree) -> bool:
 
         # TODO: There's a hidden balance property, e.g., in labels:
         #       For each opening < in a String there has to be a closing >.
-        #       See (commented) 2nd URL.
 
         result = InvariantLearner(
             DOT_GRAMMAR,
@@ -1101,7 +1100,7 @@ def prop(tree: language.DerivationTree) -> bool:
             filter_inputs_for_learning_by_kpaths=False,
             max_conjunction_size=2,
             min_recall=1,
-            min_specificity=1,
+            min_specificity=.9,
             # reduce_all_inputs=True,
             reduce_inputs_for_learning=True,
             generate_new_learning_samples=False,