Commit 5915ad3c authored by Etienne Renault's avatar Etienne Renault
Browse files

benchs: scripts to reproduce results

* benchs/extract_results.sh,
benchs/generate-fig.r: Here.
parent 570714d7
Pipeline #27516 passed with stage
in 2 minutes and 43 seconds
#! /bin/zsh
DIRS="2016-Problem1-ltl 2016-Problem2-ltl 2016-Problem4-ltl 2016-Problem5-ltl 2016-Problem7-ltl 2017-Problem1-ltl 2017-Problem2-ltl 2017-Problem4-ltl 2017-Problem5-ltl 2017-Problem7-ltl 2018-Problem1-ltl 2018-Problem2-ltl 2018-Problem4-ltl 2018-Problem5-ltl 2019-Problem1-ltl 2019-Problem2-ltl 2019-Problem4-ltl 2019-Problem5-ltl 2019-Problem7-ltl 2020-Problem1-ltl 2020-Problem2-ltl 2020-Problem4-ltl 2020-Problem5-ltl 2020-Problem7-ltl"
echo file,LOC,transpile_time,compile_time,total_time,bb_transpile_time,bb_compile_time,bb_total_time > compil.csv
for model in $DIRS; do
CLASSIC=$(tail -n 1 $model/global.csv)
for i in $(ls $model/log/formula.*.bb.log); do
TRANSPILATION=$(cat $i | grep 'transpilation time:'|head -n 1 | awk '{print $3}')
COMPILATION=$(cat $i | grep 'compilation time'| head -n 1 | awk '{print $3}')
TOTAL=$((COMPILATION+TRANSPILATION))
echo $CLASSIC,$COMPILATION,$TRANSPILATION,$TOTAL >> compil.csv
done
done
echo isempty,spottime,ltsmintime,bb_spottime,bb_ltsmintime > times.csv
rm -f /tmp/1
for model in $DIRS; do
paste -d',' $model/benchs-ltl-8.csv $model/benchs-bb-8.csv| grep -v isempty | sed 's/NOTEMPTY/Counterexample found/g' | sed 's/EMPTY/No counterexample/g' | awk -F',' '{print $2","$3","$4","$12","$13}' >> /tmp/1
done
cat /tmp/1 | grep -v ',,' >> times.csv
rm -f /tmp/1
echo isempty,spotst,spottr,ltsminst,ltsmintr,bb_spotst,bb_spottr,bb_ltsminst,bb_ltsmintr> st-tr.csv
for model in $DIRS; do
paste -d',' $model/benchs-ltl-8.csv $model/benchs-bb-8.csv| grep -v isempty | sed 's/NOTEMPTY/Counterexample found/g' | sed 's/EMPTY/No counterexample/g' | awk -F',' '{print $2","$5","$6","$7","$8","$14","$15","$16","$17}' >> /tmp/1
done
cat /tmp/1 | grep -v ',,' >> st-tr.csv
# Run it with : r < generate-fig.r --no-save
library(reshape2)
library(ggplot2)
library(scales)
#########################################################
data <- read.csv("compil.csv")
data$total_time <- data$total_time/1000
data$bb_total_time <- data$bb_total_time/1000
p <- ggplot() +
geom_line(aes(x=LOC, y=total_time, colour="Without black-boxes"), data = data) +
geom_point( aes(x=LOC, y=total_time, colour="Without black-boxes"), data = data, shape=1) +
geom_point( aes(x=LOC, y=bb_total_time, colour= "With black-boxes"), data = data, shape=1) +
stat_summary(aes(x=LOC, y=bb_total_time, colour="With black-boxes" ), data = data, fun=mean, geom="line",group=1, linetype = "dashed") +
labs(color='Go2Pins compilation time: ') + xlab("Line of Code")+ ylab("Time (secondes)") +
theme(legend.position=c(.35, .80), axis.text=element_text(size=11))
ggsave("compil.pdf", p, height = 4, width = 5)
## #########################
data <- read.csv("times.csv")
options(scipen=10000)
p <- ggplot(data, aes(x =spottime, y = bb_spottime, colour=isempty)) + geom_point()
p <- p + xlab("Time 8 threads (Spot)")+ ylab("Time 8 threads with black-boxes (Spot)")
p <- p + scale_x_continuous(trans='log10', breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250)) + scale_y_continuous(trans='log10',breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.25, .8))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p + geom_hline( yintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p + geom_vline(xintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p +mydiags
ggsave("spot-bbspot.pdf", p, height = 4, width = 5)
options(scipen=10000)
p <- ggplot(data, aes(x =ltsmintime, y = bb_ltsmintime, colour=isempty)) + geom_point()
p <- p + xlab("Time 8 threads (Ltsmin)")+ ylab("Time 8 threads with black-boxes (Ltsmin)")
p <- p + scale_x_continuous(trans='log10', breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250)) + scale_y_continuous(trans='log10',breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.25, .8))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p + geom_hline( yintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p + geom_vline(xintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p +mydiags
ggsave("ltsmin-bbltsmin.pdf", p, height = 4, width = 5)
options(scipen=10000)
p <- ggplot(data, aes(x =spottime, y = ltsmintime, colour=isempty)) + geom_point()
p <- p + xlab("Time 8 threads (Spot)")+ ylab("Time 8 threads (Ltsmin)")
p <- p + scale_x_continuous(trans='log10', breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250)) + scale_y_continuous(trans='log10',breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.7, .2))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p + geom_hline( yintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p + geom_vline(xintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p +mydiags
ggsave("spot-ltsmin.pdf", p, height = 4, width = 5)
options(scipen=10000)
p <- ggplot(data, aes(x =bb_spottime, y = bb_ltsmintime, colour=isempty)) + geom_point()
p <- p + xlab("Time 8 threads with black-boxes (Spot)")+ ylab("Time 8 threads with black-boxes (Ltsmin)")
p <- p + scale_x_continuous(trans='log10', breaks = c(0.1,0.10, 1, 10, 100), limits = c(0.1, 250)) + scale_y_continuous(trans='log10',breaks = c(0.1,0.10, 1, 10, 100))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.7, .2))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p + geom_hline( yintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p + geom_vline(xintercept=240, linetype="dashed", color = "black", size=0.4)
p <- p +mydiags
ggsave("bbspot-bbltsmin.pdf", p, height = 4, width = 5)
## #########################
data <- read.csv("st-tr.csv")
options(scipen=10000)
p <- ggplot(data, aes(x =spotst, y = bb_spotst, colour=isempty)) + geom_point()
p <- p + xlab("States 8 threads (Spot)")+ ylab("States 8 threads with black-boxes (Spot)")
p <- p + scale_x_continuous(trans='log10',limits = c(100, 10000000) ) + scale_y_continuous(trans='log10', limits = c(100, 10000000))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.25, .8))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p+ mydiags
ggsave("spot-st.pdf", p, height = 4, width = 5)
options(scipen=10000)
p <- ggplot(data, aes(x =spottr, y = bb_spottr, colour=isempty)) + geom_point()
p <- p + xlab("Transitions 8 threads (Spot)")+ ylab("Transitions 8 threads with black-boxes (Spot)")
p <- p + scale_x_continuous(trans='log10',limits = c(100, 10000000) ) + scale_y_continuous(trans='log10', limits = c(100, 10000000))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.25, .8))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p+ mydiags
ggsave("spot-tr.pdf", p, height = 4, width = 5)
options(scipen=10000)
p <- ggplot(data, aes(x =ltsminst, y = bb_ltsminst, colour=isempty)) + geom_point()
p <- p + xlab("States 8 threads (Ltsmin)")+ ylab("States 8 threads with black-boxes (Ltsmin)")
p <- p + scale_x_continuous(trans='log10',limits = c(100, 10000000) ) + scale_y_continuous(trans='log10', limits = c(100, 10000000))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.25, .8))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p+ mydiags
ggsave("ltsmin-st.pdf", p, height = 4, width = 5)
options(scipen=10000)
p <- ggplot(data, aes(x =ltsmintr, y = bb_ltsmintr, colour=isempty)) + geom_point()
p <- p + xlab("Transitions 8 threads (Ltsmin)")+ ylab("Transitions 8 threads with black-boxes (Ltsmin)")
p <- p + scale_x_continuous(trans='log10',limits = c(100, 10000000) ) + scale_y_continuous(trans='log10', limits = c(100, 10000000))
p <- p + labs(color='Verification status:')
p <- p + theme(legend.position=c(.25, .8))
mydiags <- geom_abline(intercept=c(-log10(10), 0, log10(10)), colour=c('dark grey', 'black', 'dark grey'))
p <- p+ mydiags
ggsave("ltsmin-tr.pdf", p, height = 4, width = 5)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment