[Tlaplus-users] Infinite (isabelle) loops
petros.maniatis at intel.com
Jeu 1 Juil 15:45:27 CEST 2010
So for now, the rule of thumb is to keep field names short or apply a
preprocessing step to make them short?
I'll try, thanks :)
Intel Labs Berkeley
From: Stephan Merz [mailto:Stephan.Merz at loria.fr]
Sent: Wednesday, June 30, 2010 6:32 AM
To: tlaplus-users at lists.gforge.inria.fr
Cc: Maniatis, Petros
Subject: Re: [Tlaplus-users] Infinite (isabelle) loops
thanks for alerting us to this problem. As Kaustuv points out, TLA+ records
are functions whose domains are finite sets of strings, and strings are
sequences of characters (which in turn are encoded as pairs of hexadecimal
numbers). So comparing strings takes time linear in the length of field
names, and in fact with a non-negligeable constant factor, which is
reflected in Isabelle's warning about simplification depth.
Here is hoping that better support for strings and records within Zenon will
alleviate that problem by reducing the constant overhead. If not, we'll have
to change the encoding of strings and records, maybe at the cost of
incompatibility with standard sequence operations.
On 30 Jun 2010, at 14:52, Kaustuv Chaudhuri wrote:
> Hi Petros,
> I am not able to duplicate your observation. Your second Test.tla
> seems to work fine for me on TLAPS version 0.9.2010_04_06_03. Tt does
> take some time for Isabelle to prove it -- about two minutes on my
> Core 2 Duo (T7250) laptop.
> Since record field names are strings and strings are sequences in TLA,
> even simple operations like = and # are linear in the length of the
> field names. So you will generally observe some slowdown in the
> provers if you use long field names.
> The "simplification depth exceeded" message is a benign warning
> produced by Isabelle.
> Stephan might be able to provide a better answer.
> -- Kaustuv
-------------- section suivante --------------
Une pièce jointe autre que texte a été nettoyée...
Taille: 7151 octets
Desc: non disponible
More information about the Tlaplus-users