Created
November 30, 2019 13:16
-
-
Save iriyak/5e1cb19c5997d0e2aa112b8034588c3b 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 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('}'); | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment