Build an LTLf Contradiction Checker

Build a Python CLI that finds contradictions in finite-trace LTL rules.

Introduction

30 Second Summary

A set of rules can sound reasonable when you read each one alone. The real trouble appears when no possible sequence of events can satisfy them all.

In this project, you will build a terminal-based checker that reads LTLf constraints from constraints.txt. It will use Spot to expose the first rule that makes the full specification contradictory.

What You'll Build

A single terminal command will turn your text file into a contradiction report that names the first conflicting constraint.

By the end of this project, you'll have:

  • A reusable file-driven checker that accepts new rules through constraints.txt without Python edits.
  • A step-by-step automata report that shows each rule's status beside the cumulative DFA state count.
  • A precise contradiction diagnosis that names the first rule to empty the cumulative language.
  • Secret Mission: A --core option that finds one irreducible contradictory subset.

Are there any prerequisites?

Basic Python skills plus familiarity with the LTL operators F, G, !, and -> will help. With Windows plus Windows Subsystem for Linux (WSL) with Ubuntu and Visual Studio Code ready, you can follow the project through the remaining Miniforge setup.

Before We Start

This checkpoint helps you commit to the finite-trace specification you are about to analyze. You will define the contradiction your checker needs to detect before any setup begins.

Set Up Spot in WSL Ubuntu

The contradiction decision you planned for constraints.txt depends on Spot translating LTLf rules into finite automata inside Windows Subsystem for Linux (WSL) Ubuntu.

Spot is distributed as native Linux software. A precompiled Conda package inside WSL avoids a lengthy C++ source build.

In this step, get ready to:
  • Install Miniforge in WSL Ubuntu when Conda is unavailable.
  • Create the ltlf-checker environment with Python 3.11 and Spot 2.16.2.
  • Open the WSL project folder in Visual Studio Code and verify the Spot installation.
Prepare Conda in Ubuntu

Miniforge provides Conda without requiring a separate Linux package manager. First, check whether your Ubuntu shell can already access Conda.

  • Check whether Conda is available by running this command:
conda --version

What does this check do?

The conda --version command asks the shell to locate Conda and print its installed version. The result determines whether Miniforge needs to be installed.

✔️ Conda is available

Your Ubuntu shell can already access Conda. That existing installation can create the isolated environment for this project.

ⓧ Command not found

Your Ubuntu shell needs a Conda distribution. The Miniforge installer selects the Linux package that matches your WSL architecture.

  • Install Miniforge 26.9.4-1 at ${HOME}/conda by running these commands:
MINIFORGE_VERSION=26.9.4-1
wget -O Miniforge3.sh "https://github.com/conda-forge/miniforge/releases/download/${MINIFORGE_VERSION}/Miniforge3-$(uname)-$(uname -m).sh"
bash Miniforge3.sh -b -p "${HOME}/conda"
source "${HOME}/conda/etc/profile.d/conda.sh"

What do these commands do?

  • The MINIFORGE_VERSION value pins the installer release used by this project.
  • The wget command downloads the installer that matches the Linux architecture reported by WSL.
  • The bash command performs a batch installation at ${HOME}/conda.
  • The source command initializes Conda in the current Ubuntu shell.
  • Confirm that the current shell can access Conda by running the check again:
conda --version

What should you see?

You should see a Conda version in the terminal. That output confirms the Miniforge installation is available in the current shell.

Miniforge installation stopped?

  • Check that the Ubuntu terminal has internet access before downloading the installer again.
  • Check that every command was run inside Ubuntu rather than Windows PowerShell.

Get help with diagnosing the Miniforge installation.

Create and activate the environment

A dedicated environment keeps the checker on the compatible Python series. It also pins the Spot release so every later automata operation uses the same API.

  • Create the ltlf-checker environment and activate it by running these commands:
conda create -n ltlf-checker -c conda-forge python=3.11 spot=2.16.2 -y
conda activate ltlf-checker

What do these commands do?

  • The first command creates an isolated environment named ltlf-checker from the Conda-forge channel.
  • The package specifications install Python 3.11 with Spot 2.16.2.
  • The second command activates the environment so its Python interpreter handles the checker.

That is the Linux runtime ready. You should see the environment name at the beginning of your terminal prompt.

Environment creation failed?

  • Confirm that the Conda version check from the previous substep still succeeds.
  • Check your internet connection before running the environment command again.

Get help with diagnosing the Conda environment.

Open the project folder and verify Spot

The project files need a predictable location inside WSL. Opening that location from the Ubuntu terminal keeps the editor connected to the Linux runtime.

  • Prepare your WSL Desktop location by running these commands:
mkdir -p ~/Desktop
cd ~/Desktop

What do these commands do?

The first command makes sure the Desktop directory exists inside your WSL home directory. The second command moves the terminal into that directory.

The first WSL launch of Visual Studio Code can take a short while because the editor prepares its Linux-side connection.

  • Create the ltlf-checker folder and open it in Visual Studio Code by running these commands:
mkdir ltlf-checker
cd ltlf-checker
code .

What do these commands do?

  • The mkdir command creates the folder that will hold contradiction_checker.py and constraints.txt.
  • The cd command moves the Ubuntu terminal into that folder.
  • The code . command opens the current WSL folder in Visual Studio Code.

You should see ltlf-checker open in Visual Studio Code. You should also see a WSL indicator in the lower-left corner.

Visual Studio Code did not open?

  • Restart the Ubuntu terminal before running the folder-opening command again.
  • Confirm that Visual Studio Code is available from your Windows installation.

Get help with opening the project folder through WSL.

Before you run the final check, what Spot version do you expect the activated environment to print?

  • Switch back to the Ubuntu terminal from earlier.
  • Verify the Spot installation by running this command:
python -c "import spot; print(spot.version())"

What does this check do?

The command starts the Python interpreter from the active environment. It imports the Spot bindings and prints the installed Spot version.

✔️ I see version 2.16.2

You should see 2.16.2 in the terminal. Your WSL environment can now import the exact Spot release used by the checker.

ⓧ I see a different version

A different version usually means another environment supplied the Python interpreter. Rebuilding the named environment restores the pinned packages.

  • Recreate the environment and repeat the version check by running these commands:
conda deactivate
conda env remove -n ltlf-checker -y
conda create -n ltlf-checker -c conda-forge python=3.11 spot=2.16.2 -y
conda activate ltlf-checker
python -c "import spot; print(spot.version())"

What does this recovery do?

These commands leave the active environment and remove its existing packages. They recreate the environment with the pinned Python and Spot versions before repeating the check.

You should now see 2.16.2 in the terminal.

Still seeing another version?

Get help with finding which Python environment is active.

ⓧ Spot does not import

An import failure means the active Python interpreter cannot access the Spot package. Recreating the environment installs both packages together.

  • Recreate the environment and repeat the import check by running these commands:
conda deactivate
conda env remove -n ltlf-checker -y
conda create -n ltlf-checker -c conda-forge python=3.11 spot=2.16.2 -y
conda activate ltlf-checker
python -c "import spot; print(spot.version())"

What does this recovery do?

The sequence removes the incomplete environment and recreates it from Conda-forge. The final command tests the new Spot installation immediately.

You should now see 2.16.2 in the terminal.

Spot still does not import?

Get help with diagnosing the Spot import.

Your WSL toolchain is ready to translate finite-trace formulas. Next, you will test each constraint in isolation and expose the first limitation of that approach.

Check Constraints in Isolation

Your Spot environment is ready to translate finite-trace formulas. A logical risk remains because a rule can have a valid trace on its own while the full specification has no valid trace.

This step deliberately tests each LTLf constraint in isolation. You will see why two successful checks cannot prove that the constraints work together.

In this step, get ready to:
  • Create a parser that accepts LTL formulas.
  • Translate each hard-coded constraint into its own MTDFA.
  • Run the script to expose the blind spot in isolated checks.
Build the isolated checker

Spot's parser accepts a PSL superset. The is_ltl_formula() guard keeps this checker focused on LTL input.

  • In the Visual Studio Code Explorer sidebar, create contradiction_checker.py inside the open WSL project folder.
  • Add the parser plus isolated automaton checks by pasting this code into contradiction_checker.py:
import spot


def parse_ltlf(text: str, index: int):
    formula = spot.formula(text)
    if not formula.is_ltl_formula():
        raise ValueError(f"Constraint {index} is not an LTL formula: {text}")
    return formula


formulas = ["F approved", "G !approved"]

for index, text in enumerate(formulas, start=1):
    formula = parse_ltlf(text, index)
    dfa = spot.ltlf_to_mtdfa(formula)
    status = "CONTRADICTION" if dfa.is_empty() else "SATISFIABLE"
    print(f"[{index}] individual={status}")
    print(f"    {formula}")

What does this code do?

  • The parse_ltlf() function uses spot.formula() to parse each string. Its guard rejects parsed syntax outside LTL.
  • The formulas list holds the two rules that the checker tests independently.
  • The spot.ltlf_to_mtdfa() call builds one automaton for each formula. The is_empty() call checks whether that automaton accepts any finite trace.
  • The loop prints an individual status for each constraint. It does not combine their accepted languages.

✔️ Awesome, I've got everything!

Your file now contains the complete isolated-checking script.

ⓧ I'd like to double check the full code

import spot


def parse_ltlf(text: str, index: int):
    formula = spot.formula(text)
    if not formula.is_ltl_formula():
        raise ValueError(f"Constraint {index} is not an LTL formula: {text}")
    return formula


formulas = ["F approved", "G !approved"]

for index, text in enumerate(formulas, start=1):
    formula = parse_ltlf(text, index)
    dfa = spot.ltlf_to_mtdfa(formula)
    status = "CONTRADICTION" if dfa.is_empty() else "SATISFIABLE"
    print(f"[{index}] individual={status}")
    print(f"    {formula}")
Run the isolated checks
  • Save contradiction_checker.py.

Before you run the script, do you think either formula will look contradictory when tested alone?

  • Test the isolated checker from the WSL terminal by running:
python contradiction_checker.py

Your terminal reports F approved as individually SATISFIABLE. It reports G !approved the same way.

Script not running?

  • Confirm that contradiction_checker.py is saved in the open WSL project folder.
  • Confirm that the terminal prompt still shows the ltlf-checker environment.
  • Compare your parse_ltlf() function with the full-code tab above.

Help me debug the isolated checker.

Interpret the blind spot

You have exposed the intended blind spot: both isolated checks pass even though the pair accepts no shared finite trace.

Why do both checks pass?

The formula F approved accepts finite traces where approval eventually occurs. The formula G !approved accepts finite traces where approval never occurs.

Each language contains valid traces when checked alone. Their contradiction appears when the two languages are intersected.

Your checker now demonstrates the failure of isolated reasoning. Next, you will intersect the automata so the hidden contradiction becomes visible.

Intersect DFA Languages

Your previous run proved that each rule has at least one valid finite trace on its own. The checker still cannot decide whether one finite trace satisfies the full specification.

The missing decision comes from a DFA language intersection. Spot's spot.product() operation keeps only the traces accepted by both automata.

In this step, get ready to:
  • Carry the first MTDFA forward as the cumulative automaton.
  • Intersect each later MTDFA with the cumulative language.
  • Print a diagnostic report for the first empty cumulative language.
Intersect each constraint language

The cumulative automaton represents the traces that survive every constraint processed so far. The first automaton seeds that cumulative state.

  • Switch back to contradiction_checker.py in Visual Studio Code.
  • Select everything from formulas = ["F approved", "G !approved"] through the end of the file.
  • Replace the selected code by pasting this cumulative intersection function:
def check_constraints(formulas: list[str]) -> bool:
    combined_dfa = None
    print(f"Loaded {len(formulas)} constraint(s).")

    for index, text in enumerate(formulas, start=1):
        formula = parse_ltlf(text, index)
        individual_dfa = spot.ltlf_to_mtdfa(formula)
        individual_empty = individual_dfa.is_empty()

        if combined_dfa is None:
            combined_dfa = individual_dfa
        else:
            combined_dfa = spot.product(combined_dfa, individual_dfa)

        cumulative_empty = combined_dfa.is_empty()

        if cumulative_empty:
            print(f"First contradiction introduced by constraint {index}: {formula}")
            print("Final result: CONTRADICTION")
            return False

    print("Final result: SATISFIABLE")
    return True


formulas = ["F approved", "G !approved"]
check_constraints(formulas)

What does this code do?

  • The combined_dfa variable starts as None because no constraint language has been processed.
  • The first individual_dfa becomes the starting cumulative automaton.
  • Each later spot.product() call intersects the saved language with the next constraint language.
  • The is_empty() check detects when no finite trace survives the intersection.
  • The early return False stops the function at the first contradiction.
  • Save contradiction_checker.py.
  • Predict whether the second cumulative language still contains any finite trace.
  • Run the cumulative check in the WSL terminal with this command:
python contradiction_checker.py

What should I see?

You will see Loaded 2 constraint(s). before the checker names constraint 2 as the first contradiction.

The final line reads Final result: CONTRADICTION. The two individually satisfiable languages have an empty intersection.

Checker still misses the contradiction?

  • Confirm that check_constraints() begins at the left edge of contradiction_checker.py.
  • Confirm that the old individual-only loop no longer remains below the function.
  • Check that spot.product(combined_dfa, individual_dfa) appears inside the else branch.

Help me debug the cumulative DFA intersection.

Add cumulative diagnostics

Emptiness identifies the conflict point. A state count shows how the cumulative automaton changes as each rule arrives.

  • Find the cumulative_empty = combined_dfa.is_empty() line in contradiction_checker.py.
  • Place your cursor directly below that line.
  • Add the individual status plus the cumulative diagnostics by pasting this code:
        individual_status = "CONTRADICTION" if individual_empty else "SATISFIABLE"
        cumulative_status = "CONTRADICTION" if cumulative_empty else "SATISFIABLE"
        print(
            f"[{index}] individual={individual_status} | "
            f"cumulative={cumulative_status} | "
            f"cumulative_states={combined_dfa.num_states()}"
        )
        print(f"    {formula}")

How do the diagnostics help?

  • The individual_status variable records the result for one constraint.
  • The cumulative_status variable records the result for every constraint processed so far.
  • The num_states() method reports the cumulative automaton size after each addition.
  • The second print keeps each formula beside its diagnostic line.
  • Save contradiction_checker.py.
  • Predict which constraint first changes the cumulative status without changing its individual status.
  • Run the completed intersection checker with this command:
python contradiction_checker.py

What should I see?

  • The Loaded 2 constraint(s). line confirms that the checker received both rules.
  • Constraint 1 reports individual=SATISFIABLE.
  • Constraint 1 reports cumulative=SATISFIABLE.
  • Constraint 2 still reports individual=SATISFIABLE.
  • Constraint 2 changes to cumulative=CONTRADICTION.
  • The cumulative_states= field is followed by a numeric state count on each constraint line.
  • The final report names constraint 2 with G !approved as the first cumulative conflict.

That is the checker doing its real job. It now separates individual satisfiability from joint consistency.

Missing cumulative details?

  • Confirm that the diagnostic block sits between cumulative_empty = combined_dfa.is_empty() and if cumulative_empty:.
  • Check that every diagnostic line has eight leading spaces.
  • Confirm that combined_dfa.num_states() uses the cumulative automaton.

Help me fix the cumulative status report.

✔️ Awesome, I've got everything!

Your file now matches the cumulative contradiction checker.

ⓧ I'd like to double check the full code

import spot


def parse_ltlf(text: str, index: int):
    formula = spot.formula(text)
    if not formula.is_ltl_formula():
        raise ValueError(f"Constraint {index} is not an LTL formula: {text}")
    return formula


def check_constraints(formulas: list[str]) -> bool:
    combined_dfa = None
    print(f"Loaded {len(formulas)} constraint(s).")

    for index, text in enumerate(formulas, start=1):
        formula = parse_ltlf(text, index)
        individual_dfa = spot.ltlf_to_mtdfa(formula)
        individual_empty = individual_dfa.is_empty()

        if combined_dfa is None:
            combined_dfa = individual_dfa
        else:
            combined_dfa = spot.product(combined_dfa, individual_dfa)

        cumulative_empty = combined_dfa.is_empty()
        individual_status = "CONTRADICTION" if individual_empty else "SATISFIABLE"
        cumulative_status = "CONTRADICTION" if cumulative_empty else "SATISFIABLE"
        print(
            f"[{index}] individual={individual_status} | "
            f"cumulative={cumulative_status} | "
            f"cumulative_states={combined_dfa.num_states()}"
        )
        print(f"    {formula}")

        if cumulative_empty:
            print(f"First contradiction introduced by constraint {index}: {formula}")
            print("Final result: CONTRADICTION")
            return False

    print("Final result: SATISFIABLE")
    return True


formulas = ["F approved", "G !approved"]
check_constraints(formulas)

What to compare

The complete file retains parse_ltlf() above the new check_constraints() function. The formulas list plus the function call remain at the bottom.

Your checker now exposes the exact constraint that empties the cumulative language. Next, you will move the formulas into constraints.txt so the same logic can check new specifications.

Build the Command-Line Checker

Your Spot pipeline now intersects each LTLf rule through a cumulative DFA. It also identifies the first rule that empties the combined language.

The specification still lives inside a hard-coded Python list. A command-line interface moves those rules into a reusable text file while preserving the intersection logic you have already proven.

In this step, get ready to:
  • Create a text file containing the ordered LTLf constraints.
  • Load formulas from a path supplied through the terminal.
  • Prove that editing the input file changes the final result.
Create the constraints file

A separate input file lets you test a new finite-trace specification without editing Python. The file order remains important because the checker reports the first contradictory prefix.

  • In the open Visual Studio Code window from earlier, select the new-file icon in the file sidebar.
  • Enter constraints.txt as the filename.
  • Populate constraints.txt by pasting this specification:
# A request must eventually be approved.
F approved

# Every approval must eventually be archived.
G(approved -> F archived)

# Approval is forbidden.
G !approved

What Does This File Define?

  • The first formula requires approval to occur eventually.
  • The second formula requires each approval to have a later archival event.
  • The third formula forbids approval throughout the finite trace.
  • Each line beginning with # documents the specification for a human reader.
  • Save constraints.txt.
  • Confirm that the file sidebar lists constraints.txt beside contradiction_checker.py.
  • Confirm that the saved file contains three active formulas.

Does the file look different?

Check that each formula occupies its own line. Keep the descriptive lines beginning with # separate from the formulas.

Confirm that the filename is exactly constraints.txt.

Help me check my constraints file formatting.

Load formulas from the file

The loader converts a file path into the same list of formula strings that check_constraints() already accepts. It filters documentation and empty lines before any text reaches the Spot parser.

  • In contradiction_checker.py from earlier, replace the existing import spot line with this import group:
from __future__ import annotations

import argparse
from pathlib import Path

import spot

What Do These Imports Provide?

  • The future import keeps the file's type annotations compatible with the completed checker.
  • The argparse module reads the path supplied through the terminal.
  • The Path class gives the loader a file-reading interface.
  • The spot import retains the existing formula and MTDFA operations.
  • Save contradiction_checker.py.
  • Confirm that the future import is the first code line in the file.

Seeing an import problem?

Place the future import before every regular import. Keep import spot below the standard-library imports.

Help me fix the checker imports.

  • Add the loader directly above parse_ltlf() by pasting this function:
def load_formulas(path: Path) -> list[str]:
    formulas: list[str] = []

    for raw_line in path.read_text(encoding="utf-8").splitlines():
        line = raw_line.strip()
        if line and not line.startswith("#"):
            formulas.append(line)

    if not formulas:
        raise ValueError(f"No LTLf formulas found in {path}.")

    return formulas

What Does the Loader Do?

  • The path parameter identifies the specification file.
  • The raw_line variable holds each line read from the file.
  • The line variable holds the trimmed text used by the filters.
  • The conditional keeps each non-empty line that does not begin with #.
  • The final guard rejects an input file with no active formulas.
  • Save contradiction_checker.py.

Before you run the script, do you expect defining load_formulas() to make the existing bottom lines use constraints.txt?

  • Test the current wiring in the WSL terminal from earlier by running:
python contradiction_checker.py constraints.txt

What Does the Output Prove?

The report still begins with Loaded 2 constraint(s). It still names G !approved as constraint 2.

The loader is available, but the two bottom lines still pass the hard-coded list into check_constraints(). The command-line entry point closes that wiring gap.

Did the script stop before the report?

Check that load_formulas() appears above parse_ltlf(). Match the indentation inside the loop and the empty-list guard.

Help me debug the loader function.

Connect the command-line entry point

The entry point converts the supplied argument into a Path. It then sends the loaded formulas into the existing intersection pipeline.

  • In check_constraints(), find the current reporting region from cumulative_empty through the formula print call:
        cumulative_empty = combined_dfa.is_empty()
        individual_status = "CONTRADICTION" if individual_empty else "SATISFIABLE"
        cumulative_status = "CONTRADICTION" if cumulative_empty else "SATISFIABLE"
        print(
            f"[{index}] individual={individual_status} | "
            f"cumulative={cumulative_status} | "
            f"cumulative_states={combined_dfa.num_states()}"
        )
        print(f"    {formula}")

What Does This Region Report?

This existing region converts the individual and cumulative emptiness checks into readable statuses. It also prints the cumulative MTDFA state count.

  • Replace that reporting region with this wrapped version:
        cumulative_empty = combined_dfa.is_empty()
        individual_status = (
            "CONTRADICTION" if individual_empty else "SATISFIABLE"
        )
        cumulative_status = (
            "CONTRADICTION" if cumulative_empty else "SATISFIABLE"
        )

        print(
            f"[{index}] individual={individual_status} | "
            f"cumulative={cumulative_status} | "
            f"cumulative_states={combined_dfa.num_states()}"
        )
        print(f"    {formula}")

Why Wrap the Status Lines?

The parentheses keep each conditional status readable without changing its behavior. The output text stays identical.

  • At the bottom of contradiction_checker.py, replace the hard-coded formulas list and its function call with this entry point:
def main() -> None:
    parser = argparse.ArgumentParser(
        description="Check an ordered file of LTLf constraints for contradiction."
    )
    parser.add_argument(
        "constraints_file",
        type=Path,
        help="Text file containing one LTLf formula per line.",
    )
    args = parser.parse_args()

    try:
        formulas = load_formulas(args.constraints_file)
        check_constraints(formulas)
    except (OSError, RuntimeError, ValueError) as error:
        parser.exit(status=2, message=f"Error: {error}\n")


if __name__ == "__main__":
    main()

How Does the Entry Point Work?

  • The parser defines the command description and required file argument.
  • The constraints_file argument converts the supplied text into a Path.
  • The args object stores the parsed path.
  • The protected block loads the file before calling check_constraints().
  • The error handler turns file and formula failures into a terminal message.
  • The final guard calls main() when you run the file as a program.
  • Save contradiction_checker.py.

Before you run the completed checker, which of the three constraints do you expect to empty the cumulative language?

  • Run the file-driven checker from the WSL terminal by entering:
python contradiction_checker.py constraints.txt

What Should the Full Report Show?

The report begins with Loaded 3 constraint(s). Each constraint row includes its individual status and cumulative status.

Each row also includes a cumulative DFA state count. Constraint 3 is named as the first conflict before Final result: CONTRADICTION.

Is the file path rejected or ignored?

Confirm that the hard-coded formulas list is gone from the bottom of the script. Check that load_formulas(args.constraints_file) appears inside the protected block.

Make sure contradiction_checker.py and constraints.txt are saved in the same open WSL project folder.

Help me debug the command-line path.

Prove the Input Is Reusable

A file-driven checker should change its decision when the specification changes. A reversible edit tests the input path without changing any Python code.

  • In constraints.txt, delete the G !approved line.
  • Save constraints.txt.

Before you rerun the checker, do you expect the two remaining rules to share a satisfying finite trace?

  • Test the reduced specification by running:
python contradiction_checker.py constraints.txt

What Changed?

The checker now loads two constraints. The report ends with Final result: SATISFIABLE.

This result proves that the checker reads its rules from constraints.txt on every run.

Still seeing a contradiction?

Confirm that the active G !approved formula is absent from constraints.txt. The descriptive comment can remain because the loader ignores it.

Help me inspect the reduced specification.

  • Restore G !approved beneath the approval-forbidden comment.
  • Save constraints.txt.

Before the final run, do you expect the restored third rule to make constraint 3 the first conflict again?

  • Verify the restored project state by running:
python contradiction_checker.py constraints.txt

Your Checker Is Complete

The final report names constraint 3 as the first cumulative conflict. It ends with Final result: CONTRADICTION.

That completes the checker. Your Python code now reaches both decisions from file input while preserving the cumulative DFA diagnostics.

✔️ Awesome, I've got everything!

Both project files are complete. Your restored specification produces the expected contradiction report.

ⓧ I'd like to double check the full code

  • Compare your saved constraints.txt with this complete file:
# A request must eventually be approved.
F approved

# Every approval must eventually be archived.
G(approved -> F archived)

# Approval is forbidden.
G !approved

What Should Match?

The file contains three active formulas. Each descriptive comment begins with #.

  • Compare your saved contradiction_checker.py with this complete file:
from __future__ import annotations

import argparse
from pathlib import Path

import spot


def load_formulas(path: Path) -> list[str]:
    formulas: list[str] = []

    for raw_line in path.read_text(encoding="utf-8").splitlines():
        line = raw_line.strip()
        if line and not line.startswith("#"):
            formulas.append(line)

    if not formulas:
        raise ValueError(f"No LTLf formulas found in {path}.")

    return formulas


def parse_ltlf(text: str, index: int):
    formula = spot.formula(text)
    if not formula.is_ltl_formula():
        raise ValueError(f"Constraint {index} is not an LTL formula: {text}")
    return formula


def check_constraints(formulas: list[str]) -> bool:
    combined_dfa = None
    print(f"Loaded {len(formulas)} constraint(s).")

    for index, text in enumerate(formulas, start=1):
        formula = parse_ltlf(text, index)
        individual_dfa = spot.ltlf_to_mtdfa(formula)
        individual_empty = individual_dfa.is_empty()

        if combined_dfa is None:
            combined_dfa = individual_dfa
        else:
            combined_dfa = spot.product(combined_dfa, individual_dfa)

        cumulative_empty = combined_dfa.is_empty()
        individual_status = (
            "CONTRADICTION" if individual_empty else "SATISFIABLE"
        )
        cumulative_status = (
            "CONTRADICTION" if cumulative_empty else "SATISFIABLE"
        )

        print(
            f"[{index}] individual={individual_status} | "
            f"cumulative={cumulative_status} | "
            f"cumulative_states={combined_dfa.num_states()}"
        )
        print(f"    {formula}")

        if cumulative_empty:
            print(
                f"First contradiction introduced by constraint {index}: {formula}"
            )
            print("Final result: CONTRADICTION")
            return False

    print("Final result: SATISFIABLE")
    return True


def main() -> None:
    parser = argparse.ArgumentParser(
        description="Check an ordered file of LTLf constraints for contradiction."
    )
    parser.add_argument(
        "constraints_file",
        type=Path,
        help="Text file containing one LTLf formula per line.",
    )
    args = parser.parse_args()

    try:
        formulas = load_formulas(args.constraints_file)
        check_constraints(formulas)
    except (OSError, RuntimeError, ValueError) as error:
        parser.exit(status=2, message=f"Error: {error}\n")


if __name__ == "__main__":
    main()

How to Use This Reference

Check the imports and function order. Match the indentation plus the final entry-point guard.

The hard-coded formula list should no longer appear at the bottom.

Secret mission

Find an Irreducible Contradictory Subset

The first conflicting prefix can contain rules that are unrelated to the contradiction. Add a deletion-based core search that removes unnecessary constraints until every remaining rule is essential to the conflict.

Clean Up Your Resources

Clean Up Your Resources

Your checker runs locally inside WSL with no ongoing usage charge. Decide whether to keep the resources, pause the active environment, or delete the project.

Resources you used:

  • The open WSL project folder containing contradiction_checker.py and constraints.txt.
  • The ltlf-checker Conda environment with Python 3.11 and Spot 2.16.2.
  • The Miniforge installation at ${HOME}/conda.
  • The downloaded Miniforge3.sh installer if it remains in WSL.

Keep everything running

No action is needed. Choose this if you want to keep testing finite-trace specifications with your checker.

  • Keep the open WSL project folder with contradiction_checker.py and constraints.txt.
  • Keep the ltlf-checker environment for future contradiction checks.
  • Keep the Miniforge installation at ${HOME}/conda.
  • Leave Miniforge3.sh in its current WSL location.

Pause - I'll come back to this later

End the active Conda session while preserving the environment. Your checker files remain ready for later.

  • Deactivate the ltlf-checker environment by running this command:
conda deactivate

What Does This Command Do?

This exits the active environment without deleting its packages or configuration. The environment remains available for another session.

The environment name should disappear from your terminal prompt. Your project files remain unchanged.

Delete - I don't want to use this again

Deletion is permanent. Choose this only when you no longer need the checker or its environment.

  • Deactivate and remove the ltlf-checker environment by running these commands:
conda deactivate
conda env remove -n ltlf-checker -y

What Do These Commands Remove?

  • The first command exits the active environment before deletion.
  • The second command removes the ltlf-checker environment with its installed Python and Spot packages.

You should see the environment removal finish without an error. The project files remain until you delete their folder.

Environment Still Active?

  • Run the deactivation command before trying the removal again.
  • Check that the environment name has disappeared from your terminal prompt.
  • Help me remove the Conda environment safely.
  • Delete the open WSL project folder from its parent location in the WSL filesystem.
  • Confirm the project folder no longer appears in that location.
  • Delete Miniforge3.sh from the WSL location where you downloaded it.
  • Confirm Miniforge3.sh no longer appears in that location.
  • Keep ${HOME}/conda if another Conda environment depends on it.
  • Delete ${HOME}/conda only if no other Conda environment depends on it.
  • Confirm ${HOME}/conda no longer appears in the WSL filesystem after deletion.

Nice Work!

Nice Work!

Excellent work! You've built a reusable command-line checker that pinpoints the first LTLf constraint to make an ordered specification contradictory. The optional core analysis reduces that conflict to one irreducible contradictory subset.

You've learned how to:

  • Build a file-driven contradiction checker that loads formulas from constraints.txt. The checker returns a clear SATISFIABLE or CONTRADICTION result.
  • Use Spot 2.16.2 to translate each formula into an MTDFA. Isolated checks demonstrate why individual satisfiability cannot establish joint consistency.
  • Apply incremental DFA language intersection with spot.product(). Calls to is_empty() reveal the first conflicting constraint. Calls to num_states() expose the cumulative automaton size.
  • Secret Mission: Extend the checker with --core to return one irreducible contradictory subset containing F approved plus G !approved.

Ready to quiz yourself?