Metadata-Version: 2.4
Name: vitamin-model-checker
Version: 1.6.1
Summary: The VITAMIN model checker python package
Author: VITAMIN Team
License: SOURCE-AVAILABLE NON-COMMERCIAL LICENSE
        
        Copyright (c) 2026 VITAMIN-organization.
        All rights reserved.
        
        Permission is granted to use, copy, modify, and distribute this software
        and derivative works solely for non-commercial research and educational
        purposes, provided that:
        
        1. The original copyright notice and this license notice are preserved.
        2. Proper attribution is given to the original authors.
        3. Any modified version or derivative work that is distributed must make
           its complete source code available under this same license.
        4. The software may not be used, sold, sublicensed, hosted, integrated,
           or otherwise exploited for commercial purposes without prior written
           permission from the copyright holder.
        
        Commercial use includes, but is not limited to, use by for-profit entities,
        use in commercial products or services, paid consulting, internal business
        operations, SaaS offerings, cloud services, or use that provides commercial
        advantage.
        
        NO PATENT LICENSE
        
        No patent license, express or implied, is granted under this license.
        All patent rights are reserved. Use of this software may be covered by
        pending or issued patent rights. Any patent license must be obtained
        separately in writing from the relevant patent holder.
        
        NO WARRANTY
        
        This software is provided "as is", without warranty of any kind, express
        or implied, including but not limited to the warranties of merchantability,
        fitness for a particular purpose, and non-infringement. In no event shall
        the authors or copyright holders be liable for any claim, damages, or
        other liability arising from the use of the software.
        
Project-URL: Homepage, https://github.com/VITAMIN-organisation/vitamin-model-checker
Project-URL: Repository, https://github.com/VITAMIN-organisation/vitamin-model-checker
Project-URL: Documentation, https://github.com/VITAMIN-organisation/vitamin-model-checker/tree/main/docs
Project-URL: Issues, https://github.com/VITAMIN-organisation/vitamin-model-checker/issues
Project-URL: Changelog, https://github.com/VITAMIN-organisation/vitamin-model-checker/blob/main/CHANGELOG.md
Keywords: model-checking,multi-agent-systems,temporal-logic,CTL,ATL,LTL,vitamin,verification
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: License :: Other/Proprietary License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: ply==3.11
Requires-Dist: numpy<1.27.0,>=1.26.0
Requires-Dist: pydantic>=2.7.0
Provides-Extra: dev
Requires-Dist: pytest>=7.4.0; extra == "dev"
Requires-Dist: pytest-cov>=4.1.0; extra == "dev"
Requires-Dist: pytest-mock>=3.11.0; extra == "dev"
Requires-Dist: pytest-asyncio>=0.23.0; extra == "dev"
Requires-Dist: pytest-timeout>=2.0.0; extra == "dev"
Requires-Dist: pytest-xdist>=3.6.0; extra == "dev"
Provides-Extra: docs
Requires-Dist: mkdocs>=1.5.0; extra == "docs"
Requires-Dist: mkdocs-material>=9.5.0; extra == "docs"
Requires-Dist: mkdocstrings[python]>=0.24.0; extra == "docs"
Dynamic: license-file

# VITAMIN Model Checker

Core Python library for model checking multi-agent systems. It provides formula
parsers, game-structure parsers, and explicit-state algorithms for CTL, ATL, LTL,
and many extensions.

**Requirements:** Python 3.11+

## Install

```bash
pip install vitamin-model-checker
```

Development install from a checkout:

```bash
python3 -m venv .venv
source .venv/bin/activate
pip install -e ".[dev,docs]"
```

## Quick start

```python
from model_checker.algorithms.explicit.CTL.CTL import model_checking

result = model_checking("AG p", "path/to/model.txt")
print(result)
```

Most logics expose the same `model_checking(formula, filename)` entry point and
return a plain dict suitable for serialization.

Higher-level helpers are available from the public API:

```python
from model_checker import FormulaParserFactory, execute_model_checking_with_parser

parser = FormulaParserFactory.get_parser("CTL")
# execute_model_checking_with_parser(...) for integrated workflows
```

### Supported logics

Built-in formula logics include ATL, ATLF, CapATL, CTL, IATL, ICTL, LTL, NatATL,
NatATLF, NatSL, OATL, OL, RABATL, RBATL, TCTL, TOL, and Wallet_ATL. Model
structures include CGS, BCGS, CostCGS, CapCGS, WalletCGS, and timedCGS. See
`pyproject.toml` entry points (`vitamin.parsers`, `vitamin.models`,
`vitamin.benchmarks`) for the full registry.

## Documentation

- Architecture, file formats, and logic guides live under `docs/`
- API reference pages are generated with MkDocs (`pip install -e ".[docs]"` then
  `mkdocs serve`)

## Repository role

| Project | Role |
|---|---|
| `vitamin-model-checker` | Core Python library. |
| `vitamin-benchmark-model-checker` | pyperf benchmark tool for this package. |
| `vitamin-module-integrator` | Validates logic bundles and applies them to this repo. |
| `vitamin-workbench` | User-facing web/API application that calls the model checker. |

For the cross-project view, see [docs/vitamin-stack.md](docs/vitamin-stack.md).

Links:

- Homepage: https://github.com/VITAMIN-organisation/vitamin-model-checker
- PyPI: https://pypi.org/project/vitamin-model-checker/
- Issues: https://github.com/VITAMIN-organisation/vitamin-model-checker/issues

## Run tests

```bash
pytest model_checker/tests/unit/
pytest model_checker/tests/integration/
pytest model_checker/tests/

make test          # unit + integration style suite, excluding slow tests
make test-models   # full model_checker/tests suite
```

Test-suite details live in `model_checker/tests/README.md`.

## Build docs

```bash
pip install -e ".[docs]"
mkdocs serve
mkdocs build --strict
```

## Benchmarks

Benchmark this package with `vitamin-benchmark-model-checker`, a separate pip
package that times `model_checking()` across logics via the `vitamin.benchmarks`
entry points declared here.

```bash
pip install vitamin-benchmark-model-checker
vitamin-benchmark --logic CTL --output ctl.json
```

For local development with a checkout of both repos:

```bash
pip install -e .
pip install -e ../vitamin-benchmark-model-checker
```

See the `vitamin-benchmark-model-checker` README for compare mode, plots, and
the full benchmark matrix.

## Docker

Docker is mainly for isolated build/test checks:

```bash
cd docker
make build
make test
```

See `docker/README.md` for the Docker workflow.

## Adding logic

The recommended path is to package a new logic as a VMI bundle, validate it with
`vitamin-module-integrator`, and let the integrator apply the files and entry
points to this repository.

Manual in-repo changes are still useful for maintainers working directly on the
core package. See `docs/adding_a_new_logic.md` for both workflows.

## License

Distributed under the SOURCE-AVAILABLE NON-COMMERCIAL LICENSE. See LICENSE for
the full text. Commercial use requires prior written permission from the
copyright holder.
