CHARON Department of Computer and Information Science
University of Pennsylvania
   
  | | | | | |
 Modular Specification of Hybrid Systems
 Swimming pool example
 

The swimming pool example shows a system composed of two concurrent components: a pump, which maintains the water level in the pool, and a switch, which toggles the sign "swim/don't swim", according to the water level.


Variable swim represents the state of the sign. The agents Pump and Switch have been developed independently and use different variables to represent water level. They are renamed to the same variable level in order for them to interact properly. The water level cannot be observed directly (one has to rely on the sign) and therefore is private to the agent SwimmingPool.


The pump has two states on and off, which maintain a steady rate of change for the water level. In addition, switching between the steady modes takes two units of time, during which the rate of level changes with time. This is implemented by two additional modes turnOff and turnOn and a clock timer.
 
 Text of the example
  

// ------------------------------------------------------------------------
// behavioral hierarchy - modes

// ------------------------------------------------------------------------
// water pump - a hybrid component to control water level


mode Pump( int low, int high ) {
  private analog real timer;
  write analog real y;

  mode on =      SteadyMode( 1, 0, high );
  mode off =     SteadyMode( -2, low, 10000000 );
  mode turnOn =  TransientMode( -2 );
  mode turnOff = TransientMode( 1 );

  diff { d(timer) == 1; }

  trans initTrans  from default to on      when true do { timer = 0; }
  trans requestOff from on      to turnOff when y >= 9.9 do { timer = 0; }
  trans doneOff    from turnOff to off     when timer >= 1.9 do {}
  trans requestOn  from off     to turnOn  when y <= 5.1 do { timer = 0; }
  trans doneOn     from turnOn  to on      when timer >= 1.9 do {}
}

mode SteadyMode( int rate, int low, int high ) {
  write analog real y;

  diff { d(y) == rate; }

  inv s1{ y >= low && y <= high }
}

mode TransientMode( int rate ) {
  write analog real y;
  read analog real timer;

  diff { d(y) == rate*(1-timer/2) }

  inv { timer <= 2 }
}


// ------------------------------------------------------------------------
// switch - a discrete component to highlight the sign


mode Switch( int threshold ) {
  write discrete bool toggle;
  read analog real pos;

  mode on =  empty();
  mode off = empty();

  trans init1 from default to on  when true do { toggle = true; }
  //trans init1 from default to on  when pos <= threshold do { toggle = true; }
  //trans init2 from default to off when pos >= threshold do { toggle = false; }
  trans toOff from on      to off when pos < threshold  do { toggle = false; }
  trans toOn  from off     to on  when pos > threshold  do { toggle = true; }
}

mode empty() { }


// ------------------------------------------------------------------------
// architectural hierarchy - agents

// ------------------------------------------------------------------------
// the pump agent


agent APump( int low, int high ) {
  write analog real y;

  init { y = 1.0; }
  mode top = Pump( low, high );
}


// ------------------------------------------------------------------------
// the switch agent


agent ASwitch( int threshold ) {
  write discrete bool toggle;
  read  analog  real pos;
  
  mode top = Switch( threshold );
}


// ------------------------------------------------------------------------
// the swimming pool with a switch and a pump


agent SwimmingPool() {
  private analog   real level;
  write   discrete bool swim;


  agent pump = APump( 5, 10 ) [ y := level ]
  agent sign = ASwitch( 7 )   [ pos, toggle := level, swim ]
}
Maintained by Valentina Sokolskaya