From a54d3d756a4e87f1cc3ef32b45c943477d685cee Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Fri, 20 Mar 2026 17:47:37 -0400 Subject: [PATCH] Extract LTL mutator into standalone pip-installable sub-package MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Factor out the core mutation logic (codebook, syntacticmutator, ltlnode, spotutils, ANTLR grammar) into a new `ltlmutator/` package at the repo root so it can be reused independently (closes #142). The ltltoeng circular dependency is broken via lazy import — the package works standalone without ltltoeng/inflect/wordfreq, falling back to str() for __to_english__(). All consumers updated to import from ltlmutator. Co-Authored-By: Claude Opus 4.6 --- Dockerfile | 2 + experiments/benchmark_builder.py | 10 +- experiments/benchmark_evaluator.py | 4 +- ltlmutator/pyproject.toml | 12 + ltlmutator/src/ltlmutator.egg-info/PKG-INFO | 6 + .../src/ltlmutator.egg-info/SOURCES.txt | 15 + .../ltlmutator.egg-info/dependency_links.txt | 1 + .../src/ltlmutator.egg-info/requires.txt | 1 + .../src/ltlmutator.egg-info/top_level.txt | 1 + ltlmutator/src/ltlmutator/__init__.py | 9 + .../src/ltlmutator}/codebook.py | 1130 ++++++++--------- ltlmutator/src/ltlmutator/grammar/__init__.py | 0 .../src/ltlmutator/grammar}/ltl.g4 | 0 .../src/ltlmutator/grammar}/ltl.interp | 0 .../src/ltlmutator/grammar}/ltl.tokens | 0 .../src/ltlmutator/grammar}/ltlLexer.interp | 0 .../src/ltlmutator/grammar}/ltlLexer.py | 14 +- .../src/ltlmutator/grammar}/ltlLexer.tokens | 0 .../src/ltlmutator/grammar}/ltlListener.py | 7 +- .../src/ltlmutator/grammar}/ltlParser.py | 29 +- {src => ltlmutator/src/ltlmutator}/ltlnode.py | 1030 ++++++++------- .../src/ltlmutator}/spotutils.py | 554 ++++---- .../src/ltlmutator}/syntacticmutator.py | 26 +- requirements.txt | 1 + src/app.py | 6 +- src/authroutes.py | 10 +- src/exercisebuilder.py | 10 +- src/exerciseprocessor.py | 2 +- src/feedbackgenerator.py | 2 +- src/ltltoeng.py | 24 +- src/stepper.py | 4 +- test/test_english_translation.py | 2 +- test/test_mutation.py | 96 +- test/test_parsing.py | 2 +- test/test_regression_model.py | 2 +- test/test_weighted_trace.py | 2 +- test_template_generation.py | 4 +- 37 files changed, 1550 insertions(+), 1468 deletions(-) create mode 100644 ltlmutator/pyproject.toml create mode 100644 ltlmutator/src/ltlmutator.egg-info/PKG-INFO create mode 100644 ltlmutator/src/ltlmutator.egg-info/SOURCES.txt create mode 100644 ltlmutator/src/ltlmutator.egg-info/dependency_links.txt create mode 100644 ltlmutator/src/ltlmutator.egg-info/requires.txt create mode 100644 ltlmutator/src/ltlmutator.egg-info/top_level.txt create mode 100644 ltlmutator/src/ltlmutator/__init__.py rename {src => ltlmutator/src/ltlmutator}/codebook.py (96%) create mode 100644 ltlmutator/src/ltlmutator/grammar/__init__.py rename {src => ltlmutator/src/ltlmutator/grammar}/ltl.g4 (100%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltl.interp (100%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltl.tokens (100%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltlLexer.interp (100%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltlLexer.py (97%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltlLexer.tokens (100%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltlListener.py (96%) rename {src => ltlmutator/src/ltlmutator/grammar}/ltlParser.py (99%) rename {src => ltlmutator/src/ltlmutator}/ltlnode.py (71%) rename {src => ltlmutator/src/ltlmutator}/spotutils.py (94%) rename {src => ltlmutator/src/ltlmutator}/syntacticmutator.py (98%) diff --git a/Dockerfile b/Dockerfile index 1250ba9..eefd800 100644 --- a/Dockerfile +++ b/Dockerfile @@ -2,11 +2,13 @@ FROM continuumio/miniconda3 AS build COPY requirements.txt . +COPY ltlmutator/ /ltlmutator/ RUN conda init bash && \ . /opt/conda/etc/profile.d/conda.sh && \ conda create --name myenv python=3.9 && \ conda activate myenv && \ conda install -c https://conda.anaconda.org/conda-forge spot && \ + pip install /ltlmutator && \ pip install -r requirements.txt # && \ #conda pack -n myenv -o /tmp/myenv.tar.gz diff --git a/experiments/benchmark_builder.py b/experiments/benchmark_builder.py index d8ad035..ad2589e 100644 --- a/experiments/benchmark_builder.py +++ b/experiments/benchmark_builder.py @@ -18,10 +18,10 @@ # Add src to path for LTL Tutor imports sys.path.insert(0, str(Path(__file__).parent.parent / 'src')) -from ltlnode import parse_ltl_string +from ltlmutator import parse_ltl_string import ltltoeng import spot -import codebook +from ltlmutator import codebook from sentence_transformers import SentenceTransformer @@ -132,7 +132,7 @@ def compute_sbert_distance(text1, text2, model): # Misconception distribution control def get_all_misconception_types(): """Get all misconception types from the codebook.""" - from codebook import MisconceptionCode + from ltlmutator import MisconceptionCode return [m.value for m in MisconceptionCode if m != MisconceptionCode.Syntactic] @@ -275,7 +275,7 @@ def generate_template_formulas_for_misconceptions(misconceptions_needed, num_tem template_formulas = [] # Only generate templates for misconceptions that need them - from codebook import MisconceptionCode + from ltlmutator import MisconceptionCode for misconception_name, deficit in misconceptions_needed: # Skip if no deficit (already have enough) @@ -316,7 +316,7 @@ def adjust_priorities_for_misconceptions(misconceptions_needed): # For each missing misconception, boost its associated operators for misconception_name, _ in misconceptions_needed[:3]: # Top 3 most needed try: - from codebook import MisconceptionCode + from ltlmutator import MisconceptionCode misconception_enum = MisconceptionCode(misconception_name) operators = misconception_enum.associatedOperators() diff --git a/experiments/benchmark_evaluator.py b/experiments/benchmark_evaluator.py index ef582d7..f9369e5 100644 --- a/experiments/benchmark_evaluator.py +++ b/experiments/benchmark_evaluator.py @@ -17,8 +17,8 @@ # Add src to path for LTL parsing and equivalence checking sys.path.insert(0, str(Path(__file__).parent.parent / 'src')) -from ltlnode import parse_ltl_string -from spotutils import areEquivalent +from ltlmutator import parse_ltl_string +from ltlmutator.spotutils import areEquivalent import spot diff --git a/ltlmutator/pyproject.toml b/ltlmutator/pyproject.toml new file mode 100644 index 0000000..44c21e1 --- /dev/null +++ b/ltlmutator/pyproject.toml @@ -0,0 +1,12 @@ +[project] +name = "ltlmutator" +version = "0.1.0" +description = "LTL formula semantic and syntactic mutation library" +requires-python = ">=3.9" +dependencies = [ + "antlr4-python3-runtime>=4.13.1", +] + +[build-system] +requires = ["setuptools>=61.0"] +build-backend = "setuptools.build_meta" diff --git a/ltlmutator/src/ltlmutator.egg-info/PKG-INFO b/ltlmutator/src/ltlmutator.egg-info/PKG-INFO new file mode 100644 index 0000000..c586575 --- /dev/null +++ b/ltlmutator/src/ltlmutator.egg-info/PKG-INFO @@ -0,0 +1,6 @@ +Metadata-Version: 2.4 +Name: ltlmutator +Version: 0.1.0 +Summary: LTL formula semantic and syntactic mutation library +Requires-Python: >=3.9 +Requires-Dist: antlr4-python3-runtime>=4.13.1 diff --git a/ltlmutator/src/ltlmutator.egg-info/SOURCES.txt b/ltlmutator/src/ltlmutator.egg-info/SOURCES.txt new file mode 100644 index 0000000..7fa525a --- /dev/null +++ b/ltlmutator/src/ltlmutator.egg-info/SOURCES.txt @@ -0,0 +1,15 @@ +pyproject.toml +src/ltlmutator/__init__.py +src/ltlmutator/codebook.py +src/ltlmutator/ltlnode.py +src/ltlmutator/spotutils.py +src/ltlmutator/syntacticmutator.py +src/ltlmutator.egg-info/PKG-INFO +src/ltlmutator.egg-info/SOURCES.txt +src/ltlmutator.egg-info/dependency_links.txt +src/ltlmutator.egg-info/requires.txt +src/ltlmutator.egg-info/top_level.txt +src/ltlmutator/grammar/__init__.py +src/ltlmutator/grammar/ltlLexer.py +src/ltlmutator/grammar/ltlListener.py +src/ltlmutator/grammar/ltlParser.py \ No newline at end of file diff --git a/ltlmutator/src/ltlmutator.egg-info/dependency_links.txt b/ltlmutator/src/ltlmutator.egg-info/dependency_links.txt new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/ltlmutator/src/ltlmutator.egg-info/dependency_links.txt @@ -0,0 +1 @@ + diff --git a/ltlmutator/src/ltlmutator.egg-info/requires.txt b/ltlmutator/src/ltlmutator.egg-info/requires.txt new file mode 100644 index 0000000..f091581 --- /dev/null +++ b/ltlmutator/src/ltlmutator.egg-info/requires.txt @@ -0,0 +1 @@ +antlr4-python3-runtime>=4.13.1 diff --git a/ltlmutator/src/ltlmutator.egg-info/top_level.txt b/ltlmutator/src/ltlmutator.egg-info/top_level.txt new file mode 100644 index 0000000..8e10650 --- /dev/null +++ b/ltlmutator/src/ltlmutator.egg-info/top_level.txt @@ -0,0 +1 @@ +ltlmutator diff --git a/ltlmutator/src/ltlmutator/__init__.py b/ltlmutator/src/ltlmutator/__init__.py new file mode 100644 index 0000000..4d4371a --- /dev/null +++ b/ltlmutator/src/ltlmutator/__init__.py @@ -0,0 +1,9 @@ +from .codebook import MisconceptionCode, applyMisconception, getAllApplicableMisconceptions, MutationResult +from .syntacticmutator import applyRandomMutation, applyRandomMutationNotEquivalentTo +from .ltlnode import ( + LTLNode, LiteralNode, UnaryOperatorNode, BinaryOperatorNode, + UntilNode, NextNode, GloballyNode, FinallyNode, + OrNode, AndNode, NotNode, ImpliesNode, EquivalenceNode, + parse_ltl_string, SUPPORTED_SYNTAXES +) +from . import spotutils diff --git a/src/codebook.py b/ltlmutator/src/ltlmutator/codebook.py similarity index 96% rename from src/codebook.py rename to ltlmutator/src/ltlmutator/codebook.py index 00a29af..8de270d 100644 --- a/src/codebook.py +++ b/ltlmutator/src/ltlmutator/codebook.py @@ -1,154 +1,154 @@ -from enum import Enum -import random -from ltlnode import * -import copy -import spotutils - -class MisconceptionCode(Enum): - Precedence = "Precedence" - BadStateIndex = "BadStateIndex" - BadStateQuantification = "BadStateQuantification" - ExclusiveU = "ExclusiveU" - ImplicitF = "ImplicitF" - ImplicitG = "ImplicitG" - OtherImplicit = "OtherImplicit" - WeakU = "WeakU" - - ## THIS IS A NON-MISCONCEPTION CODE USED AS A CONTROL ## - Syntactic = "RandomSyntactic" ### Should this be here??? Does adding this break anything? - - #### Ignoring these codes since they have no relevance here ### - #Unlabeled = "Unlabeled" - #BadProp = "BadProp" - #ReasonableVariant = "ReasonableVariant" - - @classmethod - def from_string(cls, code_str): - if "MisconceptionCode" in code_str: - code_str = code_str.split(".")[-1] - try: - return cls(code_str) - except ValueError: - return None - - def needsTemplateGeneration(self): - """ - Returns True if this misconception benefits from template-based formula generation - rather than purely random generation, because it requires specific structural patterns. - """ - return self in [ - MisconceptionCode.ExclusiveU, - MisconceptionCode.BadStateIndex - ] - - def generateTemplateFormula(self, atomic_props=None): - """ - Generate a formula from a template that guarantees this misconception can be applied. - Uses SPOT's randltl for subformulae to avoid trivial tautologies/contradictions. - Returns an LTLNode, or None if template generation is not applicable. - - Args: - atomic_props: List of atomic proposition strings to use. If None, uses ['p0', 'p1', 'p2'] - """ - if atomic_props is None: - atomic_props = ['p0', 'p1', 'p2'] - - if not self.needsTemplateGeneration(): - return None - - def build_subformula(tree_size=3): - """ - Build a non-trivial subformula using SPOT's randltl via spotutils. - Returns an LTLNode. - """ - formula_str = spotutils.gen_small_rand_ltl(atomic_props, tree_size=tree_size) - return parse_ltl_string(formula_str) - - # Generate template and verify it's non-trivial - max_attempts = 20 - for attempt in range(max_attempts): - template = None - - if self == MisconceptionCode.ExclusiveU: - # Generate patterns that ExclusiveU can mutate - x = build_subformula(tree_size=2) - y = build_subformula(tree_size=3) - - patterns = [ - # x U (!x & y) - explicit disjointness - UntilNode(x, AndNode(NotNode(x), y)), - # x U (x -> y) - implication pattern - UntilNode(x, ImpliesNode(x, y)), - # x U (!x | y) - or pattern with negation - UntilNode(x, OrNode(NotNode(x), y)), - ] - template = random.choice(patterns) - - elif self == MisconceptionCode.BadStateIndex: - # Generate Until/Next patterns with complex RHS - x = build_subformula(tree_size=2) - y = build_subformula(tree_size=2) - z = build_subformula(tree_size=2) - - patterns = [ - # x U (y & Fz) - Until with conjunction including Finally - UntilNode(x, AndNode(y, FinallyNode(z))), - # x U (y & Gz) - Until with conjunction including Globally - UntilNode(x, AndNode(y, GloballyNode(z))), - # x U X(y & z) - Until with Next of conjunction - UntilNode(x, NextNode(AndNode(y, z))), - # X(y & z) - Next with conjunction - NextNode(AndNode(y, z)), - ] - template = random.choice(patterns) - - if template is not None and not spotutils.is_trivial(str(template)): - return template - - # If all attempts failed, return None - return None - - def associatedOperators(self): - - TEMPORAL_OPERATORS = [FinallyNode.symbol, GloballyNode.symbol, UntilNode.symbol, NextNode.symbol] - k = random.randint(1, len(TEMPORAL_OPERATORS)) - TEMPORAL_SUBSET = random.choices(TEMPORAL_OPERATORS, k=k) - - if self == MisconceptionCode.Precedence: - ### All binary operators (ie operator.value for every class that inherits from BinaryOperatorNode) ### - return [cls.symbol for cls in BinaryOperatorNode.__subclasses__()] - elif self == MisconceptionCode.BadStateIndex: - ## Tricky -- default to a subset of temporally meaningful operators (U, X, G, F) ## - return TEMPORAL_SUBSET - elif self == MisconceptionCode.BadStateQuantification: - # Applies to responses that mis-use or swap a fan-out operator (F, G, U). - return [FinallyNode.symbol, GloballyNode.symbol, UntilNode.symbol] - elif self == MisconceptionCode.ExclusiveU: - # Boost Until AND the boolean operators that create the patterns we need - # (e.g., x U (!x & y), x U (x -> y), etc.) - return [UntilNode.symbol, AndNode.symbol, OrNode.symbol, ImpliesNode.symbol, NotNode.symbol] - elif self == MisconceptionCode.ImplicitF: - return [FinallyNode.symbol] - elif self == MisconceptionCode.ImplicitG: - return [GloballyNode.symbol] - elif self == MisconceptionCode.WeakU: - return [UntilNode.symbol] - elif self == MisconceptionCode.OtherImplicit: - ### TODO: This one is tricky, less meaningful... - ## But ensure that Next and Until are present ## - return list(set([UntilNode.symbol, NextNode.symbol] + TEMPORAL_SUBSET)) - #### Ignoring these codes since they have no relevance here ### - else: - return [] - - - -class MutationResult: - def __init__(self, node, misconception=None): - self.node = node - self.misconception = misconception - - +from enum import Enum +import random +from .ltlnode import * +import copy +from . import spotutils + +class MisconceptionCode(Enum): + Precedence = "Precedence" + BadStateIndex = "BadStateIndex" + BadStateQuantification = "BadStateQuantification" + ExclusiveU = "ExclusiveU" + ImplicitF = "ImplicitF" + ImplicitG = "ImplicitG" + OtherImplicit = "OtherImplicit" + WeakU = "WeakU" + + ## THIS IS A NON-MISCONCEPTION CODE USED AS A CONTROL ## + Syntactic = "RandomSyntactic" ### Should this be here??? Does adding this break anything? + + #### Ignoring these codes since they have no relevance here ### + #Unlabeled = "Unlabeled" + #BadProp = "BadProp" + #ReasonableVariant = "ReasonableVariant" + + @classmethod + def from_string(cls, code_str): + if "MisconceptionCode" in code_str: + code_str = code_str.split(".")[-1] + try: + return cls(code_str) + except ValueError: + return None + + def needsTemplateGeneration(self): + """ + Returns True if this misconception benefits from template-based formula generation + rather than purely random generation, because it requires specific structural patterns. + """ + return self in [ + MisconceptionCode.ExclusiveU, + MisconceptionCode.BadStateIndex + ] + + def generateTemplateFormula(self, atomic_props=None): + """ + Generate a formula from a template that guarantees this misconception can be applied. + Uses SPOT's randltl for subformulae to avoid trivial tautologies/contradictions. + Returns an LTLNode, or None if template generation is not applicable. + + Args: + atomic_props: List of atomic proposition strings to use. If None, uses ['p0', 'p1', 'p2'] + """ + if atomic_props is None: + atomic_props = ['p0', 'p1', 'p2'] + + if not self.needsTemplateGeneration(): + return None + + def build_subformula(tree_size=3): + """ + Build a non-trivial subformula using SPOT's randltl via spotutils. + Returns an LTLNode. + """ + formula_str = spotutils.gen_small_rand_ltl(atomic_props, tree_size=tree_size) + return parse_ltl_string(formula_str) + + # Generate template and verify it's non-trivial + max_attempts = 20 + for attempt in range(max_attempts): + template = None + + if self == MisconceptionCode.ExclusiveU: + # Generate patterns that ExclusiveU can mutate + x = build_subformula(tree_size=2) + y = build_subformula(tree_size=3) + + patterns = [ + # x U (!x & y) - explicit disjointness + UntilNode(x, AndNode(NotNode(x), y)), + # x U (x -> y) - implication pattern + UntilNode(x, ImpliesNode(x, y)), + # x U (!x | y) - or pattern with negation + UntilNode(x, OrNode(NotNode(x), y)), + ] + template = random.choice(patterns) + + elif self == MisconceptionCode.BadStateIndex: + # Generate Until/Next patterns with complex RHS + x = build_subformula(tree_size=2) + y = build_subformula(tree_size=2) + z = build_subformula(tree_size=2) + + patterns = [ + # x U (y & Fz) - Until with conjunction including Finally + UntilNode(x, AndNode(y, FinallyNode(z))), + # x U (y & Gz) - Until with conjunction including Globally + UntilNode(x, AndNode(y, GloballyNode(z))), + # x U X(y & z) - Until with Next of conjunction + UntilNode(x, NextNode(AndNode(y, z))), + # X(y & z) - Next with conjunction + NextNode(AndNode(y, z)), + ] + template = random.choice(patterns) + + if template is not None and not spotutils.is_trivial(str(template)): + return template + + # If all attempts failed, return None + return None + + def associatedOperators(self): + + TEMPORAL_OPERATORS = [FinallyNode.symbol, GloballyNode.symbol, UntilNode.symbol, NextNode.symbol] + k = random.randint(1, len(TEMPORAL_OPERATORS)) + TEMPORAL_SUBSET = random.choices(TEMPORAL_OPERATORS, k=k) + + if self == MisconceptionCode.Precedence: + ### All binary operators (ie operator.value for every class that inherits from BinaryOperatorNode) ### + return [cls.symbol for cls in BinaryOperatorNode.__subclasses__()] + elif self == MisconceptionCode.BadStateIndex: + ## Tricky -- default to a subset of temporally meaningful operators (U, X, G, F) ## + return TEMPORAL_SUBSET + elif self == MisconceptionCode.BadStateQuantification: + # Applies to responses that mis-use or swap a fan-out operator (F, G, U). + return [FinallyNode.symbol, GloballyNode.symbol, UntilNode.symbol] + elif self == MisconceptionCode.ExclusiveU: + # Boost Until AND the boolean operators that create the patterns we need + # (e.g., x U (!x & y), x U (x -> y), etc.) + return [UntilNode.symbol, AndNode.symbol, OrNode.symbol, ImpliesNode.symbol, NotNode.symbol] + elif self == MisconceptionCode.ImplicitF: + return [FinallyNode.symbol] + elif self == MisconceptionCode.ImplicitG: + return [GloballyNode.symbol] + elif self == MisconceptionCode.WeakU: + return [UntilNode.symbol] + elif self == MisconceptionCode.OtherImplicit: + ### TODO: This one is tricky, less meaningful... + ## But ensure that Next and Until are present ## + return list(set([UntilNode.symbol, NextNode.symbol] + TEMPORAL_SUBSET)) + #### Ignoring these codes since they have no relevance here ### + else: + return [] + + + +class MutationResult: + def __init__(self, node, misconception=None): + self.node = node + self.misconception = misconception + + def applyMisconception(node_orig, misconception, randomize_location=False): """ Apply a misconception rewrite to a formula tree. @@ -182,424 +182,424 @@ def applyMisconception(node_orig, misconception, randomize_location=False): if not res.misconception: return apply_at_location(node, applyUnderconstraint) return res - # elif misconception in [MisconceptionCode.BadProp, MisconceptionCode.Unlabeled, MisconceptionCode.ReasonableVariant]: - # return MutationResult(node) - else: - return MutationResult(node) - - -def getAllApplicableMisconceptions(node): - - formula = str(node) - def equivalentToOriginal(n) -> bool: - as_str = str(n) - return LTLNode.equiv(formula, as_str) - + # elif misconception in [MisconceptionCode.BadProp, MisconceptionCode.Unlabeled, MisconceptionCode.ReasonableVariant]: + # return MutationResult(node) + else: + return MutationResult(node) + + +def getAllApplicableMisconceptions(node): + + formula = str(node) + def equivalentToOriginal(n) -> bool: + as_str = str(n) + return LTLNode.equiv(formula, as_str) + # Use randomized location application so distractor generation is not # systematically biased toward first-match rewrite sites. xs = [applyMisconception(node, misconception, randomize_location=True) for misconception in MisconceptionCode] - xs = [ x for x in xs if (x is not None and x.misconception is not None) ] - - xs = [ x for x in xs if not equivalentToOriginal(x.node) ] - return xs - - - + xs = [ x for x in xs if (x is not None and x.misconception is not None) ] + + xs = [ x for x in xs if not equivalentToOriginal(x.node) ] + return xs + + + def collectAllMutationLocations(node, f, path=None): - """ - Collect all locations in the tree where mutation f can be applied. - Returns a list of path lists where each path is a list of directions - to reach that node from the root. - - Each returned path is an independent copy to avoid aliasing issues. - """ - if path is None: - path = [] - - locations = [] - + """ + Collect all locations in the tree where mutation f can be applied. + Returns a list of path lists where each path is a list of directions + to reach that node from the root. + + Each returned path is an independent copy to avoid aliasing issues. + """ + if path is None: + path = [] + + locations = [] + # Probe applicability on a copy since some mutation functions mutate input # nodes while constructing their result. res = f(copy.deepcopy(node)) - if res.misconception: - # Store just the path, we'll apply the mutation later - locations.append(list(path)) - - # Recurse into children - if isinstance(node, UnaryOperatorNode): - locations.extend(collectAllMutationLocations(node.operand, f, path + ['operand'])) - elif isinstance(node, BinaryOperatorNode): - locations.extend(collectAllMutationLocations(node.left, f, path + ['left'])) - locations.extend(collectAllMutationLocations(node.right, f, path + ['right'])) - - return locations - - -def applyMutationAtPath(node, f, path): - """ - Apply a mutation function f at a specific path in the tree. - Path is a list of 'left', 'right', or 'operand' directions. - - Note: This function modifies the node tree in-place and uses a pattern - where child_result.node is reassigned to point to the parent node. - This is intentional and matches the pattern used in applyTilFirst. - The caller should pass a deep copy if the original needs to be preserved. - """ - if not path: - # We're at the target node, apply the mutation - return f(node) - - # Navigate to the target location - direction = path[0] - remaining_path = path[1:] - - if isinstance(node, UnaryOperatorNode) and direction == 'operand': - child_result = applyMutationAtPath(node.operand, f, remaining_path) - # Thread the result back through the parent: replace child with mutated version, - # then update result to point to the whole subtree - node.operand = child_result.node - child_result.node = node - return child_result - elif isinstance(node, BinaryOperatorNode) and direction == 'left': - child_result = applyMutationAtPath(node.left, f, remaining_path) - node.left = child_result.node - child_result.node = node - return child_result - elif isinstance(node, BinaryOperatorNode) and direction == 'right': - child_result = applyMutationAtPath(node.right, f, remaining_path) - node.right = child_result.node - child_result.node = node - return child_result - - # Invalid path - this indicates a bug in path generation - raise ValueError(f"Invalid path: cannot apply direction '{direction}' to node of type {type(node).__name__}") - - -def applyTilFirstRandom(node, f): - """ - Apply mutation f to a randomly selected location in the tree where it's applicable. - This ensures diverse mutations when multiple locations are possible. - Use this for simple mutations like ImplicitG/ImplicitF where we want to randomly - select from all possible application sites. - """ - # Collect all possible mutation locations - locations = collectAllMutationLocations(node, f) - - if not locations: - return MutationResult(node) - - # Randomly select one location - path = random.choice(locations) - - # Apply the mutation at the selected location - return applyMutationAtPath(node, f, path) - - -def applyTilFirst(node, f): - """ - Apply mutation f at the first applicable location found (depth-first search). - This is the original behavior, used for complex mutations that should be applied - as a unit at the first matching location. - """ - res = f(node) - if res.misconception: - return res - - if isinstance(node, UnaryOperatorNode): - res = applyTilFirst(node.operand, f) - node.operand = res.node - res.node = node - return res - - if isinstance(node, BinaryOperatorNode): - res_left = applyTilFirst(node.left, f) - res_right = applyTilFirst(node.right, f) - - random_index = random.randint(0, 1) - choose_left = res_left.misconception and (not res_right.misconception or random_index == 0) - choose_right = res_right.misconception and (not res_left.misconception or random_index == 1) - - if choose_left: - node.left = res_left.node - res_left.node = node - return res_left - elif choose_right: - node.right = res_right.node - res_right.node = node - return res_right - - return MutationResult(node) - - -def applyPrecedence(node): - if isinstance(node, BinaryOperatorNode): - if isinstance(node.right, BinaryOperatorNode): - new_top = node.right - node.right = new_top.left - new_top.left = node - return MutationResult(new_top, MisconceptionCode.Precedence) - - return MutationResult(node) - - -def applyExclusiveU(node): - """ - Detect patterns where Until is used with explicit disjointness/exclusivity. - ExclusiveU misconception: treating "x U y" as if x and y cannot both be true. - """ - if isinstance(node, BinaryOperatorNode) and node.operator == UntilNode.symbol: - x = node.left - rhs = node.right - - # Pattern 1: x U (!x & y) → x U y - # Student explicitly enforces disjointness - if isinstance(rhs, BinaryOperatorNode) and rhs.operator == AndNode.symbol: - y = rhs.right - - if isinstance(rhs.left, UnaryOperatorNode) and rhs.left.operator == NotNode.symbol and LTLNode.equiv(rhs.left.operand, x): - return MutationResult(UntilNode(x, y), MisconceptionCode.ExclusiveU) - - # Pattern 1b: x U (y & !x) → x U y (order swapped) - if isinstance(rhs.right, UnaryOperatorNode) and rhs.right.operator == NotNode.symbol and LTLNode.equiv(rhs.right.operand, x): - return MutationResult(UntilNode(x, rhs.left), MisconceptionCode.ExclusiveU) - - # Pattern 2: x U (x -> y) → x U y - # Student thinks "x U (x implies y)" enforces that y happens after x stops - if isinstance(rhs, ImpliesNode) and LTLNode.equiv(rhs.left, x): - return MutationResult(UntilNode(x, rhs.right), MisconceptionCode.ExclusiveU) - - # Pattern 3: x U (!x | y) → x U y - # Student thinks "x U (!x or y)" ensures exclusivity - if isinstance(rhs, OrNode): - if isinstance(rhs.left, NotNode) and LTLNode.equiv(rhs.left.operand, x): - return MutationResult(UntilNode(x, rhs.right), MisconceptionCode.ExclusiveU) - if isinstance(rhs.right, NotNode) and LTLNode.equiv(rhs.right.operand, x): - return MutationResult(UntilNode(x, rhs.left), MisconceptionCode.ExclusiveU) - - # Reverse: x U y → one of the ExclusiveU misconception variants - # The correct formula is x U y, but a student with the ExclusiveU - # misconception might write any of these, so we randomly choose one. - variant = random.choice([ - UntilNode(x, AndNode(NotNode(x), rhs)), # x U (!x & y) - UntilNode(x, ImpliesNode(x, rhs)), # x U (x -> y) - UntilNode(x, OrNode(NotNode(x), rhs)), # x U (!x | y) - ]) - return MutationResult(variant, MisconceptionCode.ExclusiveU) - - # Pattern 4: (x U y) & G(x -> !y) → x U y - # Student adds a global constraint that x and y are mutually exclusive - if isinstance(node, AndNode): - left = node.left - right = node.right - - # Check if one side is Until and other is G(x -> !y) - until_node = None - constraint_node = None - - if isinstance(left, UntilNode) and isinstance(right, GloballyNode): - until_node = left - constraint_node = right.operand - elif isinstance(right, UntilNode) and isinstance(left, GloballyNode): - until_node = right - constraint_node = left.operand - - if until_node and constraint_node and isinstance(constraint_node, ImpliesNode): - x = until_node.left - y = until_node.right - - # Check if constraint is x -> !y - if LTLNode.equiv(constraint_node.left, x): - if isinstance(constraint_node.right, NotNode) and LTLNode.equiv(constraint_node.right.operand, y): - return MutationResult(until_node, MisconceptionCode.ExclusiveU) - - # Check if constraint is y -> !x - if LTLNode.equiv(constraint_node.left, y): - if isinstance(constraint_node.right, NotNode) and LTLNode.equiv(constraint_node.right.operand, x): - return MutationResult(until_node, MisconceptionCode.ExclusiveU) - - # Pattern 5: (x U y) & G!(x & y) → x U y - # Student adds "globally not both" constraint - if isinstance(node, AndNode): - left = node.left - right = node.right - - until_node = None - constraint_node = None - - if isinstance(left, UntilNode) and isinstance(right, GloballyNode): - until_node = left - constraint_node = right.operand - elif isinstance(right, UntilNode) and isinstance(left, GloballyNode): - until_node = right - constraint_node = left.operand - - if until_node and constraint_node: - if isinstance(constraint_node, NotNode) and isinstance(constraint_node.operand, AndNode): - and_node = constraint_node.operand - x = until_node.left - y = until_node.right - - # Check if it's !(x & y) - if (LTLNode.equiv(and_node.left, x) and LTLNode.equiv(and_node.right, y)) or \ - (LTLNode.equiv(and_node.right, x) and LTLNode.equiv(and_node.left, y)): - return MutationResult(until_node, MisconceptionCode.ExclusiveU) - - return MutationResult(node) - - -def applyImplicitG(node): - if isinstance(node, UnaryOperatorNode) and node.operator == GloballyNode.symbol: - return MutationResult(node.operand, MisconceptionCode.ImplicitG) - - return MutationResult(node) - - -def applyImplicitF(node): - if isinstance(node, UnaryOperatorNode) and node.operator == FinallyNode.symbol: - return MutationResult(node.operand, MisconceptionCode.ImplicitF) - - return MutationResult(node) - - -def applyImplicitPrefix(node): - if isinstance(node, UntilNode): - lhs = node.left - rhs = node.right - - if isinstance(lhs, NotNode) and LTLNode.equiv(lhs.operand, rhs): - return MutationResult(FinallyNode(rhs), MisconceptionCode.OtherImplicit) - - if isinstance(rhs, GloballyNode) and LTLNode.equiv(lhs, rhs.operand): - return MutationResult(AndNode(lhs, FinallyNode(rhs)), MisconceptionCode.OtherImplicit) - - if isinstance(node, AndNode): - lhs = node.left - rhs = node.right - - if isinstance(lhs, FinallyNode) and isinstance(rhs, GloballyNode): - rhs_operand = rhs.operand - if isinstance(rhs_operand, ImpliesNode): - rhs_operand_lhs = rhs_operand.left - rhs_operand_rhs = rhs_operand.right - - if LTLNode.equiv(lhs.operand, rhs_operand_lhs) and isinstance(rhs_operand_rhs, NextNode) and isinstance(rhs_operand_rhs.operand, GloballyNode) and LTLNode.equiv(rhs_operand_lhs, rhs_operand_rhs.operand.operand): - return MutationResult(AndNode(lhs.operand, NextNode(rhs)), MisconceptionCode.OtherImplicit) - - if isinstance(node, NextNode): - return MutationResult(FinallyNode(node.operand), MisconceptionCode.OtherImplicit) - - return MutationResult(node) - - - - -def applyUnderconstraint(node): - if isinstance(node, BinaryOperatorNode): - n = random.choice([node.left, node.right]) - return MutationResult(n, MisconceptionCode.OtherImplicit) - ## TODO: Yes, but this shouldn't remove F / G constraints (these aren't covered by the other code) - elif isinstance(node, UnaryOperatorNode): - return MutationResult(node.operand, MisconceptionCode.OtherImplicit) - else: - return MutationResult(node) - - -def applyWeakU(node): - if isinstance(node, UntilNode): - lhs = node.left - # Interpret until as weak-until: RHS may never happen if LHS stays true - new_node = OrNode(node, GloballyNode(lhs)) - return MutationResult(new_node, MisconceptionCode.WeakU) - - return MutationResult(node) - - -def applyBadStateQuantification(node): - if isinstance(node, GloballyNode): - op = node.operand - return MutationResult(FinallyNode(op), MisconceptionCode.BadStateQuantification) - - if isinstance(node, FinallyNode): - op = node.operand - return MutationResult(GloballyNode(op), MisconceptionCode.BadStateQuantification) - - if isinstance(node, UntilNode): - lhs = node.left - rhs = node.right - - new_node = random.choice([ - UntilNode(FinallyNode(lhs), rhs), - UntilNode(GloballyNode(lhs), rhs), - UntilNode(lhs, FinallyNode(rhs)), - UntilNode(lhs, GloballyNode(rhs)), - UntilNode(rhs, lhs) - ]) - return MutationResult(new_node, MisconceptionCode.BadStateQuantification) - - return MutationResult(node) - - -def applyBadStateIndex(node): - if isinstance(node, UntilNode): - lhs = node.left - rhs = node.right - - if isinstance(rhs, AndNode) and isinstance(rhs.right, FinallyNode): - new_node = AndNode(UntilNode(lhs, rhs.left), rhs.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(rhs, AndNode) and isinstance(rhs.right, GloballyNode): - new_node = AndNode(UntilNode(lhs, rhs.left), rhs.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(rhs, OrNode) and isinstance(rhs.right, FinallyNode): - new_node = OrNode(UntilNode(lhs, rhs.left), rhs.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(rhs, OrNode) and isinstance(rhs.right, GloballyNode): - new_node = OrNode(UntilNode(lhs, rhs.left), rhs.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(rhs, ImpliesNode) and isinstance(rhs.right, FinallyNode): - new_node = ImpliesNode(UntilNode(lhs, rhs.left), rhs.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(rhs, ImpliesNode) and isinstance(rhs.right, GloballyNode): - new_node = ImpliesNode(UntilNode(lhs, rhs.left), rhs.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(node, NextNode): - op = node.operand - - if isinstance(op, AndNode): - new_node = AndNode(NextNode(op.left), op.right) - return MutationResult(new_node, MisconceptionCode.BadStateIndex) - - if isinstance(op, NextNode): - # Count the chain of Nexts - x = op - next_count = 1 # Already have one Next from node - while isinstance(x, NextNode): - next_count += 1 - x = x.operand - - # Randomly add or remove 1-2 Nexts, but ensure we stay within reasonable bounds - change = random.choice([-2, -1, 1, 2]) - new_count = next_count + change - - # Ensure new_count is at least 1 and different from original - if new_count < 1: - new_count = 1 - if new_count == next_count: - # If change resulted in same count, adjust - new_count = next_count + (1 if change > 0 else -1) - new_count = max(1, new_count) - - # Build new chain with new_count Nexts - result = x - for _ in range(new_count): - result = NextNode(result) - - return MutationResult(result, MisconceptionCode.BadStateIndex) - - return MutationResult(node) + if res.misconception: + # Store just the path, we'll apply the mutation later + locations.append(list(path)) + + # Recurse into children + if isinstance(node, UnaryOperatorNode): + locations.extend(collectAllMutationLocations(node.operand, f, path + ['operand'])) + elif isinstance(node, BinaryOperatorNode): + locations.extend(collectAllMutationLocations(node.left, f, path + ['left'])) + locations.extend(collectAllMutationLocations(node.right, f, path + ['right'])) + + return locations + + +def applyMutationAtPath(node, f, path): + """ + Apply a mutation function f at a specific path in the tree. + Path is a list of 'left', 'right', or 'operand' directions. + + Note: This function modifies the node tree in-place and uses a pattern + where child_result.node is reassigned to point to the parent node. + This is intentional and matches the pattern used in applyTilFirst. + The caller should pass a deep copy if the original needs to be preserved. + """ + if not path: + # We're at the target node, apply the mutation + return f(node) + + # Navigate to the target location + direction = path[0] + remaining_path = path[1:] + + if isinstance(node, UnaryOperatorNode) and direction == 'operand': + child_result = applyMutationAtPath(node.operand, f, remaining_path) + # Thread the result back through the parent: replace child with mutated version, + # then update result to point to the whole subtree + node.operand = child_result.node + child_result.node = node + return child_result + elif isinstance(node, BinaryOperatorNode) and direction == 'left': + child_result = applyMutationAtPath(node.left, f, remaining_path) + node.left = child_result.node + child_result.node = node + return child_result + elif isinstance(node, BinaryOperatorNode) and direction == 'right': + child_result = applyMutationAtPath(node.right, f, remaining_path) + node.right = child_result.node + child_result.node = node + return child_result + + # Invalid path - this indicates a bug in path generation + raise ValueError(f"Invalid path: cannot apply direction '{direction}' to node of type {type(node).__name__}") + + +def applyTilFirstRandom(node, f): + """ + Apply mutation f to a randomly selected location in the tree where it's applicable. + This ensures diverse mutations when multiple locations are possible. + Use this for simple mutations like ImplicitG/ImplicitF where we want to randomly + select from all possible application sites. + """ + # Collect all possible mutation locations + locations = collectAllMutationLocations(node, f) + + if not locations: + return MutationResult(node) + + # Randomly select one location + path = random.choice(locations) + + # Apply the mutation at the selected location + return applyMutationAtPath(node, f, path) + + +def applyTilFirst(node, f): + """ + Apply mutation f at the first applicable location found (depth-first search). + This is the original behavior, used for complex mutations that should be applied + as a unit at the first matching location. + """ + res = f(node) + if res.misconception: + return res + + if isinstance(node, UnaryOperatorNode): + res = applyTilFirst(node.operand, f) + node.operand = res.node + res.node = node + return res + + if isinstance(node, BinaryOperatorNode): + res_left = applyTilFirst(node.left, f) + res_right = applyTilFirst(node.right, f) + + random_index = random.randint(0, 1) + choose_left = res_left.misconception and (not res_right.misconception or random_index == 0) + choose_right = res_right.misconception and (not res_left.misconception or random_index == 1) + + if choose_left: + node.left = res_left.node + res_left.node = node + return res_left + elif choose_right: + node.right = res_right.node + res_right.node = node + return res_right + + return MutationResult(node) + + +def applyPrecedence(node): + if isinstance(node, BinaryOperatorNode): + if isinstance(node.right, BinaryOperatorNode): + new_top = node.right + node.right = new_top.left + new_top.left = node + return MutationResult(new_top, MisconceptionCode.Precedence) + + return MutationResult(node) + + +def applyExclusiveU(node): + """ + Detect patterns where Until is used with explicit disjointness/exclusivity. + ExclusiveU misconception: treating "x U y" as if x and y cannot both be true. + """ + if isinstance(node, BinaryOperatorNode) and node.operator == UntilNode.symbol: + x = node.left + rhs = node.right + + # Pattern 1: x U (!x & y) → x U y + # Student explicitly enforces disjointness + if isinstance(rhs, BinaryOperatorNode) and rhs.operator == AndNode.symbol: + y = rhs.right + + if isinstance(rhs.left, UnaryOperatorNode) and rhs.left.operator == NotNode.symbol and LTLNode.equiv(rhs.left.operand, x): + return MutationResult(UntilNode(x, y), MisconceptionCode.ExclusiveU) + + # Pattern 1b: x U (y & !x) → x U y (order swapped) + if isinstance(rhs.right, UnaryOperatorNode) and rhs.right.operator == NotNode.symbol and LTLNode.equiv(rhs.right.operand, x): + return MutationResult(UntilNode(x, rhs.left), MisconceptionCode.ExclusiveU) + + # Pattern 2: x U (x -> y) → x U y + # Student thinks "x U (x implies y)" enforces that y happens after x stops + if isinstance(rhs, ImpliesNode) and LTLNode.equiv(rhs.left, x): + return MutationResult(UntilNode(x, rhs.right), MisconceptionCode.ExclusiveU) + + # Pattern 3: x U (!x | y) → x U y + # Student thinks "x U (!x or y)" ensures exclusivity + if isinstance(rhs, OrNode): + if isinstance(rhs.left, NotNode) and LTLNode.equiv(rhs.left.operand, x): + return MutationResult(UntilNode(x, rhs.right), MisconceptionCode.ExclusiveU) + if isinstance(rhs.right, NotNode) and LTLNode.equiv(rhs.right.operand, x): + return MutationResult(UntilNode(x, rhs.left), MisconceptionCode.ExclusiveU) + + # Reverse: x U y → one of the ExclusiveU misconception variants + # The correct formula is x U y, but a student with the ExclusiveU + # misconception might write any of these, so we randomly choose one. + variant = random.choice([ + UntilNode(x, AndNode(NotNode(x), rhs)), # x U (!x & y) + UntilNode(x, ImpliesNode(x, rhs)), # x U (x -> y) + UntilNode(x, OrNode(NotNode(x), rhs)), # x U (!x | y) + ]) + return MutationResult(variant, MisconceptionCode.ExclusiveU) + + # Pattern 4: (x U y) & G(x -> !y) → x U y + # Student adds a global constraint that x and y are mutually exclusive + if isinstance(node, AndNode): + left = node.left + right = node.right + + # Check if one side is Until and other is G(x -> !y) + until_node = None + constraint_node = None + + if isinstance(left, UntilNode) and isinstance(right, GloballyNode): + until_node = left + constraint_node = right.operand + elif isinstance(right, UntilNode) and isinstance(left, GloballyNode): + until_node = right + constraint_node = left.operand + + if until_node and constraint_node and isinstance(constraint_node, ImpliesNode): + x = until_node.left + y = until_node.right + + # Check if constraint is x -> !y + if LTLNode.equiv(constraint_node.left, x): + if isinstance(constraint_node.right, NotNode) and LTLNode.equiv(constraint_node.right.operand, y): + return MutationResult(until_node, MisconceptionCode.ExclusiveU) + + # Check if constraint is y -> !x + if LTLNode.equiv(constraint_node.left, y): + if isinstance(constraint_node.right, NotNode) and LTLNode.equiv(constraint_node.right.operand, x): + return MutationResult(until_node, MisconceptionCode.ExclusiveU) + + # Pattern 5: (x U y) & G!(x & y) → x U y + # Student adds "globally not both" constraint + if isinstance(node, AndNode): + left = node.left + right = node.right + + until_node = None + constraint_node = None + + if isinstance(left, UntilNode) and isinstance(right, GloballyNode): + until_node = left + constraint_node = right.operand + elif isinstance(right, UntilNode) and isinstance(left, GloballyNode): + until_node = right + constraint_node = left.operand + + if until_node and constraint_node: + if isinstance(constraint_node, NotNode) and isinstance(constraint_node.operand, AndNode): + and_node = constraint_node.operand + x = until_node.left + y = until_node.right + + # Check if it's !(x & y) + if (LTLNode.equiv(and_node.left, x) and LTLNode.equiv(and_node.right, y)) or \ + (LTLNode.equiv(and_node.right, x) and LTLNode.equiv(and_node.left, y)): + return MutationResult(until_node, MisconceptionCode.ExclusiveU) + + return MutationResult(node) + + +def applyImplicitG(node): + if isinstance(node, UnaryOperatorNode) and node.operator == GloballyNode.symbol: + return MutationResult(node.operand, MisconceptionCode.ImplicitG) + + return MutationResult(node) + + +def applyImplicitF(node): + if isinstance(node, UnaryOperatorNode) and node.operator == FinallyNode.symbol: + return MutationResult(node.operand, MisconceptionCode.ImplicitF) + + return MutationResult(node) + + +def applyImplicitPrefix(node): + if isinstance(node, UntilNode): + lhs = node.left + rhs = node.right + + if isinstance(lhs, NotNode) and LTLNode.equiv(lhs.operand, rhs): + return MutationResult(FinallyNode(rhs), MisconceptionCode.OtherImplicit) + + if isinstance(rhs, GloballyNode) and LTLNode.equiv(lhs, rhs.operand): + return MutationResult(AndNode(lhs, FinallyNode(rhs)), MisconceptionCode.OtherImplicit) + + if isinstance(node, AndNode): + lhs = node.left + rhs = node.right + + if isinstance(lhs, FinallyNode) and isinstance(rhs, GloballyNode): + rhs_operand = rhs.operand + if isinstance(rhs_operand, ImpliesNode): + rhs_operand_lhs = rhs_operand.left + rhs_operand_rhs = rhs_operand.right + + if LTLNode.equiv(lhs.operand, rhs_operand_lhs) and isinstance(rhs_operand_rhs, NextNode) and isinstance(rhs_operand_rhs.operand, GloballyNode) and LTLNode.equiv(rhs_operand_lhs, rhs_operand_rhs.operand.operand): + return MutationResult(AndNode(lhs.operand, NextNode(rhs)), MisconceptionCode.OtherImplicit) + + if isinstance(node, NextNode): + return MutationResult(FinallyNode(node.operand), MisconceptionCode.OtherImplicit) + + return MutationResult(node) + + + + +def applyUnderconstraint(node): + if isinstance(node, BinaryOperatorNode): + n = random.choice([node.left, node.right]) + return MutationResult(n, MisconceptionCode.OtherImplicit) + ## TODO: Yes, but this shouldn't remove F / G constraints (these aren't covered by the other code) + elif isinstance(node, UnaryOperatorNode): + return MutationResult(node.operand, MisconceptionCode.OtherImplicit) + else: + return MutationResult(node) + + +def applyWeakU(node): + if isinstance(node, UntilNode): + lhs = node.left + # Interpret until as weak-until: RHS may never happen if LHS stays true + new_node = OrNode(node, GloballyNode(lhs)) + return MutationResult(new_node, MisconceptionCode.WeakU) + + return MutationResult(node) + + +def applyBadStateQuantification(node): + if isinstance(node, GloballyNode): + op = node.operand + return MutationResult(FinallyNode(op), MisconceptionCode.BadStateQuantification) + + if isinstance(node, FinallyNode): + op = node.operand + return MutationResult(GloballyNode(op), MisconceptionCode.BadStateQuantification) + + if isinstance(node, UntilNode): + lhs = node.left + rhs = node.right + + new_node = random.choice([ + UntilNode(FinallyNode(lhs), rhs), + UntilNode(GloballyNode(lhs), rhs), + UntilNode(lhs, FinallyNode(rhs)), + UntilNode(lhs, GloballyNode(rhs)), + UntilNode(rhs, lhs) + ]) + return MutationResult(new_node, MisconceptionCode.BadStateQuantification) + + return MutationResult(node) + + +def applyBadStateIndex(node): + if isinstance(node, UntilNode): + lhs = node.left + rhs = node.right + + if isinstance(rhs, AndNode) and isinstance(rhs.right, FinallyNode): + new_node = AndNode(UntilNode(lhs, rhs.left), rhs.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(rhs, AndNode) and isinstance(rhs.right, GloballyNode): + new_node = AndNode(UntilNode(lhs, rhs.left), rhs.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(rhs, OrNode) and isinstance(rhs.right, FinallyNode): + new_node = OrNode(UntilNode(lhs, rhs.left), rhs.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(rhs, OrNode) and isinstance(rhs.right, GloballyNode): + new_node = OrNode(UntilNode(lhs, rhs.left), rhs.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(rhs, ImpliesNode) and isinstance(rhs.right, FinallyNode): + new_node = ImpliesNode(UntilNode(lhs, rhs.left), rhs.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(rhs, ImpliesNode) and isinstance(rhs.right, GloballyNode): + new_node = ImpliesNode(UntilNode(lhs, rhs.left), rhs.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(node, NextNode): + op = node.operand + + if isinstance(op, AndNode): + new_node = AndNode(NextNode(op.left), op.right) + return MutationResult(new_node, MisconceptionCode.BadStateIndex) + + if isinstance(op, NextNode): + # Count the chain of Nexts + x = op + next_count = 1 # Already have one Next from node + while isinstance(x, NextNode): + next_count += 1 + x = x.operand + + # Randomly add or remove 1-2 Nexts, but ensure we stay within reasonable bounds + change = random.choice([-2, -1, 1, 2]) + new_count = next_count + change + + # Ensure new_count is at least 1 and different from original + if new_count < 1: + new_count = 1 + if new_count == next_count: + # If change resulted in same count, adjust + new_count = next_count + (1 if change > 0 else -1) + new_count = max(1, new_count) + + # Build new chain with new_count Nexts + result = x + for _ in range(new_count): + result = NextNode(result) + + return MutationResult(result, MisconceptionCode.BadStateIndex) + + return MutationResult(node) diff --git a/ltlmutator/src/ltlmutator/grammar/__init__.py b/ltlmutator/src/ltlmutator/grammar/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/ltl.g4 b/ltlmutator/src/ltlmutator/grammar/ltl.g4 similarity index 100% rename from src/ltl.g4 rename to ltlmutator/src/ltlmutator/grammar/ltl.g4 diff --git a/src/ltl.interp b/ltlmutator/src/ltlmutator/grammar/ltl.interp similarity index 100% rename from src/ltl.interp rename to ltlmutator/src/ltlmutator/grammar/ltl.interp diff --git a/src/ltl.tokens b/ltlmutator/src/ltlmutator/grammar/ltl.tokens similarity index 100% rename from src/ltl.tokens rename to ltlmutator/src/ltlmutator/grammar/ltl.tokens diff --git a/src/ltlLexer.interp b/ltlmutator/src/ltlmutator/grammar/ltlLexer.interp similarity index 100% rename from src/ltlLexer.interp rename to ltlmutator/src/ltlmutator/grammar/ltlLexer.interp diff --git a/src/ltlLexer.py b/ltlmutator/src/ltlmutator/grammar/ltlLexer.py similarity index 97% rename from src/ltlLexer.py rename to ltlmutator/src/ltlmutator/grammar/ltlLexer.py index c4943fb..f45b0f6 100644 --- a/src/ltlLexer.py +++ b/ltlmutator/src/ltlmutator/grammar/ltlLexer.py @@ -3,9 +3,9 @@ from io import StringIO import sys if sys.version_info[1] > 5: - from typing import TextIO + from typing import TextIO else: - from typing.io import TextIO + from typing.io import TextIO def serializedATN(): @@ -79,15 +79,15 @@ class ltlLexer(Lexer): modeNames = [ "DEFAULT_MODE" ] literalNames = [ "", - "'!'", "'X'", "'AFTER'", "'NEXT_STATE'", "'F'", "'EVENTUALLY'", - "'G'", "'ALWAYS'", "'&'", "'|'", "'U'", "'UNTIL'", "'->'", "'<->'", + "'!'", "'X'", "'AFTER'", "'NEXT_STATE'", "'F'", "'EVENTUALLY'", + "'G'", "'ALWAYS'", "'&'", "'|'", "'U'", "'UNTIL'", "'->'", "'<->'", "'('", "')'" ] symbolicNames = [ "", "ID", "WS" ] - ruleNames = [ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", - "T__7", "T__8", "T__9", "T__10", "T__11", "T__12", "T__13", + ruleNames = [ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", + "T__7", "T__8", "T__9", "T__10", "T__11", "T__12", "T__13", "T__14", "T__15", "ID", "WS" ] grammarFileName = "ltl.g4" @@ -98,5 +98,3 @@ def __init__(self, input=None, output:TextIO = sys.stdout): self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) self._actions = None self._predicates = None - - diff --git a/src/ltlLexer.tokens b/ltlmutator/src/ltlmutator/grammar/ltlLexer.tokens similarity index 100% rename from src/ltlLexer.tokens rename to ltlmutator/src/ltlmutator/grammar/ltlLexer.tokens diff --git a/src/ltlListener.py b/ltlmutator/src/ltlmutator/grammar/ltlListener.py similarity index 96% rename from src/ltlListener.py rename to ltlmutator/src/ltlmutator/grammar/ltlListener.py index fcfd998..a54a7ca 100644 --- a/src/ltlListener.py +++ b/ltlmutator/src/ltlmutator/grammar/ltlListener.py @@ -1,9 +1,6 @@ # Generated from ltl.g4 by ANTLR 4.13.2 from antlr4 import * -if "." in __name__: - from .ltlParser import ltlParser -else: - from ltlParser import ltlParser +from .ltlParser import ltlParser # This class defines a complete listener for a parse tree produced by ltlParser. class ltlListener(ParseTreeListener): @@ -126,4 +123,4 @@ def exitAtomicFormula(self, ctx:ltlParser.AtomicFormulaContext): -del ltlParser \ No newline at end of file +del ltlParser diff --git a/src/ltlParser.py b/ltlmutator/src/ltlmutator/grammar/ltlParser.py similarity index 99% rename from src/ltlParser.py rename to ltlmutator/src/ltlmutator/grammar/ltlParser.py index f6f68dd..ec7b70b 100644 --- a/src/ltlParser.py +++ b/ltlmutator/src/ltlmutator/grammar/ltlParser.py @@ -38,14 +38,14 @@ class ltlParser ( Parser ): sharedContextCache = PredictionContextCache() - literalNames = [ "", "'!'", "'X'", "'AFTER'", "'NEXT_STATE'", - "'F'", "'EVENTUALLY'", "'G'", "'ALWAYS'", "'&'", "'|'", + literalNames = [ "", "'!'", "'X'", "'AFTER'", "'NEXT_STATE'", + "'F'", "'EVENTUALLY'", "'G'", "'ALWAYS'", "'&'", "'|'", "'U'", "'UNTIL'", "'->'", "'<->'", "'('", "')'" ] - symbolicNames = [ "", "", "", "", - "", "", "", "", - "", "", "", "", - "", "", "", "", + symbolicNames = [ "", "", "", "", + "", "", "", "", + "", "", "", "", + "", "", "", "", "", "ID", "WS" ] RULE_ltl = 0 @@ -141,7 +141,7 @@ def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): def getRuleIndex(self): return ltlParser.RULE_formula - + def copyFrom(self, ctx:ParserRuleContext): super().copyFrom(ctx) @@ -539,7 +539,7 @@ def formula(self, _p:int=0): self.formula(4) pass - + self.state = 44 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,2,self._ctx) @@ -608,24 +608,19 @@ def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int): def formula_sempred(self, localctx:FormulaContext, predIndex:int): if predIndex == 0: return self.precpred(self._ctx, 7) - + if predIndex == 1: return self.precpred(self._ctx, 6) - + if predIndex == 2: return self.precpred(self._ctx, 5) - + if predIndex == 3: return self.precpred(self._ctx, 4) - + if predIndex == 4: return self.precpred(self._ctx, 3) - - - - - diff --git a/src/ltlnode.py b/ltlmutator/src/ltlmutator/ltlnode.py similarity index 71% rename from src/ltlnode.py rename to ltlmutator/src/ltlmutator/ltlnode.py index 117f057..05439dd 100644 --- a/src/ltlnode.py +++ b/ltlmutator/src/ltlmutator/ltlnode.py @@ -1,491 +1,539 @@ -# Description: This file contains the classes for the nodes of the LTL syntax tree. - -import os -import random - -### TODO: Ideally, this should not be in -### src, but mocked in the test directory. - - -from spotutils import areEquivalent - - -from ltlListener import ltlListener -from antlr4 import CommonTokenStream, ParseTreeWalker -from antlr4 import ParseTreeWalker, CommonTokenStream, InputStream -from ltlLexer import ltlLexer -from ltlParser import ltlParser -from abc import ABC, abstractmethod -import ltltoeng - - -SUPPORTED_SYNTAXES = ['Classic', 'Forge', 'Electrum'] - -## Should these come from the lexer instead of being placed here -IMPLIES_SYMBOL = '->' -EQUIVALENCE_SYMBOL = '<->' -AND_SYMBOL = '&' -OR_SYMBOL = '|' -NOT_SYMBOL = '!' -NEXT_SYMBOL = 'X' -GLOBALLY_SYMBOL = 'G' -FINALLY_SYMBOL = 'F' -UNTIL_SYMBOL = 'U' - -# Operator precedence (higher number = binds tighter) -OPERATOR_PRECEDENCE = { - 'Until': 1, - 'Or': 2, - 'And': 3, - 'Not': 4, - 'Next': 5, - 'Globally': 5, - 'Finally': 5, - 'Literal': 10 -} - - -class LTLNode(ABC): - def __init__(self, type): - self.type = type - - """ - LTL Node in Classic/ Spot Syntax - """ - @abstractmethod - def __str__(self): - pass - - """ - LTL Node in English - """ - @abstractmethod - def __to_english__(self): - x = ltltoeng.apply_special_pattern_if_possible(self) - if x is not None: - return x - # We should draw inspiration from: - # https://matthewbdwyer.github.io/psp/patterns/ltl.html - pass - - """ - LTLNode in Forge Syntax - """ - @abstractmethod - def __forge__(self): - pass - - """ - LTLNode in Electrum Syntax - """ - @abstractmethod - def __electrum__(self): - pass - - - @staticmethod - def equiv(formula1, formula2): - return areEquivalent(formula1, formula2) - -class ltlListenerImpl(ltlListener) : - def __init__(self): - self.stack = [] - - def exitDisjunction(self, ctx): - right = self.stack.pop() - left = self.stack.pop() - orNode = OrNode(left, right) - self.stack.append(orNode) - - def exitConjunction(self, ctx): - right = self.stack.pop() - left = self.stack.pop() - andNode = AndNode(left, right) - self.stack.append(andNode) - - def exitU(self, ctx): - right = self.stack.pop() - left = self.stack.pop() - untilNode = UntilNode(left, right) - self.stack.append(untilNode) - - def exitImplication(self, ctx): - right = self.stack.pop() - left = self.stack.pop() - impliesNode = ImpliesNode(left, right) - self.stack.append(impliesNode) - - def exitEquivalence(self, ctx): - right = self.stack.pop() - left = self.stack.pop() - equivNode = EquivalenceNode(left, right) - self.stack.append(equivNode) - - def exitX(self, ctx): - operand = self.stack.pop() - nextNode = NextNode(operand) - self.stack.append(nextNode) - - def exitF(self, ctx): - operand = self.stack.pop() - finallyNode = FinallyNode(operand) - self.stack.append(finallyNode) - - def exitG(self, ctx): - operand = self.stack.pop() - globallyNode = GloballyNode(operand) - self.stack.append(globallyNode) - - def exitNot(self, ctx): - operand = self.stack.pop() - notNode = NotNode(operand) - self.stack.append(notNode) - - def exitParentheses(self, ctx): - formula = self.stack.pop() - self.stack.append(formula) - - def exitAtomicFormula(self, ctx): - value = ctx.ID().getText() - literalNode = LiteralNode(value) - self.stack.append(literalNode) - - def getRootFormula(self): - return self.stack[-1] - - -class UnaryOperatorNode(LTLNode): - def __init__(self, operator, operand): - super().__init__('UnaryOperator') - self.operator = operator - self.operand = operand - - def __str__(self): - return f'({self.operator} {str(self.operand)})' - - def __to_english__(self): - x = ltltoeng.apply_special_pattern_if_possible(self) - if x is not None: - return x - return self.__str__() - - def __forge__(self): - return f"({self.operator} {self.operand.__forge__()})" - - def __electrum__(self): - return f"({self.operator} {self.operand.__electrum__()})" - - -class BinaryOperatorNode(LTLNode): - def __init__(self, operator, left, right): - super().__init__('BinaryOperator') - self.operator = operator - self.left = left - self.right = right - - def __str__(self): - return f'({str(self.left)} {self.operator} {str(self.right)})' - - def __to_english__(self): - x = ltltoeng.apply_special_pattern_if_possible(self) - if x is not None: - return x - return self.__str__() - - def __forge__(self): - return f"({self.left.__forge__()} {self.operator} {self.right.__forge__()})" - - def __electrum__(self): - return f"({self.left.__electrum__()} {self.operator} {self.right.__electrum__()})" - - -class LiteralNode(LTLNode): - def __init__(self, value): - super().__init__('Literal') - self.value = value - - def __str__(self): - return self.value - - def __to_english__(self): - x = ltltoeng.apply_special_pattern_if_possible(self) - if x is not None: - return x - - # For literals, use simpler phrasing - # Note: We don't capitalize here because the literal is in quotes - # and should remain as-is per capitalize_sentence() logic - return f"'{self.value}'" - - def __forge__(self): - return self.value - - def __electrum__(self): - return self.value - - -class UntilNode(BinaryOperatorNode): - symbol = UNTIL_SYMBOL - 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('.') - - # For simple literals, provide more natural alternatives - if type(self.left) is LiteralNode and type(self.right) is LiteralNode: - patterns = [ - f"{lhs} until {rhs}", - f"{lhs} holds until {rhs} occurs", - f"maintain {lhs} until {rhs}" - ] - return ltltoeng.choose_best_sentence(patterns) - - return f"{lhs} until {rhs}" - - def __forge__(self): - return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})" - - def __electrum__(self): - return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})" - - -class NextNode(UnaryOperatorNode): - symbol = NEXT_SYMBOL - 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 f"in the next step, {op}" - - def __forge__(self): - return f"(NEXT_STATE {self.operand.__forge__()})" - - def __electrum__(self): - return f"(AFTER {self.operand.__electrum__()})" - - -class GloballyNode(UnaryOperatorNode): - symbol = GLOBALLY_SYMBOL - 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('.') - - # Provide more natural alternatives - patterns = [ - f"at all times, {op}", - f"{op} is always true", - f"{op} holds at all times", - f"it is always the case that {op}" - ] - - english = ltltoeng.choose_best_sentence(patterns) - return english - - def __forge__(self): - return f"(ALWAYS {self.operand.__forge__()})" - - def __electrum__(self): - return f"(ALWAYS {self.operand.__electrum__()})" - - -class FinallyNode(UnaryOperatorNode): - symbol = FINALLY_SYMBOL - def __init__(self, operand): - super().__init__(FinallyNode.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('.') - - # Provide more natural alternatives - if type(self.operand) is LiteralNode: - patterns = [ - f"eventually, {op}", - f"{op} will eventually occur", - f"at some point, {op} will hold" - ] - return ltltoeng.choose_best_sentence(patterns) - - return f"eventually, {op}" - - def __forge__(self): - return f"(EVENTUALLY {self.operand.__forge__()})" - - def __electrum__(self): - return f"(EVENTUALLY {self.operand.__electrum__()})" - - -class OrNode(BinaryOperatorNode): - - symbol = OR_SYMBOL - - 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('.') - - # Provide alternatives for simple literals - if type(self.left) is LiteralNode and type(self.right) is LiteralNode: - patterns = [ - f"either {lhs} or {rhs}", - f"{lhs} or {rhs}", - f"at least one of {lhs} or {rhs}" - ] - return ltltoeng.choose_best_sentence(patterns) - - return f"either {lhs} or {rhs}" - - - - -class AndNode(BinaryOperatorNode): - symbol = AND_SYMBOL - 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('.') - - # Provide alternatives for simple literals - if type(self.left) is LiteralNode and type(self.right) is LiteralNode: - patterns = [ - f"both {lhs} and {rhs}", - f"{lhs} and {rhs}", - f"{lhs} together with {rhs}" - ] - return ltltoeng.choose_best_sentence(patterns) - - return f"both {lhs} and {rhs}" - - -class NotNode(UnaryOperatorNode): - symbol = NOT_SYMBOL - def __init__(self, operand): - super().__init__(NotNode.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('.') - - ## If the operand is a literal, we can just negate it with alternatives - if isinstance(self.operand, LiteralNode): - patterns = [ - f"not {op}", - f"{op} does not hold", - f"{op} is false" - ] - return ltltoeng.choose_best_sentence(patterns) - 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('.') - - 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 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('.') - - 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 the most fluent pattern rather than picking randomly - english = ltltoeng.choose_best_sentence(patterns) - return english - - - -def parse_ltl_string(s): - # Create an input stream from the string - input_stream = InputStream(s) - - # Create a lexer and a token stream - lexer = ltlLexer(input_stream) - token_stream = CommonTokenStream(lexer) - - # Create the parser and parse the input - parser = ltlParser(token_stream) - tree = parser.ltl() - - # Create a listener - listener = ltlListenerImpl() - - # Create a ParseTreeWalker and walk the parse tree with the listener - walker = ParseTreeWalker() - walker.walk(listener, tree) - - # Get the root of the syntax tree - root = listener.getRootFormula() - - return root - - - +# Description: This file contains the classes for the nodes of the LTL syntax tree. + +import os +import random + +from .spotutils import areEquivalent + + +from .grammar.ltlListener import ltlListener +from antlr4 import CommonTokenStream, ParseTreeWalker +from antlr4 import ParseTreeWalker, CommonTokenStream, InputStream +from .grammar.ltlLexer import ltlLexer +from .grammar.ltlParser import ltlParser +from abc import ABC, abstractmethod + + +# Lazy-load ltltoeng: it's an optional dependency not included in this package. +# When available (e.g., in the full LTLTutor app), __to_english__() uses it +# for rich English translations. When unavailable, falls back to __str__(). +_ltltoeng = None +_ltltoeng_checked = False + +def _get_ltltoeng(): + global _ltltoeng, _ltltoeng_checked + if not _ltltoeng_checked: + try: + import ltltoeng + _ltltoeng = ltltoeng + except ImportError: + _ltltoeng = None + _ltltoeng_checked = True + return _ltltoeng + + +SUPPORTED_SYNTAXES = ['Classic', 'Forge', 'Electrum'] + +## Should these come from the lexer instead of being placed here +IMPLIES_SYMBOL = '->' +EQUIVALENCE_SYMBOL = '<->' +AND_SYMBOL = '&' +OR_SYMBOL = '|' +NOT_SYMBOL = '!' +NEXT_SYMBOL = 'X' +GLOBALLY_SYMBOL = 'G' +FINALLY_SYMBOL = 'F' +UNTIL_SYMBOL = 'U' + +# Operator precedence (higher number = binds tighter) +OPERATOR_PRECEDENCE = { + 'Until': 1, + 'Or': 2, + 'And': 3, + 'Not': 4, + 'Next': 5, + 'Globally': 5, + 'Finally': 5, + 'Literal': 10 +} + + +class LTLNode(ABC): + def __init__(self, type): + self.type = type + + """ + LTL Node in Classic/ Spot Syntax + """ + @abstractmethod + def __str__(self): + pass + + """ + LTL Node in English + """ + @abstractmethod + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.apply_special_pattern_if_possible(self) + if x is not None: + return x + # We should draw inspiration from: + # https://matthewbdwyer.github.io/psp/patterns/ltl.html + pass + + """ + LTLNode in Forge Syntax + """ + @abstractmethod + def __forge__(self): + pass + + """ + LTLNode in Electrum Syntax + """ + @abstractmethod + def __electrum__(self): + pass + + + @staticmethod + def equiv(formula1, formula2): + return areEquivalent(formula1, formula2) + +class ltlListenerImpl(ltlListener) : + def __init__(self): + self.stack = [] + + def exitDisjunction(self, ctx): + right = self.stack.pop() + left = self.stack.pop() + orNode = OrNode(left, right) + self.stack.append(orNode) + + def exitConjunction(self, ctx): + right = self.stack.pop() + left = self.stack.pop() + andNode = AndNode(left, right) + self.stack.append(andNode) + + def exitU(self, ctx): + right = self.stack.pop() + left = self.stack.pop() + untilNode = UntilNode(left, right) + self.stack.append(untilNode) + + def exitImplication(self, ctx): + right = self.stack.pop() + left = self.stack.pop() + impliesNode = ImpliesNode(left, right) + self.stack.append(impliesNode) + + def exitEquivalence(self, ctx): + right = self.stack.pop() + left = self.stack.pop() + equivNode = EquivalenceNode(left, right) + self.stack.append(equivNode) + + def exitX(self, ctx): + operand = self.stack.pop() + nextNode = NextNode(operand) + self.stack.append(nextNode) + + def exitF(self, ctx): + operand = self.stack.pop() + finallyNode = FinallyNode(operand) + self.stack.append(finallyNode) + + def exitG(self, ctx): + operand = self.stack.pop() + globallyNode = GloballyNode(operand) + self.stack.append(globallyNode) + + def exitNot(self, ctx): + operand = self.stack.pop() + notNode = NotNode(operand) + self.stack.append(notNode) + + def exitParentheses(self, ctx): + formula = self.stack.pop() + self.stack.append(formula) + + def exitAtomicFormula(self, ctx): + value = ctx.ID().getText() + literalNode = LiteralNode(value) + self.stack.append(literalNode) + + def getRootFormula(self): + return self.stack[-1] + + +class UnaryOperatorNode(LTLNode): + def __init__(self, operator, operand): + super().__init__('UnaryOperator') + self.operator = operator + self.operand = operand + + def __str__(self): + return f'({self.operator} {str(self.operand)})' + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.apply_special_pattern_if_possible(self) + if x is not None: + return x + return self.__str__() + + def __forge__(self): + return f"({self.operator} {self.operand.__forge__()})" + + def __electrum__(self): + return f"({self.operator} {self.operand.__electrum__()})" + + +class BinaryOperatorNode(LTLNode): + def __init__(self, operator, left, right): + super().__init__('BinaryOperator') + self.operator = operator + self.left = left + self.right = right + + def __str__(self): + return f'({str(self.left)} {self.operator} {str(self.right)})' + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.apply_special_pattern_if_possible(self) + if x is not None: + return x + return self.__str__() + + def __forge__(self): + return f"({self.left.__forge__()} {self.operator} {self.right.__forge__()})" + + def __electrum__(self): + return f"({self.left.__electrum__()} {self.operator} {self.right.__electrum__()})" + + +class LiteralNode(LTLNode): + def __init__(self, value): + super().__init__('Literal') + self.value = value + + def __str__(self): + return self.value + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.apply_special_pattern_if_possible(self) + if x is not None: + return x + + # For literals, use simpler phrasing + # Note: We don't capitalize here because the literal is in quotes + # and should remain as-is per capitalize_sentence() logic + return f"'{self.value}'" + + def __forge__(self): + return self.value + + def __electrum__(self): + return self.value + + +class UntilNode(BinaryOperatorNode): + symbol = UNTIL_SYMBOL + def __init__(self, left, right): + super().__init__(UntilNode.symbol, left, right) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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('.') + + # For simple literals, provide more natural alternatives + if eng is not None and type(self.left) is LiteralNode and type(self.right) is LiteralNode: + patterns = [ + f"{lhs} until {rhs}", + f"{lhs} holds until {rhs} occurs", + f"maintain {lhs} until {rhs}" + ] + return eng.choose_best_sentence(patterns) + + return f"{lhs} until {rhs}" + + def __forge__(self): + return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})" + + def __electrum__(self): + return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})" + + +class NextNode(UnaryOperatorNode): + symbol = NEXT_SYMBOL + def __init__(self, operand): + super().__init__(NextNode.symbol, operand) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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__()})" + + def __electrum__(self): + return f"(AFTER {self.operand.__electrum__()})" + + +class GloballyNode(UnaryOperatorNode): + symbol = GLOBALLY_SYMBOL + def __init__(self, operand): + super().__init__(GloballyNode.symbol, operand) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.apply_special_pattern_if_possible(self) + if x is not None: + return x + + op = self.operand.__to_english__().rstrip('.') + + # Provide more natural alternatives + patterns = [ + f"at all times, {op}", + f"{op} is always true", + f"{op} holds at all times", + f"it is always the case that {op}" + ] + + eng = _get_ltltoeng() + if eng is not None: + english = eng.choose_best_sentence(patterns) + return english + return patterns[0] + + def __forge__(self): + return f"(ALWAYS {self.operand.__forge__()})" + + def __electrum__(self): + return f"(ALWAYS {self.operand.__electrum__()})" + + +class FinallyNode(UnaryOperatorNode): + symbol = FINALLY_SYMBOL + def __init__(self, operand): + super().__init__(FinallyNode.symbol, operand) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.apply_special_pattern_if_possible(self) + if x is not None: + return x + op = self.operand.__to_english__().rstrip('.') + + # Provide more natural alternatives + if eng is not None and type(self.operand) is LiteralNode: + patterns = [ + f"eventually, {op}", + f"{op} will eventually occur", + f"at some point, {op} will hold" + ] + return eng.choose_best_sentence(patterns) + + return f"eventually, {op}" + + def __forge__(self): + return f"(EVENTUALLY {self.operand.__forge__()})" + + def __electrum__(self): + return f"(EVENTUALLY {self.operand.__electrum__()})" + + +class OrNode(BinaryOperatorNode): + + symbol = OR_SYMBOL + + def __init__(self, left, right): + super().__init__(OrNode.symbol, left, right) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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('.') + + # Provide alternatives for simple literals + if eng is not None and type(self.left) is LiteralNode and type(self.right) is LiteralNode: + patterns = [ + f"either {lhs} or {rhs}", + f"{lhs} or {rhs}", + f"at least one of {lhs} or {rhs}" + ] + return eng.choose_best_sentence(patterns) + + return f"either {lhs} or {rhs}" + + + + +class AndNode(BinaryOperatorNode): + symbol = AND_SYMBOL + def __init__(self, left, right): + super().__init__(AndNode.symbol, left, right) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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('.') + + # Provide alternatives for simple literals + if eng is not None and type(self.left) is LiteralNode and type(self.right) is LiteralNode: + patterns = [ + f"both {lhs} and {rhs}", + f"{lhs} and {rhs}", + f"{lhs} together with {rhs}" + ] + return eng.choose_best_sentence(patterns) + + return f"both {lhs} and {rhs}" + + +class NotNode(UnaryOperatorNode): + symbol = NOT_SYMBOL + def __init__(self, operand): + super().__init__(NotNode.symbol, operand) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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 with alternatives + if isinstance(self.operand, LiteralNode): + patterns = [ + f"not {op}", + f"{op} does not hold", + f"{op} is false" + ] + eng = _get_ltltoeng() + if eng is not None: + return eng.choose_best_sentence(patterns) + return patterns[0] + 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): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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('.') + + if eng is not None: + lhs = eng.normalize_embedded_clause(lhs) + rhs = eng.normalize_embedded_clause(rhs) + + # Potential patterns: + patterns = [ + f"if {lhs}, then {rhs}", + f"{lhs} implies {rhs}", + f"whenever {lhs}, then {rhs}" + ] + + # Choose the most fluent pattern rather than picking randomly + if eng is not None: + english = eng.choose_best_sentence(patterns) + return english + return patterns[0] + + +class EquivalenceNode(BinaryOperatorNode): + symbol = EQUIVALENCE_SYMBOL + def __init__(self, left, right): + super().__init__(EquivalenceNode.symbol, left, right) + + def __to_english__(self): + eng = _get_ltltoeng() + if eng is not None: + x = eng.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('.') + + if eng is not None: + lhs = eng.normalize_embedded_clause(lhs) + rhs = eng.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 the most fluent pattern rather than picking randomly + if eng is not None: + english = eng.choose_best_sentence(patterns) + return english + return patterns[0] + + + +def parse_ltl_string(s): + # Create an input stream from the string + input_stream = InputStream(s) + + # Create a lexer and a token stream + lexer = ltlLexer(input_stream) + token_stream = CommonTokenStream(lexer) + + # Create the parser and parse the input + parser = ltlParser(token_stream) + tree = parser.ltl() + + # Create a listener + listener = ltlListenerImpl() + + # Create a ParseTreeWalker and walk the parse tree with the listener + walker = ParseTreeWalker() + walker.walk(listener, tree) + + # Get the root of the syntax tree + root = listener.getRootFormula() + + return root diff --git a/src/spotutils.py b/ltlmutator/src/ltlmutator/spotutils.py similarity index 94% rename from src/spotutils.py rename to ltlmutator/src/ltlmutator/spotutils.py index 5a98eed..68253a7 100644 --- a/src/spotutils.py +++ b/ltlmutator/src/ltlmutator/spotutils.py @@ -1,277 +1,277 @@ -import spot -import random - - -DEFAULT_WEIGHT = 5 -DEFAULT_WEIGHT_TEMPORAL = 7 -DEFAULT_LTL_PRIORITIES = { - "ap" : DEFAULT_WEIGHT, - - "F": DEFAULT_WEIGHT_TEMPORAL, - "G": DEFAULT_WEIGHT_TEMPORAL, - "X": DEFAULT_WEIGHT_TEMPORAL, - - "U": DEFAULT_WEIGHT_TEMPORAL, - "and": DEFAULT_WEIGHT, - "or": DEFAULT_WEIGHT, - "equiv": DEFAULT_WEIGHT, - "implies":DEFAULT_WEIGHT, - "not": DEFAULT_WEIGHT, - ## TODO: Examine: Perhaps not so many trues and falses? - "false": 1, - "true":1, - "W":0, - "M":0, - "xor":0, - "R":0, - - ## Aren't these PSL not LTL - # "EConcat":0, - # "UConcat":0, - # "Closure":0, ## ? -} - - -def _count_trace_steps(trace): - """ - Count the number of steps in a trace string. - Traces use ';' as a step delimiter (e.g., 'a; b; cycle{c}' has 3 steps). - """ - return len(trace.split(';')) - - -def weighted_trace_choice(traces): - """ - Select a trace from a list of traces, with shorter traces slightly preferred. - Uses inverse step count weighting: weight = 1 / (1 + num_steps). - This gives shorter traces higher selection probability while still allowing - longer traces to be selected. - - Args: - traces: A list of trace strings to choose from - - Returns: - A randomly selected trace string, with shorter traces more likely to be chosen - """ - if not traces: - raise ValueError("Cannot choose from empty list of traces") - if len(traces) == 1: - return traces[0] - - # Calculate weights based on inverse step count - # Using 1 / (1 + num_steps) to slightly prefer shorter traces - weights = [1.0 / (1.0 + _count_trace_steps(t)) for t in traces] - - return random.choices(traces, weights=weights, k=1)[0] - - -def areEquivalent(formula1, formula2): - return isSufficientFor(formula1, formula2) and isNecessaryFor(formula1, formula2) - - - -''' -Returns true if f => g is a tautology -''' -def isSufficientFor(f, g): - - f = spot.parse_formula(str(f)) - g = spot.parse_formula(str(g)) - - - a_f = f.translate() - a_ng = spot.formula.Not(g).translate() - return spot.product(a_f, a_ng).is_empty() - - -''' -Returns true if g => f is a tautology -''' -def isNecessaryFor(f, g): - return isSufficientFor(g, f) - - -def areDisjoint(f, g): - ff = spot.parse_formula(str(f)) - gf = spot.parse_formula(str(g)) - - a_ff = ff.translate() - a_gf = gf.translate() - - return spot.product(a_ff, a_gf).is_empty() - - -def generate_accepting_words(automaton, max_runs=5): - """Generate up to max_runs distinct accepting words by excluding previously seen traces.""" - words = [] - current_aut = automaton - - for _ in range(max_runs): - # Check if current automaton is empty - if current_aut.is_empty(): - break - - run = current_aut.accepting_run() - if run: - # Convert run to a word that the automaton accepts - word = spot.twa_word(run) - word_str = str(word) - - # Only add if we haven't seen it (safety check) - if word_str not in words: - words.append(word_str) - - # Exclude this trace from future runs - try: - # Build automaton that accepts only this trace - trace_aut = word.as_automaton() - # Complement it (now accepts everything EXCEPT this trace) - not_trace_aut = spot.complement(trace_aut) - # Product with current automaton to exclude this trace - current_aut = spot.product(current_aut, not_trace_aut) - except Exception as e: - print(f"Warning: Could not exclude trace '{word_str}': {e}") - break - else: - break # Stop if no accepting run is found - return words - -def generate_accepted_traces(formula, max_traces=5): - # Parse the LTL formula - f = spot.formula(formula) - - # Translate the LTL formula to a Büchi automaton - automaton = f.translate() - - # Retrieve and return the acceptance condition - runs = generate_accepting_words(automaton, max_traces) - #w.as_automaton() shows the run as an automaton. - return runs - -## Generate traces accepted by f_accepted, and rejected by f_rejected -def generate_traces(f_accepted, f_rejected, max_traces=5): - # Parse the LTL formula - f_a = spot.formula(f_accepted) - f_r = spot.formula.Not(spot.formula(f_rejected)) - - f = spot.formula.And([f_a, f_r]) - automaton = f.translate() - runs = generate_accepting_words(automaton, max_traces) - #w.as_automaton() shows the run as an automaton. - return runs - - - -# https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/randltl.ipynb - -## TODO: Need to generate some sort of transform from Misconceptions to ltl_priorities -## That is -- each misconception should have some weight around related concepts -### Some are obvious : Implicit G means, add more G -### Some are less obvious: eg "BadStateIndex" - -def gen_rand_ltl(atoms, tree_size, ltl_priorities, num_formulae = 5): - - def to_priority_string(d): - return ','.join(f'{k}={v}' for k, v in d.items()) - - # Need to do the correct kind of manipulation here - ltl_priorities_string = to_priority_string(ltl_priorities) - - f = spot.randltl(atoms, tree_size=tree_size, ltl_priorities = ltl_priorities_string) - - return [str(next(f)) for _ in range(num_formulae)] - - -def is_trivial(formula_str): - """ - Check if a formula is a tautology or contradiction using SPOT. - - Args: - formula_str: String representation of an LTL formula - - Returns: - True if the formula simplifies to constant true (1) or false (0) - """ - try: - f = spot.formula(formula_str) - # Simplify and check if it's constant true (1) or false (0) - simplified = spot.simplify(f) - simplified_str = str(simplified) - return simplified_str in ['1', '0', 'true', 'false'] - except: - return False - - -def gen_small_rand_ltl(atoms, tree_size=3, max_attempts=10): - """ - Generate a single small non-trivial random LTL formula using SPOT. - Prioritizes atomic propositions and simple operators to avoid complexity. - - Args: - atoms: List of atomic proposition strings - tree_size: Maximum tree size for the formula (default 3) - max_attempts: Maximum number of attempts to find a non-trivial formula - - Returns: - String representation of a non-trivial LTL formula, or a random atom as fallback - """ - # Prioritize simple operators, keep tree size small - priorities = { - 'ap': 5, - 'G': 2, 'F': 2, 'X': 2, 'U': 3, - 'and': 4, 'or': 4, 'implies': 3, 'not': 3, - 'equiv': 1, 'xor': 0, 'R': 0, 'W': 0, 'M': 0, - 'true': 0, 'false': 0 - } - - for _ in range(max_attempts): - try: - formulas = gen_rand_ltl(atoms, tree_size, priorities, num_formulae=1) - formula_str = formulas[0] - - # Reject trivial formulas - if not is_trivial(formula_str): - return formula_str - except: - continue - - # Fallback to a simple literal if all attempts fail - return random.choice(atoms) - - -## Returns the Mana Pneulli classification of the formula -def get_mana_pneulli_class(formula): - - - - f = spot.formula(formula) - return spot.mp_class(f, 'v') - - -def get_aut_size(formula): - f = spot.formula(formula) - aut = spot.translate(f) - num_states = aut.num_states() - return num_states - - -### Given an LTL Trace, return if the formula is satisfied - -### This works on the spot kernel but not here. Why? -def is_trace_satisfied(trace, formula): - formula = str(formula) - trace = str(trace) - - # Parse the trace into a word - word = spot.parse_word(trace) - - # Words can be translated to automata - # w.as_automaton() - - # Translate the formula into an automaton - f = spot.formula(formula) - aut = f.translate() - wordaut = word.as_automaton() - - # Check if the automaton intersects with the word automaton - return aut.intersects(wordaut) \ No newline at end of file +import spot +import random + + +DEFAULT_WEIGHT = 5 +DEFAULT_WEIGHT_TEMPORAL = 7 +DEFAULT_LTL_PRIORITIES = { + "ap" : DEFAULT_WEIGHT, + + "F": DEFAULT_WEIGHT_TEMPORAL, + "G": DEFAULT_WEIGHT_TEMPORAL, + "X": DEFAULT_WEIGHT_TEMPORAL, + + "U": DEFAULT_WEIGHT_TEMPORAL, + "and": DEFAULT_WEIGHT, + "or": DEFAULT_WEIGHT, + "equiv": DEFAULT_WEIGHT, + "implies":DEFAULT_WEIGHT, + "not": DEFAULT_WEIGHT, + ## TODO: Examine: Perhaps not so many trues and falses? + "false": 1, + "true":1, + "W":0, + "M":0, + "xor":0, + "R":0, + + ## Aren't these PSL not LTL + # "EConcat":0, + # "UConcat":0, + # "Closure":0, ## ? +} + + +def _count_trace_steps(trace): + """ + Count the number of steps in a trace string. + Traces use ';' as a step delimiter (e.g., 'a; b; cycle{c}' has 3 steps). + """ + return len(trace.split(';')) + + +def weighted_trace_choice(traces): + """ + Select a trace from a list of traces, with shorter traces slightly preferred. + Uses inverse step count weighting: weight = 1 / (1 + num_steps). + This gives shorter traces higher selection probability while still allowing + longer traces to be selected. + + Args: + traces: A list of trace strings to choose from + + Returns: + A randomly selected trace string, with shorter traces more likely to be chosen + """ + if not traces: + raise ValueError("Cannot choose from empty list of traces") + if len(traces) == 1: + return traces[0] + + # Calculate weights based on inverse step count + # Using 1 / (1 + num_steps) to slightly prefer shorter traces + weights = [1.0 / (1.0 + _count_trace_steps(t)) for t in traces] + + return random.choices(traces, weights=weights, k=1)[0] + + +def areEquivalent(formula1, formula2): + return isSufficientFor(formula1, formula2) and isNecessaryFor(formula1, formula2) + + + +''' +Returns true if f => g is a tautology +''' +def isSufficientFor(f, g): + + f = spot.parse_formula(str(f)) + g = spot.parse_formula(str(g)) + + + a_f = f.translate() + a_ng = spot.formula.Not(g).translate() + return spot.product(a_f, a_ng).is_empty() + + +''' +Returns true if g => f is a tautology +''' +def isNecessaryFor(f, g): + return isSufficientFor(g, f) + + +def areDisjoint(f, g): + ff = spot.parse_formula(str(f)) + gf = spot.parse_formula(str(g)) + + a_ff = ff.translate() + a_gf = gf.translate() + + return spot.product(a_ff, a_gf).is_empty() + + +def generate_accepting_words(automaton, max_runs=5): + """Generate up to max_runs distinct accepting words by excluding previously seen traces.""" + words = [] + current_aut = automaton + + for _ in range(max_runs): + # Check if current automaton is empty + if current_aut.is_empty(): + break + + run = current_aut.accepting_run() + if run: + # Convert run to a word that the automaton accepts + word = spot.twa_word(run) + word_str = str(word) + + # Only add if we haven't seen it (safety check) + if word_str not in words: + words.append(word_str) + + # Exclude this trace from future runs + try: + # Build automaton that accepts only this trace + trace_aut = word.as_automaton() + # Complement it (now accepts everything EXCEPT this trace) + not_trace_aut = spot.complement(trace_aut) + # Product with current automaton to exclude this trace + current_aut = spot.product(current_aut, not_trace_aut) + except Exception as e: + print(f"Warning: Could not exclude trace '{word_str}': {e}") + break + else: + break # Stop if no accepting run is found + return words + +def generate_accepted_traces(formula, max_traces=5): + # Parse the LTL formula + f = spot.formula(formula) + + # Translate the LTL formula to a Büchi automaton + automaton = f.translate() + + # Retrieve and return the acceptance condition + runs = generate_accepting_words(automaton, max_traces) + #w.as_automaton() shows the run as an automaton. + return runs + +## Generate traces accepted by f_accepted, and rejected by f_rejected +def generate_traces(f_accepted, f_rejected, max_traces=5): + # Parse the LTL formula + f_a = spot.formula(f_accepted) + f_r = spot.formula.Not(spot.formula(f_rejected)) + + f = spot.formula.And([f_a, f_r]) + automaton = f.translate() + runs = generate_accepting_words(automaton, max_traces) + #w.as_automaton() shows the run as an automaton. + return runs + + + +# https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/randltl.ipynb + +## TODO: Need to generate some sort of transform from Misconceptions to ltl_priorities +## That is -- each misconception should have some weight around related concepts +### Some are obvious : Implicit G means, add more G +### Some are less obvious: eg "BadStateIndex" + +def gen_rand_ltl(atoms, tree_size, ltl_priorities, num_formulae = 5): + + def to_priority_string(d): + return ','.join(f'{k}={v}' for k, v in d.items()) + + # Need to do the correct kind of manipulation here + ltl_priorities_string = to_priority_string(ltl_priorities) + + f = spot.randltl(atoms, tree_size=tree_size, ltl_priorities = ltl_priorities_string) + + return [str(next(f)) for _ in range(num_formulae)] + + +def is_trivial(formula_str): + """ + Check if a formula is a tautology or contradiction using SPOT. + + Args: + formula_str: String representation of an LTL formula + + Returns: + True if the formula simplifies to constant true (1) or false (0) + """ + try: + f = spot.formula(formula_str) + # Simplify and check if it's constant true (1) or false (0) + simplified = spot.simplify(f) + simplified_str = str(simplified) + return simplified_str in ['1', '0', 'true', 'false'] + except: + return False + + +def gen_small_rand_ltl(atoms, tree_size=3, max_attempts=10): + """ + Generate a single small non-trivial random LTL formula using SPOT. + Prioritizes atomic propositions and simple operators to avoid complexity. + + Args: + atoms: List of atomic proposition strings + tree_size: Maximum tree size for the formula (default 3) + max_attempts: Maximum number of attempts to find a non-trivial formula + + Returns: + String representation of a non-trivial LTL formula, or a random atom as fallback + """ + # Prioritize simple operators, keep tree size small + priorities = { + 'ap': 5, + 'G': 2, 'F': 2, 'X': 2, 'U': 3, + 'and': 4, 'or': 4, 'implies': 3, 'not': 3, + 'equiv': 1, 'xor': 0, 'R': 0, 'W': 0, 'M': 0, + 'true': 0, 'false': 0 + } + + for _ in range(max_attempts): + try: + formulas = gen_rand_ltl(atoms, tree_size, priorities, num_formulae=1) + formula_str = formulas[0] + + # Reject trivial formulas + if not is_trivial(formula_str): + return formula_str + except: + continue + + # Fallback to a simple literal if all attempts fail + return random.choice(atoms) + + +## Returns the Mana Pneulli classification of the formula +def get_mana_pneulli_class(formula): + + + + f = spot.formula(formula) + return spot.mp_class(f, 'v') + + +def get_aut_size(formula): + f = spot.formula(formula) + aut = spot.translate(f) + num_states = aut.num_states() + return num_states + + +### Given an LTL Trace, return if the formula is satisfied + +### This works on the spot kernel but not here. Why? +def is_trace_satisfied(trace, formula): + formula = str(formula) + trace = str(trace) + + # Parse the trace into a word + word = spot.parse_word(trace) + + # Words can be translated to automata + # w.as_automaton() + + # Translate the formula into an automaton + f = spot.formula(formula) + aut = f.translate() + wordaut = word.as_automaton() + + # Check if the automaton intersects with the word automaton + return aut.intersects(wordaut) diff --git a/src/syntacticmutator.py b/ltlmutator/src/ltlmutator/syntacticmutator.py similarity index 98% rename from src/syntacticmutator.py rename to ltlmutator/src/ltlmutator/syntacticmutator.py index 3750ba3..3d20283 100644 --- a/src/syntacticmutator.py +++ b/ltlmutator/src/ltlmutator/syntacticmutator.py @@ -1,4 +1,4 @@ -from ltlnode import * +from .ltlnode import * import copy import random @@ -69,14 +69,14 @@ def findParentNode(root, node): def isEquivalentToAny(node, nodes): - + # Checks if the node is equivalent to any of the nodes in the list # Returns True if it is, False otherwise - + for n in nodes: if LTLNode.equiv(node, n): return True - + return False @@ -84,13 +84,13 @@ def isEquivalentToAny(node, nodes): def collectNodes(node): """Recursively collect all nodes in the tree.""" nodes = [node] - + if isinstance(node, UnaryOperatorNode): nodes.extend(collectNodes(node.operand)) elif isinstance(node, BinaryOperatorNode): nodes.extend(collectNodes(node.left)) nodes.extend(collectNodes(node.right)) - + return nodes def chooseRandomSubtree(node): @@ -112,7 +112,7 @@ def applyRandomMutationAtRoot(node): possible_mutations = [changeUnaryOperator] else: return node - + # Choose a random mutation from the list of possible mutations mutation = random.choice(possible_mutations) return mutation(node) @@ -125,7 +125,7 @@ def swapOperands(node : BinaryOperatorNode): return node.__class__(node.right, node.left) def changeBinaryOperator(node : BinaryOperatorNode): - + # Get the current class currentOperator = node.__class__ @@ -133,10 +133,10 @@ def changeBinaryOperator(node : BinaryOperatorNode): ## Get all classes that inherit from BinaryOperatorNode binopclasses = BinaryOperatorNode.__subclasses__() candidatebinops = [c for c in binopclasses if c != currentOperator] - + # Choose a random operator from the list of candidate operators newOperator = random.choice(candidatebinops) - + # Create a new node with the new operator newNode = binopclasses[candidatebinops.index(newOperator)](node.left, node.right) return newNode @@ -144,7 +144,7 @@ def changeBinaryOperator(node : BinaryOperatorNode): ## I think this works right? def changeUnaryOperator(node : UnaryOperatorNode): - + # Get the current operator currentOperator = node.__class__ @@ -159,7 +159,3 @@ def changeUnaryOperator(node : UnaryOperatorNode): # Create a new node with the new operator newNode = unopclasses[candidateunops.index(newOperator)](node.operand) return newNode - - - - diff --git a/requirements.txt b/requirements.txt index 5e39fe7..d3eca69 100644 --- a/requirements.txt +++ b/requirements.txt @@ -33,3 +33,4 @@ psycopg2-binary flask-login inflect wordfreq>=3.0 +./ltlmutator diff --git a/src/app.py b/src/app.py index d5ac57f..96316e5 100644 --- a/src/app.py +++ b/src/app.py @@ -2,8 +2,8 @@ from flask_login import login_required, current_user -from ltlnode import parse_ltl_string, SUPPORTED_SYNTAXES -from codebook import getAllApplicableMisconceptions +from ltlmutator import parse_ltl_string, SUPPORTED_SYNTAXES +from ltlmutator import getAllApplicableMisconceptions import os import json import sys @@ -16,7 +16,7 @@ import exerciseprocessor import exercisebuilder import random -import spotutils +from ltlmutator import spotutils from itertools import chain from collections import Counter, defaultdict import uuid diff --git a/src/authroutes.py b/src/authroutes.py index 5ec23b3..608c4b2 100644 --- a/src/authroutes.py +++ b/src/authroutes.py @@ -13,7 +13,7 @@ from functools import wraps from urllib.parse import urlparse from datetime import datetime, timezone -from ltlnode import SUPPORTED_SYNTAXES +from ltlmutator import SUPPORTED_SYNTAXES authroutes = Blueprint('authroutes', __name__) @@ -659,8 +659,8 @@ def delete_instructor_exercise(exercise_id): def suggest_distractors(): """API endpoint to suggest distractors for a question""" from flask import jsonify - import ltlnode - from codebook import getAllApplicableMisconceptions + import ltlmutator.ltlnode as ltlnode + from ltlmutator import getAllApplicableMisconceptions answer = request.form.get('answer', '') kind = request.form.get('kind', 'englishtoltl') @@ -700,9 +700,9 @@ def suggest_distractors(): def suggest_traces(): """API endpoint to suggest traces for trace satisfaction questions""" from flask import jsonify - import spotutils + from ltlmutator import spotutils import exerciseprocessor - import ltlnode + import ltlmutator.ltlnode as ltlnode formula = request.form.get('formula', '') diff --git a/src/exercisebuilder.py b/src/exercisebuilder.py index a14e387..5ffa786 100644 --- a/src/exercisebuilder.py +++ b/src/exercisebuilder.py @@ -1,14 +1,14 @@ -import spotutils +from ltlmutator import spotutils import datetime from collections import defaultdict -import codebook -from codebook import MisconceptionCode -import ltlnode +from ltlmutator import codebook +from ltlmutator import MisconceptionCode +import ltlmutator.ltlnode as ltlnode import random import re import math import ltltoeng -from syntacticmutator import applyRandomMutationNotEquivalentTo +from ltlmutator import applyRandomMutationNotEquivalentTo class ExerciseBuilder: diff --git a/src/exerciseprocessor.py b/src/exerciseprocessor.py index 7ab9cb1..93a99a9 100644 --- a/src/exerciseprocessor.py +++ b/src/exerciseprocessor.py @@ -4,7 +4,7 @@ import json import re from exercisebuilder import ExerciseBuilder -import ltlnode +import ltlmutator.ltlnode as ltlnode def load_questions_from_sourceuri(sourceuri, staticfolderpath): if sourceuri.startswith('preload:'): diff --git a/src/feedbackgenerator.py b/src/feedbackgenerator.py index c15c830..be093e3 100644 --- a/src/feedbackgenerator.py +++ b/src/feedbackgenerator.py @@ -1,4 +1,4 @@ -import spotutils +from ltlmutator import spotutils class FeedbackGenerator: diff --git a/src/ltltoeng.py b/src/ltltoeng.py index cb71e9c..0980f48 100644 --- a/src/ltltoeng.py +++ b/src/ltltoeng.py @@ -1,4 +1,4 @@ -import ltlnode +import ltlmutator.ltlnode as ltlnode import random import re @@ -454,17 +454,17 @@ def _check_final_state_pattern(node, right_node_type): left = op.left right = op.right if type(right) is right_node_type: - # Check if both left and right.operand are literals with the same value - if (type(left) is ltlnode.LiteralNode and - type(right.operand) is ltlnode.LiteralNode and - left.value == right.operand.value): - left_eng = clean_for_composition(left.__to_english__()) - return choose_best_sentence([ - f"once {left_eng} is true, it stays true", - f"once {left_eng} becomes true, it remains true", - f"after {left_eng} holds, it continues to hold forever" - ]) - return None + # Check if both left and right.operand are literals with the same value + if (type(left) is ltlnode.LiteralNode and + type(right.operand) is ltlnode.LiteralNode and + left.value == right.operand.value): + left_eng = clean_for_composition(left.__to_english__()) + return choose_best_sentence([ + f"once {left_eng} is true, it stays true", + f"once {left_eng} becomes true, it remains true", + f"after {left_eng} holds, it continues to hold forever" + ]) + return None # Pattern: G (p -> X p) diff --git a/src/stepper.py b/src/stepper.py index bb17e2a..1fa9fd9 100644 --- a/src/stepper.py +++ b/src/stepper.py @@ -1,6 +1,6 @@ -from ltlnode import UnaryOperatorNode, BinaryOperatorNode, LiteralNode, parse_ltl_string +from ltlmutator import UnaryOperatorNode, BinaryOperatorNode, LiteralNode, parse_ltl_string import ltltoeng -from spotutils import is_trace_satisfied +from ltlmutator.spotutils import is_trace_satisfied import re import random import html as html_module diff --git a/test/test_english_translation.py b/test/test_english_translation.py index bf4c9ec..c5c629b 100644 --- a/test/test_english_translation.py +++ b/test/test_english_translation.py @@ -9,7 +9,7 @@ from unittest.mock import MagicMock sys.modules['spot'] = MagicMock() -from ltlnode import * +from ltlmutator.ltlnode import * import random diff --git a/test/test_mutation.py b/test/test_mutation.py index db562ff..7657dd0 100644 --- a/test/test_mutation.py +++ b/test/test_mutation.py @@ -10,8 +10,8 @@ from unittest.mock import MagicMock sys.modules['spot'] = MagicMock() -from ltlnode import parse_ltl_string -import codebook +from ltlmutator import parse_ltl_string +from ltlmutator import codebook """ @@ -62,16 +62,16 @@ def test_bad_state_index(self): codebook.MisconceptionCode.BadStateIndex, test_cases ) - def test_bad_state_quantification(self): - test_cases = [ - ("G(a -> b)", "(F (a -> b))"), - ("F(a U b)", "(G (a U b))"), - ("F(a)", "(G a)"), - ("G(F(a))", "(F (F a))"), - ] - self.apply_and_check_misconception( - codebook.MisconceptionCode.BadStateQuantification, test_cases - ) + def test_bad_state_quantification(self): + test_cases = [ + ("G(a -> b)", "(F (a -> b))"), + ("F(a U b)", "(G (a U b))"), + ("F(a)", "(G a)"), + ("G(F(a))", "(F (F a))"), + ] + self.apply_and_check_misconception( + codebook.MisconceptionCode.BadStateQuantification, test_cases + ) random_result_cases = [ ( @@ -105,35 +105,35 @@ def test_bad_state_quantification(self): codebook.applyMisconception( ast, codebook.MisconceptionCode.BadStateQuantification ).node - ) - self.assertIn(result, expected_outputs) - - def test_get_all_applicable_misconceptions_randomizes_rewrite_location(self): - """ - Ensure distractor generation can apply a misconception at different valid - rewrite sites (not only the first match). - """ - ast = parse_ltl_string("G(F(a))") - results_seen = set() - - for i in range(NUM_DIVERSITY_ITERATIONS): - with self.subTest(iteration=i): - all_results = codebook.getAllApplicableMisconceptions(ast) - bq_results = [ - str(result.node) - for result in all_results - if result.misconception == codebook.MisconceptionCode.BadStateQuantification - ] - self.assertEqual(len(bq_results), 1) - self.assertIn(bq_results[0], {"(F (F a))", "(G (G a))"}) - results_seen.add(bq_results[0]) - - self.assertGreater( - len(results_seen), - 1, - f"Only saw {results_seen} across {NUM_DIVERSITY_ITERATIONS} attempts.", - ) - + ) + self.assertIn(result, expected_outputs) + + def test_get_all_applicable_misconceptions_randomizes_rewrite_location(self): + """ + Ensure distractor generation can apply a misconception at different valid + rewrite sites (not only the first match). + """ + ast = parse_ltl_string("G(F(a))") + results_seen = set() + + for i in range(NUM_DIVERSITY_ITERATIONS): + with self.subTest(iteration=i): + all_results = codebook.getAllApplicableMisconceptions(ast) + bq_results = [ + str(result.node) + for result in all_results + if result.misconception == codebook.MisconceptionCode.BadStateQuantification + ] + self.assertEqual(len(bq_results), 1) + self.assertIn(bq_results[0], {"(F (F a))", "(G (G a))"}) + results_seen.add(bq_results[0]) + + self.assertGreater( + len(results_seen), + 1, + f"Only saw {results_seen} across {NUM_DIVERSITY_ITERATIONS} attempts.", + ) + def test_exclusive_u(self): test_cases = [ ("(x U ((! x) & y))", "(x U y)"), @@ -234,13 +234,13 @@ def test_implicit_g_diversity(self): self.assertGreater(len(results_seen), 1, f"Only saw {results_seen} across {NUM_DIVERSITY_ITERATIONS} attempts for {input}") - def test_weak_u(self): - test_cases = [ - ("a U b", "((a U b) | (G a))"), - ("a U (G b)", "((a U (G b)) | (G a))"), - ("a U (b -> c)", "((a U (b -> c)) | (G a))"), - ] - self.apply_and_check_misconception(codebook.MisconceptionCode.WeakU, test_cases) + def test_weak_u(self): + test_cases = [ + ("a U b", "((a U b) | (G a))"), + ("a U (G b)", "((a U (G b)) | (G a))"), + ("a U (b -> c)", "((a U (b -> c)) | (G a))"), + ] + self.apply_and_check_misconception(codebook.MisconceptionCode.WeakU, test_cases) if __name__ == "__main__": diff --git a/test/test_parsing.py b/test/test_parsing.py index 2092d79..ceaddcb 100644 --- a/test/test_parsing.py +++ b/test/test_parsing.py @@ -9,7 +9,7 @@ from unittest.mock import MagicMock sys.modules['spot'] = MagicMock() -from ltlnode import * +from ltlmutator.ltlnode import * ## LTL String --> AST Node diff --git a/test/test_regression_model.py b/test/test_regression_model.py index 9a5b8d2..ea7582f 100644 --- a/test/test_regression_model.py +++ b/test/test_regression_model.py @@ -11,7 +11,7 @@ sys.modules['spot'] = MagicMock() from exercisebuilder import ExerciseBuilder -from codebook import MisconceptionCode +from ltlmutator import MisconceptionCode class MockStudentLog: diff --git a/test/test_weighted_trace.py b/test/test_weighted_trace.py index 823caf9..a75e939 100644 --- a/test/test_weighted_trace.py +++ b/test/test_weighted_trace.py @@ -9,7 +9,7 @@ from unittest.mock import MagicMock sys.modules['spot'] = MagicMock() -from spotutils import weighted_trace_choice, _count_trace_steps +from ltlmutator.spotutils import weighted_trace_choice, _count_trace_steps class TestCountTraceSteps(unittest.TestCase): diff --git a/test_template_generation.py b/test_template_generation.py index 22062a4..363defb 100644 --- a/test_template_generation.py +++ b/test_template_generation.py @@ -6,8 +6,8 @@ import sys sys.path.insert(0, 'src') -from codebook import MisconceptionCode, applyMisconception -from ltlnode import LTLNode +from ltlmutator import MisconceptionCode, applyMisconception +from ltlmutator import LTLNode def test_exclusive_u_operators(): """Test that ExclusiveU now returns boolean operators too"""