Add instructor trace-builder endpoint and UI preview

CHANGELOG.md

@@ -2,6 +2,11 @@
 
 This document summarizes notable updates since February 2025, with commit dates from the repository history for context.【728428†L1-L48】
 
+
+## 2026-03
+- Added an instructor-only trace builder endpoint (`/instructor/trace-tool`) and UI controls in the exercise builder to normalize shorthand traces (e.g., `{...}` to `cycle{...}`), preview expanded traces, and render a mermaid graph before saving questions.
+- Added normalization tests for trace shorthand parsing used by the instructor trace builder workflow.
+
 ## 2025-11
 - Improved LTL-to-English translations with grammar smoothing and capitalization applied to pattern-based phrases for more natural summaries.【F:src/ltltoeng.py†L90-L125】【F:src/ltltoeng.py†L827-L835】
 - Enhanced instructor experience with dedicated entry points for authoring and managing custom exercises alongside course links.【F:src/templates/instructorhome.html†L76-L109】

src/authroutes.py

@@ -691,6 +691,56 @@ def suggest_distractors():
     return jsonify({'distractors': distractors, 'error': error})
 
 
+
+
+@authroutes.route('/instructor/trace-tool', methods=['POST'])
+@login_required_as_courseinstructor
+def instructor_trace_tool():
+    """Normalize and preview Spot traces for instructor-authored questions."""
+    from flask import jsonify
+    import exerciseprocessor
+    import spotutils
+
+    trace = request.form.get('trace', '')
+    formula = request.form.get('formula', '').strip()
+    literals_raw = request.form.get('literals', '')
+
+    literals = [lit.strip() for lit in literals_raw.split(',') if lit.strip()]
+
+    try:
+        normalized_trace = exerciseprocessor.normalizeSpotTraceSyntax(trace)
+
+        if not normalized_trace:
+            return jsonify({
+                'error': 'Trace is required.',
+                'normalized': '',
+                'expanded': '',
+                'mermaid': '',
+                'satisfies': None
+            })
+
+        expanded_trace = exerciseprocessor.expandSpotTrace(normalized_trace, literals)
+        mermaid = exerciseprocessor.genMermaidGraphFromSpotTrace(normalized_trace)
+
+        satisfies = None
+        if formula:
+            satisfies = bool(spotutils.is_trace_satisfied(normalized_trace, formula))
+
+        return jsonify({
+            'error': None,
+            'normalized': normalized_trace,
+            'expanded': expanded_trace,
+            'mermaid': mermaid,
+            'satisfies': satisfies
+        })
+    except Exception as e:
+        return jsonify({
+            'error': str(e),
+            'normalized': '',
+            'expanded': '',
+            'mermaid': '',
+            'satisfies': None
+        })
 @authroutes.route('/instructor/suggest-traces', methods=['POST'])
 @login_required_as_courseinstructor
 def suggest_traces():

src/exerciseprocessor.py

@@ -163,7 +163,7 @@ def expand(self, literals):
 
 ## Internal ##
 def spotTraceToNodeReprs(sr):
-    sr = sr.strip()
+    sr = normalizeSpotTraceSyntax(sr)
     if sr == "":
         return []
 
@@ -186,6 +186,33 @@ def spotTraceToNodeReprs(sr):
         "cycle_states": cycle_states
     }
 
+
+def normalizeSpotTraceSyntax(trace):
+    """Normalize user-entered trace shorthand into Spot-compatible syntax.
+
+    Examples:
+        "a; !b; {a & b; !a}" -> "a;!b;cycle{a & b;!a}"
+        "{a}" -> "cycle{a}"
+    """
+    if trace is None:
+        return ""
+
+    normalized = str(trace).strip()
+    if normalized == "":
+        return ""
+
+    cycle_match = re.search(r'\{([^{}]*)\}\s*$', normalized)
+    if cycle_match:
+        cycle_body = cycle_match.group(1).strip()
+        prefix = normalized[:cycle_match.start()].rstrip().rstrip(';').strip()
+        prefix_parts = [part.strip() for part in prefix.split(';') if part.strip()] if prefix else []
+        normalized = ';'.join(prefix_parts + [f"cycle{{{cycle_body}}}"])
+    else:
+        parts = [part.strip() for part in normalized.split(';') if part.strip()]
+        normalized = ';'.join(parts)
+
+    return normalized
+
 def nodeReprListsToSpotTrace(prefix_states, cycle_states) -> str:
     prefix_string = ';'.join([str(state) for state in prefix_states])
     cycle_string = "cycle{" +  ';'.join([str(state) for state in cycle_states]) + "}"

src/templates/instructor/exercise_builder.html

@@ -249,16 +249,34 @@ <h1 class="mb-1">{{ 'Edit' if exercise else 'Create' }} Exercise</h1>
                                         <input type="text" class="form-control" id="traceText"
                                                placeholder="e.g., e & h; !e & h; cycle{e & h}">
                                         <div class="input-group-append">
+                                            <button type="button" class="btn btn-outline-secondary" onclick="buildTracePreview()" title="Normalize and preview trace syntax">
+                                                Build Trace
+                                            </button>
                                             <button type="button" class="btn btn-outline-info" onclick="suggestTraces()" title="Suggest traces based on formula">
                                                 Suggest
                                             </button>
                                         </div>
                                     </div>
                                     <small class="form-text text-muted">
-                                        Format: state1; state2; cycle{repeating_state}
+                                        Supports shorthand like <code>a; !b; {a &amp; b; !a}</code>; it is normalized to Spot syntax automatically.
                                     </small>
                                 </div>
 
+                                <div id="traceBuilderResult" class="mb-3" style="display:none;">
+                                    <div class="card border-secondary">
+                                        <div class="card-header py-2 bg-light">
+                                            <small class="font-weight-bold">Trace Builder Preview</small>
+                                        </div>
+                                        <div class="card-body p-2 small">
+                                            <div><strong>Normalized:</strong> <code id="traceBuilderNormalized"></code></div>
+                                            <div><strong>Expanded:</strong> <code id="traceBuilderExpanded"></code></div>
+                                            <div><strong>Satisfies formula:</strong> <span id="traceBuilderSatisfies">N/A</span></div>
+                                            <div class="mt-2"><strong>Graph:</strong></div>
+                                            <pre id="traceBuilderMermaid" class="mermaid mb-0"></pre>
+                                        </div>
+                                    </div>
+                                </div>
+
                                 <!-- Suggested Traces (for Y/N questions) -->
                                 <div id="suggestedTraces" class="mb-3" style="display:none;">
                                     <div class="card border-info">
@@ -431,11 +449,13 @@ <h6 class="text-danger"><small>✗ Rejecting Traces</small></h6>
         if (kind === 'englishtoltl') {
             hint.textContent = 'For English to LTL: Enter the English description of the LTL formula.';
             traceGroup.style.display = 'none';
+            document.getElementById('traceBuilderResult').style.display = 'none';
             suggestDistractorsBtn.style.display = 'inline-block';
             suggestTracesBtn.style.display = 'none';
         } else if (kind === 'tracesatisfaction_mc') {
             hint.textContent = 'For Trace Satisfaction (MC): Enter the LTL formula in the Question field. Options will be traces.';
             traceGroup.style.display = 'none';
+            document.getElementById('traceBuilderResult').style.display = 'none';
             suggestDistractorsBtn.style.display = 'none';
             suggestTracesBtn.style.display = 'inline-block';
         } else {
@@ -783,6 +803,40 @@ <h6 class="text-danger"><small>✗ Rejecting Traces</small></h6>
         });
     }
 
+    function buildTracePreview() {
+        const trace = document.getElementById('traceText').value.trim();
+        const formula = document.getElementById('questionText').value.trim();
+
+        if (!trace) {
+            showFeedback('Enter a trace to normalize/preview.', 'warning');
+            return;
+        }
+
+        $.post('{{ url_for("authroutes.instructor_trace_tool") }}', {
+            trace: trace,
+            formula: formula
+        }, function(data) {
+            if (data.error) {
+                showFeedback(`Trace tool error: ${data.error}`, 'danger');
+                return;
+            }
+
+            document.getElementById('traceText').value = data.normalized || trace;
+            document.getElementById('traceBuilderNormalized').textContent = data.normalized || '';
+            document.getElementById('traceBuilderExpanded').textContent = data.expanded || '';
+            document.getElementById('traceBuilderSatisfies').textContent = (data.satisfies === null) ? 'N/A' : (data.satisfies ? 'Yes' : 'No');
+            document.getElementById('traceBuilderMermaid').textContent = data.mermaid || '';
+            document.getElementById('traceBuilderResult').style.display = 'block';
+            if (window.mermaid) {
+                mermaid.init(undefined, document.getElementById('traceBuilderMermaid'));
+            }
+
+            showFeedback('Trace normalized and previewed.', 'success', 1200);
+        }).fail(function(xhr, status, error) {
+            showFeedback(`Trace tool request failed: ${error}`, 'danger');
+        });
+    }
+
     function suggestTraces() {
         const formula = document.getElementById('questionText').value.trim();
 

src/templates/version.html

@@ -1 +1 @@
-1.9.9
+1.9.10

test/test_trace_builder.py

@@ -0,0 +1,25 @@
+import unittest
+import sys
+import os
+from unittest.mock import MagicMock
+
+sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '../src')))
+sys.modules['spot'] = MagicMock()
+
+from exerciseprocessor import normalizeSpotTraceSyntax
+
+
+class TestTraceBuilderNormalization(unittest.TestCase):
+    def test_normalizes_cycle_shorthand(self):
+        trace = "a; !b; {a & b; !a}"
+        self.assertEqual(normalizeSpotTraceSyntax(trace), "a;!b;cycle{a & b; !a}")
+
+    def test_normalizes_bare_cycle(self):
+        self.assertEqual(normalizeSpotTraceSyntax("{a}"), "cycle{a}")
+
+    def test_trims_and_compacts_semicolons(self):
+        self.assertEqual(normalizeSpotTraceSyntax(" a ;  b ;  c "), "a;b;c")
+
+
+if __name__ == '__main__':
+    unittest.main()