Make LTL suggestion button functional and prominent

src/app.py

@@ -65,10 +65,11 @@ def enforce_https_in_production():
 answer_logger = Logger()
 PROJECT_ROOT = os.path.abspath(os.path.join(os.path.dirname(__file__), os.pardir))
 
-BENCHMARK_FILES = {
-    "near": os.path.join(PROJECT_ROOT, "semantic_benchmark_near_eng.csv"),
-    "far": os.path.join(PROJECT_ROOT, "semantic_benchmark_far_eng.csv"),
-}
+BENCHMARK_FILES = {
+    "near": os.path.join(PROJECT_ROOT, "semantic_benchmark_near_eng.csv"),
+    "far": os.path.join(PROJECT_ROOT, "semantic_benchmark_far_eng.csv"),
+}
+SUGGESTED_FORMULAS_PATH = os.path.join(os.path.dirname(__file__), "static", "ltl_formula_suggestions.json")
 
 
 def _load_benchmark_rows():
@@ -99,7 +100,30 @@ def _load_benchmark_rows():
     return data
 
 
-BENCHMARK_ROWS = _load_benchmark_rows()
+BENCHMARK_ROWS = _load_benchmark_rows()
+
+
+def _load_suggested_formulas():
+    if not os.path.exists(SUGGESTED_FORMULAS_PATH):
+        return []
+
+    try:
+        with open(SUGGESTED_FORMULAS_PATH, "r", encoding="utf-8") as handle:
+            data = json.load(handle)
+        return [
+            {
+                "formula": entry.get("formula", ""),
+                "description": entry.get("description", ""),
+                "source": entry.get("source", ""),
+            }
+            for entry in data
+            if entry.get("formula")
+        ]
+    except (json.JSONDecodeError, OSError):
+        return []
+
+
+SUGGESTED_FORMULAS = _load_suggested_formulas()
 
 
 def _highlight_differences(text_a, text_b):
@@ -380,9 +404,9 @@ def ltltoeng_rating():
 
 @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
+def ltl_to_english_ui():
+    """Simple HTML interface to translate an LTL formula to English."""
+    translation = None
     error = None
     input_formula = ""
 
@@ -400,10 +424,30 @@ def ltl_to_english_ui():
     return render_template(
         'ltltoengui.html',
         uid=getUserName(),
-        translation=translation,
-        error=error,
-        input_formula=input_formula,
-    )
+        translation=translation,
+        error=error,
+        input_formula=input_formula,
+    )
+
+
+@app.route('/ltltoeng/suggestion', methods=['GET'])
+@login_required
+def ltl_suggestion():
+    if not SUGGESTED_FORMULAS:
+        return jsonify({"error": "No suggestions available."}), 503
+
+    user_id = getUserName()
+    rated_formulas = answer_logger.getRatedEnglishFormulas(user_id)
+    available_suggestions = [
+        s for s in SUGGESTED_FORMULAS
+        if s.get("formula") and s.get("formula") not in rated_formulas
+    ]
+
+    if not available_suggestions:
+        return jsonify({"error": "No new suggestions available."}), 404
+
+    suggestion = random.choice(available_suggestions)
+    return jsonify(suggestion)
 
 @app.route('/authorquestion/', methods=['POST'])
 @login_required

src/logger.py

@@ -114,11 +114,22 @@ def __init__(self):
         if SENTENCE_PAIR_RATING_TABLE not in self.inspector.get_table_names():
             Base.metadata.tables[SENTENCE_PAIR_RATING_TABLE].create(self.engine)
 
-    def record(self, log):
-        with self.Session() as session:
-            print("Recording log")
-            session.add(log)
-            session.commit()
+    def record(self, log):
+        with self.Session() as session:
+            print("Recording log")
+            session.add(log)
+            session.commit()
+
+    def getRatedEnglishFormulas(self, user_id):
+        """Return a set of LTL formulas this user has already rated."""
+        if not isinstance(user_id, str):
+            raise ValueError("user_id should be a string")
+
+        with self.Session() as session:
+            rows = session.query(EnglishLTLRating.ltl).filter(
+                EnglishLTLRating.user_id == user_id
+            ).all()
+            return {row.ltl for row in rows if row.ltl}
 
 
     def logStudentResponse(self, userId, misconceptions, question_text, question_options, correct_answer, questiontype, mp_class, exercise, course):

src/static/css/common.css

@@ -67,4 +67,28 @@
     position: absolute;
     top: 0;
     right: 0; /* Align to the right side of the container */
+}
+
+.suggestion-btn {
+    background: linear-gradient(120deg, #1b7fbd, #0fb08a);
+    color: #fff;
+    border: none;
+    padding-left: 1rem;
+    padding-right: 1rem;
+    letter-spacing: 0.01em;
+    transition: transform 0.12s ease-in-out, box-shadow 0.12s ease-in-out;
+}
+
+.suggestion-btn:hover,
+.suggestion-btn:focus {
+    color: #fff;
+    transform: translateY(-1px);
+    box-shadow: 0 0.5rem 1rem rgba(0, 0, 0, 0.15);
+}
+
+.suggestion-btn:disabled {
+    background: #9bbccd;
+    color: #f8f9fa;
+    transform: none;
+    box-shadow: none;
 }

src/static/ltl_formula_suggestions.json

@@ -0,0 +1,42 @@
+[
+  {
+    "formula": "G(p -> F q)",
+    "description": "Response pattern: whenever p holds, q eventually follows",
+    "source": "Dwyer patterns"
+  },
+  {
+    "formula": "G((p) -> X(q))",
+    "description": "Immediate response pattern: if p is true then q must hold in the next state",
+    "source": "Dwyer patterns"
+  },
+  {
+    "formula": "F G p",
+    "description": "Stability: p will eventually hold forever",
+    "source": "VLTL Bench"
+  },
+  {
+    "formula": "G F p",
+    "description": "Recurrence: p happens infinitely often",
+    "source": "VLTL Bench"
+  },
+  {
+    "formula": "G(a -> F(b & X c))",
+    "description": "If a occurs, eventually b occurs and is immediately followed by c",
+    "source": "Dwyer patterns"
+  },
+  {
+    "formula": "G((req) -> (F grant & (!grant) U grant))",
+    "description": "A request must eventually be granted and grant stays false until then",
+    "source": "VLTL Bench"
+  },
+  {
+    "formula": "G(!(critical1 & critical2))",
+    "description": "Mutual exclusion between two critical sections",
+    "source": "VLTL Bench"
+  },
+  {
+    "formula": "G(trigger -> (trigger U response))",
+    "description": "Response within until: response eventually follows trigger and holds until then",
+    "source": "Dwyer patterns"
+  }
+]

src/templates/ltltoengui.html

@@ -18,8 +18,12 @@ <h5 class="mb-0">LTL to English Translator</h5>
             <div class="card-body">
                 <form method="POST" action="{{ url_for('ltl_to_english_ui') }}">
                     <div class="form-group">
-                        <label for="formula">Enter an LTL formula</label>
-                        <textarea class="form-control" id="formula" name="formula" rows="3" placeholder="e.g., G(p -> F q)">{{ input_formula }}</textarea>
+                        <div class="d-flex justify-content-between align-items-center">
+                            <label for="formula" class="mb-0">Enter an LTL formula</label>
+                            <button type="button" class="btn btn-sm font-weight-bold shadow suggestion-btn" id="suggest-ltl-btn">Suggested a Formula</button>
+                        </div>
+                        <div id="ltl-suggestion-status" class="small text-muted mt-1" hidden></div>
+                        <textarea class="form-control mt-2" id="formula" name="formula" rows="3" placeholder="e.g., G(p -> F q)">{{ input_formula }}</textarea>
                     </div>
                     <button type="submit" class="btn btn-primary">Translate</button>
                 </form>
@@ -95,10 +99,6 @@ <h6 class="card-title mb-2">Was this translation clear?</h6>
     <script>
         document.addEventListener('DOMContentLoaded', function () {
             const form = document.getElementById('ltl-to-eng-feedback-form');
-            if (!form) {
-                return;
-            }
-
             const unnaturalCheckbox = document.getElementById('issue-unnatural');
             const unnaturalText = document.getElementById('issue-unnatural-text');
             const otherCheckbox = document.getElementById('issue-other');
@@ -111,6 +111,10 @@ <h6 class="card-title mb-2">Was this translation clear?</h6>
             const copyBtn = document.getElementById('copy-translation-btn');
             const translationText = document.getElementById('ltl-translation-text');
             const copyStatus = document.getElementById('copy-translation-status');
+            const suggestBtn = document.getElementById('suggest-ltl-btn');
+            const suggestionStatus = document.getElementById('ltl-suggestion-status');
+            const formulaInput = document.getElementById('formula');
+            const suggestBtnDefaultLabel = suggestBtn ? suggestBtn.innerHTML : '';
 
             function toggleTarget(checkbox, target) {
                 if (!checkbox || !target) return;
@@ -133,23 +137,29 @@ <h6 class="card-title mb-2">Was this translation clear?</h6>
             }
 
             async function submitFeedback() {
+                if (!form) {
+                    return;
+                }
+
                 if (statusEl) {
                     statusEl.textContent = '';
                     statusEl.classList.remove('text-success', 'text-danger');
                 }
 
-                const selectedIssues = Array.from(form.querySelectorAll('input[name="issues"]:checked'))
-                    .map(input => {
-                        if (input.value === 'Unnatural word') {
-                            const detail = ((unnaturalText && unnaturalText.value) ? unnaturalText.value : '').trim();
-                            return detail ? `${input.value}: ${detail}` : input.value;
-                        }
-                        if (input.value === 'Other') {
-                            const detail = ((otherText && otherText.value) ? otherText.value : '').trim();
-                            return detail ? `${input.value}: ${detail}` : input.value;
-                        }
-                        return input.value;
-                    });
+                const selectedIssues = form
+                    ? Array.from(form.querySelectorAll('input[name="issues"]:checked'))
+                        .map(input => {
+                            if (input.value === 'Unnatural word') {
+                                const detail = ((unnaturalText && unnaturalText.value) ? unnaturalText.value : '').trim();
+                                return detail ? `${input.value}: ${detail}` : input.value;
+                            }
+                            if (input.value === 'Other') {
+                                const detail = ((otherText && otherText.value) ? otherText.value : '').trim();
+                                return detail ? `${input.value}: ${detail}` : input.value;
+                            }
+                            return input.value;
+                        })
+                    : [];
 
                 const suggestedTranslation = suggestionInput ? (suggestionInput.value || '').trim() : '';
 
@@ -236,6 +246,54 @@ <h6 class="card-title mb-2">Was this translation clear?</h6>
             if (copyBtn) {
                 copyBtn.addEventListener('click', copyTranslation);
             }
+
+            async function requestSuggestion() {
+                if (suggestBtn) {
+                    suggestBtn.disabled = true;
+                    suggestBtn.innerText = 'Loading suggestion...';
+                }
+                if (suggestionStatus) {
+                    suggestionStatus.textContent = 'Fetching a suggested formula...';
+                    suggestionStatus.classList.remove('text-danger');
+                    suggestionStatus.classList.add('text-muted');
+                }
+
+                try {
+                    const response = await fetch('/ltltoeng/suggestion');
+                    const suggestion = await response.json();
+
+                    if (!response.ok) {
+                        const message = suggestion.error || 'Could not load a suggestion right now.';
+                        throw new Error(message);
+                    }
+                    if (formulaInput) {
+                        formulaInput.value = suggestion.formula || '';
+                    }
+                    if (suggestionStatus) {
+                        const detail = suggestion.formula || '';
+                        suggestionStatus.textContent = detail
+                            ? `Suggested formula: ${detail}`
+                            : 'Suggested formula ready to use.';
+                        suggestionStatus.classList.remove('text-muted');
+                    }
+                } catch (error) {
+                    console.error('Error fetching suggestion:', error);
+                    if (suggestionStatus) {
+                        suggestionStatus.textContent = error.message || 'Could not load a suggestion right now.';
+                        suggestionStatus.classList.add('text-danger');
+                        suggestionStatus.classList.remove('text-muted');
+                    }
+                } finally {
+                    if (suggestBtn) {
+                        suggestBtn.disabled = false;
+                        suggestBtn.innerHTML = suggestBtnDefaultLabel;
+                    }
+                }
+            }
+
+            if (suggestBtn) {
+                suggestBtn.addEventListener('click', requestSuggestion);
+            }
         });
     </script>
     <script src="https://code.jquery.com/jquery-3.5.1.slim.min.js"></script>

src/templates/version.html

@@ -1 +1 @@
-1.9.2
+1.9.3