Understanding simulation mode

35 views
Skip to first unread message

Nicholas Fiorentini

unread,
Dec 30, 2019, 5:49:17 PM12/30/19
to tlaplus
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; *)
====

Stephan Merz

unread,
Dec 31, 2019, 3:16:29 AM12/31/19
to tla...@googlegroups.com
Hello,

here is what "Specifying Systems" says about simulation mode (section 14.3.2):

<begin quote>
In simulation mode, TLC repeatedly constructs and checks individual behaviors of a fixed maximum length. [...] In simulation mode, TLC runs until you stop it.
<end quote>

Unlike in model checking mode, simulation continues even if all states have already been encountered before.

Stephan


--
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/4b633b4b-2f02-4bce-88ac-aeccecff19e7%40googlegroups.com.

Nicholas Fiorentini

unread,
Dec 31, 2019, 8:50:53 AM12/31/19
to tlaplus
I see, thanks for the clarification.

So, if I'm looking for a specific trace, I guess I have to "stop" the simulation with an invariant that I know should be violated in the desired trace.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages