[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.


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



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).

Markus

[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.