// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// Two trains A,B that are initially dist0 apart are traveling towards each   //
// other along the same track with speeds speedA and speeB. A very fast fly   //
// is hovering just above the nose of train A. It buzzes from train A to train//
// B and turns around immediatly, flies back to train A, and turns around     //
// again. It goes on flying back and forth between the two trains until they  //
// collide. The fly's speed is speedFly miles per hour, and n counts the      //
// number that the fly meets the train A and train B.                         //
//                                                                            //
// The example has been taken from the following reference:                   //
// http://mathforum.org/dr.math/faq/faq.fly.trains.html                       //
// ************************************************************************** //

macro speedA =  60.0;
macro speedB = -90.0;
macro speedF = 120.0;
macro dist0  = 150.0;

module Trainfly(int n) {
    hybrid real posA, posB, posF;
    real dirF;
    // initial values
    posA = 0.0;     // initial x-coordinate of train A
    posB = dist0;   // initial x-coordinate of train B
    posF = 0.0;     // initial x-coordinate of the posFly
    dirF = 1.0;     // fly goes initially in direction of train A
    pause;
    loop{
        flow{
            drv(posA) <- speedA;
            drv(posB) <- speedB;
            drv(posF) <- speedF * dirF;
        } until(cont(posA<=posF | posF>=posB));
        // the fly hit one of the trains
        if(posA < posB) {
            // the trains have still not hit each other,  the fly can fly back
            next(n) = n+1;
            next(dirF) = -dirF;
        }
        pause;
    }
}