[Tlaplus-users] Infinite (isabelle) loops

Maniatis, Petros petros.maniatis at intel.com
Jeu 1 Juil 15:45:27 CEST 2010


Hi Stephan,

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 :)

Petros

------
Petros Maniatis
Research Scientist
Intel Labs Berkeley 


-----Original Message-----
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

Hi Petros,

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.

Stephan


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...
Nom: smime.p7s
Type: application/x-pkcs7-signature
Taille: 7151 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/tlaplus-users/attachments/20100701/98cecdb1/attachment.bin>


More information about the Tlaplus-users mailing list