Back -
Formal Specification | Previous - Filing Subsystem | Next - Warehouse Stock ControlTutorial Solutions - Weather Map
Let us suppose basic sets to be -
[AREA,TEMP] |
Then in general -
temp : AREA TEMP |
An example of which may be -
temp == {(b,10),(l,11),(d,11),(c,9),(f,10),(s,9),(h,6),(g,7),(w,8),(o,6)} |
Where the regions are represented by their initial letter.
Source, domain, target, and range are hence - AREA, {b,l,d,c,f,s,h,g,w,o}, TEMP and (6,7,8,9,10,11} respectively.
plus_minus_2deg_12 = {10,11,12,13,14} temp |
south_reg = temp © {b,d} |
outer_reg = temp {w,o} |
temp' = temp Å {(l,13),(s,11)} |
The state schema may be written -
ÚÄWeathermapÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
temp : AREA TEMP
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
dom temp = {b,l,d,c,f,s,h,g,w,o}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ
ÚÄInitWeatherMapÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Weathermap
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
temp = í
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ
It helps to define the set -
Scotland == {b,l,d,c,f,s,h,g,w,o} |
ÚÄUpdateÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Weathermap
reg? : AREA
deg? :
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
reg? î Scotland
temp' = temp
ÚÄLookUpÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Weathermap
reg? : AREA
deg! :
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
reg? î Scotland
reg? deg! î temp
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ
ÚÄRegionUnknownÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Weathermap
reg? : AREA
deg? :
response! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
reg? Ï
Scotland
response! = region_not_in_Scotland
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ
RUpdate Update RegionUnknown
RLookUp LookUp RegionUnknown