[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLAPS 1.2.1 released

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. 


On Friday, September 13, 2013 5:27:15 PM UTC+2, Chris Newcombe wrote:
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,


On Fri, Sep 13, 2013 at 7:18 AM, Damien Doligez <damie...@xxxxxxxx> wrote:
Dear TLA+ users,

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

It is available as usual at:

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

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...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.