Commit 44f78c9f authored by Heiko Becker's avatar Heiko Becker

Add new testcases for verification, traincar tests all fail

parent 88459e10
import daisy.lang._
import Real._
object BallBeam {
// s1 <1, 16, 14>, s2, s3, s4: <1, 16, 15>
def out(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)
(-1828.6) * s1 + (-1028.6) * s2 + (-2008.0) * s3 + (-104.0) * s4
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object BatchProcessor {
// s1, s2, s3, s4, y1, y2: <1, 16, 11>
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
}
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
}
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
}
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))))
}
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
}
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
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object BatchReactor {
// s1, s2, s3, s4, y1, y2: <1, 16, 14>
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
}
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
}
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
}
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
}
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
}
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
}
}
\ No newline at end of file
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._
object DCMotor {
// 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.112900) * s1 + (-0.021100) * s2 + (-0.009300) * s3
}
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.960883) * s1 + (0.000949) * s2 + (-0.000004) * s3 + (0.039000) * y1
}
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.602449) * s1 + (0.899089) * s2 + (-0.013648) * s3 + (0.370000) * y1
}
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.009134) * s1 + (-0.011434) * s2 + (-0.002232) * s3 + (-0.017500) * y1
}
}
\ No newline at end of file
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._
object InvertedPendulum4 {
// all: <1, 32, 30> [-1, 1]
def out1() = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1)
(1.536200) * s1 + (2.025400) * s2 + (-16.519200) * s3 + (-2.735800) * s4
}
def state1() = {
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.998301) * s1 + (0.001002) * s2 + (-0.000114) * s3 + (-0.000002) * s4 + (0.001700) * y1 + (0.000100) * y2
}
def state2() = {
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.000693) * s1 + (1.003500) * s2 + (-0.029160) * s3 + (-0.004972) * s4 + (0.002100) * y1 + (0.001800) * y2
}
def state3() = {
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.001197) * s1 + (0.000004) * s2 + (0.987778) * s3 + (0.000994) * s4 + (0.001200) * y1 + (0.012200) * y2
}
def state4() = {
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.006982) * s1 + (0.008751) * s2 + (-0.120899) * s3 + (0.987581) * s4 + (0.000000) * y1 + (0.077000) * y2
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object Pitch {
// s1, s2, s3, y1: <1, 32, 30>, [-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) * state1 + (-42.565500) * state2 + (-1.000100) * state3
}
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) * state1 + (0.046781) * state2 + (-0.000333) * state3 + (0.000100) * y1
}
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) * state1 + (0.998710) * state2 + (-0.000020) * state3 + (0.000000) * y1
}
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) * state1 + (0.056663) * state2 + (0.998299) * state3 + (0.001700) * y1
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object RigidBody {
//x1, x2, x3: < 1, 16 11>, [-15, 15]
def out1(x1: Real, x2: Real, x3: Real): Real = {
require(-15 <= x1 && x1 <= 15 && -15 <= x2 && x2 <= 15 && -15 <= x3 && x3 <= 15)
-x1*x2 - 2*x2*x3 - x1 - x3
}
// apparently this needs 17 bits, or we've not been accurate enough
def out2(x1: Real, x2: Real, x3: Real): Real = {
require(-15 <= x1 && x1 <= 15 && -15 <= x2 && x2 <= 15 && -15 <= x3 && x3 <= 15)
2*x1*x2*x3 + 3*x3*x3 - x2*x1*x2*x3 + 3*x3*x3 - x2
}
}
\ 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>
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
}
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
}
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
}
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
}
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
}
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
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object Traincar3 {
// y: <1, 30, 20> s:<1, 30, 25>
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 +
(-8.7386976105502004E+02) * (1.0)*s4 + 3.5911290954487999E+03 * (1.0)*s5 + (-2.2921226288533999E+03) * (1.0)*s6 + 2.9021426298877441E+02
}
def state1(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(0.9999996047)*s0 + (7.191445178E-07)*s1+ (-3.804306415E-07)*s2+ (0.003390948426)*s3+ (-0.007373658011)*s4 +
(0.00251435504)*s5+ (-0.001735963933)*s6+ (-3.2913896479139998E-03)*y0 + (7.2728293625470000E-03)*y1+
(-2.5109142643930001E-03)*y2+ (1.7337651582750001E-03)*y3+ (9.60292E-10)*2.9021426298877441E+02
}
def state2(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(8.311153577E-10)*s0 +(1.000000002)*s1+ (-1.019462999E-08)*s2+ (1.426096894E-04)*s3+ (0.004152887373)*s4+ (-0.002584463613)*s5+ (-0.001280301976)*s6 +
(-1.4262580017300000E-04)*y0 +(-4.0529285568870000E-03)*y1+ (2.4846129842129999E-03)*y2+ (1.2802087276050000E-03)*y3+ (4.0371E-11)*2.9021426298877441E+02
}
def state3(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(-1.413514624E-07)*s0 +(2.960957207E-07)*s1+ (0.9999997794)*s2+ (0.001259708376)*s3+ (-0.001326863654)*s4+ (0.009741383745)*s5+ (-0.01209814023)*s6 +
(-1.2598715285710000E-03)*y0 + (1.3265590608970001E-03)*y1+ (-9.6401205297600000E-03)*y2+ (1.1997334409343001E-02)*y3+ (3.56771E-10)*2.9021426298877441E+02
}
def state4(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(-2.160538622E-04)*s0 +(4.011584145E-04)*s1+ (-2.14484627E-04)*s2+ (0.9992989209)*s3+ (-3.699735601E-04)*s4+ (0.002043378232)*s5+ (-0.00122374133)*s6 +
(4.4334768343400001E-04)*y0 + (-1.2406658684299999E-04)*y1+ (-1.0483935681000001E-05)*y2+ (-7.3810400367999997E-05)*y3+ (5.66097217E-07)*2.9021426298877441E+02
}
def state5(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(7.805459445E-06)*s0 +(-7.795254622E-06)*s1+ (-1.164219329E-08)*s2+ (1.029861692E-04)*s3+ (0.9992705039)*s4+ (1.709798451E-04)*s5+ (1.943846519E-05)*s6 +
(-1.0190707901600000E-04)*y0 + (7.2728601855600000E-04)*y1+ (-1.6978291545200001E-04)*y2+ (-1.950523374E-05)*y3+ (2.9166E-11)*2.9021426298877441E+02
}
def state6(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(-1.278980488E-09)*s0 +(7.819576188E-06)*s1+ (-7.817496855E-06)*s2+ (1.807543861E-05)*s3+ (1.724117406E-04)*s4+ (0.9992790154)*s5+ (2.725773198E-04)*s6 +
(-1.8077674363999999E-05)*y0 +(-1.7132402225200001E-04)*y1+ (7.1881845635799997E-04)*y2+ (-2.7149682594400002E-04)*y3+ (5.118E-12)*2.9021426298877441E+02
}
def state7(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, y0: Real, y1: Real, y2: Real, y3: 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 && -6 <= y0 && y0 <= 10 && -6 <= y1 && y1 <= 10 && -6 <= y2 && y2 <= 10 &&
-6 <= y3 && y3 <= 10)
(-8.892911482E-09)*s0 +(1.750282868E-08)*s1+ (7.806737695E-06)*s2+ (8.234669601E-05)*s3+ (1.964473315E-06)*s4+ (2.518123976E-04)*s5+
(0.999262088)*s6 + (-8.2357312397000003E-05)*y0 + (-1.984691067E-06)*y1+ (-2.5063655913299998E-04)*y2+ (7.3676635226699999E-04)*y3+
(2.3321E-11)*2.9021426298877441E+02
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object Traincar4 {
// y: <1, 30, 16> s: <1, 30, 25>
def out1(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12)
(-1201.0) * s0 + (-4876.0) * s1 + 1.3415999999999998E+04 * s2 + (-10484.0) * s3 + (-774.0) * s4 + (-1.3620000000000002E+04) * s5 +
10481.0 * s6 + 20425.0 * s7 + (-17815.0) * s8 + 5.2121094496644555E+03
}
def state1(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
s0 + (-9.6239E-08)*s1+ (2.65102E-07)*s2+ (-2.07133E-07)*s3+ (6.97639E-05)*s4+ (-4.78152E-05)*s5+ (-2.63725E-05)*s6+ (-1.05202E-05)*s7+ (-1.57626E-05)*s8 +
(3.0220751E-05)*y0 + (-5.2453841E-05)*y1+ (2.6579541E-05)*y2+ (1.0923688E-05)*y3+ (1.5410654E-05)*y4+ (1.9755163E-11)*5.2121094496644555E+03
}
def state2(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
(-1.13598E-08)*s0 + (1.0)*s1+ (1.2786E-07)*s2+ (-9.96874E-08)*s3+ (3.36288E-05)*s4+ (3.94595E-05)*s5+ (-6.09589E-05)*s6+
(-3.51073E-05)*s7+ (2.7313E-06)*s8+ (-3.3636111E-05)*y0 + (6.0410747E-05)*y1+ (-3.8941208E-05)*y2+ (3.5301806E-05)*y3+
(-2.9009623E-06)*y4+ (9.522692E-12)*5.2121094496644555E+03
}
def state3(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
(-3.85494E-09)*s0 + (-1.55578E-08)*s1+ (1.0)*s2+ (-3.33852E-08)*s3+ (1.13515E-05)*s4+ (8.09597E-06)*s5+ (3.75166E-05)*s6+
(-7.28888E-05)*s7+ (7.51347E-06)*s8 + (-1.1353997E-05)*y0 + (-8.1397399E-06)*y1+ (6.2517037E-05)*y2+
(-2.7045432E-05)*y3+ (-7.570773E-06)*y4+ (3.2144001E-12)*5.2121094496644555E+03
}
def state4(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
(-4.88831E-09)*s0 + (-1.94328E-08)*s1+ (5.40591E-08)*s2+ (1.0)*s3+ (1.41246E-05)*s4+ (-1.33425E-05)*s5+ (4.35487E-06)*s6+
(1.06102E-04)*s7+ (-9.66574E-05)*s8+ (-1.4127737E-05)*y0 + (1.328804E-05)*y1+ (-4.3128989E-06)*y2+
(-6.0208156E-06)*y3+ (-3.4137075E-06)*y4+ (3.9997189E-12)*5.2121094496644555E+03
}
def state5(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
(-6.84591E-04)*s0 + (-0.00276041)*s1+ (0.00759572)*s2+ (-0.00593566)*s3+ (0.999506)*s4+ (-0.00770228)*s5+ (0.00593952)*s6+
(0.0115632)*s7+ (-0.0100812)*s8+ (5.4816343E-05)*y0 + (-8.1959323E-06)*y1+(-5.0852166E-06)*y2+ (-1.5117184E-07)*y3+
(-4.5614134E-06)*y4+ (5.6615597E-07)*5.2121094496644555E+03
}
def state6(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
(7.81569E-06)*s0 +(-7.83331E-06)*s1+ (3.894E-08)*s2+ (-3.04854E-08)*s3+ (1.02522E-05)*s4+ (0.999937)*s5+ (9.27415E-06)*s6+
(6.88119E-06)*s7+ (-5.63471E-06)*s8 + (-9.161729E-06)*y0 + (6.1088274E-05)*y1+ (-8.1509892E-06)*y2+ (-6.8219061E-06)*y3+ (5.5829936E-06)*y4+
(2.9031464E-12)*5.2121094496644555E+03
}
def state7(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
-2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
-2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)