types 

Map = set of Path
inv x == forall y in set x & inv_Path(y);

Path :: From: Location
        Info: PathInfo
        To: Location
inv x == x.Info.distance >= dist(x.From.coord, x.To.coord);

Location :: name: seq of char
            coord: Coord;

PathInfo   ::   id: seq of char
                distance: real
                speed: real;

Coord :: lat: real
         lon: real 

values

coord_covas = mk_Coord(234, 100);
covas = mk_Location("Covas", coord_covas);

coord_vilar = mk_Coord(239, 105);
vilar = mk_Location("Vilar", coord_vilar);

path_info1 = mk_PathInfo("CM203", 12, 35);

path1 = mk_Path(vilar, path_info1, covas);

m1 = { path1 }


functions

f: Map -> set of seq of char
f(m) == dunion { { p.From.name , p.To.name} | p in set m };

dist: Coord * Coord -> real
dist(c1, c2) == sqrt( (c1.lat - c2.lat)*(c1.lat - c2.lat) +
                      (c1.lon - c2.lon)*(c1.lon - c2.lon) ) 

types

UMap = set of UPath
inv x == forall y in set x & inv_UPath(y);

UPath :: From: ULocation
         Info: UPathInfo
         To: ULocation
inv x == x.Info.distance >= Udist(x.From.coord, x.To.coord);

ULocation :: name: seq of char
             coord: UCoord;

UPathInfo :: id: seq of char
             distance: real
             speed: real;

UCoord :: lat: real
          lon: real
          mapi: MapInfo;

MapInfo :: lat: nat
           lon: nat

values

map_info_covas = mk_MapInfo(0,0);
Ucoord_covas = mk_UCoord(234, 100, map_info_covas);
Ucovas = mk_ULocation("Covas", Ucoord_covas);

map_info_vilar = mk_MapInfo(1,0);
Ucoord_vilar = mk_UCoord(4, 105, map_info_vilar);
Uvilar = mk_ULocation("Vilar", Ucoord_vilar);

Upath_info1 = mk_UPathInfo("CM203", 12, 35);

Upath1 = mk_UPath(Uvilar, Upath_info1, Ucovas);

Um1 = { Upath1 }

functions

Uf : UMap -> set of seq of char
Uf (m) == dunion { {p.From.name, p.To.name} | p in set m };


Udist : UCoord * UCoord -> real
Udist (c1, c2) == let ct1 = c1.lat + c1.mapi.lat * 235,
                      cl1 = c1.lon + c1.mapi.lon * 235,
                      ct2 = c2.lat + c2.mapi.lat * 235,
                      cl2 = c2.lon + c2.mapi.lon * 235,
                      ct = ct1 - ct2,
                      cl = cl1 - cl2
                  in sqrt( ct*ct + cl*cl )