2 OPTION "produce-models";
5 GeoLocation: TYPE = [# longitude: INT, latitude: INT #];
8 StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
9 Facet: TYPE = [# base: StationaryObject #];
11 Segment: TYPE = [# s_f: Facet #];
12 A : TYPE = ARRAY INT OF Segment;
15 p1: GeoLocation = (# longitude := 0, latitude := 0 #);
17 s1: StationaryObject = (# geoLoc := {p1} #);
20 f0: Facet = (# base := s1 #);
23 init: (A, INT, Facet) -> BOOLEAN
24 = LAMBDA (v: A, i: INT, f: Facet):
28 ASSERT (init(a, 2, f0));