types 

Map = set of Path;

Path :: From: Location
        To: Location;

Location = token

values

guimaraes = mk_token("Guimaraes");
braga = mk_token("Braga");
porto = mk_token("Porto");
taipas = mk_token("Taipas");
melgaco = mk_token("Melgaco");

m1 = { mk_Path(guimaraes, taipas), mk_Path(taipas, braga), mk_Path(braga, porto), 
        mk_Path(porto, melgaco), mk_Path(taipas, guimaraes), mk_Path(melgaco, melgaco)};

m2 = { mk_Path(taipas, braga), mk_Path(guimaraes, taipas) };

m3 = { mk_Path(braga, melgaco), mk_Path(melgaco, porto) }

functions

symmetric: Map -> Map
symmetric(m) == { mk_Path(y,x) | mk_Path(x,y) in set m};

symmetric_closure: Map -> Map
symmetric_closure(m) == m union symmetric(m);

composition: Map * Map -> Map
composition(m1, m2) == { mk_Path(x,y) | mk_Path(x,z) in set m1, 
mk_Path(w,y) in set m2 & z = w};

reflection: Map -> Map
reflection(m) == 
        { mk_Path(x,x) | x in set ({ y | mk_Path(y,-) in set m } 
                              union { y | mk_Path(-,y) in set m})};

transitive_closure: Map -> Map
transitive_closure(m) == t_clos_aux(m, m);

t_clos_aux: Map * Map -> Map
t_clos_aux(m, mtr)  == 
        let compost = mtr union composition(mtr, m) 
        in 
                if mtr = compost 
                then mtr
                else t_clos_aux(m, compost)

types 

UMap = set of UPath;

UPath :: From: Location
         Info: PathInfo
         To: Location;

PathInfo :: name: seq of char 
            distance: real
            speed: real


values

inf1 = mk_PathInfo("G-T", 7.5, 50);
inf2 = mk_PathInfo("T-B", 15, 50);
inf3 = mk_PathInfo("B-P", 40, 60);
inf4 = mk_PathInfo("P-M", 100, 70);
inf5 = mk_PathInfo("T-G", 7.5, 40);
inf6 = mk_PathInfo("M-M", 1, 50);
inf7 = mk_PathInfo("B-M", 90, 80);
inf8 = mk_PathInfo("M-P", 100, 60);

mu1 = { mk_UPath(guimaraes, inf1, taipas), mk_UPath(taipas, inf2, braga),
 mk_UPath(braga, inf3, porto), mk_UPath(porto, inf4, melgaco), 
mk_UPath(taipas, inf5, guimaraes), mk_UPath(melgaco, inf6, melgaco)};

mu2 = { mk_UPath(taipas, inf2, braga), mk_UPath(guimaraes, inf1,taipas) };

mu3 = { mk_UPath(braga, inf7, melgaco), mk_UPath(melgaco, inf8, porto) }

functions

Usymmetric : UMap -> UMap
Usymmetric (m) == { mk_UPath(x, i, y) | mk_UPath(y, i, x) in set m };

Usymmetric_closure : UMap -> UMap
Usymmetric_closure (m) == m union Usymmetric (m);

Ucomposition : UMap * UMap -> UMap
Ucomposition (m1, m2) == { mk_UPath(x, pi(i1,i2), y) | mk_UPath(x, i1, z) 
        in set m1, mk_UPath(w, i2, y) in set m2 & z = w };

pi : PathInfo * PathInfo -> PathInfo
pi (p1, p2) == mk_PathInfo(p1.name ^['/']^ p2.name,
                           p1.distance + p2.distance,
                           speed_calc(p1,p2));

speed_calc : PathInfo * PathInfo -> real
speed_calc (p1, p2) ==  (p1.distance + p2.distance) /
                        (p1.distance / p1.speed + p2.distance / p2.speed);

Ureflection : UMap -> UMap
Ureflection (m) == 
        { mk_UPath(x,mk_PathInfo("", 0, 0),x) 
                | x in set ({ y | mk_UPath(y,-,-) in set m}
                       union { y | mk_UPath(-,-,y) in set m}) };


Utransitive_closure : UMap -> UMap
Utransitive_closure (m) == Ut_clos_aux(m, m);

Ut_clos_aux: UMap * UMap -> UMap
Ut_clos_aux(m, mtr)  == 
        let compost = mtr union Ucomposition(mtr, m) 
        in 
                if mtr = compost 
                then mtr
                else Ut_clos_aux(m, compost)