hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
183 stars 39 forks source link

Fix BecomesNull argument in Action Properties example #57

Closed federicobond closed 1 year ago

federicobond commented 1 year ago

The previous argument resulted in the following parser error:

The level of argument 1 exceeds the maximum level allowed by the operator.

I'm just learning TLA+ so I cannot verify this, but looks reasonable from a pure functional evaluation semantic.

federicobond commented 1 year ago

Btw, does "level" mean something to people experienced in TLA+ or is it just an implementation detail of the compiler?

Could be a good opportunity to rewrite that error message for clarity.

hwayne commented 1 year ago

There are four levels of operators:

  1. Constant operators (Five == 5)
  2. Operators with parameters (Add(x, y) == x + y)
  3. Actions (Inc(x) == x' = x + 1)
  4. Temporal formula ([][Inc(var)]_var)

Generally this only matters for errors like this. Good to add to a troubleshooting section though.

federicobond commented 1 year ago

Thanks for the explanation! Yeah, a troubleshooting section with common errors could be super helpful.