Model Checking Toolkit for Python
Project description
Model Checking Toolkit (MCTK)
Model Checking Toolkit in Python.
Overview
mctk
is a Python library for Explicit-State Model Checking (will also support Symbolic Model Checking and Bounded Model Checking in the future) on Kripke Structures (will also support other Transition Systems) supporting the CTL(Computation Tree Logic) operators: EX, EU, and EG.
Users can create checker instances to formally verify if a Kripke Structure (can be created during runtime or input in a JSON file) satisfies certain CTL properties. The checker instance will return a set of satisfying states and "SAT" if satisfied or an Error Trace if unsatisfied.
Getting Started
Installation
Get the latest version of mctk
from PyPI:
pip3 install mctk
If you are having trouble with pip3
, you can also install from the source code, see Developing.
Developing
Clone this Repository to your Local Environment
git clone https://github.com/marcusm117/mctk.git
Go into the Repository Directory
cd mctk
Install the Library with all Dependencies
make develop
Linting & Testing
We use a Makefile
as a command registry:
make format
: autoformat this library withblack
make lint
: perform static analysis of this library withblack
,flake8
andpylint
make annotate
: run type checking usingmypy
make test
: run automated tests withpytest
make coverage
: run automated tests withpytest
and collect coverage information
Usage
from mctk import KripkeStruct
ks = KripkeStruct()
ks.set_atoms(["p", "q"])
ks.add_state("s0", 0b10)
ks.add_state("s1", 0b01)
ks.set_start(["s0"])
ks.add_trans({"s0": ["s1"], "s1": ["s0"]})
Contributing
All contrbutions are welcome!
Please read CONTRIBUTING.md for details.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.