SPECIFICATION Spec
CONSTANTS
n = 10
Value = 0..10
And variations ( Value == ..., Value <- ...) but I continue to get errors.Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.ConfigFileException
: TLC found an error in the configuration file at line 4
It was expecting = or <-, but did not find it.
Finished in 00s at (2023-07-11 17:35:05)
Any advice welcome!
The declarationvariables [...] 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,StephanOn 10 Jul 2023, at 14:10, christin...@xxxxxxxxx <christin...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c76a27c0-2188-4620-8e77-f4b9de8904b5n%40googlegroups.com.