[lttv.git] / trunk / verif / Spin / Test / mobile2

/*
 * Simplified model of cell-phone handoff strategy in a mobile network.
 * A translation from the pi-calculus description of this
 * model presented in:
 * Fredrik Orava and Joachim Parrow, 'An algebraic verification
 * of a mobile network,' Formal aspects of computing, 4:497-543 (1992).
 * For more information on this model, email: joachim@it.kth.se
 *
 * This version exploits some Promela features to reduce the number
 * of processes -- which looks better in simulations, and reduces
 * complexity (by about 60%) in verification.
 *
 * See also the more literal version of this model in mobile1.
 *
 * The ltl property definition for this version is in mobile2.ltl
 *
 * to perform the verification with xspin, simply use the ltl property
 * manager, which will load the above .ltl file by default.
 * to perform the verificaion from a Unix command line, type:
 * 	$ spin -a -N mobile2.ltl mobile2
 * 	$ cc -o pan pan.c
 * 	$ pan -a
 */

mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };

chan in  = [1] of { mtype };
chan out = [1] of { mtype };
chan fa  = [0] of { chan };
chan fp  = [0] of { chan };
chan m1  = [0] of { chan };
chan m2  = [0] of { chan };
chan l   = [0] of { chan };

byte a_id, p_id;	/* ids of processes refered to in the property */

proctype CC()	/* communication controller */
{	chan  m_old, m_new, x;
	mtype v;

	do
	:: in?v ->
		printf("MSC: DATA\n");
		fa!data; fa!v
	:: l?m_new ->
		fa!ho_cmd; fa!m_new;
		printf("MSC: HAND-OFF\n");
		if
		:: fp?ho_com ->
			printf("MSC: CH_REL\n");
			fa!ch_rel; fa?m_old;
			l!m_old;
			x = fa; fa = fp; fp = x
		:: fa?ho_fail ->
			printf("MSC: FAIL\n");
			l!m_new
		fi
	od
}

proctype HC(chan m)	/* handover controller */
{
	do
	:: l!m; l?m
	od
}

proctype BS(chan f, m; bit how)	/* base station */
{	chan v;

	if
	:: how -> goto Active
	:: else -> goto Passive
	fi;

Active:
	printf("MSC: ACTIVE\n");
	do
	:: f?data -> f?v; m!data; m!v
	:: f?ho_cmd ->	/* handover command */
progress:	f?v; m!ho_cmd; m!v;
		if
		:: f?ch_rel ->
			f!m;
			goto Passive
		:: m?ho_fail ->
			printf("MSC: FAILURE\n");
			f!ho_fail
		fi
	od;

Passive:
	printf("MSC: PASSIVE\n");
	m?ho_acc -> f!ho_com;
	goto Active
}

proctype MS(chan m)	/* mobile station */
{	chan m_new;
	mtype v;

	do
	:: m?data -> m?v; out!v
	:: m?ho_cmd; m?m_new;
		if
		:: m_new!ho_acc; m = m_new
		:: m!ho_fail
		fi
	od
}

active proctype System()
{
	atomic {
		run HC(m1);
		run CC();
		p_id = run BS(fp, m1, 0);	/* passive base station */
		a_id = run BS(fa, m2, 1);	/* active base station */
		run MS(m2)
	}

end:	do
	:: in!red; in!white; in!blue
	od
}

active proctype Out()
{
end:	do	/* deadlocks if order is disturbed */
	:: out?red; out?white; out?blue
	od
}
Commit	Line	Data
0b55f123	1	/*
	2	* Simplified model of cell-phone handoff strategy in a mobile network.
	3	* A translation from the pi-calculus description of this
	4	* model presented in:
	5	* Fredrik Orava and Joachim Parrow, 'An algebraic verification
	6	* of a mobile network,' Formal aspects of computing, 4:497-543 (1992).
	7	* For more information on this model, email: joachim@it.kth.se
	8	*
	9	* This version exploits some Promela features to reduce the number
	10	* of processes -- which looks better in simulations, and reduces
	11	* complexity (by about 60%) in verification.
	12	*
	13	* See also the more literal version of this model in mobile1.
	14	*
	15	* The ltl property definition for this version is in mobile2.ltl
	16	*
	17	* to perform the verification with xspin, simply use the ltl property
	18	* manager, which will load the above .ltl file by default.
	19	* to perform the verificaion from a Unix command line, type:
	20	* $ spin -a -N mobile2.ltl mobile2
	21	* $ cc -o pan pan.c
	22	* $ pan -a
	23	*/
	24
	25	mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
	26
	27	chan in = [1] of { mtype };
	28	chan out = [1] of { mtype };
	29	chan fa = [0] of { chan };
	30	chan fp = [0] of { chan };
	31	chan m1 = [0] of { chan };
	32	chan m2 = [0] of { chan };
	33	chan l = [0] of { chan };
	34
	35	byte a_id, p_id; /* ids of processes refered to in the property */
	36
	37	proctype CC() /* communication controller */
	38	{ chan m_old, m_new, x;
	39	mtype v;
	40
	41	do
	42	:: in?v ->
	43	printf("MSC: DATA\n");
	44	fa!data; fa!v
	45	:: l?m_new ->
	46	fa!ho_cmd; fa!m_new;
	47	printf("MSC: HAND-OFF\n");
	48	if
	49	:: fp?ho_com ->
	50	printf("MSC: CH_REL\n");
	51	fa!ch_rel; fa?m_old;
	52	l!m_old;
	53	x = fa; fa = fp; fp = x
	54	:: fa?ho_fail ->
	55	printf("MSC: FAIL\n");
	56	l!m_new
	57	fi
	58	od
	59	}
	60
	61	proctype HC(chan m) /* handover controller */
	62	{
	63	do
	64	:: l!m; l?m
65	od
66	}
67
68	proctype BS(chan f, m; bit how) /* base station */
69	{ chan v;
70
71	if
72	:: how -> goto Active
73	:: else -> goto Passive
74	fi;
75
76	Active:
77	printf("MSC: ACTIVE\n");
78	do
79	:: f?data -> f?v; m!data; m!v
80	:: f?ho_cmd -> /* handover command */
81	progress: f?v; m!ho_cmd; m!v;
82	if
83	:: f?ch_rel ->
84	f!m;
85	goto Passive
86	:: m?ho_fail ->
87	printf("MSC: FAILURE\n");
88	f!ho_fail
89	fi
90	od;
91
92	Passive:
93	printf("MSC: PASSIVE\n");
94	m?ho_acc -> f!ho_com;
95	goto Active
96	}
97
98	proctype MS(chan m) /* mobile station */
99	{ chan m_new;
100	mtype v;
101
102	do
103	:: m?data -> m?v; out!v
104	:: m?ho_cmd; m?m_new;
105	if
106	:: m_new!ho_acc; m = m_new
107	:: m!ho_fail
108	fi
109	od
110	}
111
112	active proctype System()
113	{
114	atomic {
115	run HC(m1);
116	run CC();
117	p_id = run BS(fp, m1, 0); /* passive base station */
118	a_id = run BS(fa, m2, 1); /* active base station */
119	run MS(m2)
120	}
121
122	end: do
123	:: in!red; in!white; in!blue
124	od
125	}
126
127	active proctype Out()
128	{
129	end: do /* deadlocks if order is disturbed */
130	:: out?red; out?white; out?blue
131	od
132	}