The problem is that .. is imported from the Integers module, which TLC doesn't know about. You instead have to do something like make a new MaxValue constant, define Value == 0..MaxValue, and then in the config file set MaxValue = 10.
(You can assign 0..10 to a constant in the Toolbox IDE, which works by defining a new MC.tla file with Const_1234 == 0..10, and then putting Value <- Const_1234 in the config file.)
H
On 7/11/2023 10:40 AM, christin...@xxxxxxxxx wrote:
Ack, so silly not to spot that I'd set it to zero myself! Thank you!
Another entry-level question: if I want to set Value in a .cfg file, how do I do that? I've tried:
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!
--On Monday, July 10, 2023 at 1:52:15 PM UTC+1 Stephan Merz wrote:
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 <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.
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/f8a8171f-c661-480c-a37b-150a075f165an%40googlegroups.com.