run-ltl-bb.sh 3.15 KB
Newer Older
1
2
3
4
5
6
7
8
9
#!/bin/zsh

i=0
save=$1
formulae=$2
model=$3
dir=$4
NBTHREADS=$5

Hugo Moreau's avatar
Hugo Moreau committed
10
11
logdir="$dir"/log

12
13
14
15
16
17
18
19
20
21
22
23
if [ -f "$save" ]; then
    exit 0
fi

tmpfile="$save".tmp

formulatmp="$dir"/formula.tmp
transpile="$dir"/transpile.tmp
kripke="$dir"/kripke.tmp
kripkestate="$kripke".state

if [ ! -f "$tmpfile" ]; then
24
    echo "model,isempty,bbspottime,bbltsmintime,bbspotst,bbspottr,bbltsminst,bbltsmintr,formulae" > $tmpfile
25
26
27
28
fi

blackbox() {
    echo $1 > $formulatmp
29
30
31
32
33
    ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -formulae $formulatmp $model >> "$logdir"/formula."$i".bb."log" 2>&1
    TRANSPILE_TIME=$(grep "transpilation time:" "$logdir"/formula."$i".bb."log" | awk '{print $3}')
    COMPILE_TIME=$(grep "compilation time:" "$logdir"/formula."$i".bb."log" | awk '{print $3}')


34
35
36
37
38

    filename=$(basename -- "$model")
    filename="${filename%.*}"

    # Compute LTSmin Spot resolution time
39
    LTSMIN_F=$(echo $formula | sed 's/"//g')
40
    start=$(date +%s.%N)
41
    timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin > "$logdir"/formula."$i".bb."log".tmp 2>&1
42
    end=$(date +%s.%N)
43
44
45
46
    ltsmin_time=$(python -c "print ('%.3f' %  (${end} - ${start}))")
    echo $(date --iso-8601=ns)  >> "$logdir"/formula."$i".bb."log"
    cat "$logdir"/formula."$i".bb."log".tmp 2>&1 >> "$logdir"/formula."$i".bb."log"
    echo  >> "$logdir"/formula."$i".bb."log"
47
48

    start=$(date +%s.%N)
49
    timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$formula" -nb-threads $NBTHREADS -backend spot > "$logdir"/formula."$i".bb."log".tmp 2>&1
50
    end=$(date +%s.%N)
51
52
53
54
    spot_time=$(python -c "print ('%.3f' %  (${end} - ${start}))")
    echo $(date --iso-8601=ns)  >> "$logdir"/formula."$i".bb."log"
    cat "$logdir"/formula."$i".bb."log".tmp 2>&1 >> "$logdir"/formula."$i".bb."log"
    echo  >> "$logdir"/formula."$i".bb."log"
55

56
57
58
    statusbb=$(cat "$logdir"/formula."$i".bb."log" | grep "not_empty")
    if [ -z "$statusbb" ]; then
	statusbb="EMPTY"
Etienne Renault's avatar
Etienne Renault committed
59
    else
60
	statusbb="NOTEMPTY"
Etienne Renault's avatar
Etienne Renault committed
61
    fi
62
63
64
65
66
67
68
69
70
71
72
73

    ltsmin_st=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $5}')
    ltsmin_tr=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $7}')

    spot_st=$(cat "$logdir"/formula."$i".bb."log" | grep '^#' | awk -F',' '{print $6}')
    spot_tr=$(cat "$logdir"/formula."$i".bb."log" | grep '^#' | awk -F',' '{print $7}')

    echo "    [formulae $i] $statusbb spot:$spot_time  ($spot_st st,$spot_tr tr),ltsmin:$ltsmin_time ($ltsmin_st st,$ltsmin_tr tr) $bb"

    echo "$model,$statusbb,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> $tmpfile
    echo $(date --iso-8601=ns) "$model,$statusbb,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> "$logdir"/formula."$i".bb."log"
    rm "$logdir"/formula."$i".bb."log".tmp
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
}

while read -r formula
do
    # Detect the number of lines and skip already computed formulae
    LOC=$(wc -l $tmpfile | awk '{print $1}' )
    tmp=$((i+2))
    if [ "$tmp" -lt "$LOC" ];  then
        echo "    [SKIP] formulae $i"
        i=$((i+1))
        continue
    fi;

    blackbox $formula
    i=$((i+1))
done < $formulae

cp $tmpfile $save
rm $tmpfile