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.