run-reach-bb.sh 3.46 KB
Newer Older
1
2
3
4
5
6
7
8
# /bin/zsh

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

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

11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

if [ ! -f "$model.formulae.txt" ]; then
    echo "No specifications for $model" > $save
    exit 0
fi

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
29
    echo "model,isempty,bbspottime,bbltsmintime,bbspotst,bbspottr,bbltsminst,bbltsmintr,formulae" > $tmpfile
30
31
32
33
34
35
36
37
38
39
40
41
42
43
fi

while read -r status 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;

    echo $formula > $formulatmp
44
45
46
    ../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}')
47
48
49
50

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

51
    # Compute LTSmin Spot resolution time
52
53
    LTSMIN_F=$(echo $formula | sed 's/"//g')
    start=$(date +%s.%N)
54
    timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin > "$logdir"/formula."$i".bb."log".tmp 2>&1
55
    end=$(date +%s.%N)
56
57
58
59
60
61
    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"


62
    start=$(date +%s.%N)
63
    timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$formula" -nb-threads $NBTHREADS -backend spot > "$logdir"/formula."$i".bb."log".tmp 2>&1
64
    end=$(date +%s.%N)
65
66
67
68
    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"
69
70


71
72
73
74
75
76
77
78
79
    mystatus=$(cat "$logdir"/formula."$i".bb."log" | grep "not_empty")
    if [ -z "$mystatus" ]; then
	mystatus="EMPTY"
    else
	mystatus="NOTEMPTY"
    fi
    
    ltsmin_st=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $4}')
    ltsmin_tr=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $6}')
80

81
82
83
84
    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] $mystatus spot:$spot_time  ($spot_st st,$spot_tr tr),ltsmin:$ltsmin_time ($ltsmin_st st,$ltsmin_tr tr) $bb"
85
86


87
88
89
90
91
92
    if [ "$status" = "$mystatus" ]; then
        echo "                 Checking for Correctness: OK"
    else
        echo "                 Checking for Correctness: KO"
        echo FAIL: $model $formula
        exit 1
93
    fi
94
95
96
97
    
    echo "$model,$mystatus,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> $tmpfile
    echo $(date --iso-8601=ns) "$model,$mystatus,$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
98
99
100
101
102
103

    i=$((i+1))
done < $model.formulae.txt

cp $tmpfile $save
rm $tmpfile