[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] parsing invariant string during tlc run
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) ?
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 )? If yes, why not simply restart the simulator when
a new invariant is added?
I suggest you create a GitHub issue  to discuss the technical details.