You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

281 lines
15 KiB

2 weeks ago
<!DOCTYPE html>
<body style="background:#fab;">
<div id="container" style="margin:auto;width:700px;background:#fff"></div>
<form style="margin:auto;width:700px;background:#eee;">distance: <input type="range" min="1" max="300" value="150" class="slider" id="distance">
<p>Bovenaan staat de begintoestand. Onderaan een sink-toestand. Lijnen van een toestand naar zichzelf kunnen niet getekend worden. Geel en blauw zijn voor de twee modellen. Toestanden die vergelijkbaar zijn worden vanzelf groen. Je kunt punten verslepen, daarna staan ze vast. Nog eens klikken en zo komen weer los. Dit maakt gebruikt van <a href="https://d3js.org">d3.js</a> met de "force-directed graph layout", het werkt eigenlijk niet zo heel goed voor dit soort modellen. <a href="https://git.cs.ou.nl/joshua.moerman/fsm-diff-vis/">Source</a>.</p>
</form>
<script src="d3.v7.min.js"></script>
<script type="module">
// De twee modellen van DTLS zetten we direct hier neer. Deze transities komen
// direct uit de .dot file. Het meeste hier is hard-coded.
const alphabet = ["HELLO", "KEX", "CIPH", "FIN", "APP", "AL_W", "AL_F"];
const states1 = ["s0", "s1", "s2", "s3", "s4", "s5", "s6", "s7", "s8", "s9", "s10", "s11", "s12"];
const transitions1 = [["s0", "s2", "HELLO", "HELLO_VERIFY_REQUEST"], ["s0", "s0", "KEX", "TO"], ["s0", "s1", "CIPH", "TO"], ["s0", "s0", "FIN", "TO"], ["s0", "s0", "APP", "TO"], ["s0", "s0", "AL_W", "TO"], ["s0", "s0", "AL_F", "TO"], ["s1", "s1", "HELLO", "TO"], ["s1", "s1", "KEX", "TO"], ["s1", "s1", "CIPH", "TO"], ["s1", "s1", "FIN", "TO"], ["s1", "s1", "APP", "TO"], ["s1", "s1", "AL_W", "TO"], ["s1", "s1", "AL_F", "TO"], ["s2", "s3", "HELLO", "SER_HELLO_DONE"], ["s2", "s2", "KEX", "TO"], ["s2", "s1", "CIPH", "TO"], ["s2", "s2", "FIN", "TO"], ["s2", "s2", "APP", "TO"], ["s2", "s2", "AL_W", "TO"], ["s2", "s2", "AL_F", "TO"], ["s3", "s7", "HELLO", "TO"], ["s3", "s4", "KEX", "TO"], ["s3", "s1", "CIPH", "TO"], ["s3", "s2", "FIN", "INT_ERR"], ["s3", "s3", "APP", "TO"], ["s3", "s2", "AL_W", "AL_W"], ["s3", "s2", "AL_F", "TO"], ["s4", "s8", "HELLO", "TO"], ["s4", "s2", "KEX", "INT_ERR"], ["s4", "s5", "CIPH", "TO"], ["s4", "s2", "FIN", "INT_ERR"], ["s4", "s4", "APP", "TO"], ["s4", "s2", "AL_W", "AL_W"], ["s4", "s2", "AL_F", "TO"], ["s5", "s1", "HELLO", "INT_ERR"], ["s5", "s1", "KEX", "INT_ERR"], ["s5", "s1", "CIPH", "INT_ERR"], ["s5", "s6", "FIN", "CIPH,FIN"], ["s5", "s12", "APP", "TO"], ["s5", "s1", "AL_W", "AL_W"], ["s5", "s1", "AL_F", "TO"], ["s6", "s6", "HELLO", "NO_RENEGO"], ["s6", "s6", "KEX", "TO"], ["s6", "s1", "CIPH", "INT_ERR"], ["s6", "s6", "FIN", "TO"], ["s6", "s11", "APP", "APP"], ["s6", "s1", "AL_W", "AL_W"], ["s6", "s1", "AL_F", "TO"], ["s7", "s7", "HELLO", "TO"], ["s7", "s7", "KEX", "TO"], ["s7", "s1", "CIPH", "TO"], ["s7", "s7", "FIN", "TO"], ["s7", "s7", "APP", "TO"], ["s7", "s2", "AL_W", "AL_W"], ["s7", "s2", "AL_F", "TO"], ["s8", "s8", "HELLO", "TO"], ["s8", "s9", "KEX", "TO"], ["s8", "s10", "CIPH", "TO"], ["s8", "s9", "FIN", "TO"], ["s8", "s8", "APP", "TO"], ["s8", "s2", "AL_W", "AL_W"], ["s8", "s2", "AL_F", "TO"], ["s9", "s9", "HELLO", "TO"], ["s9", "s9", "KEX", "TO"], ["s9", "s1", "CIPH", "HANDSHAKE_FAIL"], ["s9", "s9", "FIN", "TO"], ["s9", "s9", "APP", "TO"], ["s9", "s2", "AL_W", "AL_W"], ["s9", "s2", "AL_F", "TO"], ["s10", "s1", "HELLO", "INT_ERR"], ["s10", "s10", "KEX", "TO"], ["s10", "s1", "CIPH", "INT_ERR"], ["s10", "s10", "FIN", "TO"], ["s10", "s10", "APP", "TO"], ["s10", "s1", "AL_W", "AL_W"], ["s10", "s1", "AL_F", "TO"], ["s11", "s11", "HELLO", "NO_RENEGO"], ["s11", "s11", "KEX", "TO"], ["s11", "s1", "CIPH", "TO"], ["s11", "s11", "FIN", "TO"], ["s11", "s11", "APP", "APP"], ["s11", "s1", "AL_W", "AL_W"], ["s11", "s1", "AL_F", "TO"], ["s12", "s1", "HELLO", "INT_ERR"], ["s12", "s1", "KEX", "INT_ERR"], ["s12", "s1", "CIPH", "INT_ERR"], ["s12", "s11", "FIN", "CIPH,FIN,APP"], ["s12", "s12", "APP", "TO"], ["s12", "s1", "AL_W", "AL_W"], ["s12", "s1", "AL_F", "TO"]];
const states2 = ["s0", "s1", "s2", "s3", "s4", "s5", "s6", "s7", "s8", "s9", "s10", "s11", "s12", "s13", "s14", "s15"];
const transitions2 = [["s0", "s2", "HELLO", "HELLO_VERIFY_REQUEST"], ["s0", "s0", "KEX", "TO"], ["s0", "s1", "CIPH", "TO"], ["s0", "s0", "FIN", "TO"], ["s0", "s0", "APP", "TO"], ["s0", "s0", "AL_W", "TO"], ["s0", "s0", "AL_F", "TO"], ["s1", "s1", "HELLO", "TO"], ["s1", "s1", "KEX", "TO"], ["s1", "s1", "CIPH", "TO"], ["s1", "s1", "FIN", "TO"], ["s1", "s1", "APP", "TO"], ["s1", "s1", "AL_W", "TO"], ["s1", "s1", "AL_F", "TO"], ["s2", "s3", "HELLO", "SER_HELLO_DONE"], ["s2", "s2", "KEX", "TO"], ["s2", "s1", "CIPH", "TO"], ["s2", "s2", "FIN", "TO"], ["s2", "s2", "APP", "TO"], ["s2", "s2", "AL_W", "TO"], ["s2", "s2", "AL_F", "TO"], ["s3", "s3", "HELLO", "SER_HELLO_DONE"], ["s3", "s4", "KEX", "TO"], ["s3", "s1", "CIPH", "TO"], ["s3", "s2", "FIN", "INT_ERR"], ["s3", "s3", "APP", "TO"], ["s3", "s2", "AL_W", "AL_W"], ["s3", "s2", "AL_F", "TO"], ["s4", "s8", "HELLO", "SER_HELLO_DONE"], ["s4", "s2", "KEX", "INT_ERR"], ["s4", "s6", "CIPH", "TO"], ["s4", "s12", "FIN", "CIPH,FIN"], ["s4", "s5", "APP", "TO"], ["s4", "s2", "AL_W", "AL_W"], ["s4", "s2", "AL_F", "TO"], ["s5", "s14", "HELLO", "SER_HELLO_DONE"], ["s5", "s2", "KEX", "INT_ERR"], ["s5", "s6", "CIPH", "TO"], ["s5", "s9", "FIN", "CIPH,FIN,APP"], ["s5", "s5", "APP", "TO"], ["s5", "s2", "AL_W", "AL_W"], ["s5", "s2", "AL_F", "TO"], ["s6", "s1", "HELLO", "INT_ERR"], ["s6", "s1", "KEX", "INT_ERR"], ["s6", "s6", "CIPH", "TO"], ["s6", "s7", "FIN", "CIPH,FIN"], ["s6", "s13", "APP", "TO"], ["s6", "s1", "AL_W", "AL_W"], ["s6", "s1", "AL_F", "TO"], ["s7", "s7", "HELLO", "NO_RENEGO"], ["s7", "s7", "KEX", "TO"], ["s7", "s1", "CIPH", "CIPH,FIN"], ["s7", "s7", "FIN", "TO"], ["s7", "s10", "APP", "APP"], ["s7", "s1", "AL_W", "AL_W"], ["s7", "s1", "AL_F", "TO"], ["s8", "s8", "HELLO", "SER_HELLO_DONE"], ["s8", "s4", "KEX", "TO"], ["s8", "s11", "CIPH", "TO"], ["s8", "s2", "FIN", "INT_ERR"], ["s8", "s14", "APP", "TO"], ["s8", "s2", "AL_W", "AL_W"], ["s8", "s2", "AL_F", "TO"], ["s9", "s9", "HELLO", "TO"], ["s9", "s9", "KEX", "TO"], ["s9", "s1", "CIPH", "TO"], ["s9", "s9", "FIN", "TO"], ["s9", "s9", "APP", "APP"], ["s9", "s2", "AL_W", "AL_W"], ["s9", "s2", "AL_F", "TO"], ["s10", "s10", "HELLO", "NO_RENEGO"], ["s10", "s10", "KEX", "TO"], ["s10", "s1", "CIPH", "TO"], ["s10", "s10", "FIN", "TO"], ["s10", "s10", "APP", "APP"], ["s10", "s1", "AL_W", "AL_W"], ["s10", "s1", "AL_F", "TO"], ["s11", "s1", "HELLO", "INT_ERR"], ["s11", "s6", "KEX", "TO"], ["s11", "s11", "CIPH", "TO"], ["s11", "s1", "FIN", "INT_ERR"], ["s11", "s15", "APP", "TO"], ["s11", "s1", "AL_W", "AL_W"], ["s11", "s1", "AL_F", "TO"], ["s12", "s12", "HELLO", "TO"], ["s12", "s12", "KEX", "TO"], ["s12", "s1", "CIPH", "CIPH,FIN"], ["s12", "s12", "FIN", "TO"], ["s12", "s9", "APP", "APP"], ["s12", "s2", "AL_W", "AL_W"], ["s12", "s2", "AL_F", "TO"], ["s13", "s1", "HELLO", "INT_ERR"], ["s13", "s1", "KEX", "INT_ERR"], ["s13", "s6", "CIPH", "TO"], ["s13", "s10", "FIN", "CIPH,FIN,APP"], ["s13", "s13", "APP", "TO"], ["s13", "s1", "AL_W", "AL_W"], ["s13", "s1", "AL_F", "TO"], ["s14", "s14", "HELLO", "SER_HELLO_DONE"], ["s14", "s5", "KEX", "TO"], ["s14", "s11", "CIPH", "TO"], ["s14", "s2", "FIN", "INT_ERR"], ["s14", "s14", "APP", "TO"], ["s14", "s2", "AL_W", "AL_W"], ["s14", "s2", "AL_F", "TO"], ["s15", "s1", "HELLO", "INT_ERR"], ["s15", "s13", "KEX", "TO"], ["s15", "s11", "CIPH", "TO"], ["s15", "s1", "FIN", "INT_ERR"], ["s15", "s15", "APP", "TO"], ["s15", "s1", "AL_W", "AL_W"], ["s15", "s1", "AL_F", "TO"]];
// We zetten ze om in een meer functionele data structuur, zodat we voor elke
// state en input de transitie kunnen opvragen. De prefix gebruik ik zodat de
// states van elk model een andere naam heeft.
function toModel(alphabet, states, transitions, prefix) {
// Ik gebruik een object als Map data structuur. Geen idee of dit normaal is
// in javascript, maar het werkt. Ik geloof dat de keys altijd worden omgezet
// naar een string. Dat is prima hier.
const transitionMap = {}
transitions.forEach(([s, t, i, o]) => {
transitionMap[[prefix + s, i]] = [o, prefix + t];
});
function behaviour(state, input) {
return transitionMap[[state, input]];
}
// We voegen nog een aantal dingen toe aan de functie. Dat kan gewoon in
// javascript!
behaviour.alphabet = alphabet;
behaviour.states = states.map(s => prefix + s);
behaviour.initial_state = prefix + states[0];
behaviour.id = prefix;
return behaviour;
}
// Hier zijn dan uiteindelijk de modellen, hernoemd met m1 en m2.
const model1 = toModel(alphabet, states1, transitions1, "m1");
const model2 = toModel(alphabet, states2, transitions2, "m2");
// Met de hand uitgerekend. Momenteel krijgen deze nodes een sterke
// aantrekkingskracht, maar dat werkt eigenlijk niet zo lekker. Dus ik denk
// dat het beter is zulke nodes echt te mergen. (Of de "forceManyBodies" te
// verfijnen.)
const exact_bisimulation = [{source: "m1s1", target: "m2s1"}, {source: "m1s10", target: "m2s10"}];
// BFS vanuit de begintoestanden. De zoek stops als er een fout wordt gevonden.
const approx_bisim = (() => {
const queue = [[model1.initial_state, model2.initial_state]];
const matched = []
const visited = new Set();
while(queue.length > 0) {
const [s1, s2] = queue[0];
queue.shift(0);
if (visited.has(s1) || visited.has(s2)) {
continue;
}
visited.add(s1);
visited.add(s2);
matched.push({source: s1, target: s2});
alphabet.forEach(i => {
const [o1, t1] = model1(s1, i);
const [o2, t2] = model2 (s2, i);
if (o1 == o2) {
queue.push([t1, t2]);
}
})
}
return matched;
})();
// We doen net alsof dit een bisimulation is
const bisimulation = exact_bisimulation.concat(approx_bisim);
// Punten die gematched zijn, behandelen we anders, dus we willen weten welke
// dat zijn.
const matched = new Set();
bisimulation.forEach(l => {
matched.add(l.source);
matched.add(l.target);
});
// Hier gaan we de graaf maken, we zetten gewoon alles in 1 graaf en doen
// niks ingewikkelds.
const data = (() => {
const models = [model1, model2];
const nodes = [];
const links = [];
const linksAdded = new Set();
models.forEach(m => {
m.states.forEach(s => {
nodes.push({id: s, model_id: m.id});
m.alphabet.forEach(i => {
const [o, t] = m(s, i);
if (s != t && !linksAdded.has([s, t].toString()) && !linksAdded.has([t, s].toString())) {
links.push({source: s, target: t, model_id: m.id});
linksAdded.add([s, t].toString());
}
})
})
})
console.log(links);
return {nodes, links};
})();
const chart = (() => {
const width = 700;
const height = 700;
const heightMargin = 300;
const links = data.links.map(d => Object.create(d));
const links_bisim = bisimulation.map(d => Object.create(d));
const nodes = data.nodes.map(d => Object.create(d));
// begin en "eind"-toestand van model 1
nodes[0].fy = -heightMargin;
nodes[1].fy = heightMargin;
// begin en "eind"-toestand van model 1
nodes[13].fy = -heightMargin;
nodes[14].fy = heightMargin;
function extraForces () {
var nodes = null;
function force(alpha){
for (let i = 0, n = nodes.length; i < n; ++i) {
var node = nodes[i];
// we zorgen dat nodes niet boven en onder verdwijnen
if (node.y > heightMargin) {
node.vy -= alpha * (node.y - heightMargin)
}
if (node.y < -heightMargin) {
node.vy -= alpha * (node.y + heightMargin)
}
// En ik wil het ene model links en het ander model rechts. We slaan
// nodes over die gematched zijn.
if (!matched.has(node.id)){
if (node.model_id == "m1") {
node.vx += 5 * alpha;
} else {
node.vx -= 5 * alpha;
}
}
// Voor state s2 een extra foce die m wat omhoog duwt. Dit is
// natuurlijk een hack.
if (node.id == "m1s2" || node.id == "m2s2") {
node.vy -= 40 * alpha;
}
}
}
force.initialize = function(_) { nodes = _; };
return force;
}
const simulation = d3.forceSimulation(nodes)
// Er is een kracht die alle nodes uit elkaar duwt.
.force("charge", d3.forceManyBody().distanceMin(8))
// Er is een kracht die edges kort houdt (vaste afstand, niet zo handig)
.force("link", d3.forceLink(links).id(d => d.id).strength(0.2).distance(150))
// Vergelijkbare nodes hebben afstand 0
.force("link_bisim", d3.forceLink(links_bisim).id(d => d.id).strength(2).distance(0).iterations(3))
// En ik heb nog wat extra dingen toegevoegd
.force("extra", extraForces());
// SVG container
const svg = d3.create("svg")
.attr("width", width)
.attr("height", height)
.attr("viewBox", [-width / 2, -height / 2, width, height])
.attr("style", "max-width: 100%; height: auto;");
// een groep voor alle lijnen
const link = svg.append("g")
.selectAll("line")
.data(links)
.join("line")
.attr("stroke-width", 3);
// een groep voor alle punten
const node = svg.append("g")
.attr("style", "isolation: isolate;")
.attr("stroke", "#fff")
.selectAll("circle")
.data(nodes)
.join("circle")
.attr("style", "mix-blend-mode: multiply")
.attr("r", 10);
// Elke tick moeten we de posities updaten van punten en lijnen
simulation.on("tick", () => {
link.attr("x1", d => d.source.x)
.attr("y1", d => d.source.y)
.attr("x2", d => d.target.x)
.attr("y2", d => d.target.y)
.attr("stroke", d => d.model_id == "m1" ? "#0aa4" : "#aa04");
node.attr("cx", d => d.x)
.attr("cy", d => d.y)
.attr("fill", d => d.model_id == "m1" ? "#0ee" : "#ee0")
.attr("stroke", d => d.fy == null ? "#fff" : "#000");
});
// Interactie moet de punten
const drag = d3.drag()
.on("start", dragstarted)
.on("drag", dragged)
.on("end", dragended);
node.call(drag).on("click", clickn);
function dragstarted(event) {
if (!event.active) simulation.alphaTarget(0.3).restart();
event.subject.fx = event.subject.x;
event.subject.fy = event.subject.y;
}
function dragged(event) {
event.subject.fx = event.x;
event.subject.fy = event.y;
}
function dragended(event) {
if (!event.active) simulation.alphaTarget(0);
}
function clickn(event, d) {
delete d.fx;
delete d.fy;
simulation.restart();
}
// Deze dingen hebben we buiten de block scope nog nodig.
return {
node: svg.node(),
simulation: simulation,
links: links,
};
})();
// In de html zetten
container.append(chart.node);
// Slider laten werken.
var slider = document.getElementById("distance");
// on-input is zolang je aan het slepen bent
slider.oninput = function() {
chart.simulation.force("link", d3.forceLink(chart.links).strength(0.2).distance(this.value));
chart.simulation.alphaTarget(0.3).restart();
}
// on-change is daarna
slider.onchange = function() {
chart.simulation.alphaTarget(0);
}
</script>
</body>