[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Ioannis Filippidis <jfili...@xxxxxxxxx>*Date*: Thu, 20 Apr 2017 11:55:04 -0700*References*: <1c29745d-b435-4513-be61-d7f4f1240963@googlegroups.com> <241ADACA-96AD-4340-B38B-ADABEF37B826@gmail.com>

Hi Stephan,

Thank you for explaining this behavior and suggesting currying as a workaround.

I used a definition of the form:

H(f) == [t \in Z \X Z |-> f[t[2], t[1]]]

and that led to some reasoning in the proofs about the domain having the

form of a Cartesian product. In this case it was convenient to keep working

with functions of tuples, but I will try currying the next time this arises.

About the error messages from the backends, I was running `tlapm -v` from the

command line, and there it prints fewer details about the kind of backend

errors. It did record the following messages in the file `test.tlaps/fingerprints`

(which can be viewed in readable form with `tlapm --printfp`):

isabelle : unsupported operator function (tuple)

Zenon: unsupported operator Fcn (tuple)

(I should have used the toolbox.)

Best regards,

ioannis

Thank you for explaining this behavior and suggesting currying as a workaround.

I used a definition of the form:

H(f) == [t \in Z \X Z |-> f[t[2], t[1]]]

and that led to some reasoning in the proofs about the domain having the

form of a Cartesian product. In this case it was convenient to keep working

with functions of tuples, but I will try currying the next time this arises.

About the error messages from the backends, I was running `tlapm -v` from the

command line, and there it prints fewer details about the kind of backend

errors. It did record the following messages in the file `test.tlaps/fingerprints`

(which can be viewed in readable form with `tlapm --printfp`):

isabelle : unsupported operator function (tuple)

Zenon: unsupported operator Fcn (tuple)

(I should have used the toolbox.)

Best regards,

ioannis

On Thu, Apr 20, 2017 at 1:03 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:

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 exampleg == [a, b \in S |-> TRUE]

THEOREM g = [a, b \in S |-> TRUE]

BY DEF gIf 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,StephanOn 19 Apr 2017, at 22:41, Ioannis Filippidis <jfili...@xxxxxxxxx> wrote: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/ fd345f78c7e356b53c67e24f17e99d f449d7b3a3/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+unsubscribe@googlegroups.com .

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 .

--

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@googlegroups.com .

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 .

**References**:**tuples in function constructors using tlapm ?***From:*Ioannis Filippidis

**Re: [tlaplus] tuples in function constructors using tlapm ?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLA+ model of OneThirdRule algorithm from "A Reduction Theorem" paper** - Next by Date:
**Re: [tlaplus] TLA+ model of OneThirdRule algorithm from "A Reduction Theorem" paper** - Previous by thread:
**Re: [tlaplus] tuples in function constructors using tlapm ?** - Next by thread:
**tlapm Error** - Index(es):