# [Tlaplus-users] Infinite (isabelle) loops

Maniatis, Petros petros.maniatis at intel.com
Jeu 1 Juil 16:32:20 CEST 2010

```Kaustav, you are right!

The reason for my confusion is I've started with a very similar obligation
about records on which isabelle gives up for no apparent reason to me.

I've been trying to gradually simplify that obligation by small rewrites,
trying to morph it into one of the examples that we know work. In the process
I stopped waiting for isabelle to give up and interrupted it after a minute.

Lesson learned: you can't hurry exhaustive search...

That said, I'd love to know if you have any ideas why the following module
fails to check (tlapm, uninterrupted, gives up after 2.5 minutes), while the
one after it (which only differs on missing a few conjuncts in the implication
to prove) checks fine.  If A=>B is provable and checkable then A/\C=>B should
be provable and checkable also, right?

Thanks!

Petros

-----------------------------------------MODULE
TestFails-------------------------------------------------------
VARIABLE State
CONSTANT NOPATTERN
CONSTANT Expire(_,_,_)
CONSTANT BLAH
CONSTANT BUZ
VARIABLE MommieTypeInvariant
THEOREM
ASSUME \A n, m, c :
Expire(n, m, c)
=> State'
= [[State EXCEPT
!.zaz = [State.zaz EXCEPT
![n] = BUZ]] EXCEPT
!.zbz = BLAH],
MommieTypeInvariant
=> State
= [zaz |-> State.zaz, zbz |-> State.zbz,
zcz |-> State.zcz,
zdz |-> State.zdz],
MommieTypeInvariant'
=> State'
= [zaz |-> (State').zaz, zbz |-> (State').zbz,
zcz |-> (State').zcz,
zdz |-> (State').zdz]
PROVE  \A n, m, c :
(/\ Expire(n, m, c)
/\ MommieTypeInvariant
/\ MommieTypeInvariant')
=> (/\ State'
= [[State EXCEPT
!.zaz = [State.zaz EXCEPT
![n] = BUZ]] EXCEPT
!.zbz = BLAH])
OBVIOUS
=========================================================================================================

-----------------------------------------MODULE
TestChecks-------------------------------------------------------
VARIABLE State
CONSTANT NOPATTERN
CONSTANT Expire(_,_,_)
CONSTANT BLAH
CONSTANT BUZ
VARIABLE MommieTypeInvariant
THEOREM
ASSUME \A n, m, c :
Expire(n, m, c)
=> State'
= [[State EXCEPT
!.zaz = [State.zaz EXCEPT
![n] = BUZ]] EXCEPT
!.zbz = BLAH],
MommieTypeInvariant
=> State
= [zaz |-> State.zaz, zbz |-> State.zbz,
zcz |-> State.zcz,
zdz |-> State.zdz],
MommieTypeInvariant'
=> State'
= [zaz |-> (State').zaz, zbz |-> (State').zbz,
zcz |-> (State').zcz,
zdz |-> (State').zdz]
PROVE  \A n, m, c :
(/\ Expire(n, m, c))
=> (/\ State'
= [[State EXCEPT
!.zaz = [State.zaz EXCEPT
![n] = BUZ]] EXCEPT
!.zbz = BLAH])
OBVIOUS
=========================================================================================================

-------------- 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/936b7641/attachment-0001.bin>
```