[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Advanced TLC: views and module overrides

On 25.04.2018 02:00, Andrew Helwer wrote:
> Markus mentioned module overrides in his recent TLC talk, and views came
> up in an issue on GitHub. Both of these topics are mentioned in the
> Specifying Systems TLC chapter, but not in enough detail to get them to
> work. They are of great interest to me in a spec I am currently writing.
> I have the following questions:
> 
>  1. Given a spec with some set of variables, what steps are required to
>     get TLC to run using a view on a subset of those variables? As far
>     as I can tell, we have to do something like the following:
>       * Define a tuple of variables in the TLA+ spec; these are the
>         variables you'll use in your view
>       * Use the VIEW keyword in the MC.cfg file of your model to expose
>         the view above
>       * Add the view in the TLC advanced options
>       * Add the -view flag to the TLC command line flags
>  2. Given a TLA+ module defining some operators, how do I implement
>     those operators in Java and get TLC to use the Java implementation
>     while model-checking?

Hi Andrew,

I uploaded an addendum to my talk [1] which shows how to setup a view in
the Toolbox. You will have to use a recent nightly build of the Toolbox
though that includes the fix [2] to correctly display the error trace
under a view.

With regards to module overrides, you can follow the steps outlined as
part of the Tower of Hanoi specification found in the Examples
repository [3]. As for the actual Java implementation of the module
override, there is no tooling support in the Toolbox whatsoever. You
will have to create a Java project in the IDE of your choice, add
tla2tools.jar [4] to the classpath and start from there.

Cheers
Markus

[1] https://vimeo.com/266482524
[2]
https://github.com/tlaplus/tlaplus/commit/8c342af1419fa87ae9776cbef9a960593c16d69c
[3]
https://github.com/tlaplus/Examples/blob/master/specifications/tower_of_hanoi/Bits.tla
[4] https://tla.msr-inria.inria.fr/tlatoolbox/ci/dist/tla2tools.jar