tlaplus/pluspy

Python interpreter for TLA+ specifications

For more information, visit http://lamport.azurewebsites.net/tla/tla.html

Contributing

Please read our contribution guide before you start working on your contribution. We also have a feature wishlist.

License

Copyright (c) 199?-2003 HP Corporation
Copyright (c) 2003-2020 Microsoft Corporation

Licensed under the MIT License

pluspy's Issues

Add support for 'STRING' in PlusPy

One of the TLA+ modules I have written uses 'STRING' which Pluspy declares is an 'unknown identifier'. Looking at pluspy.py, it seems like 'STRING' is not part of the ReservedWords list. Would it be possible to add support for STRING?

Parsing error on module preamble

This is some prose preceding the module definition.

\* WORKAROUND: Comment prose before the module definition.

---- MODULE AsyncGameOfLifeDistributed -----
VARIABLE x

Spec == x = TRUE /\ [][x'\in BOOLEAN]_x
====

markus@avocado:~/src/TLA/_specs/models/realworld/AsyncGameOfLife(master)$ pluspy -c 1 AsyncGameOfLifeDistributed
Parsing failed ['GModule', 'Concat', ("tok: no match with '----'", '* (AsyncGameOfLifeDistributed.tla:1:1)')]
[]
At position ('*', ('AsyncGameOfLifeDistributed.tla', 1), 1, True)
Traceback (most recent call last):
  File "/home/markus/src/TLA/_community/PlusPy/pluspy.py", line 4286, in <module>
    main()
  File "/home/markus/src/TLA/_community/PlusPy/pluspy.py", line 4251, in main
    pp = PlusPy(args[0], seed=seed)
  File "/home/markus/src/TLA/_community/PlusPy/pluspy.py", line 3587, in __init__
    raise PlusPyError("can't load " + file)
__main__.PlusPyError: PlusPyError: can't load AsyncGameOfLifeDistributed.tla

unknown identifier STRING (TLC.tla:121:42)

I am using EXTENDS with the TLC module (e.g at the HourClock module) and it gives me the error

unknown identifier STRING (TLC.tla:121:42) 

Regression test 11 fails

Hello, thank you for sharing PlusPy.

I just cloned the repository and tried to run tests with ./regres.scr and the test 11 failed.
I tried to run directly ./pluspy -S0 -c100 Exprs and I got can't load TLC : fatal error.

I believe the TLC module is missing. I'll link a pull request.