Re: [tlaplus] on tlaps semantics

Stephan

On 25 Mar 2022, at 12:33, Алексей Тимаков <timakov.alan@xxxxxxxxx> wrote:

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, Алексей Тимаков:
Seems strange. If i copy the theorem into standalone specification it works.

пятница, 25 марта 2022 г. в 10:32:52 UTC+3, 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...@xxxxxxxxx> 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>

четверг, 24 марта 2022 г. в 19:00:09 UTC+3, 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

On 24 Mar 2022, at 16:45, Алексей Тимаков <timako...@xxxxxxxxx> wrote:

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.

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bd3b0337-27ab-40e7-9eef-faf5d4c34256n%40googlegroups.com.

--
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...@xxxxxxxxxxxxxxxx.
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>

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c8d8000f-4bd2-4c61-b0d1-9e690dab85d4n%40googlegroups.com.