| 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 On 10 Jul 2023, at 14:10, christin...@xxxxxxxxx <christina.a.burge@xxxxxxxxx> wrote:
I have been thinking about ways to verify C++ templates, and I wonder if TLA+ would be good for this? I can quite trivially (for example) write a PlusCal spec to verify std::find for a specific input type, but is there a way to explore the state space for all types of data that might be in the array? I have the below, which does not initialise the array to be anything, but that seems to default set it to zero. -------------------------------- MODULE find ------------------- EXTENDS Naturals, TLC, Integers CONSTANT n (* --algorithm find variables first = 1, last \in 1 .. n , value, array = [k \in 1 .. n |-> 0], begin assert last >= first; while first /= last do if array[first] = value then skip; end if; first := first + 1; end while; end algorithm *)
--
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/c76a27c0-2188-4620-8e77-f4b9de8904b5n%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/4B8DB10E-3290-4AAB-926E-8F57F77A17F0%40gmail.com.
|