Re: [tlaplus] parsing invariant string during tlc run

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 07.10.2018 07:54, Ciprian TEODOROV wrote:
> I'm trying to develop an interactive simulator for TLA, 
> In the simulator I want let the user to interactively add invariants
> (something like watch expressions in traditional debuggers)
> is there a way to parse an user supplied expression and link it to a
> running Tool instance (tlc2.tool.Tool) ?

Hi Ciprian,

can you outline your idea some more? What does an interactive simulator
do? Do you want to build on the existing simulator (which is currently
being overhauled [1])? If yes, why not simply restart the simulator when
a new invariant is added?

I suggest you create a GitHub issue [2] to discuss the technical details.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues/147
[2] https://github.com/tlaplus/tlaplus/issues