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

/*
	The Sieve of Eratosthenes (c. 276-196 BC)
	Prints all prime numbers up to MAX
*/
#define MAX	25

mtype = { number, eof };

chan root = [0] of { mtype, int };

proctype sieve(chan c; int prime)
{	chan child = [0] of { mtype, int };
	bool haschild;
	int n;

	printf("MSC: %d is prime\n", prime);
end:	do
	:: c?number(n) ->
		if
		:: (n%prime) == 0 ->
			printf("MSC: %d = %d*%d\n", n, prime, n/prime)
		:: else ->
			if
			:: !haschild ->	/* new prime */
				haschild = true;
				run sieve(child, n);
			:: else ->
				child!number(n)
			fi;
		fi
	:: c?eof(0) ->
		break
	od;
	if
	:: haschild ->
		child!eof(0)
	:: else
	fi
}

init
{	int n = 2;

	run sieve(root, n);
	do
	:: (n <  MAX) -> n++; root!number(n)
	:: (n >= MAX) -> root!eof(0); break
	od
}
Commit	Line	Data
0b55f123	1	/*
	2	The Sieve of Eratosthenes (c. 276-196 BC)
	3	Prints all prime numbers up to MAX
	4	*/
	5	#define MAX 25
	6
	7	mtype = { number, eof };
	8
	9	chan root = [0] of { mtype, int };
	10
	11	proctype sieve(chan c; int prime)
	12	{ chan child = [0] of { mtype, int };
	13	bool haschild;
	14	int n;
	15
	16	printf("MSC: %d is prime\n", prime);
	17	end: do
	18	:: c?number(n) ->
	19	if
	20	:: (n%prime) == 0 ->
	21	printf("MSC: %d = %d*%d\n", n, prime, n/prime)
	22	:: else ->
	23	if
	24	:: !haschild -> /* new prime */
	25	haschild = true;
	26	run sieve(child, n);
	27	:: else ->
	28	child!number(n)
	29	fi;
	30	fi
	31	:: c?eof(0) ->
	32	break
	33	od;
	34	if
	35	:: haschild ->
	36	child!eof(0)
	37	:: else
	38	fi
	39	}
	40
	41	init
	42	{ int n = 2;
	43
	44	run sieve(root, n);
	45	do
	46	:: (n < MAX) -> n++; root!number(n)
	47	:: (n >= MAX) -> root!eof(0); break
	48	od
	49	}