Created
October 20, 2019 13:58
-
-
Save iriyak/66b984cce5b67de656e3b02f82197e57 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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