Improved LTL to English translation (#119)

* I think smoother translation, added engtoltl endpoint

* I think this is better?

Author: sidprasad

requirements.txt

@@ -33,4 +33,4 @@ zipp
 psycopg2-binary
 flask-login
 inflect
-
+wordfreq>=3.0

src/app.py

@@ -1,9 +1,9 @@
-from flask import Flask, render_template, request, Blueprint
-from flask_login import login_required, current_user
-
-
-from ltlnode import parse_ltl_string, SUPPORTED_SYNTAXES
-from codebook import getAllApplicableMisconceptions
+from flask import Flask, render_template, request, Blueprint, jsonify
+from flask_login import login_required, current_user
+
+
+from ltlnode import parse_ltl_string, SUPPORTED_SYNTAXES
+from codebook import getAllApplicableMisconceptions
 import os
 import json
 import sys
@@ -19,6 +19,7 @@
 import uuid
 import requests
 from stepper import traceSatisfactionPerStep
+import ltltoeng
 from authroutes import (
     authroutes,
     init_app,
@@ -170,12 +171,54 @@ def ltl():
     return render_template('ltl.html', uid = getUserName())
 
 @app.route('/loadfromjson')
-def loadfromjson():
-    return render_template('loadfromjson.html', uid = getUserName())
-
-@app.route('/authorquestion/', methods=['POST'])
-@login_required
-def authorquestion():
+def loadfromjson():
+    return render_template('loadfromjson.html', uid = getUserName())
+
+@app.route('/ltltoeng', methods=['GET'])
+def ltl_to_english():
+    """Lightweight endpoint to translate an LTL formula to English for testing."""
+    formula = request.args.get('formula', '').strip()
+    if not formula:
+        return jsonify({"error": "Missing required query parameter 'formula'."}), 400
+    try:
+        node = parse_ltl_string(formula)
+        english = ltltoeng.finalize_sentence(node.__to_english__())
+    except Exception as e:
+        return jsonify({"error": "Failed to translate formula.", "details": str(e)}), 400
+
+    return jsonify({"formula": formula, "english": english})
+
+
+@app.route('/ltltoeng/ui', methods=['GET', 'POST'])
+@login_required
+def ltl_to_english_ui():
+    """Simple HTML interface to translate an LTL formula to English."""
+    translation = None
+    error = None
+    input_formula = ""
+
+    if request.method == 'POST':
+        input_formula = request.form.get('formula', '').strip()
+        if not input_formula:
+            error = "Please enter an LTL formula."
+        else:
+            try:
+                node = parse_ltl_string(input_formula)
+                translation = ltltoeng.finalize_sentence(node.__to_english__())
+            except Exception as e:
+                error = f"Failed to translate formula: {e}"
+
+    return render_template(
+        'ltltoengui.html',
+        uid=getUserName(),
+        translation=translation,
+        error=error,
+        input_formula=input_formula,
+    )
+
+@app.route('/authorquestion/', methods=['POST'])
+@login_required
+def authorquestion():
 
     kind = request.form.get('kind')
     answer = request.form.get('answer')

src/exercisebuilder.py

@@ -436,8 +436,8 @@ def gen_nl_question(self, formula):
 
         formula_eng_corrected = ltltoeng.correct_grammar(formula_eng)
         ### If there are multiple '.' in a row, replace with a single '.'
-        formula_eng_corrected = re.sub(r'\.{2,}', '.', formula_eng)
-        return formula_eng_corrected
+        formula_eng_corrected = re.sub(r'\.{2,}', '.', formula_eng_corrected)
+        return ltltoeng.finalize_sentence(formula_eng_corrected)
 
 
     def get_options_with_misconceptions_as_formula(self, answer):
@@ -695,4 +695,4 @@ def _get_trend_label(self, trend_score):
         elif trend_score < 0.5:
             return "Needs attention"
         else:
-            return "Needs focus"
+            return "Needs focus"

src/ltlnode.py

@@ -217,13 +217,13 @@ class UntilNode(BinaryOperatorNode):
     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__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-        return ltltoeng.capitalize_sentence(f"{lhs} until {rhs}")
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+        return f"{lhs} until {rhs}"
 
     def __forge__(self):
         return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})"
@@ -237,12 +237,12 @@ class NextNode(UnaryOperatorNode):
     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__().rstrip('.')
-        return ltltoeng.capitalize_sentence(f"in the next step, {op}")
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        op = self.operand.__to_english__().rstrip('.')
+        return f"in the next step, {op}"
 
     def __forge__(self):
         return f"(NEXT_STATE {self.operand.__forge__()})"
@@ -256,20 +256,20 @@ class GloballyNode(UnaryOperatorNode):
     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__().rstrip('.')
-        patterns = [
-            f"it is always the case that {op}",
-            f"at all times, {op}",
-            f"{op} is always true"
-        ]
-
-        english = random.choice(patterns)
-        return ltltoeng.capitalize_sentence(english)
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+
+        op = self.operand.__to_english__().rstrip('.')
+        patterns = [
+            f"it is always the case that {op}",
+            f"at all times, {op}",
+            f"{op} is always true"
+        ]
+
+        english = ltltoeng.choose_best_sentence(patterns)
+        return english
 
     def __forge__(self):
         return f"(ALWAYS {self.operand.__forge__()})"
@@ -287,10 +287,10 @@ def __to_english__(self):
         x = ltltoeng.apply_special_pattern_if_possible(self)
         if x is not None:
             return x
-        op = self.operand.__to_english__().rstrip('.')
-
-        english = f"eventually, {op}"
-        return ltltoeng.capitalize_sentence(english)
+        op = self.operand.__to_english__().rstrip('.')
+
+        english = f"eventually, {op}"
+        return english
 
     def __forge__(self):
         return f"(EVENTUALLY {self.operand.__forge__()})"
@@ -306,13 +306,13 @@ class OrNode(BinaryOperatorNode):
     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__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-        return ltltoeng.capitalize_sentence(f"either {lhs} or {rhs}")
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+        return f"either {lhs} or {rhs}"
 
 
 
@@ -322,13 +322,13 @@ class AndNode(BinaryOperatorNode):
     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__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-        return ltltoeng.capitalize_sentence(f"both {lhs} and {rhs}")
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+        return f"both {lhs} and {rhs}"
 
 
 class NotNode(UnaryOperatorNode):
@@ -338,64 +338,70 @@ def __init__(self, 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__().rstrip('.')
-
-        ## If the operand is a literal, we can just negate it
-        if isinstance(self.operand, LiteralNode):
-            return ltltoeng.capitalize_sentence(f"not {op}")
-        else:
-            return ltltoeng.capitalize_sentence(f"it is not the case that {op}")
+        if x is not None:
+            return x
+
+        op = self.operand.__to_english__().rstrip('.')
+
+        ## If the operand is a literal, we can just negate it
+        if isinstance(self.operand, LiteralNode):
+            return f"not {op}"
+        else:
+            return f"it is not the case that {op}"
 
 class ImpliesNode(BinaryOperatorNode):
     symbol = IMPLIES_SYMBOL
     def __init__(self, left, right):
         super().__init__(ImpliesNode.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__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-
-        # Potential patterns:
-        patterns = [
-            f"if {lhs}, then {rhs}",
-            f"{lhs} implies {rhs}",
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+            
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+
+        lhs = ltltoeng.normalize_embedded_clause(lhs)
+        rhs = ltltoeng.normalize_embedded_clause(rhs)
+
+        # Potential patterns:
+        patterns = [
+            f"if {lhs}, then {rhs}",
+            f"{lhs} implies {rhs}",
             f"whenever {lhs}, then {rhs}"
-        ]
-
-        # Choose a pattern randomly, and then return the corrected sentence
-        english = random.choice(patterns)
-        return ltltoeng.capitalize_sentence(english)
+        ]
+
+        # Choose the most fluent pattern rather than picking randomly
+        english = ltltoeng.choose_best_sentence(patterns)
+        return english
 
 
 class EquivalenceNode(BinaryOperatorNode):
     symbol = EQUIVALENCE_SYMBOL
     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__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-
-        # Potential patterns:
-        patterns = [
-            f"{lhs} if and only if {rhs}",
-            f"{lhs} exactly when {rhs}",
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+
+        lhs = ltltoeng.normalize_embedded_clause(lhs)
+        rhs = ltltoeng.normalize_embedded_clause(rhs)
+
+        # Potential patterns:
+        patterns = [
+            f"{lhs} if and only if {rhs}",
+            f"{lhs} exactly when {rhs}",
             f"{lhs} is equivalent to {rhs}"
-        ]
-
-        # Choose a pattern randomly, and then return the corrected sentence
-        english = random.choice(patterns)
-        return ltltoeng.capitalize_sentence(english)
+        ]
+
+        # Choose the most fluent pattern rather than picking randomly
+        english = ltltoeng.choose_best_sentence(patterns)
+        return english