Canonicalize generated trace literal order (#146)

Author: sidprasad

src/app.py

@@ -588,20 +588,22 @@ def authorquestion():
 
         distractors = mergedDistractors
         new_distractors = []
-        added_traces = set([answer])
-        ## IF the kind is trace satisfaction_mc, we need to generate traces for each distractor:
-        if kind == "tracesatisfaction_mc" or kind == "tracesatisfaction_yn":
-            # This is only true for trace_satisaction questions
-            answer_formula = question
-            
-            for distractor in distractors:
-                f = distractor['formula']
-                potential_trace_choices = spotutils.generate_traces(f_accepted=f, f_rejected=answer_formula, max_traces=10)
-                trace_choices = [t for t in potential_trace_choices if t not in added_traces]
-                if len(trace_choices) > 0:
-                    c = spotutils.weighted_trace_choice(trace_choices)
-                    ms = distractor['code']
-                    new_distractors.append({
+        added_traces = set([exerciseprocessor.canonicalizeSpotTrace(answer)])
+        ## IF the kind is trace satisfaction_mc, we need to generate traces for each distractor:
+        if kind == "tracesatisfaction_mc" or kind == "tracesatisfaction_yn":
+            # This is only true for trace_satisaction questions
+            answer_formula = question
+            
+            for distractor in distractors:
+                f = distractor['formula']
+                potential_trace_choices = spotutils.generate_traces(f_accepted=f, f_rejected=answer_formula, max_traces=10)
+                potential_trace_choices = [exerciseprocessor.canonicalizeSpotTrace(t) for t in potential_trace_choices]
+                potential_trace_choices = list(dict.fromkeys(potential_trace_choices))
+                trace_choices = [t for t in potential_trace_choices if t not in added_traces]
+                if len(trace_choices) > 0:
+                    c = spotutils.weighted_trace_choice(trace_choices)
+                    ms = distractor['code']
+                    new_distractors.append({
                         'formula': c,
                         'code': ms
                     })

src/authroutes.py

@@ -721,9 +721,9 @@ def suggest_traces():
         # Generate satisfying traces
         sat_traces = spotutils.generate_accepted_traces(formula_str, max_traces=5)
         for trace in sat_traces:
-            trace_str = str(trace)
+            trace_str = exerciseprocessor.canonicalizeSpotTrace(str(trace))
             expanded = exerciseprocessor.expandSpotTrace(trace_str, literals)
-            mermaid = exerciseprocessor.genMermaidGraphFromSpotTrace(trace_str)
+            mermaid = exerciseprocessor.genMermaidGraphFromSpotTrace(expanded)
             satisfying_traces.append({
                 'trace': expanded,
                 'raw': trace_str,
@@ -735,9 +735,9 @@ def suggest_traces():
         negated = f"!({formula_str})"
         rej_traces = spotutils.generate_accepted_traces(negated, max_traces=5)
         for trace in rej_traces:
-            trace_str = str(trace)
+            trace_str = exerciseprocessor.canonicalizeSpotTrace(str(trace))
             expanded = exerciseprocessor.expandSpotTrace(trace_str, literals)
-            mermaid = exerciseprocessor.genMermaidGraphFromSpotTrace(trace_str)
+            mermaid = exerciseprocessor.genMermaidGraphFromSpotTrace(expanded)
             rejecting_traces.append({
                 'trace': expanded,
                 'raw': trace_str,

src/exercisebuilder.py

@@ -566,6 +566,8 @@ def build_english_to_ltl_question(self, answer):
         }
 
     def build_tracesat_mc_question(self, answer):
+        import exerciseprocessor
+
         options = self.get_options_with_misconceptions_as_formula(answer)
         if options is None:
             return None
@@ -589,6 +591,8 @@ def build_tracesat_mc_question(self, answer):
                     potential_trace_choices = spotutils.generate_accepted_traces(formula, max_traces=max_choice_size)
                 else:
                     potential_trace_choices = spotutils.generate_traces(f_accepted=formula, f_rejected=parenthesized_answer, max_traces=max_choice_size)
+                potential_trace_choices = [exerciseprocessor.canonicalizeSpotTrace(t) for t in potential_trace_choices]
+                potential_trace_choices = list(dict.fromkeys(potential_trace_choices))
                 existing_trace_options = [option['option'] for option in trace_options]
                 trace_choices = [t for t in potential_trace_choices if t not in existing_trace_options]
                 attempt_number += 1
@@ -617,6 +621,8 @@ def build_tracesat_mc_question(self, answer):
         }
 
     def build_tracesat_yn_question(self, answer):
+        import exerciseprocessor
+
         formulae = self.get_options_with_misconceptions_as_formula(answer)
         parenthesized_answer = self.toSpotSyntax(answer)
 
@@ -650,6 +656,9 @@ def build_tracesat_yn_question(self, answer):
 
                 feedbackString = f"The trace is accepted by the formula <code>{option_in_correct_syntax}</code>, but not by the formula <code>{correct_option_in_correct_syntax}</code>."
             misconceptions = formula['misconceptions']
+
+        potential_trace_choices = [exerciseprocessor.canonicalizeSpotTrace(t) for t in potential_trace_choices]
+        potential_trace_choices = list(dict.fromkeys(potential_trace_choices))
 
         if len(potential_trace_choices) == 0:
             return None

src/exerciseprocessor.py

@@ -91,7 +91,7 @@ def _canonicalize_state(state_str: str) -> str:
             return cleaned
 
         tokens = [t.strip() for t in re.split(rf'\s*{re.escape(NodeRepr.VAR_SEPARATOR)}\s*', cleaned) if t.strip() != ""]
-        normalized = [t.replace('(', '').replace(')', '') for t in tokens]
+        normalized = [t.replace('(', '').replace(')', '').strip() for t in tokens]
 
         def sort_key(token: str):
             is_negated = token.startswith('!')
@@ -198,6 +198,36 @@ def nodeReprListsToSpotTrace(prefix_states, cycle_states) -> str:
     return prefix_string + ";" + cycle_string
 
 
+def canonicalizeSpotTrace(sr: str) -> str:
+    """
+    Return a trace string with each state's literals in canonical order.
+    This preserves the original prefix/cycle structure and only normalizes
+    literal ordering within states.
+    """
+    sr = sr.strip()
+    if sr == "":
+        return ""
+
+    prefix_split = sr.split('cycle', 1)
+    prefix_parts = [x for x in prefix_split[0].strip().split(';') if x.strip() != ""]
+    canonical_prefix = [NodeRepr._canonicalize_state(part) for part in prefix_parts]
+
+    cycle_parts = []
+    if len(prefix_split) > 1:
+        cycled_content = getCycleContent(prefix_split[1])
+        cycle_parts = [x for x in cycled_content.split(';') if x.strip() != ""]
+        cycle_parts = [NodeRepr._canonicalize_state(part) for part in cycle_parts]
+
+    prefix_string = ';'.join(canonical_prefix)
+    if len(cycle_parts) > 0:
+        cycle_string = "cycle{" + ';'.join(cycle_parts) + "}"
+        if prefix_string == "":
+            return cycle_string
+        return prefix_string + ";" + cycle_string
+
+    return prefix_string
+
+
 
 def expandSpotTrace(sr, literals) -> str:
 

test/test_trace_canonicalization.py

@@ -0,0 +1,33 @@
+import unittest
+import sys
+import os
+
+# Add the src directory to sys.path
+sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), "../src")))
+
+# Mock spot module to avoid import error in transitive imports
+from unittest.mock import MagicMock
+sys.modules['spot'] = MagicMock()
+sys.modules['inflect'] = MagicMock()
+sys.modules['wordfreq'] = MagicMock(zipf_frequency=lambda *args, **kwargs: 0)
+
+from exerciseprocessor import canonicalizeSpotTrace
+
+
+class TestTraceCanonicalization(unittest.TestCase):
+    def test_orders_literals_lexicographically_per_state(self):
+        trace = "b & !a; c & a; cycle{!c & b; a & !b}"
+        expected = "!a & b;a & c;cycle{b & !c;a & !b}"
+        self.assertEqual(canonicalizeSpotTrace(trace), expected)
+
+    def test_handles_parentheses_and_whitespace(self):
+        trace = " ( b ) & ( !a ) ; cycle{ (d) & c } "
+        expected = "!a & b;cycle{c & d}"
+        self.assertEqual(canonicalizeSpotTrace(trace), expected)
+
+    def test_empty_trace(self):
+        self.assertEqual(canonicalizeSpotTrace("   "), "")
+
+
+if __name__ == "__main__":
+    unittest.main()