1 OPTION "produce-models";
4 GeoLocation: TYPE = [# longitude: INT, latitude: INT #];
7 StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
8 Facet: TYPE = [# base: StationaryObject #];
10 Segment: TYPE = [# s_f: Facet #];
11 A : TYPE = ARRAY INT OF Segment;
14 p1: GeoLocation = (# longitude := 0, latitude := 0 #);
16 s1: StationaryObject = (# geoLoc := {p1} #);
19 f0: Facet = (# base := s1 #);
22 init: (A, INT, Facet) -> BOOLEAN
23 = LAMBDA (v: A, i: INT, f: Facet):
27 ASSERT (init(a, 2, f0));