-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathPIF.txt
More file actions
134 lines (93 loc) · 4.39 KB
/
Copy pathPIF.txt
File metadata and controls
134 lines (93 loc) · 4.39 KB
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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
//Synchronous PIF self stabilising algorithm for a tree with 5 processes
// Written by Mehran Alidoost Nia on February 05, 2017
dtmc
const double r0=0.5;
const double r1=0.5;
const double r2=0.5;
const double r3=0.5;
const double r4=0.5;
const double q1=0.2;
const bool up1=false;
const bool up4=false;
const bool up0=true;
module process0
x0 : bool ; //state variable
l0 : [-1..4]; //id of process
a0 : bool; //active
p0 : bool; //privilege
//token-2a for root
[] (x0)&((x0=x1 & !up1)|(x0=x2 & !up2)) -> r0:(l0'=1)& (x0'=!x0)+q1:(l0'=2) & (x0'=!x0)+1-r0-q1:(l0'=-1) & (x0'=!x0);
//token-4 and active
[] (!x0)&(x0=x1 &!up1)&(x0=x2 &!up2) &a0 -> (p0'=true)&(l0'=-1) & (x0'=!x0);
//token-4 and not active
[] (!x0)&(x0=x1 &!up1)&(x0=x2 &!up2) &!a0 -> (l0'=-1) & (x0'=!x0);
endmodule
module process1
x1 : bool ; //state variable
l1 : [-1..4]; //id of process
a1 : bool; //active
p1 : bool; //privilege
//[] (x0!=x1)&(!x1)&(!a1) -> (l1'=-1) & (x1'=!x1); //token1 and not active
//[] (x0!=x1)&(!x1)&(a1) -> (l1'=1) & (x1'=!x1); //token1 and active
[] (x0!=x1)&(!x1)-> r1:(l1'=-1) & (x1'=!x1)+ 1-r1: (l1'=1) & (x1'=!x1);
[] (x0!=x1)&(x1)&(l0=1)&(l1=1) -> (p1'=true)&(x1'=!x1);//token3 and id
[] (x0!=x1)&(x1)& ((l0!=1)|(l1!=1)) -> (x1'=!x1);//token3 and not id
endmodule
module process2
x2 : bool ; //state variable
l2 : [-1..4]; //id of process
a2 : bool; //active
p2 : bool; //privilege
up2 : bool ; //up variable
//[] (x0!=x2)&(!x2)&(!a2) -> (l2'=-1) & (up2'=true) & (x2'=!x2); //token1 and not active
//[] (x0!=x2)&(!x2)&(a2) -> (l2'=2) & (up2'=false) & (x2'=!x2); //token1 and active
[] (x0!=x2)&(!x2) -> r2: (l2'=-1) & (up2'=true) & (x2'=!x2)+ 1-r2: (l2'=2) & (up2'=false) & (x2'=!x2);
[] (up2)&(x2)&(x2=x3 & l3!=-1 & up3=false )&(x0=x2) -> (l2'=3) & (up2'=false); //token-2a and parent x
[] (up2)&(x2)&( (x2=x3 & l3=-1 & up3=false)) &(x0=x2) -> (up2'=false); //token-2b
[] (x0!=x2)&(x2)&(l0=2)&(l2=2) -> (p2'=true)&(up2'=false) & (x2'=!x2);//token3 and id
[] (x0!=x2)&(x2)&(l0=2)&((l2=3))-> (up2'=true) & (x2'=!x2); //token 3 and children
[] (x0!=x2)&(x2)&((l0!=2)|((l2!=2)&(l2!=3)))-> (l2'=-1)&(up2'=false) & (x2'=!x2);
[] (up2)&(!x2)&(x2=x3)&(x0=x2) -> (up2'=false) ; //token4
endmodule
module process3
x3 : bool ; //state variable
l3 : [-1..4]; //id of process
a3 : bool; //active
p3 : bool; //privilege
up3 : bool ; //up variable
//[] (x2!=x3)&(!x3)&(!a3) -> (l3'=-1) & (up3'=true) & (x3'=!x3); //token1 and not active
//[] (x2!=x3)&(!x3)&(a3) -> (l3'=3) & (up3'=false) & (x3'=!x3); //token1 and active
[] (x2!=x3)&(!x3) -> r3: (l3'=-1) & (up3'=true) & (x3'=!x3)+ 1-r3: (l3'=3) & (up3'=false) & (x3'=!x3);
[] (up3)&(x3)&(x3=x4 & l4!=-1 & up4=false )&(x2=x3) -> (l3'=4) & (up3'=false); //token-2a and parent x
[] (up3)&(x3)&( (x3=x4 & l4=-1 & up4=false)) &(x2=x3) -> (up3'=false); //token-2b
[] (x2!=x3)&(x3)&(l2=3)&(l3=3) -> (p3'=true)&(up3'=false) & (x3'=!x3);//token3 and id
[] (x2!=x3)&(x3)&(l2=3)&((l3=4))-> (up3'=true) & (x3'=!x3); //token 3 and children
[] (x2!=x3)&(x3)&((l2!=3)|((l3!=3)&(l3!=4)))-> (l3'=-1)&(up3'=false) & (x3'=!x3);
[] (up3)&(!x3)&(x3=x4)&(x2=x3) -> (up3'=false) ; //token4
endmodule
module process4
x4 : bool ; //state variable
l4 : [-1..4]; //id of process
a4 : bool; //active
p4 : bool; //privilege
//[] (x3!=x4)&(!x4)&(!a4) -> (l4'=-1) & (x4'=!x4); //token1 and not active
//[] (x3!=x4)&(!x4)&(a4) -> (l4'=4) & (x4'=!x4); //token1 and active
[] (x3!=x4)&(!x4)-> r4:(l4'=-1) & (x4'=!x4)+ 1-r4: (l4'=4) & (x4'=!x4);
[] (x3!=x4)&(x4)&(l3=4)&(l4=4) -> (p4'=true)&(x4'=!x4);//token3 and id
[] (x3!=x4)&(x4)& ((l3!=4)|(l4!=4)) -> (x4'=!x4);//token3 and not id
endmodule
//test formula
formula f1=(up2&x2&l2=-1&a3)&(up3&x3&l3=-1&a4);
formula f2=(!up2&x2&l0=2)|((!up2&x2&l0=2)&(x3&l2=3))|(!up3&x3&l2=3)|((!up3&x3&l2=3)&(x4&l3=4))|((!up2&x2&l2=-1&!a2)&(x3&l3=-1&!a3))|((!up3&x3&l3=-1&!a3)&(x4&l4=-1&!a4))|(x1&l1=-1&!a1);
formula f3=(x0)&((x0&l0=-1)|(x3&up3&l3=-1)|(x4&up4&l4=-1))&((x1&l0=1)|(x2&l0=2&x0)|(x3&l2=3&x2)|(x4&l3=4&x3));
formula f4=(!x0)&((a2&!a3&l0=2)|(a3&l2=3&l0=2)|(a3&!a4&l2=3)|(a4&l3=4&l2=3)|(a1&l0=1));
formula stability=f4|f3|f2|f1;
// rewards (to calculate expected number of steps)
rewards "steps"
true : 1;
endrewards
init
true
endinit
// label - stable configurations
label "stable" = stability;