v08 (continue): Infer inequation under which the system is deadlock f…

…ree.

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

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)

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))

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)

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