Improving LTL to English translation

src/exercisebuilder.py

@@ -20,6 +20,8 @@ class ExerciseBuilder:
 
     def __init__(self, userLogs, complexity=5):
         self.userLogs = userLogs
+        self.numUserLogs = len(userLogs)
+
         self.DEFAULT_WEIGHT = 0.7
         self.ltl_priorities = spotutils.DEFAULT_LTL_PRIORITIES.copy()
 
@@ -163,8 +165,10 @@ def contains_undersirable_lit(s):
             TAUTOLOGY = r'\b1\b'
             UNSAT = r'\b0\b'
             # remove all the parens
-            y = s.replace('(', '').replace(')', '')
-            return bool(re.search(TAUTOLOGY, y)) or bool(re.search(UNSAT, y))
+            y = s.replace('(', ' ').replace(')', ' ').replace("'", ' ')
+            x = bool(re.search(TAUTOLOGY, y)) or bool(re.search(UNSAT, y))
+
+            return x
 
 
         self.set_ltl_priorities()
@@ -200,14 +204,54 @@ def contains_undersirable_lit(s):
             if question is not None:
                 questions.append(question)
 
-        ## Make sure we have enough questions
-        chosen_questions = random.sample(questions, min(num_questions, len(questions)))
-        return chosen_questions
+        def formula_choice_metric(question):
+
+            formula = question['question']
+            if question['type'] == self.ENGLISHTOLTL:
+                formula = question['answer']
+
+            temporal_op_count = formula.count('G') + formula.count('X') + formula.count('U') + formula.count('F')
+            aut_size = spotutils.get_aut_size(formula)
+
+
+            scaled_aut_size = aut_size * math.log(self.numUserLogs + 1)
+            return temporal_op_count + scaled_aut_size
+
+        chosen_questions = sorted(questions, key=formula_choice_metric, reverse=True)[:num_questions]
+
+
+        # Now choose the question with the highest metric, that is of each type from the chosen_questions
+
+        highest_ltl_to_eng = next((q for q in chosen_questions if q['type'] == self.ENGLISHTOLTL), None)
+        highest_trace_sat_mc = next((q for q in chosen_questions if q['type'] == self.TRACESATMC), None)
+        highest_trace_sat_yn = next((q for q in chosen_questions if q['type'] == self.TRACESATYN), None)
+
+
+        final_choices = []
+        if highest_ltl_to_eng is not None:
+            final_choices.append(highest_ltl_to_eng)
+        if highest_trace_sat_mc is not None:
+            final_choices.append(highest_trace_sat_mc)
+        if highest_trace_sat_yn is not None:
+            final_choices.append(highest_trace_sat_yn)
+
+        remaining = num_questions - len(final_choices)
+        if remaining > 0:
+            # Add the remaining questions from chosen_questions, but dont add the ones already added
+            for q in chosen_questions:
+                if q not in final_choices:
+                    final_choices.append(q)
+                    remaining -= 1
+                if remaining <= 0:
+                    break
+        return remaining
+
 
     def gen_nl_question(self, formula):
 
         formula_eng = ltlnode.parse_ltl_string(formula).__to_english__()
-        #print("Generating NL question for " + formula + " and got " + str(formula_eng))
+        if formula_eng is None or formula_eng == "":
+            return None
 
         ### If there are multiple '.' in a row, replace with a single '.'
         formula_eng = re.sub(r'\.{2,}', '.', formula_eng)
@@ -251,8 +295,14 @@ def build_english_to_ltl_question(self, answer):
         if options is None:
             return None
 
+        question = self.gen_nl_question(answer)
+
+        if question is None or question == "":
+            print("Question generation failed unexpectedly.")
+            return None
+
         return {
-            "question": self.gen_nl_question(answer),
+            "question": question,
             "type": self.ENGLISHTOLTL,
             "options": options
         }

src/ltlnode.py

@@ -7,6 +7,8 @@
 from ltlParser import ltlParser
 from abc import ABC, abstractmethod
 from spotutils import areEquivalent
+import random
+import ltltoeng
 
 ## We use this for Grammatical englsih generation
 import spacy
@@ -37,6 +39,11 @@ def __str__(self):
 
     @abstractmethod
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        # We should draw inspiration from:
+        # https://matthewbdwyer.github.io/psp/patterns/ltl.html
         pass
 
     @staticmethod
@@ -134,6 +141,9 @@ def __str__(self):
         return f'({self.operator} {str(self.operand)})'
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         return self.__str__()
 
 
@@ -148,6 +158,9 @@ def __str__(self):
         return f'({str(self.left)} {self.operator} {str(self.right)})'
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         return self.__str__()
 
 
@@ -160,6 +173,12 @@ def __str__(self):
         return self.value
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+
+        ### TODO: COuld we override so that this is more meaningful
+        # for some cases?
         return f"'{self.value}' holds"
 
 
@@ -169,6 +188,9 @@ def __init__(self, left, right):
         super().__init__(UntilNode.symbol, left, right)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         lhs = self.left.__to_english__()
         rhs = self.right.__to_english__()
         english = f"{lhs} until {rhs}."
@@ -181,6 +203,9 @@ def __init__(self, operand):
         super().__init__(NextNode.symbol, operand)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         op = self.operand.__to_english__()
         english = f"in the next state, {op}."
         return self.corrected_sentence(english)
@@ -192,8 +217,19 @@ def __init__(self, operand):
         super().__init__(GloballyNode.symbol, operand)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+
+
         op = self.operand.__to_english__()
-        english = f"from this point on, {op}."
+        patterns = [
+            f"it is always the case that {op}",
+            f"in all future states, {op}",
+            f"globally, {op}"
+        ]
+
+        english = random.choice(patterns)
         return self.corrected_sentence(english)
 
 
@@ -203,8 +239,19 @@ def __init__(self, operand):
         super().__init__(FinallyNode.symbol, operand)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         op = self.operand.__to_english__()
-        english = f"eventually, {op}."
+
+        patterns = [
+            f"eventually, {op}",
+            f"now or in the future, {op}",
+            f"at this or some future point, {op}"
+        ]
+
+
+        english = f"eventually, {op}"
         return self.corrected_sentence(english)
 
 
@@ -216,6 +263,9 @@ def __init__(self, left, right):
         super().__init__(OrNode.symbol, left, right)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         lhs = self.left.__to_english__()
         rhs = self.right.__to_english__()
         english = f"{lhs} or {rhs}."
@@ -228,6 +278,9 @@ def __init__(self, left, right):
         super().__init__(AndNode.symbol, left, right)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         lhs = self.left.__to_english__()
         rhs = self.right.__to_english__()
         english = f"{lhs} and {rhs}."
@@ -240,8 +293,21 @@ def __init__(self, operand):
         super().__init__(NotNode.symbol, operand)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+
         op = self.operand.__to_english__()
-        english = f"it is not the case that {op}."
+
+        ## If the operand is a literal, we can just negate it
+        if isinstance(self.operand, LiteralNode):
+            english = f"{op}"
+            # Replace 'holds' with does not hold in english.
+            if "holds" in english:
+                english = english.replace("holds", "does not hold")
+        ## TODO: We can start donig some more. better special cases.
+        else:
+            english = f"it is not the case that {op}."
         return self.corrected_sentence(english)
 
 class ImpliesNode(BinaryOperatorNode):
@@ -252,7 +318,15 @@ def __init__(self, left, right):
     def __to_english__(self,depth=0):
         lhs = self.left.__to_english__()
         rhs = self.right.__to_english__()
-        english = f"if {lhs} then {rhs}."
+
+        # Potential patterns:
+        patterns = [
+            f"if {lhs}, then {rhs}",
+            f"{rhs} is necessary for {lhs}"
+        ]
+
+        # Choose a pattern randomly, and then return the corrected sentence
+        english = random.choice(patterns)
         return self.corrected_sentence(english)
 
 
@@ -262,9 +336,22 @@ def __init__(self, left, right):
         super().__init__(EquivalenceNode.symbol, left, right)
 
     def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
         lhs = self.left.__to_english__()
         rhs = self.right.__to_english__()
-        english = f"{lhs} if and only if {rhs}."
+
+        # Potential patterns:
+        patterns = [
+            f"{lhs} is necessary and sufficient for {rhs}",
+            f"{lhs} exactly when {rhs}",
+            f"{lhs} is equivalent to {rhs}",
+            f"{lhs} if and only if {rhs}"
+        ]
+
+        # Choose a pattern randomly, and then return the corrected sentence
+        english = random.choice(patterns)
         return self.corrected_sentence(english)