Best practice when building a series of model refinements?

[david streader]

Hi

    Following the common methodology of B and Event B I want to build a series of ever more complex models each a refinement of the later. 

Does TCL only work on the Root module in a directory or can I build models of any module in a directory?

Last year I used symbolic links so as not to have copies of one module in different directories but now symbolic links do not appear to be recognised.

Is best practice to build a series of directories each with a different Root-module but containing a copies of the more abstract modules that the Root module refines?  Or have I missed some thing? david

[Markus Kuppe]

Hi David,

lets assume HashSet refines ArraySet refines Set. Set.tla,
ArraySet.tla, and HashSet.tla are all located in the same (OS)
directory. In the Toolbox, however, add a dedicated spec HashSet,
ArraySet, and Set to model check each one of them (see screenshot).

Markus

[Markus Kuppe]

On 26.02.20 22:13, Markus Kuppe wrote:
> lets assume HashSet refines ArraySet refines Set. Set.tla,
> ArraySet.tla, and HashSet.tla are all located in the same (OS)
> directory. In the Toolbox, however, add a dedicated spec HashSet,
> ArraySet, and Set to model check each one of them (see screenshot).

Hi David,

this screencast [1] shows how to refine specs in different folders
(without symlinks).

Markus

[1] https://tla.msr-inria.inria.fr/kuppe/RefinementNoSymlinksToolbox.gif

[Shiyao MA]

Hi David,

If you are using command line, you may consider adding the libs flag.

The following is how I run sany in cli.

#!/usr/bin/env bash
# this is the sany syntactic analyzer, which parses and checks the spec for syntax errors.


class_paths=(/Applications/TLA+\ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_*)
export CLASSPATH=${class_paths[${#class_paths[@]}-1]}


libs="-DTLA-Library=$HOME/.warehouse/tools/tlaplus/libs"


# sanny
! java $libs tla2sany.SANY "$@" | tee /dev/tty | grep -q error

For details, check out: https://groups.google.com/forum/#!topic/tlaplus/uL6o4Vedp7o

[Shiyao MA]

Hi Markus,

Could you post the source of the set, arrayset, and hashset.

Refinement is relatively opaque to me.  I'd like to know what role "refinement" plays here.

On Friday, 28 February 2020 09:34:15 UTC+8, Markus Alexander Kuppe wrote:

[Markus Kuppe]

On 27.02.20 18:55, Shiyao MA wrote:
> Could you post the source of the set, arrayset, and hashset.
>
> Refinement is relatively opaque to me.  I'd like to know what role
> "refinement" plays here.

See video lecture 10. of Lamport's video course:
https://lamport.azurewebsites.net/video/videos.html

The Set specs are incomplete examples that shouldn't be shared.

Markus