Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ jobs:
python-version: [3.9, 3.11]

steps:
- uses: actions/checkout@v3
- uses: actions/checkout@v4

- name: Set up Python ${{ matrix.python-version }}
uses: actions/setup-python@v4
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/doc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ jobs:
docs:
runs-on: windows-latest
steps:
- uses: actions/checkout@v3
- uses: actions/checkout@v4
- uses: actions/setup-python@v4
- name: Install dependencies
run: |
Expand Down
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
# Temporary Files
tmp/

# Coverage Report
python_junit.xml

Expand Down
1 change: 0 additions & 1 deletion MANIFEST.in
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ include Makefile

prune .vscode
prune .github
prune scripts
prune docs
exclude .gitignore
exclude .gitattributes
Expand Down
23 changes: 13 additions & 10 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ type: annotate
#########
# TESTS #
#########
test: ## clean and run unit tests
test: ## clean and run unit tests
python -m pytest -vv mctk/tests

# Alias
Expand All @@ -60,7 +60,7 @@ cov: coverage
###########
# VERSION #
###########
show-version:
show-version: ## doesn't work on Windows
bump2version --dry-run --allow-dirty setup.py --list | grep current | awk -F= '{print $2}'

patch:
Expand All @@ -76,25 +76,28 @@ major:
########
# DIST #
########
dist-build: # Build python dist
python setup.py sdist bdist_wheel
dist-build: ## build python dist, can also add bdist_wheel
python setup.py sdist

dist-check:
python -m twine check dist/*

dist: clean build dist-build dist-check ## Build dists
dist: deep-clean check dist-build dist-check ## build dists

publish: # Upload python assets
publish: ## upload python assets
echo "would usually run python -m twine upload dist/* --skip-existing"

# Alias
pub: publish


#########
# CLEAN #
#########
deep-clean: ## clean everything untracked from the repository
deep-clean: ## clean everything untracked from the repository
git clean -fdx

clean: ## clean the repository
clean: ## clean the repository, doesn't work on Windows
rm -rf .coverage coverage cover htmlcov logs build dist *.egg-info .pytest_cache


Expand All @@ -103,10 +106,10 @@ clean: ## clean the repository

# Thanks to Francoise at marmelab.com for this
.DEFAULT_GOAL := help
help:
help: ## doesn't work on Windows
@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | sort | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'

print-%:
@echo '$*=$($*)'

.PHONY: develop build install lint lints format fix check checks annotate test cov coverage tests show-version patch minor major dist-build dist-check dist publish clean-deep clean-linux help
.PHONY: develop build install lint lints format fix check checks annotate type test tests coverage cov show-version patch minor major dist-build dist-check dist publish pub deep-clean clean help
18 changes: 9 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
# Model Checking Toolkit (MCTK)

[![PyPI](https://img.shields.io/pypi/v/mctk-py?color=blue&label=PyPI)](https://pypi.org/project/mctk-py/) [![CI](https://github.com/marcusm117/mctk/workflows/CI/badge.svg?branch=dev)](https://github.com/marcusm117/mctk/actions?query=workflow%3A%22Build+Status%22) [![codecov](https://codecov.io/gh/marcusm117/mctk/branch/dev/graph/badge.svg)](https://codecov.io/gh/marcusm117/mctk) [![Docs](https://github.com/marcusm117/mctk/workflows/Docs/badge.svg?branch=dev)](https://marcusm117.github.io/mctk/) [![License](https://img.shields.io/badge/License-Apache_2.0-green)](https://github.com/marcusm117/mctk/blob/dev/LICENSE) [![Issues](https://img.shields.io/github/issues/marcusm117/FV_mctk?color=red&label=Issues)](https://github.com/marcusm117/mctk/issues)
[![PyPI](https://img.shields.io/pypi/v/mctk-py?color=blue&label=PyPI)](https://pypi.org/project/mctk-py/) [![CI](https://github.com/marcusm117/mctk/workflows/CI/badge.svg?branch=dev)](https://github.com/marcusm117/mctk/actions?query=workflow%3A%22Build+Status%22) [![codecov](https://codecov.io/gh/marcusm117/mctk/branch/dev/graph/badge.svg)](https://codecov.io/gh/marcusm117/mctk) [![Docs](https://github.com/marcusm117/mctk/workflows/Docs/badge.svg?branch=dev)](https://marcusm117.github.io/mctk/) [![License](https://img.shields.io/badge/License-Apache_2.0-green)](https://github.com/marcusm117/mctk/blob/dev/LICENSE) [![Issues](https://img.shields.io/github/issues/marcusm117/mctk?color=red&label=Issues)](https://github.com/marcusm117/mctk/issues)

[Model Checking Toolkit for Python.](https://marcusm117.github.io/mctk/)

## 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, EG, EF, AX, AU, AG, AF**, and the Propositional Logic operators: **NOT, AND, OR, IMPLIES, IFF**.

Users can use functions that implements CTL operators to formally verify if a Kripke Structure (can be created during runtime or input in a JSON file) satisfies certain CTL properties. All checking functions will return a set of states that satisfy the CTL property, which means that if any start state of the Kripke Structure is in the returned set, then the Kripke Structure satisfies the CTL property.
Users can use functions that implement CTL operators to formally verify if a Kripke Structure (can be created during runtime or input in a JSON file) satisfies certain CTL properties. All checking functions will return a set of states that satisfy the CTL property, which means that if any start state of the Kripke Structure is in the returned set, then the Kripke Structure satisfies the CTL property.

## Getting Started

Expand Down Expand Up @@ -138,13 +138,13 @@ ks_json = {
},
"Starts": ["s1"],
"Trans": {
's1': ['s2'],
's2': ['s3', 's4'],
's3': ['s4'],
's4': ['s7'],
's5': ['s6'],
's6': ['s7', 's5'],
's7': ['s5'],
"s1": ["s2"],
"s2": ["s3", "s4"],
"s3": ["s4"],
"s4": ["s7"],
"s5": ["s6"],
"s6": ["s7", "s5"],
"s7": ["s5"],
},
}
ks = KripkeStruct(ks_json)
Expand Down
16 changes: 8 additions & 8 deletions docs/tutorials/getstarted.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Getting Started

[![PyPI](https://img.shields.io/pypi/v/mctk-py?color=blue&label=PyPI)](https://pypi.org/project/mctk-py/) [![CI](https://github.com/marcusm117/mctk/workflows/CI/badge.svg?branch=dev)](https://github.com/marcusm117/mctk/actions?query=workflow%3A%22Build+Status%22) [![codecov](https://codecov.io/gh/marcusm117/mctk/branch/dev/graph/badge.svg)](https://codecov.io/gh/marcusm117/mctk) [![Docs](https://github.com/marcusm117/mctk/workflows/Docs/badge.svg?branch=dev)](https://marcusm117.github.io/mctk/) [![License](https://img.shields.io/badge/License-Apache_2.0-green)](https://github.com/marcusm117/mctk/blob/dev/LICENSE) [![Issues](https://img.shields.io/github/issues/marcusm117/FV_mctk?color=red&label=Issues)](https://github.com/marcusm117/mctk/issues)
[![PyPI](https://img.shields.io/pypi/v/mctk-py?color=blue&label=PyPI)](https://pypi.org/project/mctk-py/) [![CI](https://github.com/marcusm117/mctk/workflows/CI/badge.svg?branch=dev)](https://github.com/marcusm117/mctk/actions?query=workflow%3A%22Build+Status%22) [![codecov](https://codecov.io/gh/marcusm117/mctk/branch/dev/graph/badge.svg)](https://codecov.io/gh/marcusm117/mctk) [![Docs](https://github.com/marcusm117/mctk/workflows/Docs/badge.svg?branch=dev)](https://marcusm117.github.io/mctk/) [![License](https://img.shields.io/badge/License-Apache_2.0-green)](https://github.com/marcusm117/mctk/blob/dev/LICENSE) [![Issues](https://img.shields.io/github/issues/marcusm117/mctk?color=red&label=Issues)](https://github.com/marcusm117/mctk/issues)

[Model Checking Toolkit for Python.](https://marcusm117.github.io/mctk/)

Expand Down Expand Up @@ -136,13 +136,13 @@ ks_json = {
},
"Starts": ["s1"],
"Trans": {
's1': ['s2'],
's2': ['s3', 's4'],
's3': ['s4'],
's4': ['s7'],
's5': ['s6'],
's6': ['s7', 's5'],
's7': ['s5'],
"s1": ["s2"],
"s2": ["s3", "s4"],
"s3": ["s4"],
"s4": ["s7"],
"s5": ["s6"],
"s6": ["s7", "s5"],
"s7": ["s5"],
},
}
ks = KripkeStruct(ks_json)
Expand Down
4 changes: 4 additions & 0 deletions mctk/__init__.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,7 @@
# Authors: marcusm117
# License: Apache 2.0


from .models import KripkeStruct, KripkeStructError
from .checking import SAT_atom, NOT, AND, OR, IMPLIES, IFF, EX, AX, EF, AF, EG, AG, EU, AU

Expand Down
16 changes: 9 additions & 7 deletions mctk/checking.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
# Authors: marcusm117
# License: Apache 2.0


"""This Module contains functions for Explicit-State Model Checking CTL properties on the class KripkeStruct.

We plan to support Symbolic Model Checking and Bounded Model Checking in the future.
Expand All @@ -19,13 +21,13 @@
... },
... "Starts": ["s1"],
... "Trans": {
... 's1': ['s2'],
... 's2': ['s3', 's4'],
... 's3': ['s4'],
... 's4': ['s7'],
... 's5': ['s6'],
... 's6': ['s7', 's5'],
... 's7': ['s5'],
... "s1": ["s2"],
... "s2": ["s3", "s4"],
... "s3": ["s4"],
... "s4": ["s7"],
... "s5": ["s6"],
... "s6": ["s7", "s5"],
... "s7": ["s5"],
... },
... }
>>> ks = KripkeStruct(ks_json)
Expand Down
3 changes: 3 additions & 0 deletions mctk/models.py
Original file line number Diff line number Diff line change
@@ -1,11 +1,14 @@
# Authors: marcusm117
# License: Apache 2.0


"""This Module contains a class KripkeStruct, which is a graph implementation of Kripke Structures.

We plan to support other Transition Systems as well in the future.

"""


# Standard Libraries
from typing import List, Dict, Set, Tuple
from collections import defaultdict, UserDict
Expand Down
1 change: 1 addition & 0 deletions mctk/tests/test_checking.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
# Authors: marcusm117
# License: Apache 2.0


# Standard Libraries
from copy import deepcopy

Expand Down
1 change: 1 addition & 0 deletions mctk/tests/test_models.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
# Authors: marcusm117
# License: Apache 2.0


# Standard Libraries
from collections import defaultdict

Expand Down
3 changes: 2 additions & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ build-backend="setuptools.build_meta"

[project]
name = "mctk-py"
authors = [{name = "marcusm117", email = "marcusmin117@gmail.com"}]
authors = [{name = "marcusm117", email = "authors@gmail.com"}]
description="Model Checking Toolkit for Python"
readme = "README.md"
version = "0.1.1"
Expand Down Expand Up @@ -37,6 +37,7 @@ repository = "https://github.com/marcusm117/mctk"
[project.optional-dependencies]
develop = [
"black>=23",
"black[jupyter]",
"bump2version>=1.0.0",
"check-manifest",
"flake8>=3.7.8",
Expand Down