-------------------------------- 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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c76a27c0-2188-4620-8e77-f4b9de8904b5n%40googlegroups.com.
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 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.)
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f8a8171f-c661-480c-a37b-150a075f165an%40googlegroups.com.