m_inc2.js

var process_P = [
	["P0", ["read", "P1", function (r) { return true },
		function (r) { r.t1 = r.x }]],
	["P1", ["inc", "P2", function (r) { return true },
		function (r) { r.t1 = r.t1 + 1 }]],
	["P2", ["write", "P3", function (r) { return true },
		function (r) { r.x = r.t1 }]],
	["P3", []]
];

var process_Q = [
	["Q0", ["read", "Q1", function (r) { return true },
		function (r) { r.t2 = r.x }]],
	["Q1", ["inc", "Q2", function (r) { return true },
		function (r) { r.t2 = r.t2 + 1 }]],
	["Q2", ["write", "Q3", function (r) { return true },
		function (r) { r.x = r.t2 }]],
	["Q3", []]
];

var ps = {
	p: process_P, 
	q: process_Q
};

var r0 = {
	x: 0,
	t1: 0,
	t2: 0
};

// ((P0, Q0), (x, t1, t2))

var s0 = [{ p: "P0", q: "Q0" }, r0, { idx: 0, visited: false, next: [] }];
var q = [s0];

function viz_proc(process) {
	console.log('digraph {');
	process.forEach(function (each) {
		if (each[1].length > 0) {
			console.log('\t', [each[0], '->', each[1][1], '[label="' + each[1][0] + '"]', ';'].join(' '));
		}
	});
	console.log('}');
}

function viz() {
	console.log('digraph {');
	q.forEach(function (each, idx) {
		console.log([
			'\t',
			idx,
			' ',
			'[label="',
			idx,
			'\\n',
			JSON.stringify(each[0]).replace(/"/g, ''),
			'\\n',
			JSON.stringify(each[1]).replace(/"/g, '').replace(/:/g, '='),
			'",',
			idx == 0 ? 'style=filled,fillcolor=cyan' : each[2].next.length == 0 ? 'style=filled,fillcolor=pink' : '',
			'];'
			].join(''));
	});

	q.forEach(function (each) {
		if (each[2].next.length > 0) {
			each[2].next.forEach(function (elm) {
				console.log([
					'\t',
					each[2].idx,
					' -> ',
					elm.status[2].idx,
					' ',
					'[label="',
					elm.label,
					'",',
					'];'
					].join(''));
			});
		}
	});
	console.log('}');
}

function go() {
	for (var i = 0;;) {
		i = q.length;
		step();
		if (i == q.length)
			break;
	}
	q.forEach(function (each, idx) {
		each[2].idx = idx;
	})
}

function step() {
	if (q.find(function (each) { return !each[2].visited})) {
		var l = q.length;
		for (var i = 0; i < l; i++) {
			next(q[i], ps);
		}
	}
}

function reset() {
	q = [[{ p: "P0", q: "Q0" }, r0, { idx: 0, visited: false, next: [] }]];
}

function clone(o) {
	return Object.assign({}, o);
}

function next(status, ps) {
	var current_p_status = status[0].p;
	var current_q_status = status[0].q;
	var current_sharedvars = status[1];
	var new_sharedvars_p = clone(current_sharedvars);
	var new_sharedvars_q = clone(current_sharedvars);

	if (status[2].visited)
		return;
	status[2].visited = true;

	ps.q.forEach(function (each) {
		if (each[0] == current_q_status) {
			if (each[1].length > 0) {
				var guard = each[1][2];
				if (guard(current_sharedvars)) {
					var action = each[1][3];
					action(new_sharedvars_q);
					var new_status = [{ p: current_p_status, q: each[1][1]}, new_sharedvars_q, { idx: 0, visited: false, next: [] }];
					var idx = findIndex(new_status, q);
					if (idx == -1) {
						q.push(new_status);
						status[2].next.push({ label: each[1][0], status: new_status});
					} else {
						status[2].next.push({ label: each[1][0], status: q[idx]});
					}
				}
			}
		}
	})

	ps.p.forEach(function (each) {
		if (each[0] == current_p_status) {
			if (each[1].length > 0) {
				var guard = each[1][2];
				if (guard(current_sharedvars)) {
					var action = each[1][3];
					action(new_sharedvars_p);
					var new_status = [{ p: each[1][1], q: current_q_status}, new_sharedvars_p, { idx: 0, visited: false, next: [] }];
					var idx = findIndex(new_status, q);
					if (idx == -1) {
						q.push(new_status);
						status[2].next.push({ label: each[1][0], status: new_status});
					} else {
						status[2].next.push({ label: each[1][0], status: q[idx]});
					}
				}
			}
		}
	})
}

function findIndex(status, q) {
	return q.findIndex(function (elm) {
		return (
			elm[0].p == status[0].p && 
			elm[0].q == status[0].q &&
			elm[1].x == status[1].x &&
			elm[1].t1 == status[1].t1 &&
			elm[1].t2 == status[1].t2
		)
	});
}

go();
viz();