Hi Frederic,
1 - Can we have a macro that returns a macro? I suppose no.
I don't understand this, because macros don't "return" anything.
Perhaps what want a macro uses another macro. This is allowed,
as long as the macro being used precedes the macro using it.
2 - In pcal the variables generated by the parameters of the
procedures appears after the macros, it is unfortunate.
I don't understand this, because the variables I believe you are
talking about are part of the TLA+ translation, and the macros are in
the PlusCal source.
3 - Suppose I want to develop an algorithm with pcal under toolbox .
There are several procedures. I want to test each procedure with a
model before testing the main algorithm. There is no simple way to
have models that do that I think. I mean we can't have a model that
tests a procedure, another model that tests another procedure and
eventually a model that tests the main algorithm.
I don't know of any programming language that lets you test a
procedure; they only let you test a program that calls the procedure.
If you describe how you would do what you want for procedures in a
program, perhaps we can figure out how it should be done in PlusCal.
Cheers,
Leslie
1 - Can we have a macro that returns a macro? I suppose no.
I don't understand this, because macros don't "return" anything.
2 - In pcal the variables generated by the parameters of the
procedures appears after the macros, it is unfortunate.I don't understand this, because the variables I believe you are
talking about are part of the TLA+ translation, and the macros are in
the PlusCal source.
I don't know of any programming language that lets you test a
procedure; they only let you test a program that calls the procedure.
1 - Can we have a macro that returns a macro? I suppose no.
I don't understand this, because macros don't "return" anything.
I wanted a macro like:Macro(a,b) = Test(x) == x.out = a /\ x.in = bThat way I could write later:SelectSeq(u, Macro(1,2))
I do not understand what you intend but this must be wrong. You can only pass expressions as arguments to operators (such as SelectSeq), whereas you seem to intend your Macro to produce a definition. Definitions are not expressions in TLA+.
Secondly, I do not understand the example because SelectSeq is a ternary operator, and the second and third argument are expected to be integers whereas the right-hand side of your Test operator is a Boolean expression.
3 - Suppose I want to develop an algorithm with pcal under toolbox . There are several procedures. I want to test each procedurewith a model before testing the main algorithm. There is no simple way to have models that do that I think. I mean we can't havea model that tests a procedure, another model that tests another procedure and eventually a model that tests the main algorithm.
SelectSeq(u, LAMBDA x : Test(1,2,x))
Hi Frederic,
Each model is stored in a separate directory, along with the version
of the spec on which it was last run. And models can be locked.
However, I don't see the use of essentially keeping a separate copy of
each procedure in a model since, if testing the entire algorithm
reveals that a procedure needs to be changed, you'd want to change
that copy as well.
Anyway, all programming languages have some form of procedure. If no
one has thought it important enough to add such a feature to their
debugging tools, I have no reason to believe that it will be useful
enough to warrant adding it to the Toolbox. Especially when there are
so many other things that we'd like to do if we had the time.
Leslie
Anyway, all programming languages have some form of procedure. If no
one has thought it important enough to add such a feature to their
debugging tools,
Hi Frederic,
You're right; I wasn't thinking. The Java debugger allows one to
execute any method that's callable in the current context. Debuggers
are based on executing code one step at a time. You can't do that in
TLC. Instead, you can start TLC in any state by specifying the
appropriate Init predicate. So you can check any procedure by
starting in an initial state in which control is at the beginning of
the procedure. Of course, if you want to execute the procedure by a
single process in a multi-process algorithm, you'll have to change the
next-state action.
Debugging a procedure by itself makes sense in programming. But it
doesn't make much sense testing the procedure inside a debugger,
manually entering each input. Instead, one writes a "harness"--a
program that calls the procedure repeatedly and checks its output.
You can do that just as well in PlusCal by making each harness a
separate spec.
However, PlusCal isn't a programming language; it's much more
expressive than any programming language. I wonder if you're not
taking advantage of that. It sounds like you're writing a procedure
to compute a value. Why are you doing that rather than just writing a
TLA+ operator that computes the value and using the operator in an
expression in the PlusCal algorithm? If you're using PlusCal to help
you write a program, then you can write a separate little PlusCal
algorithm that implements the computation of the operator.
Breaking a program into procedures is a method of hierarchical
decomposition. You write and test the separate parts, then write and
test the program that combines the parts. This is a bottom up
procedure. If you find out that combining the parts doesn't work, you
have to re-implement some of the parts and try again. TLA+ allows you
to work top-down. You write a specification of what the system is
supposed to do. You then implement that specification as a set of
components, showing that if each of the components satisfies its
specification, then their combination satisfies the system's
specification. You then implement each component, knowing that if
each component meets its specification, then the system meets its
specification. The downside of the top-down approach is that it's
possible that you discover you're unable to implement a component that
satisfies its spec, so you have to re-do your high-level
implementation. Preventing that looping requires the engineering
skill to know what you can implement. Preventing looping in a
bottom-up development requires the much rarer ability of being able to
figure out in your head how a collection of components are going to
work when put together.
Maybe you should be working top-down instead of bottom-up.
Leslie
You write a specification of what the system is
supposed to do. You then implement that specification as a set of
components, showing that if each of the components satisfies its
specification, then their combination satisfies the system's
specification. You then implement each component, knowing that if
each component meets its specification, then the system meets its
specification.
A solution might be to have a library of boosted specifications. For
example a specification of a sorting algorithm but with a piece of
code behind to speed up TLC.
The only good reason to write a library module to aid model checking
is to define operators that TLC can't handle (except perhaps at
exorbitant computation cost) without overriding the definition with
Java code. For example, it seems to be impossible to define Seq so
that TLC can evaluate the expression seq \in Seq(Nat) when seq is a
sequence. For example, there was no need for the standard Bags
module.
The problem of writing a sorting operator that TLC can evaluate
efficiently is discussed in Section 9.2 of the Hyperbook. The
definition given there is five lines long. The time-complexity of
that algorithm is O(n^2). If you need a more efficient algorithm, you
could find one in an algorithm book somewhere and code it as a
recursively defined TLA+ operator. But if O(n^2) isn't good enough,
you are probably using TLA+ to do things it wasn't meant to do.