[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>


More information about the Tlaplus-users mailing list