Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Expectations regarding record values causing error #53

Open
Vanlightly opened this issue Dec 19, 2024 · 0 comments
Open

Expectations regarding record values causing error #53

Vanlightly opened this issue Dec 19, 2024 · 0 comments

Comments

@Vanlightly
Copy link

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]

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant