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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 10 Jul 2023 14:52:00 +0200*References*: <c76a27c0-2188-4620-8e77-f4b9de8904b5n@googlegroups.com>

The declaration variables [...] value, array = [k \in 1 .. n |-> 0] initializes all array elements to zero. Also, the PlusCal translator initializes `value` to a default value (that will be different from standard values such as integers). Instead, you could parameterize your specification by introducing a set Value as follows: CONSTANT n, Value [...] variables [...], value \in Value, array \in [1..n -> Value] In this way, `value` will be a non-deterministically chosen element of the parameter set and `array` will be non-deterministically initialized to hold values in that set. When running TLC, you'll instantiate the parameter Value by a specific set such as 0 .. 3 (an interval of integers), {"a", "b", "c"} (a set of strings) or {v1, v2, v3} (a set of abstract "model" values). Hope this helps, 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/4B8DB10E-3290-4AAB-926E-8F57F77A17F0%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] TLA+ and C++ templates***From:*christin...@xxxxxxxxx

**References**:**[tlaplus] TLA+ and C++ templates***From:*christin...@xxxxxxxxx

- Prev by Date:
**[tlaplus] TLA+ and C++ templates** - Next by Date:
**[tlaplus] About stuttering steps, deadlock and Implementation** - Previous by thread:
**[tlaplus] TLA+ and C++ templates** - Next by thread:
**Re: [tlaplus] TLA+ and C++ templates** - Index(es):