-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathinstall_inputs.sh
executable file
·97 lines (78 loc) · 4.2 KB
/
install_inputs.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
#! /bin/bash
set -x
mkdir website
cd website
# grab the vmdk file image for all inputs
mkdir INPUTS
wget --no-check-certificate --progress=dot:mega https://mcc.lip6.fr/2022/archives/mcc2022-input.tar.gz
tar xvzf mcc2022-input.tar.gz
../7z e mcc2022-input.vmdk
../ext2rd 0.img ./:INPUTS
# for some reason there are a few decompressed examples
rm -rf INPUTS/RERS2020-PT-pb101 INPUTS/RERS2020-PT-pb102 INPUTS/RERS2020-PT-pb103 INPUTS/RERS2020-PT-pb104 INPUTS/RERS2020-PT-pb105 INPUTS/RERS2020-PT-pb106 INPUTS/RERS2020-PT-pb107 INPUTS/RERS2020-PT-pb108 INPUTS/RERS2020-PT-pb109
# cleanup
rm -f *.vmdk 0.img *.gz 1
# remove strange MacOS specific stuff 'LIBARCHIVE.xattr.com.apple.quarantine'
echo "Patching tgz archives"
set +x
cd INPUTS
for i in *.tgz ;
do
tar xzf $i
model=$(echo $i | sed 's/.tgz//g')
# echo "Treating : $model"
rm $i
tar czf $i $model/
rm -rf $model/
done
cd ..
set -x
if [ ! -f raw-result-analysis.csv ]
then
# grab the raw results file from MCC website
wget --no-check-certificate --progress=dot:mega https://mcc.lip6.fr/2022/archives/raw-result-analysis.csv.zip
unzip raw-result-analysis.csv.zip
fi
# create oracle files
mkdir oracle
# all results available
cat raw-result-analysis.csv | grep -v StateSpace | grep -v UpperBound | cut -d ',' -f2,3,16 | sed 's/\s//g' | sort | uniq | ../csv_to_control.pl
# UpperBounds => do not remove whitespace
cat raw-result-analysis.csv | grep UpperBound | cut -d ',' -f2,3,16 | sort | uniq | ../csv_to_control.pl
# Patching bad consensus
# this series is due to errors in ITS-Tools + reinforced by being Gold21 (sorry !)
# Symmetric choice reduction rule was applied without enough safeguards in this context (LIVENESS/QUASILIVENESS).
sed -i -e "s/QuasiLiveness TRUE/QuasiLiveness FALSE/" SieveSingleMsgMbox-PT-d1m06-QL.out
sed -i -e "s/QuasiLiveness TRUE/QuasiLiveness FALSE/" SieveSingleMsgMbox-PT-d1m18-QL.out
sed -i -e "s/QuasiLiveness TRUE/QuasiLiveness FALSE/" SieveSingleMsgMbox-PT-d1m36-QL.out
sed -i -e "s/QuasiLiveness TRUE/QuasiLiveness FALSE/" SieveSingleMsgMbox-PT-d1m64-QL.out
sed -i -e "s/QuasiLiveness TRUE/QuasiLiveness FALSE/" SieveSingleMsgMbox-PT-d1m96-QL.out
# these points agree with Gold2021 (ITSTools) and current ITSTools 2022-09
# but disagree with consensus that is based on ITSTools 2022-05 answer (possibly a bug in SMT solver interaction ? not reproduced so far)
# no other tool provided an answer on these formulas.
# We currently believe ITSTools2021+2022-09 is right.
sed -i -e "s/StigmergyCommit-PT-11a-ReachabilityCardinality-06 TRUE/StigmergyCommit-PT-11a-ReachabilityCardinality-06 FALSE/" StigmergyCommit-PT-11a-RC.out
sed -i -e "s/StigmergyCommit-PT-11a-ReachabilityCardinality-13 FALSE/StigmergyCommit-PT-11a-ReachabilityCardinality-13 TRUE/" StigmergyCommit-PT-11a-RC.out
sed -i -e "s/StigmergyCommit-PT-11a-ReachabilityCardinality-14 TRUE/StigmergyCommit-PT-11a-ReachabilityCardinality-14 FALSE/" StigmergyCommit-PT-11a-RC.out
sed -i -e "s/StigmergyCommit-PT-11a-ReachabilityCardinality-15 FALSE/StigmergyCommit-PT-11a-ReachabilityCardinality-15 TRUE/" StigmergyCommit-PT-11a-RC.out
# this point is an error from Tapaal22 that got consensus from Gold21=Tapaal
# confirmed manually, formula reduces to true trivially (markings are >= 0)
sed -i -e "s/RERS17pb115-PT-5-LTLCardinality-04 FALSE/RERS17pb115-PT-5-LTLCardinality-04 TRUE/" RERS17pb115-PT-5-LTLC.out
# this is an error of GreatSPN, nobody else answered the query
# GreatSPN has other errors in LTLF on this model
# and manual inspection confirms that the transitions cannot stay indefinitely enabled
sed -i -e "s/DNAwalker-PT-05track28LR-LTLFireability-06 FALSE/DNAwalker-PT-05track28LR-LTLFireability-06 TRUE/" DNAwalker-PT-05track28LR-LTLF.out
# this seems to be an error of Enpac, nobody else answered the query
# EnPAC has other errors in LTLC on this model
# ITS-tools proves it using knowledge approach
sed -i -e "s/Sudoku-COL-BN16-LTLCardinality-14 FALSE/Sudoku-COL-BN16-LTLCardinality-14 TRUE/" Sudoku-COL-BN16-LTLC.out
sed -i -e "s/Sudoku-COL-BN09-LTLCardinality-12 TRUE/Sudoku-COL-BN09-LTLCardinality-12 FALSE/" Sudoku-COL-BN09-LTLC.out
mv *.out oracle/
#rm -f raw-result-analysis.csv*
cd oracle
tar xzf ../../oracleSS.tar.gz
cd ..
tar czf oracle.tar.gz oracle/
rm -rf oracle/
tree -H "." > index.html
cd ..