Stephan, yes, linear arithmetic is all that I need. I'll paste some Z3 code below as a small example of what might be produced by my imagined TLA+ model.
I originally thought encoding symbolic expressions (or polynomials, or in some cases rationals) would be a way to get around the lack of support for reals, but then it became clear I would be duplicating what some SMT solvers do anyway, so I started looking for an SMT front-end that could give me that.
The reason for wanting a front-end is so I can work easily with both transition systems and real numbers (linear arithmetic for the vast majority of problems of interest to me, and I would guess others, in analysis and control).
Thanks also for the links to dReal and MetiTarski, which might come in handy for other problems.
I haven't looked at the TLAPS code base, and am not sure if I would be a help or a hindrance, but I would be happy to participate in some way if this is of interest, recognizing you must have other priorities.
John
--
(declare-const x Real)
(declare-const y Real)
(declare-const ab Real)
(declare-const ba Real)
(declare-const bc Real)
(declare-const cb Real)
(assert (> x 10))
(assert (< x 100))
(assert (> y 10))
(assert (< y 100))
(assert (= x (- (* 0.5 (+ (+ 0 (- (* (+ (+ 0 ba) bc) 0.5) (- (* 0.5 (* 0 (+ 0 ab))) ba))) (- (- (* (+ (+ 0 ba) bc) 0.5) bc) (* 0.5 (* (+ 0 cb) 1))))) (- (* (* (+ 0 (- (- (* 0 (+ 0 ab)) ab) (* (* (+ (+ 0 ba) bc) 0.5) 0.5))) 0) 0.5) (- (* (+ (+ 0 ba) bc) 0.5) (- (* 0.5 (* 0 (+ 0 ab))) ba))))))
(assert (= y (- (- (- (- ba (* 0.5 (* 0 (+ 0 ab)))) (* 0.5 (+ (+ 0 ba) bc))) (* 0.5 (* 0 (+ 0 (- (- ab (* 0 (+ 0 ab))) (* 0.5 (* 0.5 (+ (+ 0 ba) bc)))))))) (* 0.5 (+ (+ 0 (- (- ba (* 0.5 (* 0 (+ 0 ab)))) (* 0.5 (+ (+ 0 ba) bc)))) (- (- bc (* 0.5 (+ (+ 0 ba) bc))) (* 0.5 (* 1 (+ 0 cb)))))))))
(assert (= x y))
(check-sat)
(get-model)
; $ ./z3 -smt2 foo.z3
; sat
; (model
; (define-fun ba () Real
; (/ 22.0 3.0))
; (define-fun cb () Real
; (/ 88.0 3.0))
; (define-fun y () Real
; 11.0)
; (define-fun x () Real
; 11.0)
; (define-fun bc () Real
; 0.0)
; )
On Sunday, October 12, 2014 5:23:31 AM UTC-4, Stephan Merz wrote:
If there is demand, extending the SMT backend of TLAPS for handling real numbers is not difficult. What fragment of reasoning about real numbers are you interested in? Current solvers behave very erratically outside the fragment of linear real arithmetic, although several groups are looking into different approaches for effectively supporting non-linear real arithmetic: you may want to have a look at dReal (http://dreal.cs.cmu.edu/#!index.md), MetiTarski (http://www.cl.cam.ac.uk/~lp15/papers/Arith/) or Redlog (http://www.redlog.eu).
The Event-B language as defined by Abrial does not have real numbers (see e.g. http://wiki.event-b.org/images/EventB-Summary.pdf), and as far as I know there is no implementation of its provers that handles real numbers.
Stephan
On 12 Oct 2014, at 10:18, Leslie Lamport <tlap...@xxxxxxxxx> wrote:
> I don't know what SAL is, but translating TLA+ into any backend prover is a formidable task. You would probably wind up writing a possibly correct translation for a tiny subset of TLA+. Since there already exists a TLA+ to Z3 translation, it would probably be easier to produce a complete translation to Z3 that can reason about reals. I don't know if the Event-B prover handles reals. If it does, another possible alternative is to modify their TLA+ to Event-B translator to allow you to do that. However, that would probably be hard because I don't imagine that they translate proofs. Hand translating to another prover seems to be the only reasonable alternative to modifying TLAPS.
>
> Leslie