Commit c37e4263 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' of gitlab.mpi-sws.org:hbecker/daisy

parents 70e00619 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
import daisy.lang._
import Real._
import Real._
object BallBeam {
// s1 <1, 16, 14>, s2, s3, s4: <1, 16, 15>
def ballBeamDowncast(s1: Real, s2: Real, s3: Real, s4: Real) = {
def ballbeam(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(0 <= s1 && s1 <= 1 && -0.5 <= s2 && s2 <= 0.5 && 0 <= s3 && s3 <= 0.5 && 0 <= s4 && s4 <= 0.5)
val s5 = (-1828.6) * s1
s5 + (-1028.6) * s2 + (-2008.0) * s3 + (-104.0) * s4
(-1828.6) * s1 + (-1028.6) * s2 + (-2008.0) * s3 + (-104.0) * s4
}
......
import daisy.lang._
import Real._
object BatchProcessor {
// s1, s2, s3, s4, y1, y2: <1, 16, 11>
// 7 binary operations
def out1(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(-10 <= s1 && s1 <= 10 && -10 <= s2 && s2 <= 10 && -10 <= s3 && s3 <= 10 && -10 <= s4 && s4 <= 10)
(-0.0429) * s1 + (-0.9170) * s2 + (-0.3299) * s3 + (-0.8206) * s4
}
//7 binary operations
def out2(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(-10 <= s1 && s1 <= 10 && -10 <= s2 && s2 <= 10 && -10 <= s3 && s3 <= 10 && -10 <= s4 && s4 <= 10)
2.4908 * s1 + 0.0751 * s2 + 1.7481 * s3 + (-1.1433) * s4
}
//9 binary operations
def state1(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real) = {
require(-10 <= s1 && s1 <= 10 && -10 <= s2 && s2 <= 10 && -10 <= s3 && s3 <= 10 && -10 <= s4 && s4 <= 10 &&
-10 <= y1 && y1 <= 10)
0.9670 * s1 + (-0.0019) * s2 + 0.0187 * s3 + (-0.0088) * s4 + 0.0447 * y1
}
//11 binary operations
def state2(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-10 <= s1 && s1 <= 10 && -10 <= s2 && s2 <= 10 && -10 <= s3 && s3 <= 10 && -10 <= s4 && s4 <= 10 &&
-10 <= y1 && y1 <= 10 && -10 <= y2 && y2 <= 10)
(-0.0078) * s1 + 0.9052 * s2 + (-0.0181) * s3 + (-0.0392) * s4 + (-0.0003) * y1 + 0.0020 * y2
//((0.9052 * s2) + (((s3 * -0.0181) + (-0.0078 * s1)) + (((-0.0392 * s4) + (-0.0003 * y1)) + (0.002 * y2))))
}
//11 binary operations
def state3(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-10 <= s1 && s1 <= 10 && -10 <= s2 && s2 <= 10 && -10 <= s3 && s3 <= 10 && -10 <= s4 && s4 <= 10 &&
-10 <= y1 && y1 <= 10 && -10 <= y2 && y2 <= 10)
(-0.0830) * s1 + 0.0222 * s2 + 0.8620 * s3 + 0.0978 * s4 + 0.0170 * y1 + 0.0058 * y2
}
//11 binary operations
def state4(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-10 <= s1 && s1 <= 10 && -10 <= s2 && s2 <= 10 && -10 <= s3 && s3 <= 10 && -10 <= s4 && s4 <= 10 &&
-10 <= y1 && y1 <= 10 && -10 <= y2 && y2 <= 10)
(-0.0133) * s1 + 0.0243 * s2 + (-0.0043) * s3 + 0.9824 * s4 + 0.0127 * y1 + 0.0059 * y2
}
}
import daisy.lang._
import Real._
object BatchReactor {
// s1, s2, s3, s4, y1, y2: <1, 16, 14>
//7 operations
def out1(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1)
(-0.058300) * s1 + (-0.908300) * s2 + (-0.325800) * s3 + (-0.872100) * s4
}
//7 operations
def out2(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1)
(2.463800) * s1 + (0.050400) * s2 + (1.709900) * s3 + (-1.165300) * s4
}
//11 operations
def state1(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(0.934292) * s1 + (0.008415) * s2 + (-0.014106) * s3 + (0.023954) * s4 + (0.077400) * y1 + (-0.010300) * y2
}
//11 operations
def state2(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(-0.006769) * s1 + (0.884924) * s2 + (-0.016066) * s3 + (-0.044019) * s4 + (-0.002200) * y1 + (0.022700) * y2
}
//11 operations
def state3(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(-0.092148) * s1 + (-0.011039) * s2 + (0.853511) * s3 + (0.107537) * s4 + (0.026700) * y1 + (0.039800) * y2
}
//11 operations
def state4(s1: Real, s2: Real, s3: Real, s4: Real, y1: Real, y2: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(-0.036410) * s1 + (0.030194) * s2 + (-0.027155) * s3 + (1.004619) * s4 + (0.035600) * y1 + (0.000100) * y2
}
}
import daisy.lang._
import Real._
object Bicycle {
// s1, s2, s3, y1: <1, 16, 14>, [-1, 1]
def out1(s1: Real, s2: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1)
(-3.025300) * s1 + (-12.608900) * s2
}
def state1(s1: Real, s2: Real, y1: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= y1 && y1 <= 1)
(0.961270) * s1 + (-0.095962) * s2 + (0.013200) * y1
}
def state2(s1: Real, s2: Real, y1: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= y1 && y1 <= 1)
(-0.058217) * s1 + (0.727430) * s2 + (0.102100) * y1
}
}
\ No newline at end of file
import daisy.lang._
import Real._
/**
Equation and initial ranges from:
L. Zhang, Y. Zhang, and W. Zhou. Tradeoff between Approximation Accuracy and
Complexity for Range Analysis using Affine Arithmetic.
*/
object Bsplines {
def bspline0(u: Real): Real = {
require(0 <= u && u <= 1)
(1 - u) * (1 - u) * (1 - u) / 6.0
} ensuring (res => 0 <= res && res <= 0.17 && res +/- 1e-15)
// proven in paper: [-0.05, 0.17]
def bspline1(u: Real): Real = {
require(0 <= u && u <= 1)
(3 * u*u*u - 6 * u*u + 4) / 6.0
} ensuring (res => 0.16 <= res && res <= 0.7 && res +/- 1e-15)
// in paper [-0.05, 0.98]
def bspline2(u: Real): Real = {
require(0 <= u && u <= 1)
(-3 * u*u*u + 3*u*u + 3*u + 1) / 6.0
} ensuring (res => 0.16 <= res && res <= 0.7 && res +/- 1e-15)
// in paper [-0.02, 0.89]
def bspline3(u: Real): Real = {
require(0 <= u && u <= 1)
-u*u*u / 6.0
} ensuring (res => -0.17 <= res && res <= 0.0 && res +/- 1e-15)
// in paper [-0.17, 0.05]
}
......@@ -2,27 +2,27 @@ import daisy.lang._
import Real._
object Pitch {
object DCMotor {
// s1, s2, s3, y1: <1, 32, 30>, [-1, 1]
def out1(s1: Real, s2: Real, s3: Real): Real = {
// s1, s2, s3, y1: <1, 16, 14>, [-1, 1]
def out1(s1: Real, s2: Real, s3: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1)
(0.120200) * s1 + (-42.565500) * s2 + (-1.000100) * s3
(-0.112900) * s1 + (-0.021100) * s2 + (-0.009300) * s3
}
def state1(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
def state1(s1: Real, s2: Real, s3: Real, y1: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(0.999715) * s1 + (0.046781) * s2 + (-0.000333) * s3 + (0.000100) * y1
(0.960883) * s1 + (0.000949) * s2 + (-0.000004) * s3 + (0.039000) * y1
}
def state2(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
def state2(s1: Real, s2: Real, s3: Real, y1: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(-0.000011) * s1 + (0.998710) * s2 + (-0.000020) * s3 + (0.000000) * y1
(-0.602449) * s1 + (0.899089) * s2 + (-0.013648) * s3 + (0.370000) * y1
}
def state3(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
def state3(s1: Real, s2: Real, s3: Real, y1: Real) = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(-0.000000) * s1 + (0.056663) * s2 + (0.998299) * s3 + (0.001700) * y1
(-0.009134) * s1 + (-0.011434) * s2 + (-0.002232) * s3 + (-0.017500) * y1
}
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object Doppler {
def doppler(u: Real, v: Real, T: Real): Real = {
require(-100.0 <= u && u <= 100 && 20 <= v && v <= 20000 && -30 <= T && T <= 50)
val t1 = 331.4 + 0.6 * T
(- (t1) *v) / ((t1 + u)*(t1 + u))
}
}
\ No newline at end of file
import daisy.lang._
import Real._
/*
Real2Float
Optimization problems
A Collection of Test Problems for
Constrained Global Optimization Algorithms,
Floudas, Pardalos 1990
*/
object Floudas {
//40 operations
def floudas26(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real,
x7: Real, x8: Real, x9: Real, x10: Real): Real = {
require(0 <= x1 && x1 <= 1 && 0 <= x2 && x2 <= 1 && 0 <= x3 && x3 <= 1 && 0 <= x4 && x4 <= 1 &&
0 <= x5 && x5 <= 1 && 0 <= x6 && x6 <= 1 && 0 <= x7 && x7 <= 1 && 0 <= x8 && x8 <= 1 &&
0 <= x9 && x9 <= 1 && 0 <= x10 && x10 <= 1)
48*x1 + 42*x2 + 48*x3 + 45*x4 + 44*x5 + 41*x6 + 47*x7 + 42*x8 + 45*x9 + 46*x10 -
50*(x1*x1 + x2*x2 + x3*x3 + x4*x4 + x5*x5 + x6*x6 + x7*x7 + x8*x8 + x9*x9 + x10*x10)
}// 5.15e-13
//25 operations
def floudas33(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(0 <= x1 && x1 <= 6 && 0 <= x2 && x2 <= 6 && 1 <= x3 && x3 <= 5 &&
0 <= x4 && x4 <= 6 && 1 <= x5 && x5 <= 5 && 0 <= x6 && x6 <= 10)
(-1) * (25 * (x1 - 2)*(x1 - 2)) - (x2 - 2)* (x2 - 2) - (x3 - 1)*(x3 - 1) -
(x4 - 4)*(x4 - 4) - (x5 - 1)*(x5 - 1) - (x6 - 4)* (x6 - 4)
} //5.81e–13
//3 operations
def floudas34(x1: Real, x2: Real, x3: Real): Real = {
require(0 <= x1 && x1 <= 2 && 0 <= x2 && x2 <= 2 && 0 <= x3 && x3 <= 3)
-2 * x1 + x2 - x3
} //2.67e - 15
//2 operations
def floudas46(x1: Real, x2: Real): Real = {
require(0 <= x1 && x1 <= 3 && 0 <= x2 && x2 <= 4)
(-1 * x1) - x2
} //1.38e–15
//5 operations
def floudas47(x1: Real, x2: Real): Real = {
require(0 <= x1 && x1 <= 2 && 0 <= x2 && x2 <= 3)
-12*x1 - 7*x2 +x2 *x2
} //1.01e–14
//24 operations
// from FPTaylor github
def floudas1(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(0 <= x1 && x1 <= 6 && 0 <= x2 && x2 <= 6 && 1 <= x3 && x3 <= 5 &&
0 <= x4 && x4 <= 6 && 1 <= x5 && x5 <= 5 && 0 <= x6 && x6 <= 10)
-25 * ((x1 - 2) * (x1 - 2)) - ((x2 - 2) * (x2 - 2)) - ((x3 - 1) * (x3 - 1)) -
((x4 - 4) * (x4 - 4)) - ((x5 - 1) * (x5 - 1)) - ((x6 - 4) * (x6 - 4))
}
}
import daisy.lang._
import Real._
/*
Real2Float
From a global optimization problem
A Numerical Evaluation of Several Stochastic Algorithms on
Selected Continuous Global Optimization problems,
Ali, Khompatraporn, Zabinsky, 2005
*/
object HimmilbeauLet {
//15 operations
def himmilbeau(x1: Real, x2: Real) = {
require(-5 <= x1 && x1 <= 5 && -5 <= x2 && x2 <= 5)
val t1 = x1*x1 + x2
val t2 = x1 + x2*x2
(t1 - 11)*(t1 - 11) + (t2 - 7)*(t2 - 7)
} //1.43e–12
}
import daisy.lang._
import Real._
object InvertedPendulum {
// s1: <1, 16, 9> s2: <1, 16, 11> s3,s4: <1, 16, 15>
def out(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(-50 <= s1 && s1 <= 50 && -10 <= s2 && s2 <= 10 && -0.785 <= s3 && s3 <= 0.785 && -0.785 <= s4 && s4 <= 0.785)
1.0000 * s1 + 1.6567 * s2 + (-18.6854) * s3 + (-3.4594) * s4
}
}
\ No newline at end of file
import daisy.lang._
import Real._
/*
These benchmarks were used by the Real2Float tool,
and come from the proof of the Kepler conjecture
Introduction to the flyspec project, T.C. Hales, Dagstuhl 2006
*/
object Kepler {
//15 operations
def kepler0(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
val t = ((-1 * x1) + x2 + x3 - x4 + x5 + x6)
x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * t
} // 1.15e-15
//24 operations
def kepler1(x1: Real, x2: Real, x3: Real, x4: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
4 <= x4 && x4 <= 6.36)
val t = ((-1 * x1) + x2 + x3 - x4)
x1 * x4 * t + x2 * (x1 - x2 + x3 + x4) + x3 * (x1 + x2 - x3 + x4) -
x2 * x3 * x4 - x1 * x3 - x1 * x2 - x4
} // 4.50e–13
//36 operations
def kepler2(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
val t = ((-1 * x1) + x2 + x3 - x4 + x5 + x6)
val t2 = (x1 - x2 + x3 + x4 - x5 + x6)
x1 * x4 * t + x2 * x5 * t2 +
x3* x6 * (x1 + x2 - x3 + x4 + x5 - x6) - x2 * x3 * x4 -
x1* x3* x5 - x1 * x2 * x6 - x4 * x5 * x6
} //2.08e–12
}
import daisy.lang._
import Real._
object RigidBody {
def rigidBody1(x1: Real, x2: Real, x3: Real): Real = {
require(-15.0 <= x1 && x1 <= 15 && -15.0 <= x2 && x2 <= 15.0 && -15.0 <= x3 && x3 <= 15)
-x1*x2 - 2*x2*x3 - x1 - x3
}
def rigidBody2(x1: Real, x2: Real, x3: Real): Real = {
require(-15.0 <= x1 && x1 <= 15 && -15.0 <= x2 && x2 <= 15.0 &&
-15.0 <= x3 && x3 <= 15)
val x_tmp = x1 * x2 * x3
2*(x_tmp) + (3*x3*x3) - x2*(x_tmp) + (3*x3*x3) - x2
}
}
import daisy.lang._
import Real._
object Science {
def verhulst(r: Real, K: Real, x: Real): Real = {
require(r >= 4.0 && r <= 4.0 && K >= 1.11 && K <= 1.11 && 0.1 <= x && x <= 0.3)
(r*x) / (1 + (x/K))
}
def predatorPrey(r: Real, K: Real, x: Real): Real = {
require(r >= 4.0 && r <= 4.0 && K >= 1.11 && K <= 1.11 && 0.1 <= x && x <= 0.3)
(r*x*x) / (1 + (x/K)*(x/K))
}
def carbonGas(T: Real, a: Real, b: Real, N: Real, p: Real, V: Real): Real = {
require(T >= 300 && T <= 300 && a >= 0.401 && a <= 0.401 && b >= 42.7e-6 && b <= 42.7e-6 && N >= 1000 && N <= 1000 &&
p >= 3.5e7 && p <= 3.5e7 && 0.1 < V && V < 0.5)
val k: Real = 1.3806503e-23
(p + a * (N / V) * (N / V)) * (V - N * b) - k * N * T
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object Traincar1 {
// y1, y2: <1, 30, 16> s1, s2, s3: <1, 30, 25>
def out1(s0: Real, s1: Real, s2: Real) = {
require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10)
(-3.795323e2) * s0 + (-5.443608e2) * s1 + 92.729 * s2 + 4.5165916241610748e3
}
def state1(s0: Real, s1: Real, s2: Real, y0: Real, y1: Real) = {
require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10)
(9.9992292212695999e-01)*s0+ (6.7987387059578006e-02)*s1+ (-5.7849982690687002e-02)*s2 +
(-6.7093068270769995e-02)*y0 + (5.6868444245656999e-02)*y1+ (1.93109421e-07)*4.5165916241610748e+03
}
def state2(s0: Real, s1: Real, s2: Real, y0: Real, y1: Real) = {
require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10)
(-2.1755689728790001e-03)*s0+ (9.8343791204296505e-01)*s1+ (2.6908497812900001e-03)*s2 +
(1.3497550507479000e-02)*y0 + (-2.1628302791680000e-03)*y1+ (5.615999103e-06)*4.5165916241610748e+03
}
def state3(s0: Real, s1: Real, s2: Real, y0: Real, y1: Real) = {
require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10)
(7.5141305955000001e-05)*s0+ (2.4840831806619999e-03)*s1+ (9.9188004018882503e-01)*s2 + (-2.4770170720600001e-03)*y0 +
(8.1097048460159991e-03)*y1+ (7.060315e-09)*4.5165916241610748e+03
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object Traincar2 {
// y1, y2, y3:<1, 30, 24> s.:<1, 30, 25>
//10 operations
def out1(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real) = {
require(-2 <= s0 && s0 <= 9 && -2 <= s1 && s1 <= 9 && 0 <= s2 && s2 <= 10 && 0 <= s3 && s3 <= 10 && 0 <= s4 && s4 <= 10)
(-2.9829300077345002E+00) * s0 + 2.8399180104656203E+01 * s1 + (-1.5201325206209998E+02) * s2 +
3.5623840930436779E+02 * s3 + (-2.0636383424191501E+02) * s4 + 2.1660394157545902E+01
}
//17 operations
def state1(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, y0: Real, y1: Real, y2: Real) = {
require(-2 <= s0 && s0 <= 9 && -2 <= s1 && s1 <= 9 && 0 <= s2 && s2 <= 10 && 0 <= s3 && s3 <= 10 && 0 <= s4 && s4 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10 && 0 <= y2 && y2 <= 10)
(9.9999998913656896E-01)*s0+ (1.6994651E-08)*s1+ (1.7498543776970001E-03)*s2+ (-1.4024571647840000E-03)*s3+ (-6.5504777638499998E-04)*s4 +
(-1.6499310260960000E-03)*y0 + (1.3026354031020000E-03)*y1+ (6.5494511318299996E-04)*y2+ (4.95505E-10)*2.1660394157545902E+01
}
//17 operations
def state2(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, y0: Real, y1: Real, y2: Real) = {
require(-2 <= s0 && s0 <= 9 && -2 <= s1 && s1 <= 9 && 0 <= s2 && s2 <= 10 && 0 <= s3 && s3 <= 10 && 0 <= s4 && s4 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10 && 0 <= y2 && y2 <= 10)
(2.094468E-09)*s0 +(9.9999999447142096E-01)*s1+ (5.8521627784900005E-04)*s2+ (9.9584190606899991E-04)*s3+ (-1.6218071590199999E-03)*s4 +
(-5.8524111148300004E-04)*y0 +(-8.9578466384499997E-04)*y1+ (1.5217743914859999E-03)*y2+ (1.65715E-10)*2.1660394157545902E+01
}
//17 operations
def state3(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, y0: Real, y1: Real, y2: Real) = {
require(-2 <= s0 && s0 <= 9 && -2 <= s1 && s1 <= 9 && 0 <= s2 && s2 <= 10 && 0 <= s3 && s3 <= 10 && 0 <= s4 && s4 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10 && 0 <= y2 && y2 <= 10)
(-6.146088015E-06)*s0 +(1.6077937611999999E-05)*s1+ (9.9960914235631004E-01)*s2+ (2.4348362886800001E-04)*s3+ (-7.6912511450999999E-05)*s4 +
(3.0415154725900001E-04)*y0 + (-4.1163170637999999E-05)*y1+ (-3.9928229421000001E-05)*y2+ (5.66185021E-07)*2.1660394157545902E+01
}
//17 operations
def state4(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, y0: Real, y1: Real, y2: Real) = {
require(-2 <= s0 && s0 <= 9 && -2 <= s1 && s1 <= 9 && 0 <= s2 && s2 <= 10 && 0 <= s3 && s3 <= 10 && 0 <= s4 && s4 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10 && 0 <= y2 && y2 <= 10)
(7.818052258E-06)*s0 +(-7.817588962E-06)*s1+ (5.7051393301999997E-05)*s2+ (9.9968914504599404E-01)*s3+ (4.600832536E-05)*s4 +
(-5.596127001E-05)*y0 + (3.0867555741500002E-04)*y1+ (-4.4919087053000003E-05)*y2+ (1.6155E-11)*2.1660394157545902E+01
}
//16 operations
def state5(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, y0: Real, y1: Real, y2: Real) = {
require(-2 <= s0 && s0 <= 9 && -2 <= s1 && s1 <= 9 && 0 <= s2 && s2 <= 10 && 0 <= s3 && s3 <= 10 && 0 <= s4 && s4 <= 10 &&
0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10 && 0 <= y2 && y2 <= 10)
s0 +(7.81854687E-06)*s1+ (4.9735362656000002E-05)*s2+ (4.7301196887999997E-05)*s3+ (9.9971578912639303E-01)*s4 +
(-4.9737493605000002E-05)*y0 +(-4.6203604013000001E-05)*y1+ (2.8311538117500000E-04)*y2+ (1.4084E-11)*2.1660394157545902E+01
}
}
import daisy.lang._
import Real._
object Traincar3 {
// y: <1, 30, 20> s:<1, 30, 25>
//17 operations
def out1(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real) = {
require(-3 <= s0 && s0 <= 5 && -3 <= s1 && s1 <= 5 && -3 <= s2 && s2 <= 5 && -6 <= s3 && s3 <= 11 && -6 <= s4 && s4 <= 11 &&
-6 <= s5 && s5 <= 11 && -6 <= s6 && s6 <= 11)
(-3.7377847506227999E+02) * s0 + 7.0862205220929002E+02 * s1 + (-3.7886044910192999E+02) * s2 + (-4.5413076942315001E+02) * s3 +