blob: 8bdbde79ab82a70c47b9055f006025e49d1e20a2 (
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
31
32
33
34
35
36
|
% COMMAND-LINE: --finite-model-find
% EXPECT: sat
DATATYPE
myType = A | B
END;
%%% structured datatypes
myTypeSet: TYPE = SET OF myType;
myTypeGammaSet: TYPE = [# pos: myTypeSet, neg: myTypeSet #];
delta: TYPE = ARRAY myType OF myTypeGammaSet;
labels: TYPE = ARRAY myType OF SET OF STRING;
%%% the empty myTypes set
emptymyTypeSet : SET OF myType;
ASSERT emptymyTypeSet = {} :: SET OF myType;
d: delta;
l: labels;
ASSERT (l[A] = {"L","H"});
ASSERT (l[B] = {"L"});
ic0_i : myTypeSet;
ic0_c : myTypeSet;
ASSERT FORALL (r:myType):
(r IS_IN ic0_i) => FORALL (r2: myType): (r2 IS_IN d[r].neg) => r2 IS_IN ic0_c;
ASSERT {A} <= ic0_i;
ASSERT ((EXISTS (e0 : myType): (e0 IS_IN ic0_i) => (l[A] <= l[e0]))) OR ((ic0_i & ic0_c) <= emptymyTypeSet);
ic1_i : myTypeSet;
ic1_c : myTypeSet;
ASSERT FORALL (r:myType):
(r IS_IN d[B].pos) => r IS_IN ic1_i;
ASSERT ((EXISTS (e1 : myType): (e1 IS_IN ic1_i) => (l[B] <= l[e1]))) OR ((ic1_i & ic1_c) <= emptymyTypeSet);
CHECKSAT;
%COUNTEREXAMPLE;
|
