Skip to content

GitLab

F
FloVer
Commit 99097397 authored by Eva Darulova's avatar Eva Darulova
Browse files
Options

new mixed-precision errors fro CPP2018 evaluation

parent 39caf498
Hide whitespace changes
Inline Side-by-side
Showing with 179 additions and 152 deletions
scripts/formal/cpp2018_error_script.sh 0 → 100755
View file @ 99097397
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("BallBeam" "BatchProcessor" "BatchReactor" "Bicycle" "Bsplines" \
"DCMotor" "Doppler" "Floudas" "HimmilbeauLet" "InvertedPendulum" "KeplerLet" \
"RigidBody" "Science" "Traincar1" "Traincar2" "Traincar3" "Traincar4" \
"TurbineLet")
# Make sure the code is compiled
sbt compile
# generate daisy script
if [ ! -e daisy ]
then
sbt script
fi
# Run daisy on each testfile
for file in "${files[@]}"
do
./daisy --errorMethod=interval --mixed-precision="testcases/mixed-precision-maps/${file}.txt" \
"testcases/cpp2018/${file}.scala"
done
\ No newline at end of file
testcases/mixed-precision-maps/BatchProcessor.txt
View file @ 99097397
out1 = {
s1: Float
s1: Double
s2: Double
s3: Double
s4: Float
s4: Double
}
out2 = {
s1: Double
s2: Float
s3: Float
s2: Double
s3: Double
s4: Double
}
state1 = {
s1: Float
s2: Float
s1: Double
s2: Double
s3: Double
s4: Float
s4: Double
y1: Double
}
state2 = {
s1: Float
s1: Double
s2: Double
s3: Double
s4: Float
y1: Float
s4: Double
y1: Double
y2: Double
}
state3 = {
s1: Float
s1: Double
s2: Double
s3: Double
s4: Float
s4: Double
y1: Double
y2: Float
y2: Double
}
state4 = {
s1: Float
s2: Float
s1: Double
s2: Double
s3: Double
s4: Float
y1: Float
y2: Float
s4: Double
y1: Double
y2: Double
}
testcases/mixed-precision-maps/BatchReactor.txt
View file @ 99097397
out1 = {
s1: Float
s1: Double
s2: Double
s3: Double
s4: Float
s4: Double
}
out2 = {
s1: Double
s2: Float
s3: Float
s2: Double
s3: Double
s4: Double
}
state1 = {
s1: Float
s2: Float
s1: Double
s2: Double
s3: Double
s4: Float
s4: Double
y1: Double
}
state2 = {
s1: Float
s1: Double
s2: Double
s3: Double
s4: Float
y1: Float
s4: Double
y1: Double
y2: Double
}
state3 = {
s1: Float
s1: Double
s2: Double
s3: Double
s4: Float
s4: Double
y1: Double
y2: Float
y2: Double
}
state4 = {
s1: Float
s2: Float
s1: Double
s2: Double
s3: Double
s4: Float
y1: Float
y2: Float
s4: Double
y1: Double
y2: Double
}
testcases/mixed-precision-maps/Doppler.txt
View file @ 99097397
doppler = {
u: Double
v: Double
T: Float
v: Float
T: Double
t1: Float
}
testcases/mixed-precision-maps/Floudas.txt
View file @ 99097397
floudas26 = {
x1: Double
x2: Float
x2: Double
x3: Double
x4: Double
x5: Float
x5: Double
x6: Double
x7: Float
x7: Double
x8: Double
x9: Double
x10: Double
......@@ -13,34 +13,34 @@ floudas26 = {
floudas33 = {
x1: Double
x2: Float
x2: Double
x3: Double
x4: Double
x5: Float
x5: Double
x6: Double
}
floudas34 = {
x1: Double
x2: Float
x2: Double
x3: Double
}
floudas46 = {
x1: Double
x2: Float
x2: Double
}
floudas47 = {
x1: Double
x2: Float
x2: Double
}
floudas1 = {
x1: Double
x2: Float
x2: Double
x3: Double
x5: Float
x5: Double
x6: Double
}
......
testcases/mixed-precision-maps/KeplerLet.txt
View file @ 99097397
kepler0 = {
x1: Double
x1: Float
x2: Float
x3: Double
x4: Double
x5: Float
x5: Double
x6: Double
t: Float
}
kepler1 = {
x1: Double
x1: Float
x2: Float
x3: Double
x4: Double
......@@ -17,12 +17,12 @@ kepler1 = {
}
kepler2 = {
x1: Double
x1: Float
x2: Float
x3: Double
x4: Double
x5: Float
x5: Double
x6: Double
t: Float
t2: Double
t2: Float
}
\ No newline at end of file
testcases/mixed-precision-maps/Traincar2.txt
View file @ 99097397
......@@ -2,8 +2,8 @@ out1 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
}
......@@ -11,11 +11,11 @@ state1 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
y0: Double
y1: Double
y2: Float
y2: Double
}
......@@ -23,42 +23,42 @@ state2 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
y0: Double
y1: Double
y2: Float
y2: Double
}
state3 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
y0: Double
y1: Double
y2: Float
y2: Double
}
state4 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
y0: Double
y1: Double
y2: Float
y2: Double
}
state5 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
y0: Double
y1: Double
y2: Float
y2: Double
}
testcases/mixed-precision-maps/Traincar3.txt
View file @ 99097397
......@@ -2,8 +2,8 @@ out1 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
}
......@@ -13,13 +13,13 @@ state1 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
......@@ -28,13 +28,13 @@ state2 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
......@@ -42,13 +42,13 @@ state3 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
......@@ -56,13 +56,13 @@ state4 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
......@@ -70,13 +70,13 @@ state5 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
......@@ -84,13 +84,13 @@ state6 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
......@@ -98,13 +98,13 @@ state7 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
}
testcases/mixed-precision-maps/Traincar4.txt
View file @ 99097397
......@@ -2,12 +2,12 @@ out1 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
}
......@@ -15,17 +15,17 @@ state1 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
......@@ -33,134 +33,134 @@ state2 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state3 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state4 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state5 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state6 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state7 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state8 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float
s3: Double
s4: Double
s5: Double
s6: Double
s7: Float
s8: Float
s7: Double
s8: Double
y0: Double
y1: Double
y2: Float
y2: Double
y3: Double
y4: Float
y4: Double
}
state9 = {
s0: Double
s1: Double
s2: Double
s3: Float
s4: Float