Skip to main content

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:

  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.

    See section 3.7 of the PlusCal manual.

  3. 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.

Filename, size & hash SHA256 hash help File type Python version Upload date
pluscal-0.4.2-py2.py3-none-any.whl (30.9 kB) Copy SHA256 hash SHA256 Wheel py2.py3
pluscal-0.4.2.tar.gz (12.3 kB) Copy SHA256 hash SHA256 Source None

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page