Toyota Powertrain Control Benchmark

powertrain.drh

// Toyota Powertrain Control Verification Benchmark:
// This is based on the following paper:
//
// Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and
// Ken Butts. 2014. Powertrain control verification benchmark. In
// Proceedings of the 17th international conference on Hybrid systems:
// computation and control (HSCC '14). ACM, New York, NY, USA,
// 253-262. DOI=http://dx.doi.org/10.1145/2562059.2562140
//
// Originally written by Kyungmin Bae (kbae@cs.cmu.edu)
// Modified by Soonho Kong (soonhok@cs.cmu.edu)

#define c1	0.41328   // page 262 (table 3)
#define c2	-0.366    // page 262 (table 3)
#define c3	0.08979   // page 262 (table 3)
#define c4	-0.0337   // page 262 (table 3)
#define c5	0.0001    // page 262 (table 3)
#define c6	2.821     // page 262 (table 3)
#define c7	-0.05231  // page 262 (table 3)
#define c8	0.10299   // page 262 (table 3)
#define c9	-0.00063  // page 262 (table 3)
#define c10	1.0       // page 262 (table 3)
#define c11	14.7      // page 262 (table 3)
#define c11P	12.5      // page 262 (table 3)
#define c12	0.9       // page 262 (table 5)
#define c13	0.04      // page 262 (table 3)
#define c14	0.14      // page 262 (table 3)
#define c15	13.893    // page 262 (table 5)
#define c16	-35.2518  // page 262 (table 5)
#define c17	20.7364   // page 262 (table 5)
#define c18	2.6287    // page 262 (table 5)
#define c19	-1.592    // page 262 (table 5)
#define c20	-2.3421   // page 262 (table 5)
#define c21     2.7799    // page 262 (table 5)
#define c22	-0.3273   // page 262 (table 5)
#define c23	1.0       // page 262 (table 5)
#define c24	1.0       // page 262 (table 5)
#define c25	1.0       // page 262 (table 5)
#define c26	4.0       // page 262 (table 5)

#define tauI	10  //
#define h	2.0

#define thetaHat   (c6 + c7*theta + c8*theta*theta + c9*theta*theta*theta) // page 256 (throttle air dynamics)
#define dmAf       (2 * thetaHat * sqrt(p/c10 - (p/c10)^2))  // page 256, (2)
#define mCf(x)     (c2 + c3*w*x + c4*w*x*x + c5*w*w*x)
#define dmC        (c12 * mCf(p))  // page 256, (3)

#define thetaI_init 55
#define thetaI_amp 10

[0,180] theta;
[0,10]   p;
[0,100] lambda;

[0,10]   pe;
[0,100] i;
[0,100] tau;
[0,10]  fc;

[0,180] thetaI;
[0,150] w;

[0,h]   t;
[0,h]   time;


// startup
{mode 1;
  flow:
    d/dt[theta]  = 10 * (thetaI - theta); // page 255, (1)
    d/dt[p]      = c1 * (dmAf - dmC);     // page 256, (4)
    d/dt[lambda] = c26 * (dmC / (c25 * fc) - lambda);  // page 257, (10, 11)
    d/dt[pe]     = 0;
    d/dt[i]      = 0;
    d/dt[tau]    = 0;
    d/dt[fc]     = 0;
    d/dt[t]      = 1;
    d/dt[thetaI] = thetaI_amp * 10 * cos(10 * t);
    d/dt[w]      = 5 * 10 * cos(10 * t);
  jump:
    // stay in the startup mode
    (t = h) ==>
    @1 (and (theta' = theta)
            (p' = p)
            (lambda' = lambda)
            (thetaI' = thetaI)
            (w' = w)
            (pe' = pe)
            (i' = 0)                                      // gi, page 258, (16)
            (tau' = tau + h)                              // gi, page 258, (16)
            (fc' = mCf(pe) / c11)                         // gi, page 258, (16)
            (t' = h));

    // go to the normal mode
    (tau >= tauI) ==>
    @2 (and (theta' = theta)
            (p' = p)
            (lambda' = lambda)
            (thetaI' = thetaI)
            (w' = w)
            (pe' = pe)
            (i' = i)
            (tau' = tau)
            (fc' = fc)
            (t' = h));
}


// normal
{mode 2;
  flow:
    d/dt[theta]  = 10 * (thetaI - theta);  // page 255, (1)
    d/dt[p]      = c1 * (dmAf - dmC);      // page 256, (4)
    d/dt[lambda] = c26 * (dmC / (c25 * fc) - lambda);  // page 257, (10, 11)
    d/dt[pe]     = 0;
    d/dt[i]      = 0;
    d/dt[tau]    = 0;
    d/dt[fc]     = 0;
    d/dt[t]      = 1;
    d/dt[thetaI] = thetaI_amp * 10 * cos(10 * t);
    d/dt[w]      = 5 * 10 * cos(10 * t);
  jump:
    // stay in the normal mode
    (t = h) ==>
    @2 (and (theta' = theta)
            (p' = p)
            (lambda' = lambda)
            (thetaI' = thetaI)
            (w' = w)
            (pe' = pe + h * c1 * (c23 * dmAf - mCf(pe)))
            (i' = i + h * c14 * (c24 * lambda - c11))                    // gc, page 258, (13)
            (tau' = 0)                                                   // gc, page 258, (15)
            (fc' = (1 + i + c13 * (c24 * lambda - c11)) * mCf(pe) / c11) // gc, page 258, (14)
            (t' = 0));

    // goes to the power mode
    (theta >= 70) ==>
    @3 (and (theta' = theta)
            (p' = p)
            (lambda' = lambda)
            (thetaI' = thetaI)
            (w' = w)
            (pe' = pe)
            (i' = i)
            (tau' = tau)
            (fc' = fc)
            (t' = 0));

    // Soonho: For now, we ignore sensor_fail mode
    // // goes to the sensor_fail mode (at any time)
    // (and (t = 0)) ==>  // Soonho: how to model fail_event??
    // @4 (and (theta' = theta)
    //         (p' = p)
    //         (lambda' = lambda)
    //         (thetaI' = thetaI)
    //         (w' = w)
    //         (pe' = pe)
    //         (i' = i)
    //         (tau' = tau)
    //         (fc' = fc)
    //         (t' = 0));
}

// power
{mode 3;
  flow:
    d/dt[theta]  = 10 * (thetaI - theta);  // page 255, (1)
    d/dt[p]      = c1 * (dmAf - dmC);      // page 255, (1)
    d/dt[lambda] = c26 * (dmC / (c25 * fc) - lambda);  // page 257, (10, 11)
    d/dt[pe]     = 0;
    d/dt[i]      = 0;
    d/dt[tau]    = 0;
    d/dt[fc]     = 0;
    d/dt[t]      = 1;
    d/dt[thetaI] = thetaI_amp * 10 * cos(10 * t);
    d/dt[w]      = 5 * 10 * cos(10 * t);
  jump:
    // stay in the power mode
    (t = h) ==>
    @3 (and (theta' = theta)
            (p' = p)
            (lambda' = lambda)
            (thetaI' = thetaI)
            (w' = w)
            (pe' = pe + h * c1 * (c23 * dmAf - mCf(pe)))  // g0, page 258, (12)
            (i' = 0)                                      // g0, page 258, (16)
            (tau' = 0)                                    // g0, page 258, (16)
            (fc' = mCf(pe) / c11P)                        // g0, page 258, (16)
            (t' = 0));

    // goes to the normal mode
    (theta <= 50) ==>
    @2 (and (theta' = theta)
            (p' = p)
            (lambda' = lambda)
            (thetaI' = thetaI)
            (w' = w)
            (pe' = pe)
            (i' = i)
            (tau' = tau)
            (fc' = fc)
            (t' = 0));
}

// Soonho: For now, we ignore sensor_fail mode
//
// // sensor_fail mode
// {mode 4;
//   flow:
//     d/dt[theta]  = 10 * (thetaI - theta);  // page 255, (1)
//     d/dt[p]      = c1 * (dmAf - dmC);      // page 255, (1)
//     d/dt[lambda] = c26 * (dmC / (c25 * fc) - lambda);  // page 257, (10, 11)
//     d/dt[pe]     = 0;
//     d/dt[i]      = 0;
//     d/dt[tau]    = 0;
//     d/dt[fc]     = 0;
//     d/dt[t]      = 1;
//     d/dt[thetaI] = thetaI_amp * 10 * cos(10 * t);
//     d/dt[w]      = 5 * 10 * cos(10 * t);
//   jump:
//     // stay in the sensor_fail mode
//     (t = h) ==>
//     @3 (and (theta' = theta)
//             (p' = p)
//             (lambda' = lambda)
//             (thetaI' = thetaI)
//             (w' = w)
//             (pe' = pe + h * c1 * (c23 * dmAf - mCf(pe)))  // g0, page 258, (16)
//             (i' = 0)                                      // g0, page 258, (16)
//             (tau' = 0)                                    // g0, page 258, (16)
//             (fc' = mCf(pe) / c11)                         // g0, page 258, (16)
//             (t' = 0));
// }

init: @2 (and (theta = 8.8)    // page 257, 3.2 (plant HIOA)
              (p = 0.9833)     // page 257, 3.2 (plant HIOA)
              (lambda = 14.7)  // page 257, 3.2 (plant HIOA)
              (pe = 0)         // page 258. 3.2 (controller HIOA)
              (i = 0)          // page 258, 3.2 (controller HIOA)
              (tau = 0)        // page 258, 3.2 (controller HIOA)
              (fc = 0.6537)    // page 258, 3.2 (controller HIOA)
              (t = 0)
              (w = 110)
              (thetaI = thetaI_init));

goal: @2 (and (t >= 1.5)
              (or (((lambda - c11) / c11) > 0.05)
                  (((lambda - c11) / c11) < -0.05)));