Skip to content

Expectations regarding record values causing error #53

@Vanlightly

Description

@Vanlightly

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]

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions