Download all sources:
chapter7.zip
chapter7.zip
class CongestionMonitor is subclass of TrafficControl
instance variables
sensor: CongestionSensor;
actuator: ActuatorManager;
status: CongestionSensor`CongestionStatus;
previousstatus: CongestionSensor`CongestionStatus;
operator: OperatorControl;
types
public Signal = <NoWarning>|<PreAnnouncement>|
<CongestionWarning>;
operations
public CongestionMonitor: CWS`Location * PassageSensor * ActuatorManager *
OperatorControl ==> CongestionMonitor
CongestionMonitor(loc, sen, act, op) ==
( location := loc;
sensor := new CongestionSensor(sen);
actuator := act;
status := <NoCongestion>;
previousstatus := <NoCongestion>;
operator := op;
);
public UpdateCongestionStatus: () ==> ()
UpdateCongestionStatus() ==
( def newstatus = sensor.IssueCongestionStatus ();
in
( cases mk_(previousstatus, status, newstatus):
mk_(-, <NoCongestion>, <Congestion>),
mk_(<NoCongestion>, <Doubt>, <Congestion>) ->
( actuator.ShowSignal(location, <CongestionWarning>);
operator.WriteLog("Congestion occurred at ", location);
),
mk_(-, <Congestion>, <NoCongestion>),
mk_(<Congestion>, <Doubt>, <NoCongestion>) ->
( actuator.ShowSignal(location, <NoWarning>);
operator.WriteLog("Congestion resolved at ", location);)
;
if not (newstatus = <Doubt> and status = <Doubt>)
then
( previousstatus := status;
status := newstatus;
);
);
);
end CongestionMonitorclass ActuatorManager
instance variables
as: seq of Actuator := [];
operations
public ReplaceActuator: CWS`Location ==> ()
ReplaceActuator(loc) ==
def act = new Actuator();
in
as := as ++ {loc |-> act}
pre loc in set inds as;
public AddActuator: CWS`Location ==> ()
AddActuator(loc) ==
def act = new Actuator();
in
as := as(1,...,loc) ^ [act] ^ as(loc+1,..., len as)
pre loc in set inds as;
public ShowSignal: CWS`Location *
CongestionMonitor`Signal ==> ()
ShowSignal(location, signal) ==
( let downstream = as(location + 1),
actuator = as(location),
upstream = as(location - 1)
in
-- Set the right signal at the location itself
( ShowSignalAtLoc(signal,downstream,actuator);
-- Set the right signal upstream
ShowSignalUpstream(signal,upstream);
);
)
pre location in set inds as \ {1, len as } and
signal in set {<NoWarning>, <CongestionWarning>};
ShowSignalAtLoc: CongestionMonitor`Signal * Actuator *
Actuator ==> ()
ShowSignalAtLoc(signal,downstream,actuator) ==
if signal = <NoWarning>
then def downstreamsignal = downstream.GetSignal();
in
if downstreamsignal = <CongestionWarning>
then actuator.SetSignal(<PreAnnouncement>)
else actuator.SetSignal(<NoWarning>)
else def currentsignal = actuator.GetSignal();
in
let safest = MostRestrictive(currentsignal,
signal)
in
actuator.SetSignal(safest);
ShowSignalUpstream: CongestionMonitor`Signal * Actuator ==> ()
ShowSignalUpstream(signal,upstream) ==
def upstreamsignal = upstream.GetSignal ();
in
if upstreamsignal <> <CongestionWarning>
then if signal = <CongestionWarning>
then upstream.SetSignal(<PreAnnouncement>)
else upstream.SetSignal(<NoWarning>);
functions
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 ActuatorManagerclass LoopDetector is subclass of DrivingTimesSensor
values
distanceBetweenLoops: nat1 = 2500;
operations
public CarPassingEvent: nat1 ==> ()
CarPassingEvent(drivingTime) ==
NewPassage(distanceBetweenLoops * drivingTime);
end LoopDetectorclass Actuator
instance variables
signalshown: CongestionMonitor`Signal;
operations
public GetSignal: () ==> CongestionMonitor`Signal
GetSignal() ==
return signalshown;
public SetSignal: CongestionMonitor`Signal ==> ()
SetSignal(signal) ==
signalshown := signal;
end Actuator
class OperatorControl
instance variables
messageLog: seq of seq1 of char := [];
locations : seq of CWS`Location := [];
inv len messageLog = len locations;
operations
public ResetLog: () ==> ()
ResetLog() ==
messageLog := [];
public WriteLog: seq1 of char * CWS`Location ==> ()
WriteLog(message, location) ==
( messageLog := messageLog ^
[ message ^ ConvertNum2String(location) ];
locations := locations ^ [location];
);
public CongestionSpots: () ==> set of CWS`Location
CongestionSpots() ==
return elems locations;
ConvertLog2File: () ==> seq of char
ConvertLog2File() ==
return conc messageLog;
functions
ConvertNum2String: nat1 -> seq1 of char
ConvertNum2String(n) ==
is not yet specified;
end OperatorControlclass TrafficControl
instance variables
protected location: CWS`Location;
end TrafficControl class CWS
types
public Speed = nat;
public Location = nat1;
instance variables
roadNetwork: seq of CongestionMonitor := [];
sensors : seq of PassageSensor := [];
inv len roadNetwork = len sensors;
am: ActuatorManager := new ActuatorManager();
op: OperatorControl := new OperatorControl();
operations
public AddCongestionMonitor: Location ==> ()
AddCongestionMonitor(loc) ==
( def sensor = new PassageSensor(loc);
cm = new CongestionMonitor(loc, sensor, am, op);
in
let numberOfWarners = len roadNetwork
in
atomic( roadNetwork := roadNetwork(1,...,loc) ^
[cm] ^
roadNetwork(loc+1,...,numberOfWarners);
sensors := sensors(1,...,loc) ^ [sensor] ^
sensors(loc+1,...,numberOfWarners);
);
am.AddActuator(loc);
);
end CWSclass Sensor
instance variables
protected location: CWS`Location;
end Sensor class DrivingTimesSensor is subclass of PassageSensor
operations
public CarPassingEvent: nat1 ==> ()
CarPassingEvent(-) ==
is subclass responsibility;
end DrivingTimesSensorclass PassageSensor is subclass of Sensor
instance variables
passages: seq of CWS`Speed := [];
operations
public PassageSensor: CWS`Location ==> PassageSensor
PassageSensor(loc) ==
location := loc;
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)
in
( for speed in passInAccount do
accSpeed := accSpeed + speed;
return (accSpeed/numberOfPassages);
);
)
pre len passages >= numberOfPassages;
end PassageSensor