mode eagerState ( real deadline , real latenessFactor , int actorID )
{
  write analog real w_dist , w_attr , w_crowd, w_coord ;
  read discrete real velocity ;
  read discrete bool late ;
  read discrete int startIndex, endIndex , goalIndex ;
  read analog real xPos , yPos ;
  read analog real time ;
  read discrete real endX , endY ;

  diff { d(w_dist) == State.weightDistanceEager ( velocity , late ,
                                                        w_dist ) ;
         d(w_attr) == State.weightAttractiveEager ( velocity ,
                                                          startIndex ,
                                                          endIndex , w_attr ,
                                                          actorID ) ;
         d(w_crowd)== State.weightCrowdEager ( velocity , startIndex ,                                                     endIndex , late ,
                                                     w_crowd ) ; }
  alge { w_coord == 0.0 ; 
        late == (Distance.manhattan( xPos , yPos , endX , endY ) >=
                 deadline - time - latenessFactor) ; }

  inv { Distance.euclidean ( xPos , yPos , endX , endY ) > 0.1 &&
        w_dist >= w_attr } 
}

(A full explanation is beyond the scope of even this supplementary material.) Note that the right-hand sides of the three differential constraints are given by Java functions. As an example, we include one here:

public static double weightAttractiveEager ( double vel , int startCorner ,
                                                 int endCorner ,
                                                 double currentWeight ,
                                                 int actorID )
    {
        double result = vel/city.getDelta()/2 ;

        double attr = city.getAttractiveness ( startCorner , endCorner ,
                                               actorID ) ;
        if ( attr >= 2 )
            result += (attr-2)/8*vel/city.getDelta() - vel/city.getDelta()/2;
        else if ( attr >= -2 )
            result -= vel/city.getDelta()/2 ;
        else
            result += (attr-2)/(-8)*vel/city.getDelta()-vel/city.getDelta()/2;

        double res = saturation ( result , currentWeight ) ;

        if ( currentWeight >= 0 )
            return res ;

        return max ( -currentWeight , res ) ;
    }

In the above, vel refers to the actor's velocity, and getDelta() is the distance between intersections in the city. The nested ifs demonstrate the way in which world attributes (here only attractiveness attr) affect behavior.

Note that saturation is a function that ensures that values do not grossly exceed desired bounds, and we also placed an optional constraint here that an actor's weight on attractiveness should not be less than zero. Our framework is flexible enough to model the behavior of actors who actually favor the less attractive parts of a virtual city, but we did not feel such behavior was appropriate for our simple demonstration.