ltlrers2go.sh 4.11 KB
Newer Older
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
# Copyright (C) 2020 Laboratoire de Recherche et Developpement
# de l'EPITA (LRDE).
#
# This file is part of Go2Pins, a tool for Golang model-checking
#
# Go2Pins is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Go2Pins is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program.  If not, see <http://www.gnu.org/licenses/>.
#
#! /bin/bash

MODEL=Problem7
YEAR=2020
CONSTRAINTS=constraints-$MODEL.txt
RES="$YEAR-$MODEL-ltl"
cp /Users/etienne/Desktop/RERS/$YEAR/$MODEL/$CONSTRAINTS .
cp /Users/etienne/Desktop/RERS/$YEAR/$MODEL/$MODEL.c .


################################################################################
# First remove useless stuff from $MODEL.c
################################################################################

# Remove output and replace it by setting a variable
cat $MODEL.c | sed 's/printf("%d\\n",/final_output=/g' | sed 's/); fflush(stdout);/;/g' > /tmp/1

cat /tmp/1 | sed 's/#include <stdio.h>//g'                                      | \
    sed 's/#include <assert.h>//g'                                              | \
    sed 's,#include <math.h>,// outputs,g'                                      | \
    sed "s,#include <stdlib.h>,int final_output = 0;,g"                         | \
    sed 's/extern void __VERIFIER_error(int);/void __VERIFIER_error(int n){}/g' | \
    sed 's/int input;/int __RERS__;/g' | sed 's/(input !=/(__RERS__ !=/g'       | \
    sed 's/calculate_output(input);/calculate_output(__RERS__);/g'              | \
    sed "s/scanf(\"%d\", &input);/__RERS__ = __RERS__ + 1;/g"                   | \
    sed "s/return -2;/break;/g"| sed "s#fprintf.*#; // REMOVED#g" > /tmp/$MODEL.c

################################################################################
# Call C4GO to tranpile the $MODEL.c
################################################################################

./c4go transpile /tmp/$MODEL.c
mv $MODEL.go $RES.go

# This last step is mandatory to handle the tranduction of the C instruction
# "a ? b : c" which is translated using closure.
gsed -i 's/int32/int/g' $RES.go


################################################################################
# Rewrite constraints
################################################################################

cat $CONSTRAINTS | grep inputs |  sed 's/#inputs \[//g' | sed 's/]//g' | tr ',' '\n' | tr -d ' ' > /tmp/1

##
# transformation of input
cat /tmp/1 | sed 's/^/i/' > /tmp/2

# convert to position in the alphabet
cat /tmp/1 |  tr -d "\n" | od -An -t uC | sed 's/^ *//g'  | tr ' ' '\n' | sed '/^$/d' | tr ' ' '\n' | sed '/^$/d'  | sed 's/^/echo $((/' | sed 's/$/-64))/' | sh > /tmp/3

# and fix correct variable
cat /tmp/3 | sed 's/^/"main_main___RERS__ == /g' | sed 's/$/"/g' > /tmp/4
mv /tmp/4 /tmp/3

paste -d ':' /tmp/2 /tmp/3 | sed 's/\([^:]*\):\([^:]*\)/s%\1%\2%g/' > sed.script

##
# Transformation of the output

cat $CONSTRAINTS | grep outputs |  sed 's/#outputs \[//g' | sed 's/]//g' | tr ',' '\n' | tr -d ' ' > /tmp/1

# transformation of input
cat /tmp/1 | sed 's/^/o/' > /tmp/2

# convert to position in the alphabet
cat /tmp/1 |  tr -d "\n" | od -An -t uC | sed 's/^ *//g'  | tr ' ' '\n' | sed '/^$/d' | tr ' ' '\n' | sed '/^$/d'  | sed 's/^/echo $((/' | sed 's/$/-64))/' | sh > /tmp/3

# and fix correct variable
89
cat /tmp/3 | sed 's/^/"/main_final_output == /g' | sed 's/$/"/g' > /tmp/4
90
91
92
93
94
95
96
mv /tmp/4 /tmp/3

paste -d ':' /tmp/2 /tmp/3 | sed 's/\([^:]*\):\([^:]*\)/s%\1%\2%g/' >> sed.script

sed -f sed.script $CONSTRAINTS | grep -v '#' | sort -u | sed '/^$/d' | sed 's/WU/W/g' | sed 's/&/&&/g'  | sed 's/|/||/g' > $RES.go.formulae.txt

sed -f sed.script $CONSTRAINTS | grep -v '#' | sort -u | sed '/^$/d' | sed 's/WU/W/g' | sed 's/&/&&/g'  | sed 's/|/||/g' |  sed 's/^/! /g' >> $RES.go.formulae.txt