Re: parsing invariant string during tlc run

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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

On Sunday, October 7, 2018 at 7:54:11 AM UTC-7, Ciprian TEODOROV wrote:

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