Operators from standard modules do not work

[lemmy]

---- MODULE Issue7 ----
EXTENDS TLC, Naturals, FiniteSets

VARIABLES x

Init == x = {}

Next == x' = Cardinality(x)

====

---- MODULE Issue7 ----
EXTENDS TLC, Naturals, Sequences

VARIABLES x

Init == x = <<>>

Next == x' = Len(x)

====

TypeError: Cannot read properties of undefined (reading 'length')
    at eval.js:900:40
    at lodash.min.js:98:241
    at lodash.min.js:54:66
    at ue (lodash.min.js:35:327)
    at Function.Kc [as mapValues] (lodash.min.js:98:213)
    at evalEq (eval.js:896:30)
    at evalBoundInfix (eval.js:1025:16)
    at evalBoundInfix (eval.js:2079:15)
    at evalExpr (eval.js:1598:16)
    at evalExpr (eval.js:2070:15)

[lemmy]

/cc @fhackett-ms

[lemmy]

---- MODULE Issue7 ----
EXTENDS Sequences

VARIABLES x

Init == x = DOMAIN <<>>

Next == x' = x

====

TypeError: Cannot read properties of undefined (reading 'length')
    at eval.js:900:40
    at lodash.min.js:98:241
    at lodash.min.js:54:66
    at ue (lodash.min.js:35:327)
    at Function.Kc [as mapValues] (lodash.min.js:98:213)
    at evalEq (eval.js:896:30)
    at evalBoundInfix (eval.js:1025:16)
    at evalBoundInfix (eval.js:2079:15)
    at evalExpr (eval.js:1598:16)
    at evalExpr (eval.js:2070:15)

[will62794]

Partially addressed in 806197a, 30f4151, 56b2ab8, f498057

Some of the remaining standard modules that are not fully implemented:

• Bags
• Sequences
• FiniteSets

See also #14 for some notes on handling module semantics more generally.

[lemmy]

Some of them will need CHOOSE, which doesn't seem supported:

---- MODULE Issue7 ----
Len(s) == CHOOSE n \in Nat : DOMAIN s = 1..n

VARIABLE x

Init == x = CHOOSE n \in {1,2,3} : TRUE

Next == x' = x
====

Note that the semantics of CHOOSE are difficult to implement.

[will62794]

Preliminary CHOOSE support added in 338d5ae.

[will62794]

Closing for now in favor of new issues that can be scoped to specific, unimplemented standard module operators as they come up.