Best practice when building a series of model refinements?

40 views
Skip to first unread message

david streader

unread,
Feb 26, 2020, 10:34:53 PM2/26/20
to tlaplus
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

unread,
Feb 27, 2020, 1:13:50 AM2/27/20
to tla...@googlegroups.com
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
Screenshot from 2020-02-26 22-01-19.png

Markus Kuppe

unread,
Feb 27, 2020, 8:34:15 PM2/27/20
to tla...@googlegroups.com
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

unread,
Feb 27, 2020, 9:54:40 PM2/27/20
to tlaplus
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



Shiyao MA

unread,
Feb 27, 2020, 9:55:45 PM2/27/20
to tlaplus
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

unread,
Feb 27, 2020, 10:37:26 PM2/27/20
to tla...@googlegroups.com
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
Reply all
Reply to author
Forward
0 new messages