parsing invariant string during tlc run

[Ciprian TEODOROV]

Hi,

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) ?

best regards,

ciprian

[Markus Kuppe]

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

[Leslie Lamport]

I presume the tool you want to build stores its data in the tool field
of the nodes in the semantic tree, so reparsing the spec isn't an
option.  The ability to parse an expression in the context of any
point in a spec is something that I said should be implemented in the
parser.  This was either forgotten or ignored by the implementers of
the parser and would probably be very difficult to add now.  However,
it might not be too difficult to modify the parser to allow it to
parse a new module that EXTENDS an already parsed module.  That may be
your best bet.  And it could have other uses--for example so the
entire spec doesn't have to be reparsed to run the Spec Explorer.  But
beware that the original implementer of the Toolbox was unable to get
TLC to use the output the parser provided to the Toolbox instead of
having to parse the spec again.  I think that was TLC's fault and

not the parser's, but I'm not sure.

Let's take this discussion off the group.

Leslie