Hi there,
I'm learning and experimenting with TLA+. I'm now curious to play with simulation mode. To my understanding, it should be useful to explore a random trace in large models to see, among other things, if the model behave as expected.
I wrote a fair simple model (see below) where I can easily assume the expected behaviour. When I run the model checker, it quickly finish without errors finding ~ 200K states (80K distinct).
Then, when I run the simulation mode, it seems to never finish, and after a while it finds hundred of million of states, and counting. I've also tried reducing the depth to a small number (like 5).
What I'm missing?
Thanks
---- MODULE simulation ----
EXTENDS TLC, Integers
CONSTANT Controllers, NULL
(*--algorithm labels1
variables
status = "ready",
requester = NULL,
counter = [c \in Controllers |-> 0];
process controller \in Controllers
begin
Request:
while TRUE do
await status = "ready";
requester := self;
status := "request";
end while;
end process;
process executer = "Executer"
begin
Execute:
await status = "request";
counter[requester] := (counter[requester] + 1) % 10; \* to limit a little the number of states
status := "ready";
goto Execute;
end process;
end algorithm; *)
====