| Hi Ioannis,
as you noticed (and as stated on the Web site), the parser of the PM rejects any bindings involving tuples, such as
\E <<x,y>> \in S : ... or { ... : <<x,y>> \in S }
The next major release of TLAPS will be based on the SANY parser, so this limitation will disappear, but we don't know yet when the release will be ready.
Additionally, the backends currently have extremely poor support for functions that take more than one argument, such as in your example
g == [a, b \in S |-> TRUE]
THEOREM g = [a, b \in S |-> TRUE]
BY DEF g
If you look at the messages in the TLAPM console, you'll see that SMT, Zenon and Isabelle all complain about unsupported constructs. For the moment, I recommend as a workaround that you use "curried" functions instead and replace
[a,b \in S |-> TRUE] by [a \in S |-> [b \in S |-> TRUE]]
and similarly
[S \X T -> U] by [S -> [T -> U]]
Thanks for reminding us about this issue, which has been on our to-do list for too long already ...
Regards, Stephan
This question seems to be answered by the documentation about partially supported features [1],
but I would like to confirm I am not doing something wrongly.
`tlapm` does not parse syntax of the form: `[<< a, b >> \in S |-> TRUE]`, so it appears to be unsupported.
`tlapm` parses `[a \in S, b \in S |-> TRUE]` and `[a, b \in S |-> TRUE]`, but it does not prove equality,
as shown in the module below. Is such syntax unsupported by `tlapm == 1.4.3`?
Does the development version of `tlapm` support syntax of this form?
Searching through the repository for usage of `|->`, I couldn't find any example of this form, except for a comment [2].
[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html
[2] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/src/oldpm/expr.ml#L81
Best regards,
ioannis
------------------------------- MODULE test --------------------------------
(* tlapm --version
1.4.3 (build 34695)
*)
CONSTANT S
(* `tla2sany test.tla` confirms that the theorem below is well formed (p.304).
`tlapm -v -C test.tla` raises:
File "./test.tla", line 3, character 8
required expressions(s) missing before '['
File "<unknown>":
Error: Could not parse "./test.tla" successfully.
tlapm ending abnormally with Failure("Module.Parser.parse_file")
*)
(*
f == [<< a, b >> \in S |-> TRUE]
THEOREM f = [<< a, b >> \in S |-> TRUE]
BY DEF f
*)
(* The below is well formed too, but `tlapm` raises:
Error: Could not prove or check:
ASSUME NEW CONSTANT S,
g == [a, b \in S |-> TRUE]
PROVE g = [a, b \in S |-> TRUE]
*)
g == [a, b \in S |-> TRUE]
THEOREM g = [a, b \in S |-> TRUE]
BY DEF g
(* `tlapm` can prove the following claims. *)
h == [a \in S |-> TRUE]
THEOREM h = [a \in S |-> TRUE]
BY DEF h
p == [t \in S \X S |-> << t[1], t[0] >> ]
THEOREM p = [t \in S \X S |-> << t[1], t[0] >> ]
BY DEF p
================================================================================
--
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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|