[tlaplus] Re: TLC reports error (undefined identifier), but it's defined...

[Johan Persson <johan.z.persson@xxxxxxxxx>]

I have a similar issue with a simple specification for an exclusive workspace lock:

In evaluation, the identifier locks is either undefined or not an operator.

line 20, col 12 to line 20, col 16 of module WorkspaceLock

I cannot for the life of me figure out what is incorrect. Anyone got any ideas?

/ Johan

On Monday, June 10, 2019 at 6:18:13 PM UTC+2, Marko Schuetz-Schmuck wrote:

Dear All,

I'm trying to use TLC, but I'm getting the error:

In evaluation, the identifier chan is either undefined or not an
operator.

Channel is the module from Specifying Systems.

I don't see what's wrong with my specs. Any hints?

Best regards,

Marko

-- 
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/8312fbba-ed17-456e-9f11-51141643d4e2%40googlegroups.com.

Attachment: WorkspaceLock.tla
Description: Binary data