blob: 75f8de2265adbffb1db989f37054bfff58ebd1d3 (
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type SendState = map<int, seq<int>>
function UnAckedMessages(s:SendState) : set<int>
{
set m,dst | dst in s && m in s[dst] :: m
}
predicate UnAckedMessage2(s:SendState, m:int)
{
exists dst :: dst in s && m in s[dst]
}
/* the following bound can't be determined since we only know what to do with binary operations
function UnAckedMessagesA(s:SendState) : set<int>
{
set m | UnAckedMessage2(s, m) :: m
}
*/
function UnAckedMessagesForDst(s:SendState, dst:int) : set<int>
requires dst in s;
{
set m | m in s[dst] :: m
}
function UnAckedMessages3(s:SendState) : set<int>
{
set m,dst | dst in s && m in UnAckedMessagesForDst(s, dst) :: m
}
function SeqToSet<T>(s:seq<T>) : set<T>
{
set i | i in s
}
/* does not verify, with element may not in domain error
function UnAckedMessages4(s:SendState) : set<int>
{
set m,dst | m in SeqToSet(s[dst]) && dst in s :: m
}
*/
function UnAckedLists(s:SendState) : set<seq<int>>
{
set dst | dst in s :: s[dst]
}
function UnAckedMessages5(s:SendState) : set<int>
{
set m, list | list in UnAckedLists(s) && m in list :: m
}
|