pif/PIF3.txt at master · alidoostnia/pif · GitHub

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
//Synchronous PIF self stabilising algorithm for a tree with 3 processes
// Written by Mehran Alidoost Nia on February 03, 2017

dtmc

const double r0=0.5;
const double r1=0.5;
const double r2=0.5;
const bool up2=false;
const bool up0=true;

module process0

	x0 : bool ; //state variable
	l0 : [-1..2];  //id of process
	a0 : bool; //active
	p0 : bool; //privilege

	//token-2a for root
	[] (x0)&((x0=x1 & !up1))  -> r0:(l0'=1)& (x0'=!x0)+1-r0:(l0'=-1) & (x0'=!x0);

	//token-4 and active
	[] (!x0)&(x0=x1 &!up1)&a0 -> (p0'=true)&(l0'=-1) & (x0'=!x0);

	//token-4 and not active
	[] (!x0)&(x0=x1 &!up1)&!a0 -> (l0'=-1) & (x0'=!x0);

endmodule

module process1

	x1 : bool ; //state variable
	l1 : [-1..2];  //id of process
	a1 : bool; //active
	p1 : bool; //privilege
	up1 : bool ; //up variable

	//[] (x0!=x1)&(!x1)&(!a1) -> (l1'=-1) & (up1'=true) & (x1'=!x1); //token1 and not active
	//[] (x0!=x1)&(!x1)&(a1) -> (l1'=1) & (up1'=false) & (x1'=!x1); //token1 and active
	[] (x0!=x1)&(!x1) -> r1: (l1'=-1) & (up1'=true) & (x1'=!x1)+ 1-r1: (l1'=1) & (up1'=false) & (x1'=!x1);

	[] (up1)&(x1)&(x1=x2  & l2!=-1 & up2=false )&(x0=x1) -> (l1'=2) & (up1'=false); //token-2a and parent x
	[] (up1)&(x1)&( (x1=x2  & l2=-1 & up2=false)) &(x0=x1) -> (up1'=false); //token-2b
	[] (x0!=x1)&(x1)&(l0=1)&(l1=1) -> (p1'=true)&(up1'=false) & (x1'=!x1);//token3 and id
	[] (x0!=x1)&(x1)&(l0=1)&((l1=2))-> (up1'=true) & (x1'=!x1); //token 3 and children
	[] (x0!=x1)&(x1)&((l0!=1)|((l1!=1)&(l1!=2)))-> (l1'=-1)&(up1'=false) & (x1'=!x1);
	[] (up1)&(!x1)&(x1=x2)&(x0=x1) -> (up1'=false) ; //token4

endmodule


module process2

	x2 : bool ; //state variable
	l2 : [-1..2];  //id of process
	a2 : bool; //active
	p2 : bool; //privilege

	//[] (x1!=x2)&(!x2)&(!a2) -> (l2'=-1) & (x2'=!x2); //token1 and not active
	//[] (x1!=x2)&(!x2)&(a2) -> (l2'=2) & (x2'=!x2); //token1 and active
	[] (x1!=x2)&(!x2)-> r2:(l2'=-1) & (x2'=!x2)+ 1-r2: (l2'=2) & (x2'=!x2);
	[] (x1!=x2)&(x2)&(l1=2)&(l2=2) -> (p2'=true)&(x2'=!x2);//token3 and id
	[] (x1!=x2)&(x2)& ((l1!=2)|(l2!=2)) -> (x2'=!x2);//token3 and not id


endmodule


//test formula
formula f1=(up1&x1&l1=-1&a2);
formula f2=(!up1&x1&l0=1)|((!up1&x1&l0=1)&(x2&l1=2))|((!up1&x1&l1=-1&!a1)&(x2&l2=-1&!a2));
formula f3=(x0)&((x0&l0=-1)|(x2&up2&l2=-1))&((x1&l0=1)|(x2&l1=2&x1));
formula f4=(!x0)&((a1&!a2&l0=1)|(a2&l1=2&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;