src/Game/Football.dcl

   1 definition module Football
   2
   3 /**     The Football data type and a number of access functions.
   4 */
   5
   6 import Footballer, randomstream
   7
   8 ::      FootballState   = Free     !Football
   9                                         | GainedBy !FootballerID
  10 ::      Football                = { ballPos             :: !Position3D
  11                                           , ballSpeed   :: !Speed3D
  12                                           }
  13 ::      BounceDirection = Down | Up | Forward | Back
  14
  15 instance zero         Football
  16 instance toPosition   Football
  17 instance toPosition3D Football
  18
  19 /*      mkFootball returns a football with 3D dimensions.
  20 */
  21 mkFootball                      :: !Position !Speed -> Football
  22
  23 /*      ballIsFree yields True iff argument is (Free ...).
  24 */
  25 ballIsFree                      :: !FootballState -> Bool
  26
  27 /*      ballIsGainedBy yields True iff the ball is in possession by the given player.
  28 */
  29 ballIsGainedBy          :: !FootballerID !FootballState -> Bool
  30
  31 /*      getFootball returns the football (containing its position and speed-information)
  32         that is either free or gained by a footballer.
  33         For this reason, the list of footballers must contain all footballers, otherwise
  34         this function may fail.
  35 */
  36 getFootball                     :: !FootballState !.[Footballer] -> Football
  37
  38 radius_football         :== m 0.113                                     // radius of football
  39 surface_resistance      :== 0.85                                        // maximum speed of ball when moving over surface
  40 air_resistance          :== 0.95                                        // maximum speed of ball when moving through air (should depend on velocity)
  41 accelleration_sec       :== ms 9.81                                     // acceleration difference per square second