Metadata-Version: 2.1
Name: pluscal
Version: 0.2.0
Summary: PlusCal AST and builder in Python
Home-page: https://github.com/jessemyers/pluscal
Author: Jesse Myers
License: Apache 2.0
Keywords: PlusCal TLA+
Platform: UNKNOWN
Classifier: Programming Language :: Python :: 3.7
Requires-Python: >=3.7
Description-Content-Type: text/markdown
Provides-Extra: dist
Requires-Dist: bumpversion (>=0.5.3) ; extra == 'dist'
Requires-Dist: pip (>=19.0.3) ; extra == 'dist'
Requires-Dist: setuptools (>=40.8.0) ; extra == 'dist'
Requires-Dist: twine (>=1.13.0) ; extra == 'dist'
Provides-Extra: lint
Requires-Dist: flake8 (>=3.7.7) ; extra == 'lint'
Requires-Dist: flake8-isort (>=2.7.0) ; extra == 'lint'
Requires-Dist: flake8-print (>=3.1.0) ; extra == 'lint'
Provides-Extra: test
Requires-Dist: coverage (>=4.5.3) ; extra == 'test'
Requires-Dist: nose (>=1.3.7) ; extra == 'test'
Requires-Dist: PyHamcrest (>=1.9.0) ; extra == 'test'
Provides-Extra: typehinting
Requires-Dist: mypy (>=0.670.0) ; extra == 'typehinting'

# pluscal

[PlusCal][1] AST and builder in Python

 [1]: https://lamport.azurewebsites.net/tla/p-manual.pdf


## What Is This?

`PlusCal` is an algorithm language that compiles into a `TLA+` specification. This library defines
*Python types* that form an abstract syntax tree (AST) of the `PlusCal` P-Syntax grammar as well as
a *builder* API for fluently constructing algorithms. The implementation leans heavily on Python
`dataclasses` and type-hinting; a type checker (e.g. `mypy`) can be used to validate the grammar.

It is anticipated that this library will be used both by humans and by programs to construct grammatically
correct specifications and run them through the TLC model checker.


## Usage

Install from pip:

    pip install pluscal

Create an algorithm:

```python
>>> from pluscal.api import Algorithm, Print, Variable

>>> algorithm = Algorithm(
    "hello_world",
).declare(
    Variable("s").in_set("Hello", "World!"),
).do(
    Print("s", label="A"),
)

>>> print(algorithm)
--algorithm hello_world
variable s \in {"Hello", "World!"};
begin
  A:
    print s;
end algorithm
```


## Limitations

This library is not complete. Some known limitations include:

 1. The lower-level `TLA+` grammar used by the `Expr`, `Field`, `Label`, `Name`, and `Variable` types
    are neither modeled nor validated fully. These types are essentially strings at this time.

 2. The validation logic does not express the full nuances of `PlusCal`, especially as it relates to
    label placement.

 3. Some language features, especially as related to fairness, are not yet implemented.


