-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTOR.ucl
106 lines (96 loc) · 2.78 KB
/
TOR.ucl
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
module main
{
type packet_t = record {
source : integer,
d1 : integer,
d2 : integer,
d3 : integer,
destination : integer,
stage : integer
};
define valid_stage(s : integer) : boolean =
(s >= 1 && s <= 5);
define valid_packet(p : packet_t) : boolean =
p.source != p.d1 && p.source != p.d2 && p.source != p.d3 && p.source != p.destination &&
p.d1 != p.d2 && p.d1 != p.d3 && p.d1 != p.destination &&
p.d2 != p.d3 && p.d2 != p.destination &&
p.d3 != p.destination ;
var total_routers : integer;
var packets : [integer]packet_t;
const num_packets : integer = 4;
var iteration , previous_location , current_location , next_location , current_stage , packet_number: integer;
procedure move_packet(i : integer)
returns (previous_location ,current_location , next_location ,
current_stage : integer)
modifies packets;
{
var p : packet_t;
p = packets[i];
current_stage = p.stage + 1;
p.stage = p.stage + 1 ;
if (current_stage == 6){current_stage = 1;p.stage = 1;}
packets[i] = p;
case
(p.stage == 1) : {
previous_location = -1;
current_location = p.source;
next_location = p.d1;
}
(p.stage == 2) : {
previous_location = p.source;
current_location = p.d1;
next_location = p.d2;
}
(p.stage == 3) : {
previous_location = p.d1;
current_location = p.d2;
next_location = p.d3;
}
(p.stage == 4) : {
previous_location = p.d2;
current_location = p.d3;
next_location = p.destination;
}
(p.stage == 5) : {
previous_location = p.d3;
current_location = p.destination;
next_location = -1;
}
esac
}
init {
iteration = 0;
for (i : integer) in range(0, num_packets) {
var p : packet_t;
p = packets[i];
p.stage = 0;
total_routers = 10;
//assume valid_stage(packets[i]);
assume valid_packet(packets[i]);
assume (p.source >= 1 && p.source <= total_routers );
assume (p.d1 >= 1 && p.d1 <= total_routers );
assume (p.d2 >= 1 && p.d2 <= total_routers );
assume (p.d3 >= 1 && p.d3 <= total_routers );
assume (p.destination >= 1 && p.destination <= total_routers );
packets[i] = p;
}
}
next {
var p : packet_t;
p = packets[iteration];
packet_number' = iteration+1;
call( previous_location' , current_location' , next_location' , current_stage') =
move_packet(iteration);
iteration' = if(iteration == 4) then 1 else iteration + 1;
}
invariant always_false: false;
control {
v = unroll(20);
check;
print_results;
v.print_cex(
packet_number ,previous_location, current_location, next_location,
current_stage
);
}
}