A Python implementation of a Computation Tree Logic (CTL) model checker that represents state sets symbolically using Binary Decision Diagrams (BDDs). A reference explicit-state checker is included for comparison and benchmarking.
The project requires Python 3.10+. Source code lives in src/
, and unit
tests are in tests/
.
git clone <repo-url>
cd cs6840finalProject
python3 -m venv venv
source venv/bin/activate # On Windows: .\venv\Scripts\activate
pip install -r requirements.txt
Execute the test suite from the repository root:
pytest
A minimal demonstration is provided in example_usage.py
:
python example_usage.py
The script prints a label and result for each CTL formula, e.g.:
BDD EF p: True
BDD AG p: False
...
Explicit A[q U p]: False
Two benchmarking scripts live in the benchmarks/
directory:
run_benchmarks.py
compares runtime and peak memory usage of the BDD and explicit checkers on a ring topology.variable_order.py
measures the effect of reversing the BDD variable order on a simple chain.
Run them from the repository root:
python benchmarks/run_benchmarks.py
python benchmarks/variable_order.py
Sample results are available in BENCHMARK_RESULTS.md.
For an overview of project goals, module layout, and example workflows, see PROJECT_DOCUMENTATION.md.