[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Best practice when building a series of model refinements?
If you are using command line, you may consider adding the libs flag.
The following is how I run sany in cli.
# this is the sany syntactic analyzer, which parses and checks the spec for syntax errors.
! 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).
this screencast  shows how to refine specs in different folders
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.