[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Yet another stuttering question



Hello,

it may be helpful to know what property you are trying to verify.

However, I was curious why, say, w1 wouldn't be required to take a step in the final state of your execution. One would imagine that it should be able to perform W_Work, but in fact the definition of that action is

W_Work(self) ==
    /\ pc[self] = "W_Work"
    /\ work_done = work_done + 1
    /\ pc' = [pc EXCEPT ![self] = "W_Exit"]

I am sure you meant to write

    /\ work_done' = work_done + 1  \* mind the prime

Independently of this, I would recommend avoiding the CHOOSE _expression_ in the definition of NotStartedWorker since CHOOSE is deterministic choice, but probably you'd rather run any worker that hasn't started yet. You could change the definition of L_Start as follows:

L_Start ==
    /\ pc["loop"] = "L_Start"
    /\ IF started_workers /= Cardinality(Workers) /\ started_workers < Parallelism
        THEN \E worker \in Workers : 
            /\ pc[worker] = "W_Not_Started"
            /\ pc' = [pc EXCEPT !["loop"] = "L_Start", ![worker] = "W_Work"]
            /\ started_workers' = started_workers + 1
            /\ running_workers' = running_workers + 1
            /\ UNCHANGED work_done
        ELSE pc' = [pc EXCEPT !["loop"] = "L_Wait"]
            /\ UNCHANGED all_vars_but_pc

As a minor issue, note that the update of pc["loop"] in the THEN branch is a no-op and can be removed (same for action L_Wait).

In fact, the actions L_Start and L_Wait look very similar: it is not clear to me why you want to distinguish them (the information about the number of running workers is available separately from the pc value), and the action L_Complete can never be enabled because no action sets pc["loop"] to "L_Complete".

Hope this helps,
Stephan


On 13 Apr 2022, at 11:35, Luca Tumedei <luca@xxxxxxxxxxxxxxxxx> wrote:

Hello everyone,

I'm a PHP developer that recently got very interested into TLA+, I'm trying to learn to use it and ran into a blocker while trying to write my first specification.
I'm trying to model a system composed of a Loop that will spawn workers to execute jobs; I'm not reinventing the wheel and would like to try my hand at writing the specification in TLC.
I've read the Practical TLA+ book and watched a number of videos online in my spare time, so my TLC is influenced by that.
The first version of the specification is simple enough: 1 Loop, 3 workers, a parallelism of 2.
I _think_ I got the part where the Loop starts 2 workers correctly, but now I'm stuck on a Stuttering error I cannot understand the cause of.
The Loop and Worker actions all are weakly fair, and it's my understanding the system should move on, but it doesn't. It might be glaringly obvious to experts, but I've been staring at it for too long to understand what is (not) going on.

Here is the spec:

---- MODULE loop_and_workers ----
EXTENDS TLC, Integers, FiniteSets

VARIABLES pc, started_workers, running_workers, work_done

Parallelism == 2
Workers == {"w1", "w2", "w3"}

vars == << pc, started_workers, running_workers, work_done >>
all_vars_but_pc == << started_workers, running_workers, work_done >>

NotStartedWorker == CHOOSE x \in Workers: pc[x] = "W_Not_Started"

Init ==
    /\ started_workers = 0
    /\ running_workers = 0
    /\ work_done = 0
    /\ pc = [self \in {"loop"} \cup Workers |->
                CASE self = "loop" -> "L_Start"
                [] self \in Workers -> "W_Not_Started"]

L_Start ==
    /\ pc["loop"] = "L_Start"
    /\ IF started_workers /= Cardinality(Workers) /\ started_workers < Parallelism
        THEN LET worker == NotStartedWorker IN
            pc' = [pc EXCEPT !["loop"] = "L_Start", ![worker] = "W_Work"]
            /\ started_workers' = started_workers + 1
            /\ running_workers' = running_workers + 1
            /\ UNCHANGED work_done
        ELSE pc' = [pc EXCEPT !["loop"] = "L_Wait"]
            /\ UNCHANGED all_vars_but_pc

L_Wait ==
        /\ pc["loop"] = "L_Wait"
        /\ IF work_done /= Cardinality(Workers) /\ started_workers < Parallelism
            THEN LET worker == NotStartedWorker IN
                /\ pc' = [pc EXCEPT !["loop"] = "L_Wait", ![worker] = "W_Work"]
                /\ started_workers' = started_workers + 1
                /\ running_workers' = running_workers + 1
                /\ UNCHANGED work_done
            ELSE UNCHANGED vars
   
L_Complete ==
    /\ pc["loop"] = "L_Complete"
    /\ work_done = Cardinality(Workers)
    /\ pc' = [pc EXCEPT !["loop"] = "Done"]

W_Work(self) ==
    /\ pc[self] = "W_Work"
    /\ work_done = work_done + 1
    /\ pc' = [pc EXCEPT ![self] = "W_Exit"]

W_Exit(self) ==
    /\ pc[self] = "W_Exit"
    /\ running_workers' = running_workers - 1
    /\ pc' = [pc EXCEPT ![self] = "Done"]

loop == L_Start \/ L_Wait \/ L_Complete
worker(self) == W_Work(self) \/ W_Exit(self)

Next == loop
    \/ (\E self \in Workers: worker(self))

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(loop)
        /\ \A self \in Workers: WF_vars(worker(self))

ParallelismRespected == running_workers <= Parallelism
====

And here is the output of the model checking:

Temporal properties were violated.
The following behavior constitutes a counter-example:
1: <Initial predicate>
/\ work_done = 0
/\ running_workers = 0
/\ pc = ( w1 :> "W_Not_Started" @@
w2 :> "W_Not_Started" @@
w3 :> "W_Not_Started" @@
"loop" :> "L_Start" )
/\ started_workers = 0
2: <L_Start line 23, col 5 to line 31, col 40 of module loop_and_workers>
/\ work_done = 0
/\ running_workers = 1
/\ pc = ( w1 :> "W_Work" @@
w2 :> "W_Not_Started" @@
w3 :> "W_Not_Started" @@
"loop" :> "L_Start" )
/\ started_workers = 1
3: <L_Start line 23, col 5 to line 31, col 40 of module loop_and_workers>
/\ work_done = 0
/\ running_workers = 2
/\ pc = ( w1 :> "W_Work" @@
w2 :> "W_Work" @@
w3 :> "W_Not_Started" @@
"loop" :> "L_Start" )
/\ started_workers = 2
4: <L_Start line 23, col 5 to line 31, col 40 of module loop_and_workers>
/\ work_done = 0
/\ running_workers = 2
/\ pc = ( w1 :> "W_Work" @@
w2 :> "W_Work" @@
w3 :> "W_Not_Started" @@
"loop" :> "L_Wait" )
/\ started_workers = 2
5: Stuttering

I will keep reading the group conversations and try to find a solution on my own.
Should that be the case, I will reply to it to provide my discoveries and solution.

Thanks in advance to anyone that took the time to read this or reply, much appreciated.

All the best,

Luca

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6f31d511-b6cf-488b-ac30-bcfbb42bda85n%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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/60B4EC04-193E-4946-917F-827F55A10A77%40gmail.com.