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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 19 Dec 2022 09:56:57 +0100*References*: <6c72f651-82f0-416c-b01f-744a7bef5662n@googlegroups.com> <ECAA9F9A-1BE6-4CB9-A832-56E384F2A9D8@gmail.com> <1d759b36-d03a-4bb3-a33a-7ba05d47914dn@googlegroups.com> <B34824F7-21B5-4757-9DB0-6655E72E42C7@gmail.com> <17c1a443-829b-4c81-8119-f4414211af8en@googlegroups.com> <405d1a39-1eca-451c-b85e-f11aa8cf5b41n@googlegroups.com> <11a602f5-3bef-4262-8645-765b6079e5fdn@googlegroups.com> <EC81EA75-9368-473C-A651-17347531F655@gmail.com> <8d453cbb-7202-4d1d-83ec-1cd9057529d7n@googlegroups.com> <304E30C5-9126-49B0-A7B7-554AFE28954B@gmail.com> <710c16c8-29c7-4813-aa47-2de91a324d7an@googlegroups.com>

Hello, you forgot to click on "set of model values" when instantiating the set "Character". Attached is the TLA+ module and a screenshot of how the instance should be displayed. TLC indicates an error when evaluating the _expression_ text[i+j] since both i and j may be 0. Please remember that TLA+ sequences are indexed from 1, not 0. But the instantiation works. Stephan 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/AE5956FE-C390-494C-ABC6-BFAD42E75818%40gmail.com. |

**Attachment:
bm.tla**

-- 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/AE5956FE-C390-494C-ABC6-BFAD42E75818%40gmail.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/AE5956FE-C390-494C-ABC6-BFAD42E75818%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**References**:**[tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Andrew Helwer

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

**Re: [tlaplus] Functions in the standard libraries***From:*Stephan Merz

**Re: [tlaplus] Functions in the standard libraries***From:*mohan radhakrishnan

- Prev by Date:
**Re: [tlaplus] Functions in the standard libraries** - Next by Date:
**Re: [tlaplus] Functions in the standard libraries** - Previous by thread:
**Re: [tlaplus] Functions in the standard libraries** - Next by thread:
**Re: [tlaplus] Functions in the standard libraries** - Index(es):