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
|
% COMMAND-LINE: --finite-model-find -i
% EXPECT: not_entailed
% EXPECT: entailed
prin:TYPE;
form:TYPE;
signed:(prin,form)->BOOLEAN;
says:(prin,form)->BOOLEAN;
speaksfor:(prin,prin)->form;
signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y);
saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z);
ASSERT(signedE);
ASSERT(saysE);
julie:prin;
dave:prin;
alice:prin;
openfile:form;
x2:BOOLEAN = signed(alice,openfile);
ASSERT(x2);
x3:BOOLEAN = signed(dave,speaksfor(alice,dave));
ASSERT(x3);
QUERY NOT says(dave,openfile); % this is invalid
QUERY says(dave,openfile); % this is valid
|
