Commit 6633ae37 authored by Heiko Becker's avatar Heiko Becker
Browse files

Benchmarks can be run now and we only get two timeouts for HOL-Light

parent 57cd2183
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
#################################################################################### ####################################################################################
#Configure a 20 minute stimeout for the HOL-Light scripts #Configure a 20 minute stimeout for the HOL-Light scripts
TIMEOUT=20m TIMEOUT=40m
arr=() arr=()
while IFS= read -r -d $'\0'; do while IFS= read -r -d $'\0'; do
...@@ -18,32 +18,32 @@ done < <(find ./testcases/formal/ -name "*.scala" -print0) ...@@ -18,32 +18,32 @@ done < <(find ./testcases/formal/ -name "*.scala" -print0)
for file in "${arr[@]}" for file in "${arr[@]}"
do do
echo $file echo $file
## echo "Coq certificate" echo "Coq certificate"
## time (./daisy $file --certificate=coq >/dev/null) time (./daisy $file --certificate=coq >/dev/null)
echo "HOL Certificate" echo "HOL Certificate"
time (./daisy $file --certificate=hol >/dev/null) time (./daisy $file --certificate=hol >/dev/null)
echo "" echo ""
done done
# #
#echo "" echo ""
#echo "[Certificate Test]" echo "[Certificate Test]"
#echo "" echo ""
#cd coq cd coq
#arrCoq=() arrCoq=()
#while IFS= read -r -d $'\0'; do while IFS= read -r -d $'\0'; do
# arrCoq+=("$REPLY") arrCoq+=("$REPLY")
#done < <(find ./output/ -name "*.v" -print0) done < <(find ./output/ -name "*.v" -print0)
#
#for file in "${arrCoq[@]}" for file in "${arrCoq[@]}"
#do do
# echo $file echo $file
# echo "" echo ""
# time (coqc -R ./ Daisy $file) time (coqc -R ./ Daisy $file)
#done done
#cd ../hol cd ../hol
cd hol #cd hol
arrHOL=() arrHOL=()
while IFS= read -r -d $'\0'; do while IFS= read -r -d $'\0'; do
......
...@@ -7,22 +7,22 @@ object Pitch { ...@@ -7,22 +7,22 @@ object Pitch {
// s1, s2, s3, y1: <1, 32, 30>, [-1, 1] // s1, s2, s3, y1: <1, 32, 30>, [-1, 1]
def out1(s1: Real, s2: Real, s3: Real): Real = { def out1(s1: Real, s2: Real, s3: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1) require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1)
(0.120200) * state1 + (-42.565500) * state2 + (-1.000100) * state3 (0.120200) * s1 + (-42.565500) * s2 + (-1.000100) * s3
} }
def state1(s1: Real, s2: Real, s3: Real, y1: Real): Real = { def state1(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1) require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(0.999715) * state1 + (0.046781) * state2 + (-0.000333) * state3 + (0.000100) * y1 (0.999715) * s1 + (0.046781) * s2 + (-0.000333) * s3 + (0.000100) * y1
} }
def state2(s1: Real, s2: Real, s3: Real, y1: Real): Real = { def state2(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1) require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(-0.000011) * state1 + (0.998710) * state2 + (-0.000020) * state3 + (0.000000) * y1 (-0.000011) * s1 + (0.998710) * s2 + (-0.000020) * s3 + (0.000000) * y1
} }
def state3(s1: Real, s2: Real, s3: Real, y1: Real): Real = { def state3(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1) require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(-0.000000) * state1 + (0.056663) * state2 + (0.998299) * state3 + (0.001700) * y1 (-0.000000) * s1 + (0.056663) * s2 + (0.998299) * s3 + (0.001700) * y1
} }
} }
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