diff --git a/CHANGELOG.md b/CHANGELOG.md index 72a503b..dbc6bee 100644 --- a/CHANGELOG.md +++ b/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】 diff --git a/src/authroutes.py b/src/authroutes.py index cbc2ccd..9655c36 100644 --- a/src/authroutes.py +++ b/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(): diff --git a/src/exerciseprocessor.py b/src/exerciseprocessor.py index 0481c03..f6e0330 100644 --- a/src/exerciseprocessor.py +++ b/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]) + "}" diff --git a/src/templates/instructor/exercise_builder.html b/src/templates/instructor/exercise_builder.html index 7d2d490..57f2a28 100644 --- a/src/templates/instructor/exercise_builder.html +++ b/src/templates/instructor/exercise_builder.html @@ -249,16 +249,34 @@

{{ 'Edit' if exercise else 'Create' }} Exercise

+
- Format: state1; state2; cycle{repeating_state} + Supports shorthand like a; !b; {a & b; !a}; it is normalized to Spot syntax automatically. + +