-
Notifications
You must be signed in to change notification settings - Fork 15
Open
Description
I have a specification that, in a LET, can set a value to either a model value called None, or a record value. This breaks TLA web with the following error recVal.applyArg is not a function. This is because sometimes the value is a record and sometimes it is the model value None.
How to reproduce:
The spec I am testing is in this Gist: https://gist.github.com/Vanlightly/3683f6419b8504996a0adfba3959db70
Simply uncomment the CompletePartialTxn action and its line in the Next state formula to reproduce. The problematic line in CompletePartialTxn(b, tid) is: txn_metadata == tc_tid_metadata[b][tid]
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels