mctk-py 0.0.1

Model Checking Toolkit for Python

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 with black
• make lint: perform static analysis of this library with black, flake8 and pylint
• make annotate: run type checking using mypy
• make test: run automated tests with pytest
• make coverage: run automated tests with pytest 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.