Dear Çagatay,
Thanks for taking the time to write down your ideas. What I will do
now is show you how to do what I think you want in the current
Toolbox. It won't be nearly as convenient as you want, but I think it
will show that we don't need any fundamental change to the logical
structure of the Toolbox. If I'm right, then you can get what you
want by improving the Toolbox interface.
First of all, your proposal is based on a misconception of what is
required to evaluate an _expression_. In general, evaluating an
_expression_ requires a model to specify the values of declared
constants and a pair of states to specify the values of primed and
unprimed declared variables. Constant expressions can be evaluated on
a model. Expressions with constants and unprimed variables can be
evaluated on a state in a model. (The state may contain model
values.) You cannot evaluate anything on "the initial state" of a
specification because a specification can permit many initial states
(often infinitely many). It follows from this that your notebook must
exist within a model of a specification.
I believe you have a single specification--the one you're writing--and
you want to be able to open multiple notebooks on it. Let's call that
single specification S. Make each notebook a separate specification.
The root module EXTENDS S and contains any definitions and
declarations you want to add. The interface you described has a
single model for this notebook specification, although you can have
multiple models. The notebook's changes to the definitions of S are
made in the model (see the Advanced Model page).
Put the constant expressions you want evaluated in the notebook as the
elements of a tuple in the model's Evaluate Constant _expression_
section. Arbitrary expressions (including primed expressions) can be
evaluated on error traces in the Error-Trace Exploration section of
the TLC Errors window. (You need to have the error window to enter
those expressions, but once entered they appear whenever the error
window is opened.)
- Instead of making a notebook a new specification, perhaps
it could be the copy of the spec saved with a model, as I
suggested in a response to Chris.
- The method of entering and displaying the values of
constant expressions and non-constant expressions could be
made more consistent--e.g., multiple constant expressions
enabled by check boxes.
- Some mouse clicking should be replaced by keystrokes.
As I've indicated before, instant evaluation won't be possible without
significant changes to TLC. You'll probably have to click or type a
command to re-evaluate expressions when the spec changes, although
it's possible to do it when you save changes to the spec. Moreover,
if evaluation of one _expression_ fails with an error, then the
evaluation of everything will probably fail.
However, before worrying about convenience, you should try this method
of implementing what I think you want to do. The design of the
Toolbox was based on 10 years of experience using TLA+ and TLC.
Using the Toolbox this way will let you see if you really want
to do what you now think you do. And let us know what you find out.
Leslie