Re: [tlaplus] Some user feedback

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 20.11.2014 00:07, James Fisher wrote:
> My third bad experience was with the command-line tools. It took time
> and effort to install them: why a jar and a zip? Why do I have to do
> some Java-specific stuff to use it; shouldn't their Java
> implementation be an implementation detail? It then took time to work
> out how to run the programs; I didn't even know how *find out* how to
> use them. TLA+ needs to put the command-line tools first: in the
> programmer's world, command-line tools are how we interact with our
> files. In an ideal world this is how I would interact with TLA+:
> 
>     > sudo apt-get install tla
>     > man tla  # if this doesn't work, try `tla --help` or just `tla`
>     > tla repl  # play around building a spec
>     > nano clock.tla  # eventually put it in a file
>     > tla syntax-check clock.tla
>     > nano clock.tlamodel
>     > tla model-check clock.tlamodel > results.txt
>     > git add clock.tla clock.tlamodel
>     > git commit
>     > git push
>     [CI server runs tla model-check and rejects my commit if it finds
> errors]

I do have a similar setup based on Jenkins that I used for my
performance analysis of the tools.

However, I am not sure the regular TLA workflow benefits much from
continuous integration. Maybe Chris Newcombe can share how Amazon's
workflow looked like for large groups of people.

> I want my models to be
> hand-written, first-class citizens that I can put where I want, add to
> version control, etc. I want my model-checking results in a standard
> format that can be consumed by a CI server, like my unit test results.

A model is a first class citizen. The .toolbox folder and .launch files
just have meaning for the Toolbox itself. You only need the .tla and
.cfg files. E.g. see
https://github.com/lemmy/tlc-perf/tree/master/models for a SCM
controlled folder with a bunch of specs and even more models.

Markus