[tlaplus] Re: Minimum level bound on an operator?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Okay I actually just managed to figure it out approximately one minute after sending this message. Here's a parse input that will trigger it:

---- MODULE Scratch ----
VARIABLE v
op(F(_)) == F(v')
op2(x) == x'
op3 == op(op2)
====

Which results in error message:

line 5, col 8 to line 5, col 14 of module Scratch

Level error in applying operator op:
The permitted level of argument 1 of the operator argument 1 must be at least 2.

So it's about constraints on operator parameters. Dcoding the error message "The permitted level of argument 1 of the operator argument 1 must be at least 2" is a bit tricky; "argument 1 of the operator argument 1" is referring to the "_" in "F(_)" inside "op(F(_))", and "at least 2" means "either action or temporal level" (using the rubric constant = 0, variable = 1, action = "" temporal = 3). And so when we call F(v'), that asserts that F must accept at least action-level (level 2) parameters. But "op2(x)" cannot accept action-level parameters, it can only accept variable-level parameters (because it primes them and we don't want to double-prime an _expression_). So "op(op2)" triggers this constraint.

Anyway I'm sure I'll have many more of these amusing puzzles to solve & will require all your help in the future!

Andrew Helwer

On Wednesday, February 19, 2025 at 4:47:55 PM UTC-5 Andrew Helwer wrote:

I'm currently working on developing a semantic error test corpus, which is basically a large set of tiny TLA+ files that trigger all the semantic errors in SANY. This is an amusing sort of reverse-engineering process where I look at the code where an error is being raised and try to guess a TLA+ parse input that will trigger that error. There are a few I'm puzzled by: in particular, this one seems to imply it's possible for operators to have a lower bound on their accepted levels?

"Level error in applying operator " + opDef.getName() + ":\n"

"The permitted level of argument " + (j+1) + " of the operator argument "

+ (i+1) + " \nmust be at least " + opDef.getMinMaxLevel(i, j) + ".");

Does anybody know of an operator with a level lower bound, or is this dead code from a previous incarnation of the level-checker? Thanks!

Andrew Helwer

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4fd6ec23-6b95-4a24-b768-c576b35cce8dn%40googlegroups.com.