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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 19 Dec 2022 10:53:48 +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> <AE5956FE-C390-494C-ABC6-BFAD42E75818@gmail.com> <eeb46b71-9813-45e7-a7a6-cedd7f443b91n@googlegroups.com>

Since Character is now a parameter rather than containing fixed char codes between 0 and 256, the variable flag must now be a function with domain Character. You want to modify its initialization to flag = [g \in Character |-> -1]; Also, in the initial loop, the instruction flag[i] := 1 should certainly be flag[p] := 1 (as it indeed was in your initial version of the PlusCal algorithm). Please do not rely on members of this Google group for debugging errors in your specification. 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/B97FBBAA-78D3-435A-BA81-1F59DE9EEDE6%40gmail.com. |

**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

**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] Converting TLA+ spec to PlusCal** - Previous by thread:
**Re: [tlaplus] Functions in the standard libraries** - Next by thread:
**[tlaplus] Converting TLA+ spec to PlusCal** - Index(es):