Skip to content

Instantly share code, notes, and snippets.

@iriyak
Created October 20, 2019 13:58
Show Gist options
  • Save iriyak/66b984cce5b67de656e3b02f82197e57 to your computer and use it in GitHub Desktop.
Save iriyak/66b984cce5b67de656e3b02f82197e57 to your computer and use it in GitHub Desktop.
var process_P = [
["P0", ["lock 0", "P1", function (r) { return r.m0 == 0 },
function (r) { r.m0 = 1 }]],
["P1", ["lock 1", "P2", function (r) { return r.m1 == 0 },
function (r) { r.m1 = 1 }]],
["P2", ["unlock 1", "P3", function (r) { return true },
function (r) { r.m1 = 0 }]],
["P3", ["unlock 0", "P0", function (r) { return true },
function (r) { r.m0 = 0 }]]
];
var process_Q = [
["Q0", ["lock 1", "Q1", function (r) { return r.m1 == 0 },
function (r) { r.m1 = 1 }]],
["Q1", ["lock 0", "Q2", function (r) { return r.m0 == 0 },
function (r) { r.m0 = 1 }]],
["Q2", ["unlock 0", "Q3", function (r) { return true },
function (r) { r.m0 = 0 }]],
["Q3", ["unlock 1", "Q0", function (r) { return true },
function (r) { r.m1 = 0 }]]
];
var ps = {
p: process_P,
q: process_Q
};
var r0 = {
m0: 0,
m1: 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, idx) {
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,
'",',
walk_bfs(4).find(e => e.visited == true && e.e[0] == each[2].idx && e.e[1] == elm.status[2].idx) ? 'style=bold,color=red' : '',
'];'
].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]);
}
}
}
function reset() {
q = [[{ p: "P0", q: "Q0" }, r0, { idx: 0, visited: false, next: [] }]];
}
function clone(o) {
return Object.assign({}, o);
}
function next(status) {
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);
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);
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) {
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
)
});
}
function find_deadlock() {
return q.filter(function (each) {
return each[2].next.length == 0
})
}
// node> q.map(e => [e[2].idx, e[2].next.map(e => e.status[2].idx)])
// [
// [ 0, [ 1, 2 ] ],
// [ 1, [ 3, 4 ] ],
// [ 2, [ 4, 5 ] ],
// [ 3, [ 6 ] ],
// [ 4, [] ],
// [ 5, [ 7 ] ],
// [ 6, [ 0, 8 ] ],
// [ 7, [ 9, 0 ] ],
// [ 8, [ 2 ] ],
// [ 9, [ 1 ] ]
// ]
// node> lis.map(e1 => e1[1].map(e2 => [e1[0], e2])).flat()
// [
// [ 0, 1 ], [ 0, 2 ],
// [ 1, 3 ], [ 1, 4 ],
// [ 2, 4 ], [ 2, 5 ],
// [ 3, 6 ], [ 5, 7 ],
// [ 6, 0 ], [ 6, 8 ],
// [ 7, 9 ], [ 7, 0 ],
// [ 8, 2 ], [ 9, 1 ]
// ] //
function walk_bfs(idx) {
var lis = q.map(e => [e[2].idx, e[2].next.map(e => e.status[2].idx)]);
var lis2 = lis.map(e1 => e1[1].map(e2 => [e1[0], e2])).flat()
var x = lis2.map(e => { return { visited: false, e: e } });
return walk_bfs_3(idx, x);
}
function walk_bfs_2(idx, x) {
var r = x.find(e => idx == e.e[0] && !e.visited);
while (r != undefined) {
r.visited = true;
if (r.e[1] == 0)
break;
r = x.find(e => r.e[1] == e.e[0] && !e.visited);
}
return x;
}
function walk_bfs_3(dst, x) {
var r = x.find(e => dst == e.e[1] && !e.visited);
while (r != undefined) {
r.visited = true;
if (r.e[0] == 0)
break;
r = x.find(e => r.e[0] == e.e[1] && !e.visited);
}
return x;
}
// なかなか!
function path(s, d) {
var edges = lis2;
var results = [];
results.push(edges.filter(e => e[0] == s));
return results;
}
function traverse(lis2, key) {
var x = lis2.find(e => e[1] == key);
var acc = [];
if (x == -1 || key == 0)
return acc;
else {
acc.push(key);
return traverse2(lis2, x[0], acc);
}
}
function traverse2(lis2, key, acc) {
var x = lis2.find(e => e[1] == key);
if (x == -1 || key == 0)
return [acc, key].flat();
else {
acc.push(key);
return traverse2(lis2, x[0], acc);
}
}
// go();
// viz();
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment