From 8e536cba9e188d41b80bf0a1bfa28ababa840aa0 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 30 Jan 2020 22:38:13 -0800 Subject: [PATCH] v08 (continue): Infer inequation under which the system is deadlock free. --- BlockingQueue.cfg | 2 +- BlockingQueue.tla | 4 +- R/ContinueInequation.R | 33 + R/ContinueInequation.svg | 328 ++ R/TraceLength.R | 31 + R/TraceLength.csv | 256 + R/TraceLengthCorrelation.svg | 466 ++ R/TraceLengthPairs.svg | 10414 +++++++++++++++++++++++++++++++++ README.md | 29 + 9 files changed, 11561 insertions(+), 2 deletions(-) create mode 100644 R/ContinueInequation.R create mode 100644 R/ContinueInequation.svg create mode 100644 R/TraceLength.R create mode 100644 R/TraceLength.csv create mode 100644 R/TraceLengthCorrelation.svg create mode 100644 R/TraceLengthPairs.svg diff --git a/BlockingQueue.cfg b/BlockingQueue.cfg index 0816640..68da9c1 100644 --- a/BlockingQueue.cfg +++ b/BlockingQueue.cfg @@ -2,7 +2,7 @@ CONSTANTS BufCapacity = 3 Producers = {p1,p2,p3,p4} - Consumers = {c1,c2,c3} + Consumers = {c1,c2,c3,c4} INIT Init NEXT Next diff --git a/BlockingQueue.tla b/BlockingQueue.tla index 864b88b..58e9de5 100644 --- a/BlockingQueue.tla +++ b/BlockingQueue.tla @@ -68,7 +68,9 @@ TypeInv == /\ buffer \in Seq(Producers) /\ waitSet \subseteq (producers \cup consumers) (* No Deadlock *) -Invariant == waitSet # (producers \cup consumers) +Invariant == IF waitSet # (producers \cup consumers) + THEN TRUE \* Inv not violated. + ELSE PrintT(<<"InvVio", bufCapacity, Cardinality(producers \cup consumers)>>) /\ FALSE (* The Permutations operator is defined in the TLC module. *) Sym == Permutations(Producers) \union Permutations(Consumers) diff --git a/R/ContinueInequation.R b/R/ContinueInequation.R new file mode 100644 index 0000000..437d654 --- /dev/null +++ b/R/ContinueInequation.R @@ -0,0 +1,33 @@ +library(ggplot2) + +data <- read.table(sep=",",header=T,text="vio,x,y +n, 1, 2 +d, 1, 3 +d, 1, 4 +d, 1, 5 +d, 1, 6 +d, 1, 7 +d, 1, 8 +n, 2, 2 +n, 2, 3 +n, 2, 4 +d, 2, 5 +d, 2, 6 +d, 2, 7 +d, 2, 8 +n, 3, 2 +n, 3, 3 +n, 3, 4 +n, 3, 5 +n, 3, 6 +d, 3, 7 +d, 3, 8") + +ggplot(data, aes(x=x, y=y, shape=vio, group=vio)) + + geom_point(size=3) + + scale_shape_identity()+ + xlab("bufCapacity")+ + ylab("|producers \\cup consumers|")+ + annotate("segment", x = 1, xend = 3, y = 2.5, yend = 6.5, + colour = "blue")+ + scale_x_continuous(breaks=c(1,2,3)) diff --git a/R/ContinueInequation.svg b/R/ContinueInequation.svg new file mode 100644 index 0000000..49bbba3 --- /dev/null +++ b/R/ContinueInequation.svg @@ -0,0 +1,328 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/R/TraceLength.R b/R/TraceLength.R new file mode 100644 index 0000000..adfaad9 --- /dev/null +++ b/R/TraceLength.R @@ -0,0 +1,31 @@ +setwd("/home/markus/src/TLA/models/tutorials/BlockingQueueTLA/R") +data <- read.csv(header=TRUE, file = 'TraceLength.csv') + +# Rename column headers for readability. +colnames(data) +names(data)[names(data) == "cons_prod"] <- "|Cons U Prod|" +names(data)[names(data) == "prod"] <- "|Prod|" +names(data)[names(data) == "cons"] <- "|Cons|" + + +##install.packages("scatterplot3d") +#library(scatterplot3d) +#scatterplot3d( +# data[,1:3], pch = 19, color = "steelblue", +# grid = TRUE, box = FALSE, +# mar = c(3, 3, 0.5, 3) +#) + +##install.packages("GGally") +library(GGally) +library(ggplot2) +ggpairs(data) + +##install.packages("ggcorrplot") +library("ggcorrplot") +my_data <- data[, c(1,2,3,4,5)] +corr <- round(cor(my_data), 1) +ggcorrplot(corr, p.mat = cor_pmat(my_data), + hc.order = TRUE, type = "lower", + color = c("#FC4E07", "white", "#00AFBB"), + outline.col = "white", lab = TRUE) diff --git a/R/TraceLength.csv b/R/TraceLength.csv new file mode 100644 index 0000000..d067eb2 --- /dev/null +++ b/R/TraceLength.csv @@ -0,0 +1,256 @@ +BufCapacity, cons_prod, prod, cons, Length +1, 10, 2, 8, 14 +1, 10, 2, 8, 15 +1, 10, 3, 7, 14 +1, 10, 3, 7, 15 +1, 10, 4, 6, 14 +1, 10, 4, 6, 15 +1, 10, 5, 5, 14 +1, 10, 5, 5, 15 +1, 10, 6, 4, 14 +1, 10, 6, 4, 15 +1, 10, 7, 3, 14 +1, 10, 7, 3, 15 +1, 10, 8, 2, 14 +1, 10, 8, 2, 15 +1, 11, 3, 8, 15 +1, 11, 3, 8, 16 +1, 11, 4, 7, 15 +1, 11, 4, 7, 16 +1, 11, 5, 6, 15 +1, 11, 5, 6, 16 +1, 11, 6, 5, 15 +1, 11, 6, 5, 16 +1, 11, 7, 4, 15 +1, 11, 7, 4, 16 +1, 11, 8, 3, 15 +1, 11, 8, 3, 16 +1, 12, 4, 8, 16 +1, 12, 4, 8, 17 +1, 12, 5, 7, 16 +1, 12, 5, 7, 17 +1, 12, 6, 6, 16 +1, 12, 6, 6, 17 +1, 12, 7, 5, 16 +1, 12, 7, 5, 17 +1, 12, 8, 4, 16 +1, 12, 8, 4, 17 +1, 13, 5, 8, 17 +1, 13, 5, 8, 18 +1, 13, 6, 7, 17 +1, 13, 6, 7, 18 +1, 13, 7, 6, 17 +1, 13, 7, 6, 18 +1, 13, 8, 5, 17 +1, 13, 8, 5, 18 +1, 14, 6, 8, 18 +1, 14, 6, 8, 19 +1, 14, 7, 7, 18 +1, 14, 7, 7, 19 +1, 14, 8, 6, 18 +1, 14, 8, 6, 19 +1, 15, 7, 8, 19 +1, 15, 7, 8, 20 +1, 15, 8, 7, 19 +1, 15, 8, 7, 20 +1, 16, 8, 8, 20 +1, 16, 8, 8, 21 +1, 3, 1, 2, 7 +1, 3, 2, 1, 8 +1, 4, 1, 3, 8 +1, 4, 2, 2, 8 +1, 4, 2, 2, 9 +1, 4, 3, 1, 9 +1, 5, 1, 4, 9 +1, 5, 2, 3, 10 +1, 5, 2, 3, 9 +1, 5, 3, 2, 10 +1, 5, 3, 2, 9 +1, 5, 4, 1, 10 +1, 6, 1, 5, 10 +1, 6, 2, 4, 10 +1, 6, 2, 4, 11 +1, 6, 3, 3, 10 +1, 6, 3, 3, 11 +1, 6, 4, 2, 10 +1, 6, 4, 2, 11 +1, 6, 5, 1, 11 +1, 7, 1, 6, 11 +1, 7, 2, 5, 11 +1, 7, 2, 5, 12 +1, 7, 3, 4, 11 +1, 7, 3, 4, 12 +1, 7, 4, 3, 11 +1, 7, 4, 3, 12 +1, 7, 5, 2, 11 +1, 7, 5, 2, 12 +1, 7, 6, 1, 12 +1, 8, 1, 7, 12 +1, 8, 2, 6, 12 +1, 8, 2, 6, 13 +1, 8, 3, 5, 12 +1, 8, 3, 5, 13 +1, 8, 4, 4, 12 +1, 8, 4, 4, 13 +1, 8, 5, 3, 12 +1, 8, 5, 3, 13 +1, 8, 6, 2, 12 +1, 8, 6, 2, 13 +1, 8, 7, 1, 13 +1, 9, 1, 8, 13 +1, 9, 2, 7, 13 +1, 9, 2, 7, 14 +1, 9, 3, 6, 13 +1, 9, 3, 6, 14 +1, 9, 4, 5, 13 +1, 9, 4, 5, 14 +1, 9, 5, 4, 13 +1, 9, 5, 4, 14 +1, 9, 6, 3, 13 +1, 9, 6, 3, 14 +1, 9, 7, 2, 13 +1, 9, 7, 2, 14 +1, 9, 8, 1, 14 +2, 10, 2, 8, 18 +2, 10, 3, 7, 18 +2, 10, 3, 7, 22 +2, 10, 4, 6, 18 +2, 10, 4, 6, 20 +2, 10, 5, 5, 18 +2, 10, 5, 5, 20 +2, 10, 6, 4, 18 +2, 10, 6, 4, 20 +2, 10, 7, 3, 20 +2, 10, 7, 3, 24 +2, 10, 8, 2, 20 +2, 11, 3, 8, 19 +2, 11, 3, 8, 23 +2, 11, 4, 7, 19 +2, 11, 4, 7, 21 +2, 11, 5, 6, 19 +2, 11, 5, 6, 21 +2, 11, 6, 5, 19 +2, 11, 6, 5, 21 +2, 11, 7, 4, 19 +2, 11, 7, 4, 21 +2, 11, 8, 3, 21 +2, 11, 8, 3, 25 +2, 12, 4, 8, 20 +2, 12, 4, 8, 22 +2, 12, 5, 7, 20 +2, 12, 5, 7, 22 +2, 12, 6, 6, 20 +2, 12, 6, 6, 22 +2, 12, 7, 5, 20 +2, 12, 7, 5, 22 +2, 12, 8, 4, 20 +2, 12, 8, 4, 22 +2, 13, 5, 8, 21 +2, 13, 5, 8, 23 +2, 13, 6, 7, 21 +2, 13, 6, 7, 23 +2, 13, 7, 6, 21 +2, 13, 7, 6, 23 +2, 13, 8, 5, 21 +2, 13, 8, 5, 23 +2, 14, 6, 8, 22 +2, 14, 6, 8, 24 +2, 14, 7, 7, 22 +2, 14, 7, 7, 24 +2, 14, 8, 6, 22 +2, 14, 8, 6, 24 +2, 15, 7, 8, 23 +2, 15, 7, 8, 25 +2, 15, 8, 7, 23 +2, 15, 8, 7, 25 +2, 16, 8, 8, 24 +2, 16, 8, 8, 26 +2, 5, 1, 4, 13 +2, 5, 2, 3, 21 +2, 5, 3, 2, 23 +2, 5, 4, 1, 15 +2, 6, 1, 5, 14 +2, 6, 2, 4, 14 +2, 6, 3, 3, 18 +2, 6, 3, 3, 20 +2, 6, 4, 2, 16 +2, 6, 5, 1, 16 +2, 7, 1, 6, 15 +2, 7, 2, 5, 15 +2, 7, 3, 4, 15 +2, 7, 3, 4, 19 +2, 7, 4, 3, 17 +2, 7, 4, 3, 21 +2, 7, 5, 2, 17 +2, 7, 6, 1, 17 +2, 8, 1, 7, 16 +2, 8, 2, 6, 16 +2, 8, 3, 5, 16 +2, 8, 3, 5, 20 +2, 8, 4, 4, 16 +2, 8, 4, 4, 18 +2, 8, 5, 3, 18 +2, 8, 5, 3, 22 +2, 8, 6, 2, 18 +2, 8, 7, 1, 18 +2, 9, 1, 8, 17 +2, 9, 2, 7, 17 +2, 9, 3, 6, 17 +2, 9, 3, 6, 21 +2, 9, 4, 5, 17 +2, 9, 4, 5, 19 +2, 9, 5, 4, 17 +2, 9, 5, 4, 19 +2, 9, 6, 3, 19 +2, 9, 6, 3, 23 +2, 9, 7, 2, 19 +2, 9, 8, 1, 19 +3, 10, 4, 6, 22 +3, 10, 4, 6, 28 +3, 10, 5, 5, 28 +3, 10, 5, 5, 31 +3, 10, 6, 4, 25 +3, 10, 6, 4, 31 +3, 11, 5, 6, 23 +3, 11, 5, 6, 29 +3, 11, 6, 5, 26 +3, 11, 6, 5, 32 +3, 12, 6, 6, 24 +3, 12, 6, 6, 27 +3, 7, 1, 6, 19 +3, 7, 2, 5, 31 +3, 7, 3, 4, 43 +3, 7, 4, 3, 46 +3, 7, 5, 2, 34 +3, 7, 6, 1, 22 +3, 8, 2, 6, 20 +3, 8, 3, 5, 32 +3, 8, 4, 4, 32 +3, 8, 4, 4, 35 +3, 8, 5, 3, 35 +3, 8, 6, 2, 23 +3, 9, 3, 6, 21 +3, 9, 4, 5, 27 +3, 9, 4, 5, 30 +3, 9, 5, 4, 27 +3, 9, 5, 4, 30 +3, 9, 6, 3, 24 +4, 10, 4, 6, 42 +4, 10, 5, 5, 50 +4, 10, 5, 5, 54 +4, 10, 6, 4, 46 +4, 11, 5, 6, 43 +4, 11, 5, 6, 47 +4, 11, 6, 5, 43 +4, 11, 6, 5, 47 +4, 12, 6, 6, 36 +4, 12, 6, 6, 40 +4, 9, 3, 6, 57 +4, 9, 4, 5, 73 +4, 9, 5, 4, 77 +4, 9, 6, 3, 61 +5, 11, 5, 6, 111 +5, 11, 6, 5, 116 +5, 12, 6, 6, 72 +5, 12, 6, 6, 77 +6, 13, 6, 7, 157 diff --git a/R/TraceLengthCorrelation.svg b/R/TraceLengthCorrelation.svg new file mode 100644 index 0000000..0ccadda --- /dev/null +++ b/R/TraceLengthCorrelation.svg @@ -0,0 +1,466 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/R/TraceLengthPairs.svg b/R/TraceLengthPairs.svg new file mode 100644 index 0000000..b1939f4 --- /dev/null +++ b/R/TraceLengthPairs.svg @@ -0,0 +1,10414 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/README.md b/README.md index b5fa937..3680bfd 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,35 @@ This tutorial is work in progress. More chapters will be added in the future. In -------------------------------------------------------------------------- +### v08 (continue): Infer inequation under which the system is deadlock free. + +Based on the scaffolding in the two previous steps, we run TLC with the [```-continue```](https://lamport.azurewebsites.net/tla/tlc-options.html?back-link=tools.html) option to not stop state space exploration after a violation of the invariant has been found. In other words, we ask TLC to find all violations, not just one of the shortest ones (Breadth-First search guarantees that TLC finds the shortest counterexample first). + +```bash +java -jar /opt/TLA+Toolbox/tla2tools.jar -deadlock -continue BlockingQueue | grep InvVio | sort | uniq +<<"InvVio", 1, 3>> +<<"InvVio", 1, 4>> +<<"InvVio", 1, 5>> +<<"InvVio", 1, 6>> +<<"InvVio", 1, 7>> +<<"InvVio", 1, 8>> +<<"InvVio", 2, 5>> +<<"InvVio", 2, 6>> +<<"InvVio", 2, 7>> +<<"InvVio", 2, 8>> +<<"InvVio", 3, 7>> +<<"InvVio", 3, 8>> +``` + +A little bit of bashery trims TLC's output so that we - with some squinting - notice that ```BlockingQueue``` is deadlock free iff ```2*BufCapacity >= Cardinality(Producers \cup Consumers)```. A simple [R plot](./R/ContinueInequation.R) makes this even more visible ('d' indicates a configuration that deadlocks): + +![ContinueInequation](./R/ContinueInequation.svg) + +Collecting even more [data](./R/TraceLength.csv), we can [correlate](./R/TraceLength.R) the length of the error trace with the constants (```Cardinality(Producers)```, ```Cardinality(Consumers)```, ```BufCapacity```, and ```Cardinality(Producers \cup Consumers)```): + +![TraceLengthCorrelation](./R/TraceLengthCorrelation.svg) ([ggcorrplot](http://www.sthda.com/english/wiki/ggcorrplot-visualization-of-a-correlation-matrix-using-ggplot2)) + + ### v07 (continue): Declare Producers and Consumers to be symmetry sets. The sets ```Producers``` and ```Consumers``` are symmetry sets for the ```BlockingQueue``` specification, meaning that permuting the elements in the sets does not change whether or not a behavior satisfies that behavior spec. TLC can take advantage of this to reduce the number of (distinct) states it has to examine from 57254 to 1647!