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

Re: [tlaplus] Best practice when building a series of model refinements?

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.

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


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

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

On Friday, 28 February 2020 09:34:15 UTC+8, Markus Alexander Kuppe wrote:
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).


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

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b74c5cff-6e7e-420f-be4b-e4c305bf8b04%40googlegroups.com.