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--On Tuesday, April 13, 2021 at 9:47:54 PM UTC-7 pfeod...@xxxxxxxxx wrote: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
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/a80b90f7-09e0-4e34-8078-23f2b4ce3ac2n%40googlegroups.com.