blob: 7f6f247eed7abe7ef3d9a0dc0348dc083eff68ce (
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
|
% EXPECT: sat
%%%
%%% DATA TYPES DEFINITIONS
%%%
%%% the roles
DATATYPE
role = r1 | r2 | r3
%%% adding two more roles ( | r4 | r5 ) to the type, but never referring to them make things work
END;
%%% structured datatypes
roleSet: TYPE = SET OF role;
roleGammaSet: TYPE = [# pos: roleSet, neg: roleSet #];
delta: TYPE = ARRAY role OF roleGammaSet;
emptyRoleSet : roleSet;
ASSERT emptyRoleSet = {} :: SET OF role;
d: delta;
ASSERT d[r3].pos = {r1};
ASSERT d[r2].pos = {r2,r3};
ASSERT d[r2].neg = {r1};
CHECKSAT;
%COUNTEREXAMPLE;
|