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