diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a5ee6fa..67c87a7 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -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 diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index ba10ce7..dd6d5f5 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -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: | diff --git a/.gitignore b/.gitignore index 37396e7..eacb868 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ +# Temporary Files +tmp/ + # Coverage Report python_junit.xml diff --git a/MANIFEST.in b/MANIFEST.in index 4819e53..36d04a3 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -9,7 +9,6 @@ include Makefile prune .vscode prune .github -prune scripts prune docs exclude .gitignore exclude .gitattributes diff --git a/Makefile b/Makefile index dd749c9..f555066 100644 --- a/Makefile +++ b/Makefile @@ -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 @@ -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: @@ -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 @@ -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 diff --git a/README.md b/README.md index 2098a2d..3db67bc 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # 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/) @@ -8,7 +8,7 @@ `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 @@ -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) diff --git a/docs/tutorials/getstarted.md b/docs/tutorials/getstarted.md index 764d01a..211b858 100644 --- a/docs/tutorials/getstarted.md +++ b/docs/tutorials/getstarted.md @@ -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/) @@ -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) diff --git a/mctk/__init__.py b/mctk/__init__.py index 7236459..97a140c 100644 --- a/mctk/__init__.py +++ b/mctk/__init__.py @@ -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 diff --git a/mctk/checking.py b/mctk/checking.py index 052a28c..0560dad 100644 --- a/mctk/checking.py +++ b/mctk/checking.py @@ -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. @@ -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) diff --git a/mctk/models.py b/mctk/models.py index bfb9a7d..e99c72d 100644 --- a/mctk/models.py +++ b/mctk/models.py @@ -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 diff --git a/mctk/tests/test_checking.py b/mctk/tests/test_checking.py index 3edcd70..44bd682 100644 --- a/mctk/tests/test_checking.py +++ b/mctk/tests/test_checking.py @@ -1,6 +1,7 @@ # Authors: marcusm117 # License: Apache 2.0 + # Standard Libraries from copy import deepcopy diff --git a/mctk/tests/test_models.py b/mctk/tests/test_models.py index c0c47cb..76009ee 100644 --- a/mctk/tests/test_models.py +++ b/mctk/tests/test_models.py @@ -1,6 +1,7 @@ # Authors: marcusm117 # License: Apache 2.0 + # Standard Libraries from collections import defaultdict diff --git a/pyproject.toml b/pyproject.toml index cc14bdf..b0d5325 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -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" @@ -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",