composition_prep.js

var proc_P = [
		["A", "in", "B"],
		["B", "sync", "A"]
];

var proc_Q = [
		["Δ", "sync", "Θ"],
		["Θ", "out", "Δ"]
];

var ps = { p: proc_P, q: proc_Q };

var evts =  ["sync"];

var s0 = [{ p: "A", q: "Δ" }, { idx: 0, visited: false, next: [] }];

var q = [s0];

var syncq = [];

function reset() {
	s0 = [{ p: "A", q: "Δ" }, { idx: 0, visited: false, next: [] }];
	q = [s0];
	syncq = [];
}

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

function step() {
	if (q.find(e => { return !e[1].visited })) {
		let l = q.length;
		for (let i = 0; i < l; i++)
			next(q[i]);
	}
}

function next(status) {
	let current_p_status = status[0].p;
	let current_q_status = status[0].q;
	if (status[1].visited)
		return;
	status[1].visited = true;

	ps.q.forEach(function (each) {
		if (each[0] == current_q_status) {
			let new_status = [
				{ p: current_p_status, q: each[2]}, 
				{ idx: 0, visited: false, next: [] }
			];
			let trans = each[1];
			if (evts.includes(trans)) {
				if (hasTransition(status, trans))
					if (findIndex(status, syncq) == -1)
						syncq.push(status);
			} else {
				let idx = findIndex(new_status, q);
				if (idx == -1) {
					q.push(new_status);
					status[1].next.push({ label: each[1], status: new_status});
				} else {
					status[1].next.push({ label: each[1], status: q[idx]});
				}		
			}
		}
	});

	ps.p.forEach(function (each) {
		if (each[0] == current_p_status) {
			let new_status = [
				{ p: each[2], q: current_q_status }, 
				{ idx: 0, visited: false, next: [] }
			];
			let trans = each[1];
			if (evts.includes(trans)) {
				if (hasTransition(status, trans))
					if (findIndex(status, syncq) == -1)
						syncq.push(status);
			} else {
				let idx = findIndex(new_status, q);
				if (idx == -1) {
					q.push(new_status);
					status[1].next.push({ label: each[1], status: new_status});
				} else {
					status[1].next.push({ label: each[1], status: q[idx]});
				}		
			}
		}
	});
	while (syncq.length > 0) {
		let status = syncq.shift();
		let new_status = [
			{ p: trans(ps.p, status[0].p), q: trans(ps.q, status[0].q) },
			{ idex: 0, visited: false, next: [] }
		];
		let idx = findIndex(new_status, q);
		if (idx == -1) {
			q.push(new_status);
			let l = label(ps.p, status[0].p);
			status[1].next.push({ label: l, status: new_status});
		} else {
			status[1].next.push({ label: l, status: q[idx]});
		}
	}
}

function findIndex(status, q) {
	return q.findIndex(e => {
		return e[0].p == status[0].p && e[0].q == status[0].q;
	});
}

function hasTransition(status, trans) {
	let current_p_status = status[0].p;
	let current_q_status = status[0].q;
	return ps.q.findIndex(function (e) {
			return e[0] == current_q_status && e[1] == trans;
		}) > -1 &&
		ps.p.findIndex(function (e) {
			return e[0] == current_p_status && e[1] == trans;
		}) > -1;
}

//	var s1 = [ { p: "A", q: "Δ" }, { idx: 0, visited: false, next: [] }];
//	var s2 = [ { p: "B", q: "Δ" }, { idx: 0, visited: false, next: [] }];
//	var s3 = [ { p: "A", q: "Θ" }, { idx: 0, visited: false, next: [] }];
//	var s4 = [ { p: "B", q: "Θ" }, { idx: 0, visited: false, next: [] }];

function trans(proc, state) {
	let result = proc.find(e => { return e[0] == state });
	return result == undefined ? undefined : result[2];
}

function label(proc, state) {
	let result = proc.find(e => { return e[0] == state });
	return result == undefined ? undefined : result[1];
}

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

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

function viz2() {
	console.log('digraph {');
	q.forEach(function (each, idx) {
		console.log([
			'\t',
			idx,
			' ',
			'[label="',
			idx,
			'\\n',
			each[0].p + each[0].q,
			'\\n"',
			idx == 0 ? 'style=filled,fillcolor=cyan' : each[1].next.length == 0 ? 'style=filled,fillcolor=pink' : '',
			'];'
			].join(''));
	});

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