PlusCal AST and builder in Python
Project description
pluscal
PlusCal AST and builder in Python
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:
>>> 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:
-
The lower-level
TLA+
grammar used by theExpr
,Field
,Label
,Name
, andVariable
types are neither modeled nor validated fully. These types are essentially strings at this time. -
The validation logic does not express the full nuances of
PlusCal
, especially as it relates to label placement.See section
3.7
of the PlusCal manual. -
Some of the fainess operations are not yet yet implemented.
See section
4.6
of the PlusCal manual.
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for pluscal-0.3.0-py2.py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4c9af118e2abc4d957970372da7d89e162d34b0359b90ad0f11ef216109ddf98 |
|
MD5 | 4dbf2a15b136bfd3779d78a5137b85d3 |
|
BLAKE2b-256 | 200f728348cf1a6fafe22670c04a81154075b5874f283f5920a7a36a691325b7 |