Producer-Consumer System/TLC Model Checking

Write configuration file

 
SPECIFICATION Prog
CONSTANTS     Producers = {p1,p2,p3}
              Consumers = {c1,c2}
              BufCapacity = 2
              Data = {m1}
INVARIANT     TypeInv
PROPERTY      NoDeadlock

Then use the tlc tool

root@ip-172-31-35-176:/home/ubuntu/Apps/tla-bin# tlc Buffer.tla
TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Running breadth-first search Model-Checking with fp 30 and seed 7137671703377064303 with 1 worker on 8 cores with 7079MB heap and 64MB offheap memory (Linux 5.8.0-1035-aws amd64, Private Build 1.8.0_292 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ubuntu/Apps/tla-bin/Buffer.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module Buffer
Starting... (2021-08-25 13:52:12)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2021-08-25 13:52:12.
Error: Invariant NoDeadlock is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ buffer = <<>>
/\ waitSet = {}

State 2: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1>>
/\ waitSet = {}

State 3: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {}

State 4: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1}

State 5: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2}

State 6: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2, p3}

State 7: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1>>
/\ waitSet = {p2, p3}

State 8: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p3}

State 9: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p3, c1}

State 10: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p3, c1, c2}

State 11: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1>>
/\ waitSet = {c1, c2}

State 12: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {c2}

State 13: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, c2}

State 14: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2, c2}

State 15: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2, p3, c2}

State 16: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1>>
/\ waitSet = {p2, p3, c2}

State 17: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p2, p3}

State 18: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p2, p3, c1}

State 19: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p2, p3, c1, c2}

State 20: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1>>
/\ waitSet = {p3, c1, c2}

State 21: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {c1, c2}

State 22: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, c1, c2}

State 23: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2, c1, c2}

State 24: <Next line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2, p3, c1, c2}

385 states generated, 86 distinct states found, 2 states left on queue.
The depth of the complete state graph search is 24.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
Finished in 01s at (2021-08-25 13:52:12)

Branch:

• [If there is an error] Next: Producer-Consumer System/Intepret Error Trace
• [If there is no error] Next: Producer-Consumer System/Finish