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

*From*: Ian Wilkinson <ian.wi...@xxxxxxxx>*Date*: Tue, 5 May 2015 03:36:54 -0700 (PDT)*References*: <9323db0d-63f1-49f8-9c10-f880113eacc9@googlegroups.com> <e523b095-f67a-4b50-bd86-b1088f216cc2@googlegroups.com>

Hi Leslie, Disaster! Defeated in the second paragraph. Yes, we would be employing real numbers. Apologies, we should have given greater care on consideration and discovery on TLA+ support for this. Conceptually, it sounded a fine approach for us. Hugely grateful for insight, ian On Tuesday, May 5, 2015 at 11:12:17 AM UTC+1, Leslie Lamport wrote: > Hi Ian, > The answer to your question depends on what you want to do with the > specifications you write. My guess is that you want to write > algorithms in TLA+/PlusCal, debug the algorithms using the TLC model > checker (or possibly by writing proofs of correctness that you check > with the TLAPS proof system), and then implement those algorithms in > programs (probably in Python with SciPy and NumPy). If this guess is > incorrect, please stop reading now and tell us what you do want to do > with the specifications. > If you're still reading, the answer depends on whether your algorithms > manipulate real numbers (presumably implemented in the programs with > floating-point arithmetic). If they do, then TLA+ is probably not for > you because TLC does not do arithmetic with real numbers. (If you > only want to write proofs the answer is probably the same because > TLAPS does not have good facilities to handle real arithmetic, but > it's not completely out of the question.) > If you've gotten this far, then your algorithms use only integer > arithmetic and things look promising. So, we come to your question > about SciPy and NumPy, about which I know nothing. Wikipedia tells me > that NumPy provides an efficient implementation of dynamic > multi-dimensional arrays. TLA+ (and hence PlusCal) handles "dynamic > multi-dimensional arrays" (which are simply what mathematicians call > functions over a Cartesian product). However, it does not provide > "efficient implementation". Model checking effectively does > exhaustive testing of a small model of the algorithm--for example, > over all arrays with a very small dimension and a small number of > elements. How big "small" is depends on the application. > As for SciPy, it seems to be a mixed bag. Probably none of the things > it offers are already built into TLA+. Some things are obviously not > something TLA+ is good for--like plotting. Anything that involves > mathematical computations can in principle be written in TLA+. > Anything that can be described by a mathematical function is probably > easy to write in a few lines of TLA+. Other things, like symbolic > math, might be too much work to be worth the effort. Again, don't > expect efficiency. > Leslie

**References**:**Availability of foundation modules with SciPy and NumPy capability***From:*ian . wi . . .

**Re: Availability of foundation modules with SciPy and NumPy capability***From:*Leslie Lamport

- Prev by Date:
**Re: Availability of foundation modules with SciPy and NumPy capability** - Next by Date:
**Spec explorer improvement in 1.5.x (was Re: [tlaplus] Re: Toolbox 1.5.0 release candidates)** - Previous by thread:
**Re: Availability of foundation modules with SciPy and NumPy capability** - Next by thread:
**Toolbox running under Java 1.8** - Index(es):