// -*-Javascript-*-
-var old_timer = null;
-var old_node = null;
-var make_button = function (target, label)
-{
- var msg = '<button onclick="';
- msg += 'activate(\'' + target + '\')"';
- if (target == 'node-1') msg+= ' disabled="disabled" ';
- msg+= '>' + label + '</button>';
- return msg;
+var hide_nodes = function () {
+ var v = document.getElementById('relnodes').value;
+ for(i = 0; i < last_id; i++) {
+ var id = 'node' + i;
+ var rect = document.getElementById(id);
+
+ if ((v-0) <= tree[id].max)
+ rect.style.fillOpacity = 1;
+ else
+ rect.style.fillOpacity = 0.3;
+ }
};
+var activate_parent = function () {
+ if (current_node) activate(tree[current_node].par);
+};
+var activate_previous = function () {
+ if (current_node) activate(tree[current_node].ps);
+};
+var activate_next = function () {
+ if (current_node) activate(tree[current_node].ns);
+};
+var activate_first = function () {
+ if (current_node) activate(tree[current_node].fc);
+};
+var buttons = document.getElementsByTagName("button");
var activate = function (id)
{
- if (old_node) {
- clearInterval(old_timer);
- old_node.style.fillOpacity = 1.0;
- old_node.style.stroke = 'black';
- old_node.classList.remove('blink');
+ if (id == nil_id) return;
+ if (current_node) {
+ var rect = document.getElementById(current_node);
+ rect.style.fillOpacity = 1.0;
+ rect.style.stroke = 'black';
+ rect.classList.remove('blink');
};
+ hide_nodes();
+ current_node = id;
+ buttons[0].disabled = tree[id].par == nil_id;
+ buttons[1].disabled = tree[id].ps == nil_id;
+ buttons[2].disabled = tree[id].fc == nil_id;
+ buttons[3].disabled = tree[id].ns == nil_id;
+
var node = document.getElementById(id);
var div = document.getElementById('svg');
var node_dim = node.getBBox();
var d = document.getElementById('data');
var msg = '';
- for (i=0; i < rounds; i++)
- msg += ('<p>round: ' + i + ':<br/>') + data[i][id] + '</p>\n';
-
- var rect = document.getElementById(id);
- var fce = rect.firstElementChild;
- var nse = fce.nextElementSibling;
- var pare = nse.nextElementSibling;
- var pse = pare.nextElementSibling;
- var fc = fce.textContent;
- var ns = nse.textContent;
- var par = pare.textContent;
- var ps = pse.textContent;
- msg += make_button(par, "↑");
- msg += make_button(ps, "←");
- msg += make_button(fc, "↓");
- msg += make_button(ns,"→");
+ for (i=0; i <= rounds; i++)
+ msg += ('<p>round ' + i + ':<br/>new states:') + tree[id].dlist[i]
+ + '<br/>all states:' + tree[id].flist[i] + '</p>\n';
d.innerHTML = msg;
return;
};