Download all sources:
chapter10.zip
chapter10.zip
class OnBoardComp
types
public AlarmLevel = <SpeedOk> | <AlarmSpeed> | <EmergencyBreakSpeed>;
values
alarmSpeedAdd = 5;
emergencySpeedAdd = 10;
functions
public CheckSpeed: real * real -> AlarmLevel
CheckSpeed(speed, maxSpeed) ==
if speed < maxSpeed + alarmSpeedAdd
then <SpeedOk>
elseif speed < maxSpeed + emergencySpeedAdd
then <AlarmSpeed>
else <EmergencyBreakSpeed>;
end OnBoardComp
class CSL
instance variables
cabDisplay : CabDisplay := new CabDisplay();
emergencyBrake: EmergencyBrake := new EmergencyBrake();
onboardComp : OnBoardComp := new OnBoardComp();
announcements : seq of AnnounceBeacon := [];
speedRestrictions: seq of LimitBeacon := [];
inv len speedRestrictions <= 5;
firstSpeedRestriction: bool := true;
driverCard: [DriverCard] := nil;
faults : set of Fault := {};
values
maxSpeed: real = 180;
operations
public HeadMeetsBeacon: Beacon ==> ()
HeadMeetsBeacon(beacon) ==
cases true:
(isofclass(AnnounceBeacon, beacon)) ->
AnnounceSpeedRestriction(beacon),
(isofclass(LimitBeacon, beacon)) ->
AddSpeedRestriction(beacon),
(isofclass(CancelBeacon, beacon)) ->
DeleteAnnouncements()
pre isofclass(LimitBeacon, beacon) =>
NotEmpty[AnnounceBeacon](announcements);
public TailMeetsBeacon: Beacon ==> ()
TailMeetsBeacon(beacon) ==
cases true:
(isofclass(LimitBeacon, beacon)) ->
if not firstSpeedRestriction
then RemoveSpeedRestriction()
else firstSpeedRestriction := false,
(isofclass(EndBeacon, beacon)) ->
( firstSpeedRestriction := true;
RemoveSpeedRestriction ();)
pre ((isofclass(LimitBeacon, beacon) and
not firstSpeedRestriction) or
isofclass(EndBeacon, beacon)) =>
NotEmpty[LimitBeacon](speedRestrictions);
public AnnounceSpeedRestriction: AnnounceBeacon ==> ()
AnnounceSpeedRestriction(annobea) ==
( announcements := announcements ^ [annobea];
DeletePossibleGroundFault(); );
public AddSpeedRestriction: LimitBeacon ==> ()
AddSpeedRestriction(limitbea) ==
if len speedRestrictions < 5
then ( let speed = (hd announcements).GetTargetSpeed()
in
limitbea.SetSpeedRestriction(speed);
speedRestrictions := speedRestrictions ^ [limitbea];
announcements := tl announcements;
DeletePossibleGroundFault();
)
else RaiseGroundFault()
pre NotEmpty[AnnounceBeacon](announcements);
public DeleteAnnouncements: () ==> ()
DeleteAnnouncements() ==
( announcements := [];
DeletePossibleGroundFault();
);
public RemoveSpeedRestriction: () ==> ()
RemoveSpeedRestriction() ==
( speedRestrictions := tl speedRestrictions;
DeletePossibleGroundFault();
)
pre NotEmpty[LimitBeacon](speedRestrictions);
public RaiseGroundFault: () ==> ()
RaiseGroundFault() ==
cabDisplay.SetGroundFault();
public DeletePossibleGroundFault: () ==> ()
DeletePossibleGroundFault() ==
let mk_(-,-,gf) = cabDisplay.GetDisplay()
in
if gf
then cabDisplay.UnsetGroundFault();
public NoBeaconMet: () ==> ()
NoBeaconMet() ==
( announcements := tl announcements;
RaiseGroundFault();
)
pre NotEmpty[AnnounceBeacon](announcements);
public CheckSpeed: real ==> ()
CheckSpeed(speed) ==
let speedAlarm = onboardComp.CheckSpeed (speed, GetMaxSpeed())
in
cases speedAlarm:
<SpeedOk> -> if not emergencyBrake.GetEmergencyBrake()
then cabDisplay.UnsetAlarm(),
<AlarmSpeed> -> if not emergencyBrake.GetEmergencyBrake()
then cabDisplay.SetAlarm(),
<EmergencyBreakSpeed> -> ( cabDisplay.SetEmergencyBrake();
emergencyBrake.SetEmergencyBrake();
)
;
public GetMaxSpeed: () ==> real
GetMaxSpeed() ==
if speedRestrictions <> []
then let speeds = { limit.GetSpeedRestriction()
| limit in set elems speedRestrictions } in
let minspeed in set speeds be st forall sp in set speeds &
minspeed <= sp in
return minspeed
else return maxSpeed;
public ReleaseEmergencyBrake: real ==> ()
ReleaseEmergencyBrake(sp) ==
if sp = 0
then ( cabDisplay.UnsetEmergencyBrake();
emergencyBrake.UnsetEmergencyBrake();
)
pre let mk_(-,eb,-) = cabDisplay.GetDisplay() in eb and
emergencyBrake.GetEmergencyBrake();
public GetCabDisplay: () ==> CabDisplay
GetCabDisplay() ==
return cabDisplay;
public GetEmergencyBrake: () ==> EmergencyBrake
GetEmergencyBrake() ==
return emergencyBrake;
public GetAnnouncements: () ==> seq of AnnounceBeacon
GetAnnouncements() ==
return announcements;
public GetSpeedRestrictions: () ==> seq of LimitBeacon
GetSpeedRestrictions() ==
return speedRestrictions;
public GetFaults: () ==> set of Fault
GetFaults() ==
return faults;
functions
NotEmpty[@T]: seq of @T -> bool
NotEmpty(list) ==
list <> [];
BeaconsAnnounced: seq of Beacon -> bool
BeaconsAnnounced(beaL) ==
forall i in set inds beaL &
let sub = beaL(1,...,i)
in
NumOfBeacon(sub,<ANNOUNCE>) >= NumOfBeacon(sub,<LIMIT>);
NumOfBeacon: seq of Beacon * (<ANNOUNCE> | <LIMIT>) -> nat
NumOfBeacon(beaL,kind) ==
let realbeaL = FilterCancelEnd(beaL)
in
card {i | i in set inds realbeaL
& if kind = <ANNOUNCE>
then isofclass(AnnounceBeacon, realbeaL(i))
else isofclass(LimitBeacon, realbeaL(i))};
FilterCancelEnd: seq of Beacon -> seq of Beacon
FilterCancelEnd(beaL) ==
if exists bea in set elems beaL & CancelOrEnd(bea)
then let maxi in set inds beaL be st
CancelOrEnd(beaL(maxi)) and
forall j in set inds beaL &
j > maxi => not CancelOrEnd(beaL(j))
in
beaL(maxi+1,...,len beaL)
else beaL;
CancelOrEnd: Beacon -> bool
CancelOrEnd(bea) ==
isofclass(CancelBeacon, bea) or isofclass(EndBeacon, bea);
Max5SpeedLimits: seq of Beacon -> bool
Max5SpeedLimits(beaL) ==
forall i in set inds beaL & NumOfBeacon(beaL(1,...,i),<LIMIT>) <= 5;
end CSL
class CheckSpeedEvent is subclass of Event
instance variables
speed : real;
operations
public CheckSpeedEvent: real ==> CheckSpeedEvent
CheckSpeedEvent(s) ==
speed := s;
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
( csl.CheckSpeed(speed);
let mk_(a,e,g) = csl.GetCabDisplay().GetDisplay(),
e' = csl.GetEmergencyBrake().GetEmergencyBrake()
in
return mk_Test`CSLstate(mk_Test`CabDisp(a,e,g),
mk_Test`EmerBrake(e'));
);
end CheckSpeedEvent class EndBeacon is subclass of Beacon
end EndBeacon
class Event
operations
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
is subclass responsibility;
end Event
class CancelBeacon is subclass of Beacon
end CancelBeacon
class NoBeaconMetEvent is subclass of Event
operations
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
( csl.NoBeaconMet();
let mk_(a,e,g) = csl.GetCabDisplay().GetDisplay(),
e' = csl.GetEmergencyBrake().GetEmergencyBrake()
in
return mk_Test`CSLstate(mk_Test`CabDisp(a,e,g),
mk_Test`EmerBrake(e'));
);
end NoBeaconMetEvent
class MaxSpeedEvent is subclass of Event
operations
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
( let ms = csl.GetMaxSpeed()
in
return mk_Test`MaxSpeed(ms);
);
end MaxSpeedEvent
class Supervisor
instance variables
instance variables
driverInfo: map DriverCard to Driver := {|->};
trainInfo : map TrainId to CSL := {|->};
types
public TrainId = token;
operations
public
Supervisor: map DriverCard to Driver * map TrainId to CSL ==>
Supervisor
Supervisor(drive,train) ==
(driverInfo := drive;
trainInfo := train;);
public
CardReturn: TrainId * DriverCard ==> ()
CardReturn(trainid,driverid) ==
let newfaults = trainInfo(trainid).GetFaults()
in
driverInfo(driverid).AddFaults(newfaults)
pre trainid in set dom trainInfo and driverid in set dom driverInfo;
end Supervisor
class EmergencyBrake
instance variables
emergencybrake: bool := false;
operations
public SetEmergencyBrake: () ==> ()
SetEmergencyBrake() ==
emergencybrake := true;
public UnsetEmergencyBrake: () ==> ()
UnsetEmergencyBrake() ==
emergencybrake := false;
public GetEmergencyBrake: () ==> bool
GetEmergencyBrake() ==
return emergencybrake;
end EmergencyBrake
class CabDisplay
instance variables
instance variables
alarm : bool := false;
emergencyBrake: bool := false;
groundFault : bool := false;
operations
public SetAlarm: () ==> ()
SetAlarm() ==
alarm := true
pre not emergencyBrake and not groundFault;
public UnsetAlarm: () ==> ()
UnsetAlarm() ==
alarm := false;
public SetEmergencyBrake: () ==> ()
SetEmergencyBrake() ==
( alarm := false;
emergencyBrake := true ;);
public UnsetEmergencyBrake: () ==> ()
UnsetEmergencyBrake() ==
emergencyBrake := false;
public SetGroundFault: () ==> ()
SetGroundFault() ==
groundFault := true;
public UnsetGroundFault: () ==> ()
UnsetGroundFault() ==
groundFault := false;
public GetDisplay: () ==> bool * bool * bool
GetDisplay() ==
return mk_(alarm, emergencyBrake, groundFault);
end CabDisplay
class Fault
instance variables
speedlimit : real;
actualspeed : real;
operations
public Fault: real * real ==> Fault
Fault(max,act) ==
( speedlimit := max;
actualspeed := act;
);
end Fault class Test
types
public TestResult = CSLstate | BeaconsMet | MaxSpeed;
public CSLstate :: cd : CabDisp
eb : EmerBrake;
public CabDisp :: alarm : bool
emerbr : bool
grfault : bool;
public EmerBrake :: break : bool;
public BeaconsMet :: ann : seq of Announce
res : seq of Limit;
public Announce :: ts : real;
public Limit :: sp : real;
public MaxSpeed :: ms: real;
instance variables
csl : CSL := new CSL();
operations
public RunTests: seq of Event ==> seq of TestResult
RunTests(events) ==
return [events(i).Execute(csl) | i in set inds events ];
public RunOneTest: Event ==> TestResult
RunOneTest(event) ==
return event.Execute(csl);
end Test class AnnounceBeacon is subclass of Beacon
instance variables
targetspeed: real;
operations
public AnnounceBeacon: real ==> AnnounceBeacon
AnnounceBeacon(ts) ==
targetspeed := ts;
public GetTargetSpeed : () ==> real
GetTargetSpeed() ==
return targetspeed;
end AnnounceBeacon
class Driver
instance variables
faults: set of Fault := {};
types
public DriverId = token;
operations
public AddFaults: set of Fault ==> ()
AddFaults(newfaults) ==
faults := faults union newfaults;
public GetFaults: () ==> set of Fault
GetFaults() ==
return faults;
end Driver
class HeadMeetBeaconEvent is subclass of Event
instance variables
beacon : Beacon;
operations
public HeadMeetBeaconEvent: Beacon ==> HeadMeetBeaconEvent
HeadMeetBeaconEvent(b) ==
beacon := b;
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
( csl.HeadMeetsBeacon(beacon);
let anns = csl.GetAnnouncements(),
restr = csl.GetSpeedRestrictions()
in
return mk_Test`BeaconsMet(
[ mk_Test`Announce(anns(i).GetTargetSpeed()) |
i in set inds anns ],
[ mk_Test`Limit(restr(i).GetSpeedRestriction()) |
i in set inds restr ]); );
end HeadMeetBeaconEvent
class DriverCard
instance variables
id: DriverId;
types
public DriverId = token;
operations
public SetId: DriverId ==> ()
SetId(newid) ==
id := newid;
public GetId: () ==> DriverId
GetId() ==
return id;
end DriverCard
class TailMeetBeaconEvent is subclass of Event
instance variables
beacon : Beacon;
operations
public
TailMeetBeaconEvent: Beacon ==> TailMeetBeaconEvent
TailMeetBeaconEvent(b) ==
beacon := b;
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
( csl.TailMeetsBeacon(beacon);
let anns = csl.GetAnnouncements(),
restr = csl.GetSpeedRestrictions()
in
return mk_Test`BeaconsMet(
[ mk_Test`Announce(anns(i).GetTargetSpeed()) |
i in set inds anns ],
[ mk_Test`Limit(restr(i).GetSpeedRestriction()) |
i in set inds restr ]); );
end TailMeetBeaconEventclass LimitBeacon is subclass of Beacon
instance variables
speed: [real] := nil;
operations
public SetSpeedRestriction: real ==> ()
SetSpeedRestriction(s) ==
speed := s;
public GetSpeedRestriction: () ==> real
GetSpeedRestriction() ==
return speed
pre speed <> nil;
end LimitBeacon
class Beacon
end Beacon
class CSLStateEvent is subclass of Event
operations
public Execute: CSL ==> Test`TestResult
Execute(csl) ==
let mk_(a,e,g) = csl.GetCabDisplay().GetDisplay(),
e' = csl.GetEmergencyBrake().GetEmergencyBrake()
in
return mk_Test`CSLstate(mk_Test`CabDisp(a,e,g),
mk_Test`EmerBrake(e'));
end CSLStateEvent