# [tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator" • From: "G.Cordier" <jg.cordier@xxxxxxxxx> • Date: Fri, 6 May 2022 05:28:34 -0700 (PDT) • Ironport-data: A9a23:OTLL16PIrcd01F3vrR0/ksFynXyQoLVcMsEvi/4bfWQNrUor1GMEz 2VOWDvQP/rcZ2qhf99xYd7i9xgOvsDWzYUwHnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EsLd9IR2NYy24DkW13V4 LsenuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB23vM9qz fcR7qfpUBYNNa/Qx+dNXTlhRnQW0a1uoNcrIFC6uM2XilTaKj7imqU1Sk4xOoIc96B8BmQmG f4wcmhcKEDewbvomPTiGrIEascLdKEHOKsDvnh4ySzCTvwgSrroZ5Tg2uJ1h2sRrOoSQNeEX OggTBVWQTjuWyZpAX4/B5U5k+OliWP4biVD7lmSoMLb5kCKl1chgOSxarI5fPSIX+dagEaf/ FjLxGv7JUExH+Oukza8pyfEaujnxHunAur+DoaQ+v9xi0CI3UQPDBRQUECh5Pi/kE+3HdNZM U0dvCQ0xZXe72SuR9j5GgSk+TuK505HHdVXFOI+5UeGza+8Dxul6nYscB1ec9kE6JQNHCU78 lSLg4zqVTJPiejAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQMaIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srEHHtLNOddbCCFaGu 3cAlo6V6+Vm4XCxeM6lH7ll8FKBvazt3NjgbbhHQ8ZJG9OFpy/LQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp3lPe4So+7DK+ENLKih6SdkifXrEmCgmbAjwjQfLQEzMnTx L/AL53zVyhEYUiZ5GPsGb1NuVPU+szO7TqLGcqTI+WP3r2Za3qYIYrpw3PfBt3VGJis8VW92 48HaaOikkwDOMWjPHS/2dNNfDgicChqbbir+pc/XrPScmJORjt9Y9ePmulJU9I+z8xoehLgp CHVtrlwkwWu2hUq6GyiNhheVV8Ydcsh/S9jYXxwbD5FGRELOO6S0UvWTLNvFZFPyQCp5acco yAtd5rSD/JRZC7A/jhBP5DxoJY7KkakggWBOyeqej8iZ4UmTAvMo4e2cgzq/SgILyy2qcpv8 +b7j1iEH8UOF1Z4EcLbSPOz1Fft73ITr+R/AhnTKd5JdUSwrYVncnSjjvI+L8wWBw/Ewz+Wi 1SfDRsC9LvCpoY09J/CgqXd99WlFO53H0x7GWjH7ObuZXOKoDb7mYIZCbSGZzHQUm/w6Z6OX +QNwqGuKuADkXZLr5F4TORmwKc40N3l+O1XwwFiK3PUNgj5B75lJE6G6slBrKh6wLFU5FmtU UWV99gGYLiENZq+Ql4cLQYodN6OzfUFhj7W4ahnKUn2/nYprrWAVkpWMhaWjzFFN/1+N4Z8m bUtv8sf6gqejBs2M4fW1XsNrDvScXFQAb86spw6AZPwjlZ5wF91Z5GBWDT954uCaokRP0Qnf m2Uia7Fi+gOz0bOaSBvR33E3O4YnIhX/R4TnAREKFOOld7IwPQw2UQJozgwSw1UyDRB0v5ya jc3bRwrff3W8mc6ntVHUkCtBxpFWE+T9Hv3xgZbj2beVUSpCjHAITxvPeeW4H0f6H9WejQHr riUxHy7AWTvdcD1wixgVklipPjuQsZ26xXZ3cWuGc2KEtphPmq03vLwNTVR8kWkHMUqmUfcr vNr9utYZqr8OiodrLc8FpGBk78XTUncdmBFRPhg+oIPHH3dKWHpgmHVdB7ud5MfPeHO/G+5F 9dqepBFWSO42XvctTscH6MNf+J5kfJ1ttMOdqm3dDwGr6eHtWgu953K8TXmnykkRNJhlct7I YTUMD2YFXGIwmdQknfJsdIDIXeyetIeZQfx0e3pov8FEYkP7LNlfU0oiOfmunyUNE5+40vRs lqTPOnZyOttzYkqlIzpS/0RCwKxINL1deKJ7AHj7IgUPI2XaZ/D51EPt13qHwVKJr9NCd55o rKA7Yzs10TfsbdqDm3UlvFtzUWSCRlegQaWDi72EJWetS6LWcup+gdavm7heccPn9Ra6c2qA QC/baNcsDLTt8h1nBVoh+p2Sn7xyJgbqo/voiSyq/mDEB8AyReBJ9SinZMsRX8ObTcGYvUSF Set08tDJblkQEBkCxgDCPVrDIV/PUf4H6AhcrUdcNVe4naA2ju/h1cpqfbsBfwnxJVJ/AYWL K8pniTDSSk= • Ironport-hdrordr: A9a23:pLWRPasqAKtTfL++2xAvcrzK7skD6dV00zEX/kB9WHVpm62j5r qTdZEgv3LJYVkqKRUdcLy7Sc69qZ21z+8A3WE+VY3SKTUO+1HYXb2L1OPZsk/d8lTFh5lgPM RbAtND4GiaNykFsS+F2njALz96+qj5zEnAv463pAYOcegNUdAd0+5XMGmm+yZNNXF77PQCZf yhDgsunUvCRZ3VVKqG77s+M9QqF7bw5eHbiNI9ZiLOGGK1/E6VAXfBc2n84j4uFwlXybNn22 nImQ706+GCtLWU0RnBzgbonuRrpOc= • Ironport-sdr: w0u3ZQxyn1B0Jg+zEmpjMB2/xUxLwcc0zrz/Lr8umH2dQRNI+yH9L+79SnTwkekSTIxZstyHAq b02Kvbs4+7FM7xR8EzQl6ZeumCzStgE9YUlV0V8j9bOnr6UFaeLqFAtm6hsD+PS9jmCTexYuIv OW3RPrHPcj/Sc7bXy6jxhWJ6ouzpGziRX8/pJYMoGp+8V1jUeABlsNBSTk4O/sqAXjJ3hO++qI vtihKkextPU1iEj8XnycpGnkyPm+qGvWTj7D0E9nE8xBtoBjNiDqq8VrmxfDCPbAN0jd0P08wi wwY+fxbcuhZCxy0RwD38W5I0 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: BEGINNING
EXTENDS Naturals
VARIABLE h

Init == h \in (0 .. 23)
Next == h' = (h+1)%24
Spec == Init /\ [][Next]_h

THEOREM T == Spec => []Init
/// TLA SPECS: END

then 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.

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.