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

[tlaplus] Overriding operator which is used in a temporal property


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 ==

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.


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/7b2ac6e8-f04e-4067-a893-3bb8f85a30a6n%40googlegroups.com.