Add support for 'STRING' in PlusPy

[amanshaikh75]

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?

[lemmy]

There is nobody actively maintaining PlusPy, but we can probably review a PR. By the way, TLC has now also an executor mode. It can execute a blocking queue and a prototype of asynchronous game of life.

[amanshaikh75]

Hi @lemmy - thanks for your message. Can you tell me a bit more about the executor mode of TLC? I tried looking around but could not find any information about it.

[lemmy]

Like PlusPy, you can map a (randomly generated) TLA+ (prefix of a) behavior to code. Can you share more about your use case?

https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/TLAPlusExecutor.java https://github.com/lemmy/BlockingQueue/blob/980e5a30fad6859662c343de34e20f34a7463c18/impl/src/org/kuppe/App.java

[amanshaikh75]

I was trying out PlusPy out of curiosity. I wanted to see what kind of things I can do when I interface with a TLA+ spec using a commonly used programming language like Python.

That said, let me take this opportunity to pick your brain on a couple of things:

(1) I have written a TLA+ spec of how route selection and propagation in BGP - protocol used for routing Internet traffic - works. In a typical scenario, I am more interested in the 'converged' state of a BGP network and how the network converges. In TLA+ parlance, this amounts to the system reaching a deadlock. When I use TLC in model checking mode, any reasonable-sized network (e.g., consisting of about 10-15 BGP speakers) leads to state-explosion which makes it hard to know if the network converges or not. I've tried running TLC in simulation and DFS mode. The latter is of great interest to me because with DFS where TLC picks exactly one state (randomly) out of 'n' possible next states should allow me to check for convergence without a state explosion. However, I think TLC seems to pick more than one state after every action. Any thoughts you can share on this would be great.

(2) I also see TLA+ specs and running TLC over them is a great way to see and learn about how your system evolves with "toy examples". Being able to tap into the system state after every action through a programmable API allows the user more freedom in "playing with" the toy examples and their behavior. In fact, being able to create a toy example and see/process its behavior via a widely used programming language like Java might make it easier for people to use and interact with a TLA+ spec without knowing much about TLA+ itself. This in turn might lower the barrier to TLA+ use. I'm probably speculating here, but I'm quite intrigued by the possibility of "interacting" with a TLA+ spec in a programmatic manner.

[lemmy]

1)

• Make sure to exploit symmetry reduction
• TLC doesn't support DFS but depth-first search iterative deepening; this mode is still exhaustive, i.e., explores all successor states
• TLC's simulation mode pick a single successor (uniformly at random)
• TLC nightly comes with experimental DFS. You can activate it by running TLC with -Dtlc2.tool.queue.IStateQueue=StateDeque

2)

• I've learned TLA+ by debugging TLC :-) It is defintely not the most efficient way to learn TLA+
• TLC now has a debugger that can step through the evaluation of the next-state relation and through the construction of the state graph
• tlaweb allows to explore specs interactively
• State-spaces (of toy examples) can be visualized with GraphViz
• Animations are a great way to understand systems

[amanshaikh75]

Thanks, Markus, for all the pointers.

BTW, it looks like PlusPy does not support 'BOOLEAN' reserved work either.