Congestion Warning System

class CongestionMonitor is subclass of TrafficControl

types
public Signal = <NoWarning>|<PreAnnouncement>|<CongestionWarning>;

instance variables
sensor: CongestionSensor;
nameServer: NameServer;
status: CongestionSensor`CongestionStatus  := <NoCongestion>;
previousstatus: CongestionSensor`CongestionStatus  := <NoCongestion>;
operator: OperatorControl;

operations

public CongestionMonitor: CWS`Location * (inmap CWS`Lane to PassageSensor) *
                          NameServer * OperatorControl ==>
                          CongestionMonitor
CongestionMonitor (loc, sen, ns, op) ==
( location := loc;
  sensor := new CongestionSensor(sen);
  nameServer := ns;
  operator := op;
);

public UpdateCongestionStatus: () ==> ()
UpdateCongestionStatus () ==
( def newstatus = sensor.IssueCongestionStatus () ;
  in
  ( cases mk_(previousstatus, status, newstatus):
      mk_(-, <NoCongestion>, <Congestion>),
      mk_(<NoCongestion>, <Doubt>, <Congestion>) ->
         ( nameServer.GetActuatorManager (location).
             ShowSignal (location, <CongestionWarning>);
          operator.WriteLog ("Congestion occurred at ", location);),
      mk_(-, <Congestion>, <NoCongestion>),
      mk_(<Congestion>, <Doubt>, <NoCongestion>) ->
         ( nameServer.GetActuatorManager (location).
             ShowSignal (location, <NoWarning>);
          operator.WriteLog ("Congestion resolved at ", location);)
       ;
    if not (newstatus = <Doubt> and status = <Doubt>) then
    ( previousstatus := status;
      status := newstatus;
    );
  );
);

end CongestionMonitor

class CongestionSensor is subclass of Sensor

types
public CongestionStatus = <Congestion>|<NoCongestion>|<Doubt>;

instance variables
passageSensors: map CWS`Lane to PassageSensor;

values
NoPassages: nat1 = 4;
CongestionThreshold: nat = 100;
NoCongestionThreshold: nat=  150;

operations

public
CongestionSensor: map CWS`Lane to PassageSensor ==> CongestionSensor
CongestionSensor(sensors) ==
  passageSensors := sensors;

public IssueCongestionStatus:
         () ==> CongestionSensor`CongestionStatus
IssueCongestionStatus() ==
  def averagespeed = min ({passageSensors(lane).
                             AverageSpeed(NoPassages)
                          | lane in set
                            dom passageSensors});
  in
    if averagespeed < CongestionThreshold
    then return <Congestion>
    elseif averagespeed > NoCongestionThreshold
    then return <NoCongestion>
    else return <Doubt>;

functions
min: set of nat -> nat
min(numbers) ==
  let n in set numbers be st
    not exists n2 in set numbers & n2 < n
  in
    n;

end CongestionSensor

class ActuatorManager

instance variables
as: inmap CWS`Location to Actuator := {|->};
ns: NameServer;

operations

public RemoveActuator: Actuator ==> ()
RemoveActuator(actuator) ==
  as := as :-> {actuator};

public ReplaceActuator: Actuator * Actuator ==> ()
ReplaceActuator(actuator, newActuator) ==
  as := as ++ {(inverse as)(actuator) |-> newActuator};

public AddActuator: CWS`Location ==> ()
AddActuator(loc) ==
  def actuator = new Actuator() ;
  in
  ( as := merge { as, { loc |-> actuator } };
    ns.SetLocation(self, loc);
  )
pre loc not in set dom as;

public GetSignal: [CWS`Location] ==>
                  [CongestionMonitor`Signal]
GetSignal(location) ==
  if location = nil or location not in set dom as
  then return nil
  else return as(location).GetSignal();

public ShowSignal: CWS`Location * CongestionMonitor`Signal
                   ==> ()
ShowSignal(location, signal) ==
( def downstreamLocation =
        Downstream(location, ns.GetLocations());
      downstreamManager =
        ns.GetActuatorManager(downstreamLocation);
      downstreamSignal =
        if downstreamManager <> nil
        then downstreamManager.
               GetSignal(downstreamLocation)
        else nil;
      actuator = as(location);
      upstreamLocation = Upstream(location,
                                  ns.GetLocations());
      upstreamManager = ns.GetActuatorManager(
                             upstreamLocation);
      upstreamSignal =
        if upstreamManager <> nil
        then upstreamManager.GetSignal(upstreamLocation)
        else nil;
  in

  ( -- Set the right signal at the current location
    ShowSignalAtLoc(signal,downstreamLocation,
                    downstreamSignal,actuator);

    -- Set the right signal upstream
    ShowSignalUpstream(signal,upstreamLocation,
                       upstreamManager,upstreamSignal);
  ) ;
)
pre location in set dom as;

ShowSignalAtLoc: CongestionMonitor`Signal * [CWS`Location] *
                 CongestionMonitor`Signal * Actuator ==> ()
ShowSignalAtLoc(signal,downstreamLocation,downstreamSignal,actuator) ==
  if signal = <NoWarning> and downstreamLocation <> nil
  then if downstreamSignal = <CongestionWarning>
       then actuator.SetSignal(<PreAnnouncement>)
       else actuator.SetSignal(<NoWarning>)
  else let safest = MostRestrictive(actuator.GetSignal(), signal)
       in
         actuator.SetSignal(safest);

ShowSignalUpstream: CongestionMonitor`Signal * [CWS`Location] *
                    [ActuatorManager] *
                    CongestionMonitor`Signal ==> ()
ShowSignalUpstream(signal,upstreamLocation,upstreamManager,
                   upstreamSignal) ==
  if upstreamLocation <> nil
  then if upstreamSignal <> <CongestionWarning>
       then if signal = <CongestionWarning>
            then upstreamManager.
                   ShowSignal(upstreamLocation,
                              <PreAnnouncement>)
            else upstreamManager.
                   ShowSignal(upstreamLocation,
                              <NoWarning>);

functions
Downstream: CWS`Location * set of CWS`Location ->
            [CWS`Location]
Downstream(loc, locations) ==
  if not exists l in set locations & l > loc
  then nil
  else let l in set locations
         be st l > loc and
         not exists l2 in set locations & l2 < l
       in
         l;

Upstream: CWS`Location * set of CWS`Location ->
          [CWS`Location]
Upstream(loc, locations) ==
  if not exists l in set locations & l < loc
  then nil
  else let l in set locations
         be st l < loc and
         not exists l2 in set locations & l2 > l
       in
         l;


MostRestrictive: CongestionMonitor`Signal * CongestionMonitor`Signal
                 -> CongestionMonitor`Signal
MostRestrictive(s1, s2) ==
  if s1 = <CongestionWarning> or s2 = <CongestionWarning>
  then <CongestionWarning>
  elseif s1 = <PreAnnouncement> or s2 = <PreAnnouncement>
  then <PreAnnouncement>
  else <NoWarning>;

end ActuatorManager

class NameServer

instance variables
am: map ActuatorManager to (set of CWS`Location) := {|->};

operations

public SetActuatorManager: ActuatorManager *
                           set of CWS`Location ==> ()
SetActuatorManager(actuatorManager, locations) ==
  am := am ++ {actuatorManager |-> locations};

public SetLocation: ActuatorManager * CWS`Location ==> ()
SetLocation(actuatorManager, location) ==
  am(actuatorManager) := am(actuatorManager) union {location}
pre actuatorManager in set dom am;

public GetActuatorManager: [CWS`Location] ==> [ActuatorManager]
GetActuatorManager(loc) ==
  if loc = nil
  then return nil
  else let locations = inverse am
       in
         let locationSet in set dom locations be st
             loc in set locationSet
         in
           return locations (locationSet);

public GetLocations: () ==> set of CWS`Location
GetLocations() ==
  return dunion rng am;

end NameServer

class OperatorControl

instance variables
messageLog: map CWS`Location to (seq of (seq1 of char)) := {|->};

operations

public WriteLog: seq1 of char * CWS`Location ==> ()
WriteLog(message, location) ==
  let newMessage = message ^ int2String(location),
      messages = if location in set dom messageLog
                 then messageLog(location) ^
                      [ newMessage ]
                 else [ newMessage ]
  in
    messageLog := messageLog ++ {location |-> messages};

public CongestionSpots: () ==> set of CWS`Location
CongestionSpots() ==
  return dom messageLog;

ConvertLog2File: () ==> seq of char
ConvertLog2File() ==
( dcl messages: seq of (seq1 of char) := [];
  ( for all m in set rng messageLog
    do messages := messages ^ m;
    return conc messages;
  );
);

public ResetLog: () ==> ()
ResetLog() ==
  messageLog := {|->};

functions
int2String: nat1 -> seq1 of char
int2String(n) ==
  is not yet specified;

end OperatorControl

class PassageSensor is subclass of Sensor

instance variables
passages: seq of CWS`Speed := [];
lane: CWS`Lane;

operations

public PassageSensor: CWS`Location * CWS`Lane ==> PassageSensor
PassageSensor (loc, l) ==
( location := loc;
  lane := l;
);

public NewPassage: CWS`Speed ==> ()
NewPassage (speed) ==
passages := [speed] ^ passages;

public AverageSpeed: nat1 ==> CWS`Speed
AverageSpeed (numberofpassages) ==
( dcl accspeed: CWS`Speed := 0 ;
  let passInAccount = passages(1,..., numberofpassages),
      imax = len passInAccount in
  ( for speed in passInAccount do
      accspeed := accspeed + speed;
    return (accspeed/imax);
  );
)
pre len passages >= numberofpassages;

end PassageSensor

class CWS

types
public Speed = nat;
public Location = nat1;
public Lane = nat1;

instance variables
roadNetwork: inmap Location to CongestionMonitor := {|->};
sensors: inmap Location to (inmap Lane to PassageSensor)
       := {|->};
ns: NameServer := new NameServer ();
op: OperatorControl := new OperatorControl ();

operations

public AddSensor: Location * Lane ==> ()
AddSensor(loc, lane) ==
def passageSensor = new PassageSensor(loc, lane);
in
  let sensorAtLane = {lane |-> passageSensor}
  in
    if loc in set dom sensors
    then sensors(loc) := sensors(loc) munion sensorAtLane
    else sensors := sensors munion {loc |-> sensorAtLane};

public AddCongestionMonitor: Location ==> ()
AddCongestionMonitor(loc) ==
let newmon = new CongestionMonitor(loc, sensors (loc),
                                   ns, op)
in
  roadNetwork := roadNetwork munion { loc |-> newmon }
pre loc not in set dom roadNetwork and
    loc in set dom sensors;

end CWS