blob: 1ccf7fa9e102b31ca678102f2a2bf5544f950b2d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
% EXPECT: sat
OPTION "produce-models";
% GeoLocation
GeoLocation: TYPE = [# longitude: INT, latitude: INT #];
% Stationary object
StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
Facet: TYPE = [# base: StationaryObject #];
Segment: TYPE = [# s_f: Facet #];
A : TYPE = ARRAY INT OF Segment;
a : A;
p1: GeoLocation = (# longitude := 0, latitude := 0 #);
s1: StationaryObject = (# geoLoc := {p1} #);
f0: Facet = (# base := s1 #);
init: (A, INT, Facet) -> BOOLEAN
= LAMBDA (v: A, i: INT, f: Facet):
v[0].s_f = f;
ASSERT (init(a, 2, f0));
CHECKSAT TRUE;
|