Commit 6d7731d7 authored by Etienne Renault's avatar Etienne Renault
Browse files

benchs: automatic extraction from RERS

* benchs/RERS/ltlrers2go.sh: Here.
parent fb7266af
# 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
cat /tmp/3 | sed 's/^/"final_output == /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
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
Markdown is supported
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