add ability to convert from SAT result to LTL formula

ltl_learner/__main__.py

@@ -1,9 +1,17 @@
 import argparse
+import logging
+import sys
 import time
 from pathlib import Path
 
 from ltl_learner.learner import Learner
 
+root = logging.getLogger()
+root.setLevel(logging.INFO)
+handler = logging.StreamHandler(sys.stdout)
+handler.setLevel(logging.INFO)
+root.addHandler(handler)
+
 
 def positive_integer(n: int):
     n = int(n)

ltl_learner/constants.py

@@ -1,11 +1,11 @@
-_operators = {'!', 'X', '|', '&', '>', 'U'}
-_binary = {'|', '&', '>', 'U'}
+# _operators = {'!', 'X', '|', '&', '>', 'U'}
+# _binary = {'|', '&', '>', 'U'}
 
 # _operators = {'!', 'X', '|', '&', '>'}
 # _binary = {'|', '&', '>'}
 
-# _operators = {'U', 'X', '|', '!', '&', 'G', 'F', '>'}
-# _binary = {'U', '|', '&', '>'}
+_operators = {'U', 'X', '|', '!', '&', 'G', 'F', '>'}
+_binary = {'U', '|', '&', '>'}
 _unary = _operators - _binary
 
 operators = {

ltl_learner/learner.py

@@ -1,5 +1,5 @@
 import json
-import os
+import logging
 from copy import deepcopy
 from datetime import datetime
 from pathlib import Path
@@ -11,6 +11,8 @@
 from ltl_learner.ltl.converter import LTLConverter
 from ltl_learner.traces import Sample
 
+logger = logging.getLogger(__name__)
+
 
 class Learner:
     def __init__(self, k: int = 10, sample: Path = None, syntax = None):
@@ -41,6 +43,8 @@ def is_sat(self):
         return self.solver.model()
 
     def write_model(self):
+        logger.info('Writing z3 model expression tree.')
+        logger.info(f'  Using file {self.output_file}')
         with open(self.output_file, 'w') as f:
             f.write(f';; Run {self.file_name}\n')
             f.write(f';; Parameters\n')
@@ -50,17 +54,22 @@ def write_model(self):
             f.write(self.solver.sexpr())
 
     def main(self):
-        n = 0
+        logger.info('Starting to compute an LTL formula.')
+        n = 1
+        logger.info(f'Computing DAG of length {n}')
+        self.builder.build(n, self.positive, self.negative)
         while True:
-            n += 1
             if self.is_sat() or n > self.cutoff:
                 break
             self.solver.reset()
+            n += 1
+            logger.info(f"Computing DAG of length {n}")
             self.builder.build(n, self.positive, self.negative)
         if n <= self.cutoff:
-            print("Found a valid truth assignation. Registering in results.")
+            logger.info("Found a valid truth assignation.")
             self.write_model()
-            return self.converter.build()
+            logger.info('Now computing the matching LTL formula.')
+            return self.converter.build(length = n)
         else:
-            print("Unable to determine a formula within the given constraint.")
+            logger.info("Unable to determine a formula within the given constraint.")
             return self.solver

ltl_learner/ltl/converter.py

@@ -1,14 +1,69 @@
+import logging
+
 from z3 import And, Solver, is_true
 
+from ltl_learner.constants import operators
+
+logger = logging.getLogger(__name__)
+
+
+class Node:
+    def __init__(self, id, label, left = None, right = None):
+        self.label = label
+        self.left = left
+        self.right = right
+        self.id = id
+
+    def __str__(self):
+        acc = f'{self.label}'
+        if self.label in operators['all']:
+            acc += '('
+            if self.left:
+                acc += f'{self.left}'
+            if self.right:
+                acc += f',{self.right}'
+            acc += ')'
+        return acc
+
+class Tree:
+    def __init__(self):
+        self.root = None
+
+    def add_node(self, node):
+        self.nodes.append(node)
+
+    def get_formula(self):
+        return str(self.root)
+
 
 class LTLConverter:
     def __init__(self, solver: Solver):
         self.solver = solver
 
-    def build(self):
-        psi = self.solver.model()
-        true_vars = {x.name(): x for x in psi.decls() if is_true(psi[x])}
-        dag = [x for x in true_vars.keys() if x.startswith('x_') or x.startswith('l_') or x.startswith('r_')]
-        ys = [y for y in true_vars.keys() if y.startswith('y_')]
-        print(dag)
-        print(ys)
+    def build(self, length: int, true_nodes = None):
+        if not true_nodes:
+            psi = self.solver.model()
+            true_vars = {x.name(): x for x in psi.decls() if is_true(psi[x])}
+            dag = [x for x in true_vars.keys() if x.startswith('x_') or x.startswith('l_') or x.startswith('r_')]
+            logger.info(f"Variables set to true:  {dag}")
+            true_nodes = list(sorted(dag, key = lambda n: n.split('_')[1]))
+        tree = Tree()
+        nodes = {}
+        for i in range(length):
+            label = [n for n in true_nodes if n.startswith(f'x_{i}_')][0].split('_')[-1]
+            nodes[i] = Node(i, label)
+        for i in range(length):
+            left = [n for n in true_nodes if n.startswith(f'l_{i}_')]
+            if left:
+                left = int(left[0].split('_')[-1])
+                nodes[i].left = nodes[left]
+            right = [n for n in true_nodes if n.startswith(f'r_{i}_')]
+            if right:
+                right = int(right[0].split('_')[-1])
+                nodes[i].right = nodes[right]
+        tree.root = nodes[length - 1]
+        logger.info('Computed tree from SAT assignation.')
+        logger.info(f'  {tree}')
+        logger.info('LTL Formula:')
+        logger.info(f'  {tree.get_formula()}')
+        return tree.get_formula()

tests/fixtures/results.py

@@ -0,0 +1,30 @@
+import pytest
+from z3 import Solver
+
+from ltl_learner.ltl.converter import LTLConverter
+
+
+@pytest.fixture
+def converter():
+    return LTLConverter(Solver())
+
+
+@pytest.fixture
+def result_length_7():
+    return [
+        'x_6_U',
+        'l_6_4',
+        'x_4_!',
+        'l_4_3',
+        'x_3_F',
+        'l_3_2',
+        'x_2_&',
+        'l_2_1',
+        'x_1_crit2',
+        'r_2_0',
+        'x_0_crit1',
+        'r_6_5',
+        'x_5_|',
+        'l_5_1',
+        'r_5_0',
+    ]

tests/test_converter.py

@@ -0,0 +1,5 @@
+from tests.fixtures.results import result_length_7, converter
+
+def test_tree_str(result_length_7, converter):
+    tree = converter.build(length = 7, true_nodes = result_length_7)
+    assert tree == 'U(!(F(&(crit2,crit1))),|(crit2,crit1))'