three-parallel-demo.smv

MODULE program(x1)

VAR
	location : {l1,l2};
ASSIGN
	init(location) := l1;
	next(location) :=
		case
			(location = l1) & x1<200 : l2;
			(location = l2) : l1;
			TRUE : location;
		esac;
	next(x1) := 
		case
			(location = l2) & (x1 < 1000): x1+1;
			TRUE : x1;
		esac;

MODULE program1(x1)
VAR
	location : {m1,m2};

ASSIGN
	init(location) := m1;
	next(location) :=
		case
			(location = m1) & x1>0 : m2;
			(location = m2) : m1;
			TRUE: location;
		esac;
	next(x1) :=
		case
			location = m2 & (x1 > -1000): x1 - 1;
			TRUE : x1;
		esac;

MODULE program2(x1)
VAR
	location: {n1,n2};
ASSIGN
	init(location) := n1;
	next(location) := 
		case
			(location = n1) & x1=200: n2;
			location = n2 : n1;
			TRUE : location;
		esac;
	next(x1) :=
		case
			(location = n2) : 0;
			TRUE : x1;
		esac;

MODULE main
VAR
x : -1000 .. 1000;
thread1 : process program(x);
thread2 : process program1(x);
thread3 : process program2(x);
ASSIGN
	init(x) := 0;