on tlaps semantics

[Алексей Тимаков]

Hi all

Can anyone tell me why this assumption cannot be proved.

THEOREM TEST4 == ASSUME NEW P1, NEW P2, NEW pred1 (_,_), NEW l, NEW pred2(_),
                        l =  {x \in {pred1(c1, c2) : c1 \in P1, c2 \in P2} : pred2(x)}
                        PROVE \A l1 \in l : \E s1 \in P1, s2 \in P2 : l1 = pred1(s1, s2)
                 PROOF OBVIOUS  

or even

THEOREM TEST2 == ASSUME NEW P1, NEW P2, NEW pred1 (_,_), NEW l,
                        l =  {pred1(c1, c2) : c1 \in P1, c2 \in P2}
                        PROVE \A l1 \in l : \E s1 \in P1, s2 \in P2 : l1 = pred1(s1, s2)
                 PROOF OBVIOUS   

Thanks.

[Stephan Merz]

Hello,

for me both of your theorems are proved (by the SMT backend). Can you use SMT to prove simple theorems such as

THEOREM

   ASSUME NEW x \in Int

   PROVE x+1 = 1+x

   OBVIOUS

or do you perhaps have a problem with your TLAPS installation?

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bd3b0337-27ab-40e7-9eef-faf5d4c34256n%40googlegroups.com.

[Алексей Тимаков]

Hello.

TLAPS seems to work normal.

четверг, 24 марта 2022 г. в 19:00:09 UTC+3, Stephan Merz:

[Stephan Merz]

Your theorem TEST3 is proved by Zenon and Isabelle, unlike the two others, so this doesn't prove that the SMT backend works correctly in your installation. The screenshot shows an error message "Cannot reach fixed point" that comes from a pre-processing step of SMT. If you are adventurous, you may try downloading the current version of TLAPS [1] and compiling from source [2].

Hope this helps,

Stephan

[1] https://github.com/tlaplus/tlapm

[2] See INSTALL at [1], but use a more recent version of OCaml, such as 4.11. https://tla.msr-inria.inria.fr/tlaps/content/Download/Source.html may also be useful, but you should be able to use your existing versions of Zenon and Isabelle.

On 25 Mar 2022, at 08:20, Алексей Тимаков <timako...@gmail.com> wrote:

Hello.

TLAPS seems to work normal.

<Screenshot from 2022-03-25 10-16-23.png><Screenshot from 2022-03-25 10-17-13.png>

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/47586f9c-e56f-41f7-9cea-3e9daa29e245n%40googlegroups.com.
<Screenshot from 2022-03-25 10-17-13.png><Screenshot from 2022-03-25 10-16-23.png>

[Алексей Тимаков]

Seems strange. If i copy the theorem into standalone specification it works.

пятница, 25 марта 2022 г. в 10:32:52 UTC+3, Stephan Merz:

[Алексей Тимаков]

Ohh. Found.

It happens because my spec extends Apalache.tla module which includes recursive operations.

https://github.com/informalsystems/apalache

пятница, 25 марта 2022 г. в 14:31:21 UTC+3, Алексей Тимаков:

[Stephan Merz]

Glad you could sort this out. By the way, the upcoming release of TLAPS will at least not choke on recursive operator definitions.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c8d8000f-4bd2-4c61-b0d1-9e690dab85d4n%40googlegroups.com.

[Алексей Тимаков]

Thanks a lot.

пятница, 25 марта 2022 г. в 14:38:40 UTC+3, Stephan Merz: