TLAPS 1.2.1 released

[Damien Doligez]

Dear TLA+ users,

We have the pleasure of introducing a new release of TLAPS: version 1.2.1.

It is available as usual at:
http://tla.msr-inria.inria.fr/tlaps/content/Download.html

Here are the main changes from version 1.1.1:

- many changes and improvements to the SMT back-ends
- addition of SMT to the default list of back-end provers
- new back-end pragmas: AllProvers[T], AllSMT[T], AllIsa[T]
- new library files with theorems on functions and finite sets (experimental)
- speed improvements in the handling of multi-module specifications
- removal of the (unsound) Cooper back-end
- addition of a back-end for using TPTP-based first-order provers (experimental)
- new option "--stretch <n>" to globally change all the timeouts on a given run
- various bug fixes

Note that we had to change the SMT back-ends to remove some soundness
bugs. This means that some of your proofs may not work any more. In that
case, you should try Z3 instead of the default CVC3, or decompose the
failing steps into more detailed proofs.

On some Linux machines, the binaries may fail with this error message:
libc.so.6: version `GLIBC_2.15' not found
In this case, you will have to update your Linux or recompile from source.
If there is enough demand, we will provide binaries for these machines.

Thanks for your support and have fun with TLA+

-- Damien Doligez for the TLA+ team

[Chris Newcombe]

Hi Damien,

This is great news, thankyou!  I'm looking forward to trying it.

On this:

   >> many changes and improvements to the SMT back-ends

Does this include any direct support for sequences?  Or do we need to continue to use SequencesTheorems.tla?

many thanks,

Chris

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.

[hernan.vanzetto]

Hi Chris,

There have been no changes in this release to the sequences translation in the SMT backend. We still have it as a priority, hopefully for the next release. For the moment the best is to continue using the SequencesTheorems.tla library. 

Best,

Hernán

[freder...@laposte.net]

It would be nice. I have spent several hours to compile eveything. And I
still have problems with a "smt3" that is not found

By the way may I suggest that a combined release with batteries included
could help the end user. I mean toolbox, tlaps end so on

[freder...@laposte.net]

(I rewrite my post because google had sent it before I had finished it.)

Hi Damien

> If there is enough demand, we will provide binaries for these machines.

It would be nice. I have spent several hours to compile eveything. And I
still have problems with a "smt3" that is not found

By the way may I suggest that a joint release with batteries included
could help the end user. I mean that the release would include
toolbox, tlaps, tlaplus and compilers as well.

(That would solve problems of versioning.)

That way you would simply plug the directory in /usr/local, run the
build and get everything that fits your machine with no
problems with too recent versions of libc or of inadequate compilers.

--
FL

[ivans...@gmail.com]

Where can one download linux binaries? The link here http://tla.msr-inria.inria.fr/tlaps/content/Home.html amusingly uses cygwin to get a *nix environment on windows, but doesn't provide linux binaries.

Thanks,
Ivan

[Stephan Merz]

Dear Ivan,

have you noticed the tab called "Linux" to the left of the Download pane from where the binary is available? The direct link is http://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries/Linux.html. (Haven't tried it myself but pretty sure that it's got nothing to do with Cygwin.)

Stephan

[Ivan Alagenchev]

Ah. Thanks a lot Stephan. The website uses javascript to display the left menu and displays only the windows option when javascript is disabled.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/X_NEKUzIUKg/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.