// ************************************************************************** // // 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 // // ************************************************************************** // The movement of the boat is determined by the velocity induced by the motor // and the water drift. // The landing place is assumed to be reached when the boat has a distance of // delta or smaller from it. In this example delta = 0.1. // // The example has been taken from the following reference: // @phdthesis{Baue12, // key ={Baue12}, // author ={K. Bauer}, // title ={A New Modelling Language for Cyber-physical Systems}, // address ={Kaiserslautern, Germany}, // editor ={K. Schneider and R. Majumdar}, // month ={January}, // school ={Department of Computer Science, University of Kaiserslautern, Germany}, // year ={2012}, // note ={PhD}, // remark ={rsg} // } // ****************************************************************************** module Boat( hybrid real ?motorX, ?motorY, ?waterX, ?waterY, hybrid real boatX, boatY, real ?accuracy, ?landingX, ?landingY, bool landingReached ) { landingReached = false; lBoat, lBoat2:flow{ drv(boatX) <− cont(waterX) + cont(motorX); drv(boatY) <− cont(waterY) + cont(motorY); } until(((cont(boatX) − landingX <= 0.1) and (landingX − cont(boatX)<=0.1)) and ((cont(boatY) − landingY <= 0.1) and (landingY − cont(boatY)<=0.1))); landingReached = true; loop{ arrived: pause; } }