[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "G.Cordier" <jg.cordier@xxxxxxxxx>*Date*: Fri, 6 May 2022 05:28:34 -0700 (PDT)

Hi,

When I check a constant _expression_ with the TLA+ Tool box,

(Model > Model Checking Results : Evaluate constant _expression_),

I get the following error

The level of argument 2 exceeds the maximum level allowed by the operator"

For instance, if I check the below theorem T,

/// TLA Specs: BEGINNING

Init == h \in (0 .. 23)

Next == h' = (h+1)%24

Spec == Init /\ [][Next]_h

/// TLA SPECS: END

Could someone please explain me (1) what does such error message mean, (2) where does the error come from, (3) how to evaluate theorems and constant expressions?

Thank you very much by advance.

Best

Gabriel

-- 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 on the web visit https://groups.google.com/d/msgid/tlaplus/57858f0a-8b02-474f-9206-c2118c408ccen%40googlegroups.com.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] How to read a liveness dot dump** - Next by Date:
**Re: [tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator"** - Previous by thread:
**Re: [tlaplus] How to read a liveness dot dump** - Next by thread:
**Re: [tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator"** - Index(es):