3 var hide_nodes = function () {
4 var v = document.getElementById('relnodes').value;
5 for(i = 0; i < last_id; i++) {
7 var rect = document.getElementById(id);
9 if ((v-0) <= tree[id].max)
10 rect.style.fillOpacity = 1;
12 rect.style.fillOpacity = 0.3;
16 var activate_parent = function () {
17 if (current_node) activate(tree[current_node].par);
19 var activate_previous = function () {
20 if (current_node) activate(tree[current_node].ps);
22 var activate_next = function () {
23 if (current_node) activate(tree[current_node].ns);
25 var activate_first = function () {
26 if (current_node) activate(tree[current_node].fc);
28 var buttons = document.getElementsByTagName("button");
29 var activate = function (id)
31 if (id == nil_id) return;
33 var rect = document.getElementById(current_node);
34 rect.style.fillOpacity = 1.0;
35 rect.style.stroke = 'black';
36 rect.classList.remove('blink');
40 buttons[0].disabled = tree[id].par == nil_id;
41 buttons[1].disabled = tree[id].ps == nil_id;
42 buttons[2].disabled = tree[id].fc == nil_id;
43 buttons[3].disabled = tree[id].ns == nil_id;
45 var node = document.getElementById(id);
46 var div = document.getElementById('svg');
47 var node_dim = node.getBBox();
48 var div_dim = div.getBoundingClientRect();
51 var hs = nx - (div_dim.width / 2 - node_dim.width / 2);
52 var vs = ny - (div_dim.height / 2 - node_dim.height / 2);
55 node.style.stroke = 'red';
57 node.classList.add('blink');
59 var d = document.getElementById('data');
61 for (i=0; i <= rounds; i++)
62 msg += ('<p>round ' + i + ':<br/>new states:') + tree[id].dlist[i]
63 + '<br/>all states:' + tree[id].flist[i] + '</p>\n';