Skip to content

Commit 50c7a1b

Browse files
lemmylemmy
committed
CSV columns are off
1 parent 444ebff commit 50c7a1b

File tree

5 files changed

+137
-10
lines changed

5 files changed

+137
-10
lines changed

Diff for: ‎specifications/ewd998/EWD998Chan_opts.tla

+2-2
Original file line numberDiff line numberDiff line change
@@ -103,8 +103,8 @@ AtTerminationDetected ==
103103
EWD998!terminationDetected =>
104104
/\ LET o == TLCGet("stats").behavior.actions
105105
IN \* Append record to CSV file on disk.
106-
/\ CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s",
107-
<< F, N, TLCGet("level"), TLCGet("level") - TLCGet(1),
106+
/\ CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s#%10$s",
107+
<< F, N, TLCGet("level"), TLCGet(1), TLCGet("level") - TLCGet(1),
108108
o["InitiateProbe"],o["PassTokenOpts"], \* Note "Opts" suffix!
109109
o["SendMsg"],o["RecvMsg"],o["Deactivate"]
110110
>>,

Diff for: ‎specifications/ewd998/EWD998_opts.R

+127
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
library(ggplot2)
2+
library(dplyr)
3+
4+
data <- read.csv(header=TRUE, sep = "#", file = file.choose())
5+
6+
summary = summarise(group_by(data,Variant, Node),
7+
mean_Length = mean(Length),
8+
sd_Length = sd(Length),
9+
mean_IP = mean(InitiateProbe),
10+
sd_IP = sd(InitiateProbe),
11+
mean_PT = mean(PassToken),
12+
sd_PT = sd(PassToken),
13+
mean_SM = mean(SendMsg),
14+
sd_SM = sd(SendMsg),
15+
mean_RM = mean(RecvMsg),
16+
sd_MR = sd(RecvMsg),
17+
mean_DA = mean(Deactivate),
18+
sd_DA = sd(Deactivate),
19+
mean_T = mean(T),
20+
sd_T = sd(T),
21+
mean_T2TD = mean(T2TD),
22+
sd_T2TD = sd(T2TD)
23+
)
24+
Nodes <- unique(summary$Node)
25+
26+
####
27+
#### T2TD
28+
####
29+
for (n in Nodes) {
30+
print(ggplot(filter(summary, Node == n),
31+
aes(x = reorder(Variant, mean_T2TD), y = mean_T2TD, fill = Variant)) +
32+
geom_bar(stat = "identity") +
33+
geom_errorbar(aes(ymin=mean_T2TD-sd_T2TD, ymax=mean_T2TD+sd_T2TD), width=.2,
34+
position=position_dodge(.9)) +
35+
scale_x_discrete(guide = guide_axis(n.dodge=3))+
36+
theme_minimal() +
37+
labs(
38+
x = "Spec variant",
39+
y = "Average length while terminated /\\ ~terminationDetected holds",
40+
title = paste(
41+
"Number of Nodes: ", n, "Traces:", nrow(filter(data, Node == n))
42+
)
43+
))
44+
}
45+
46+
####
47+
#### InitiateProbe actions
48+
####
49+
for (n in Nodes) {
50+
print(ggplot(filter(summary, Node == n),
51+
aes(x = reorder(Variant, mean_IP), y = mean_IP, fill = Variant)) +
52+
geom_bar(stat = "identity") +
53+
geom_errorbar(aes(ymin=mean_IP-sd_IP, ymax=mean_IP+sd_IP), width=.2,
54+
position=position_dodge(.9)) +
55+
scale_x_discrete(guide = guide_axis(n.dodge=3))+
56+
theme_minimal() +
57+
labs(
58+
x = "Spec variant",
59+
y = "Average number of InitiateProbe actions",
60+
title = paste(
61+
"Number of Nodes: ", n, "Traces:", nrow(filter(data, Node == n))
62+
)
63+
))
64+
}
65+
66+
####
67+
#### Length & T
68+
####
69+
for (n in Nodes) {
70+
print(ggplot(filter(summary, Node == n),
71+
aes(x = reorder(Variant, mean_Length), y = mean_Length, fill = Variant)) +
72+
geom_bar(stat = "identity") +
73+
geom_errorbar(aes(ymin=mean_Length-sd_Length, ymax=mean_Length+sd_Length), width=.2,
74+
position=position_dodge(.9)) +
75+
scale_x_discrete(guide = guide_axis(n.dodge=3))+
76+
theme_minimal() +
77+
labs(
78+
x = "Spec variant",
79+
y = "Average length of behaviors",
80+
title = paste(
81+
"Number of Nodes: ", n, "Traces:", nrow(filter(data, Node == n))
82+
)
83+
))
84+
}
85+
86+
########
87+
######## Occurrences of actions
88+
########
89+
for (n in Nodes) {
90+
print(ggplot(filter(summary, Node == n)) +
91+
geom_point(aes(x=reorder(Variant, mean_PT), y = mean_PT,colour = "PassToken",shape = "PassToken")) +
92+
geom_point(aes(x=reorder(Variant, mean_IP),y=mean_IP,colour = "InitiateProbe",shape = "InitiateProbe")) +
93+
# geom_point(aes(x=Variant,y=mean_IP,colour = "InitiateProbe",shape = "InitiateProbe")) +
94+
geom_point(aes(x=reorder(Variant, mean_SM),y=mean_SM,colour = "SendMsg",shape = "SendMsg")) +
95+
geom_point(aes(x=reorder(Variant, mean_RM),y=mean_RM,colour = "RecvMsg",shape = "RecvMsg")) +
96+
geom_point(aes(x=reorder(Variant, mean_DA),y=mean_DA,colour = "Deactivate",shape = "Deactivate")) +
97+
## x-axis labels should not overlap.
98+
scale_x_discrete(guide = guide_axis(n.dodge=3))+
99+
#scale_x_discrete(guide = guide_axis(check.overlap = TRUE))+
100+
#coord_flip() +
101+
theme_minimal() +
102+
#theme(legend.position = "none") +
103+
labs(
104+
x = "Spec variant",
105+
y = "Average number of occurrences in behaviors",
106+
title = paste(
107+
"Number of Nodes: ", n, " Traces:", nrow(filter(data, Node == n))
108+
)
109+
))
110+
}
111+
112+
########
113+
######## Correlations
114+
########
115+
116+
##install.packages("ggcorrplot")
117+
library("ggcorrplot")
118+
my_data <- filter(summary, Node == 113)[, c("mean_Length", "mean_SM", "mean_RM", "mean_IP", "mean_PT", "mean_DA", "mean_T")]
119+
p.mat <- cor_pmat(my_data)
120+
## Check for correlation in 'data'
121+
## 'spearman' (3) correlation because data has no normal distribution
122+
## (see previous plots).
123+
corr <- round(cor(my_data), 3)
124+
ggcorrplot(corr, p.mat = cor_pmat(my_data),
125+
hc.order = TRUE, type = "lower",
126+
color = c("#FC4E07", "white", "#00AFBB"),
127+
outline.col = "white", lab = TRUE)

Diff for: ‎specifications/ewd998/EWD998_opts.tla

+3-4
Original file line numberDiff line numberDiff line change
@@ -98,11 +98,10 @@ AtTerminationDetected ==
9898
terminationDetected =>
9999
/\ LET o == TLCGet("stats").behavior.actions
100100
IN \* Append record to CSV file on disk.
101-
/\ CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s",
102-
<< F, N, TLCGet("level"),
101+
/\ CSVWrite("%1$s#%2$s#%3$s#%4$s#%5$s#%6$s#%7$s#%8$s#%9$s#%10$s",
102+
<< F, N, TLCGet("level"), TLCGet(1), TLCGet("level") - TLCGet(1),
103103
o["InitiateProbe"],o["PassTokenOpts"], \* Note "Opts" suffix!
104-
o["SendMsg"],o["RecvMsg"],o["Deactivate"],
105-
TLCGet(1) >>,
104+
o["SendMsg"],o["RecvMsg"],o["Deactivate"] >>,
106105
IOEnv.Out)
107106
\* Reset the counter for the next behavior.
108107
/\ TLCSet(1, 0)

Diff for: ‎specifications/ewd998/EWD998_optsSC.tla

+1-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ CSVFile ==
2121
\* this script and forks the nested instances of TLC that simulate the spec
2222
\* and collect the statistics.
2323
ASSUME
24-
CSVWrite("Variant#Node#Length#T#InitiateProbe#PassToken#SendMsg#RecvMsg#Deactivate",
24+
CSVWrite("Variant#Node#Length#T#T2TD#InitiateProbe#PassToken#SendMsg#RecvMsg#Deactivate",
2525
<<>>, CSVFile)
2626

2727
\* Command to fork nested TLC instances that simulate the spec and collect the

Diff for: ‎specifications/ewd998/README.Rmd

+4-3
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,8 @@ summary = summarise(group_by(data,Variant, Node),
120120
mean_SM = mean(SendMsg), sd_SM = sd(SendMsg),
121121
mean_RM = mean(RecvMsg), sd_MR = sd(RecvMsg),
122122
mean_DA = mean(Deactivate), sd_DA = sd(Deactivate),
123-
mean_T = mean(T), sd_T = sd(T)
123+
mean_T = mean(T), sd_T = sd(T),
124+
mean_T2TD = mean(T2TD), sd_T2TD = sd(T2TD)
124125
)
125126
Nodes <- unique(summary$Node)
126127
```
@@ -131,9 +132,9 @@ Nodes <- unique(summary$Node)
131132
132133
for (n in Nodes) {
133134
## Ideally, filtering on Variant column would not rely on string matching.
134-
print(ggplot(filter(summary, !grepl('pt1|pt2', Variant), Node == n), aes(x = reorder(Variant, mean_T), y = mean_T, fill = Variant)) +
135+
print(ggplot(filter(summary, !grepl('pt1|pt2', Variant), Node == n), aes(x = reorder(Variant, mean_T), y = mean_T2TD, fill = Variant)) +
135136
geom_bar(stat = "identity") +
136-
geom_errorbar(aes(ymin=mean_T-sd_T, ymax=mean_T+sd_T), width=.2) +
137+
geom_errorbar(aes(ymin=mean_T2TD-sd_T2TD, ymax=mean_T2TD+sd_T2TD), width=.2) +
137138
scale_x_discrete(guide = guide_axis(n.dodge=3))+
138139
theme_minimal() +
139140
labs(

0 commit comments

Comments
 (0)