Overriding operator which is used in a temporal property

35 views
Skip to first unread message

pfeod...@gmail.com

unread,
Apr 14, 2021, 12:47:54 AM4/14/21
to tlaplus
Hi, 

Is there any way that I could use an overridden operator in a temporal property? E.g. `prop` is a `PROPERTY` and `MyOperator` is overridden by a Java method.

```
prop ==
  <>[]MyOperator(mainVar)
```

It works when not overridden, otherwise it gives me the following error (using the `TLAPlusOperator` interface)

Error: In evaluation, the identifier mainVar is either undefined or not an operator.

I'm doing this for a personal project and I understand that the evaluation of temporal properties is complex enough that I guess I should not be able to do this, but who knows.

Thanks

Markus Kuppe

unread,
Apr 14, 2021, 1:01:13 AM4/14/21
to tla...@googlegroups.com
Hi,

pretty much all standard operators are overridden. Please open a Github
issue with more detail.

Thanks,
Markus

Paulo Feodrippe

unread,
Apr 14, 2021, 7:28:47 AM4/14/21
to tla...@googlegroups.com
Oh yeah, right.

Thanks o/

--
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/018dfe06-2b29-3362-50b2-c97ff7fe721b%40lemmster.de.

Leslie Lamport

unread,
Apr 14, 2021, 11:44:13 AM4/14/21
to tlaplus
Pretty much all constant operators are overridden with Java code.  If you are overriding a constant operator, the problem is almost certainly in your Java code.  Try testing it with the "Evaluate Constant Expression" feature of the Toolbox.  I don't know if it's possible to override a non-constant operator with Java code, but I expect you'd need to know a lot about how TLC works to do it.

Leslie

Paulo Feodrippe

unread,
Apr 14, 2021, 7:13:25 PM4/14/21
to tla...@googlegroups.com
Yeah, I'm working on trying to understand more about TLC, it's a amusing codebase.

Thanks, Lamport and Markus o/ I will open the issue soon.

--
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.
Reply all
Reply to author
Forward
0 new messages