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

*From*: "G.Cordier" <jg.cordier@xxxxxxxxx>*Date*: Fri, 6 May 2022 05:58:06 -0700 (PDT)*References*: <57858f0a-8b02-474f-9206-c2118c408ccen@googlegroups.com> <9EAB03D6-B561-46D9-A4E9-63C7ACA4449C@gmail.com>

Hello,

Thank you Stephan, this helps, definitely.

Best

Gabriel

Gabriel

On Friday, May 6, 2022 at 2:37:51 PM UTC+2 Stephan Merz wrote:

Hello,constant expressions involve only constant operators, no variables, no primes, no temporal formulas. You can read more about levels of TLA formulas in chapter 16 of "Specifying Systems". You can use that functionality in order to evaluate constant expressions such as{ 2*i+1 : i \in 0 .. 5 }What you are really trying to do is check an invariant of a specification. To do that, tell TLC to interpret "Spec" as the specification that you are checking and "Init" as the invariant to check. For example, in the TLA+ Toolbox, create a new model, make sure that Spec appears in the "What is the behavior spec?" section of the Model Overview pane, and add Inv as an invariant in the "What to check?" section of that pane.Hope this helps,StephanOn 6 May 2022, at 14:28, G.Cordier <jg.co...@xxxxxxxxx> wrote:Hi,

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

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

I get the following error"Level error in applying operator $Tuple:

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

For instance, if I check the below theorem T,

/// TLA Specs: BEGINNINGEXTENDSNaturalsVARIABLEh

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

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

Spec == Init /\ [][Next]_hTHEOREMT == Spec => []Init/// TLA SPECS: ENDthen I get the error message. I am really puzzled...

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.

BestGabriel--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57858f0a-8b02-474f-9206-c2118c408ccen%40googlegroups.com.

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/8483b69c-b77e-4484-876a-94af6acac275n%40googlegroups.com.

**References**:

- Prev by Date:
**Re: [tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator"** - Next by Date:
**[tlaplus] TLA+ Toolbox issues?** - Previous by thread:
**Re: [tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator"** - Next by thread:
**[tlaplus] TLA+ Toolbox issues?** - Index(es):