Back - Formal Specification | Previous - Filing Subsystem | Next - Warehouse Stock Control

Tutorial 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 Å {reg? deg?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄ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