Spaces:
Sleeping
Sleeping
| /* ββββββββββββββββββββββββββββββββββββββββββββ | |
| PDA SIMULATOR β SCRIPT.JS | |
| Handles: navigation, API calls, diagram, | |
| step simulation, stack/tape render | |
| ββββββββββββββββββββββββββββββββββββββββββββ */ | |
| // ββ State βββββββββββββββββββββββββββββββββββββ | |
| let simSteps = []; // all steps returned by backend | |
| let curStep = -1; // current displayed step index | |
| let playing = false; | |
| let playTimer = null; | |
| let diagramData = null; // {states, start_state, final_states, transitions} | |
| let samplesCache = null; // loaded once | |
| // ββ Navigation ββββββββββββββββββββββββββββββββ | |
| function navTo(sectionId) { | |
| document.querySelectorAll('.section').forEach(s => s.classList.remove('active')); | |
| const target = document.getElementById(sectionId); | |
| if (target) { | |
| target.classList.add('active'); | |
| target.scrollIntoView({ behavior: 'smooth', block: 'start' }); | |
| } | |
| // Update nav buttons | |
| document.querySelectorAll('.sidenav button').forEach(btn => { | |
| btn.classList.toggle('active', btn.getAttribute('data-sec') === sectionId); | |
| }); | |
| } | |
| // Highlight nav item based on scroll | |
| const sections = ['hero','concepts','pda-input','diagram-section','simulation','result-section']; | |
| const observer = new IntersectionObserver(entries => { | |
| entries.forEach(e => { | |
| if (e.isIntersecting) { | |
| const id = e.target.id; | |
| document.querySelectorAll('.sidenav button').forEach(btn => | |
| btn.classList.toggle('active', btn.getAttribute('data-sec') === id) | |
| ); | |
| } | |
| }); | |
| }, { threshold: 0.4 }); | |
| window.addEventListener('DOMContentLoaded', () => { | |
| sections.forEach(id => { | |
| const el = document.getElementById(id); | |
| if (el) observer.observe(el); | |
| }); | |
| }); | |
| // ββ Toast βββββββββββββββββββββββββββββββββββββ | |
| function showToast(msg, type = 'error') { | |
| const t = document.getElementById('toast'); | |
| t.textContent = msg; | |
| t.className = `toast ${type}`; | |
| t.classList.remove('hidden'); | |
| clearTimeout(t._timer); | |
| t._timer = setTimeout(() => t.classList.add('hidden'), 5000); | |
| } | |
| // ββ Sample loader βββββββββββββββββββββββββββββ | |
| async function loadSamples() { | |
| if (samplesCache) return samplesCache; | |
| try { | |
| const r = await fetch('/api/samples'); | |
| samplesCache = await r.json(); | |
| } catch (e) { | |
| samplesCache = {}; | |
| } | |
| return samplesCache; | |
| } | |
| async function loadSample(key) { | |
| const samples = await loadSamples(); | |
| const s = samples[key]; | |
| if (!s) return; | |
| document.getElementById('states').value = s.states.join(', '); | |
| document.getElementById('input_alphabet').value = s.input_alphabet.join(', '); | |
| document.getElementById('stack_alphabet').value = s.stack_alphabet.join(', '); | |
| document.getElementById('start_state').value = s.start_state; | |
| document.getElementById('initial_stack').value = s.initial_stack; | |
| document.getElementById('final_states').value = s.final_states.join(', '); | |
| document.getElementById('transitions').value = s.transitions.join('\n'); | |
| document.getElementById('acceptance').value = s.acceptance; | |
| // Pick first test string | |
| document.getElementById('input_string').value = s.test_strings ? s.test_strings[0] : ''; | |
| showToast(`Loaded sample: ${s.name}`, 'success'); | |
| } | |
| // ββ Run Simulation ββββββββββββββββββββββββββββ | |
| async function runSimulation() { | |
| const btn = document.getElementById('simulateBtn'); | |
| btn.disabled = true; | |
| btn.querySelector('span').textContent = 'β³ Simulatingβ¦'; | |
| const body = { | |
| states: document.getElementById('states').value, | |
| input_alphabet: document.getElementById('input_alphabet').value, | |
| stack_alphabet: document.getElementById('stack_alphabet').value, | |
| start_state: document.getElementById('start_state').value, | |
| initial_stack: document.getElementById('initial_stack').value, | |
| final_states: document.getElementById('final_states').value, | |
| transitions: document.getElementById('transitions').value.split('\n').filter(l=>l.trim()), | |
| input_string: document.getElementById('input_string').value, | |
| acceptance: document.getElementById('acceptance').value, | |
| }; | |
| try { | |
| const resp = await fetch('/api/simulate', { | |
| method: 'POST', | |
| headers: { 'Content-Type': 'application/json' }, | |
| body: JSON.stringify(body) | |
| }); | |
| const data = await resp.json(); | |
| if (!resp.ok) { | |
| showToast(data.error || 'Simulation failed'); | |
| return; | |
| } | |
| // Store results | |
| simSteps = data.steps || []; | |
| diagramData = data.diagram; | |
| // Draw diagram | |
| drawDiagram(diagramData); | |
| document.getElementById('diagram-hint').style.display = 'none'; | |
| // Init simulation display | |
| curStep = -1; | |
| renderTimeline(); | |
| stepNext(); | |
| // Render result | |
| renderResult(data); | |
| // Navigate to diagram | |
| navTo('diagram-section'); | |
| setTimeout(() => navTo('simulation'), 800); | |
| } catch (e) { | |
| showToast('Network error: ' + e.message); | |
| } finally { | |
| btn.disabled = false; | |
| btn.querySelector('span').textContent = 'βΆ Simulate'; | |
| } | |
| } | |
| // ββ Reset βββββββββββββββββββββββββββββββββββββ | |
| function resetAll() { | |
| ['states','input_alphabet','stack_alphabet','start_state','initial_stack', | |
| 'final_states','transitions','input_string'].forEach(id => { | |
| const el = document.getElementById(id); | |
| el.value = ''; | |
| }); | |
| document.getElementById('acceptance').value = 'final_state'; | |
| document.getElementById('toast').classList.add('hidden'); | |
| simSteps = []; curStep = -1; diagramData = null; | |
| document.getElementById('pda-diagram').innerHTML = ''; | |
| document.getElementById('diagram-hint').style.display = ''; | |
| clearTapeStack(); | |
| document.getElementById('timeline').innerHTML = ''; | |
| resetCurrentPanel(); | |
| } | |
| // ββ Diagram Drawing βββββββββββββββββββββββββββ | |
| function drawDiagram(data) { | |
| const svg = document.getElementById('pda-diagram'); | |
| svg.innerHTML = ''; | |
| if (!data) return; | |
| const W = svg.parentElement.clientWidth || 800; | |
| const H = 420; | |
| svg.setAttribute('viewBox', `0 0 ${W} ${H}`); | |
| const states = data.states; | |
| const n = states.length; | |
| const cx = W / 2, cy = H / 2; | |
| const R = Math.min(W, H) * 0.32; | |
| const r = 36; // node radius | |
| // Position states in a circle | |
| const pos = {}; | |
| states.forEach((s, i) => { | |
| const angle = (2 * Math.PI * i / n) - Math.PI / 2; | |
| pos[s] = { x: cx + R * Math.cos(angle), y: cy + R * Math.sin(angle) }; | |
| }); | |
| // Defs (arrowhead marker) | |
| const defs = svgEl('defs'); | |
| ['normal','active','start'].forEach(type => { | |
| const marker = svgEl('marker'); | |
| const color = type === 'active' ? '#7c4dff' : type === 'start' ? '#00e5ff' : 'rgba(0,229,255,.4)'; | |
| Object.assign(marker, {}); | |
| marker.setAttribute('id', `arrow-${type}`); | |
| marker.setAttribute('markerWidth', '8'); | |
| marker.setAttribute('markerHeight', '6'); | |
| marker.setAttribute('refX', '7'); | |
| marker.setAttribute('refY', '3'); | |
| marker.setAttribute('orient', 'auto'); | |
| const poly = svgEl('polygon'); | |
| poly.setAttribute('points', '0 0, 8 3, 0 6'); | |
| poly.setAttribute('fill', color); | |
| marker.appendChild(poly); | |
| defs.appendChild(marker); | |
| }); | |
| svg.appendChild(defs); | |
| // Start arrow to start state | |
| const sp = pos[data.start_state]; | |
| if (sp) { | |
| const arrow = svgEl('line'); | |
| arrow.setAttribute('x1', sp.x - r - 28); | |
| arrow.setAttribute('y1', sp.y); | |
| arrow.setAttribute('x2', sp.x - r - 4); | |
| arrow.setAttribute('y2', sp.y); | |
| arrow.setAttribute('class', 'start-arrow'); | |
| arrow.setAttribute('marker-end', 'url(#arrow-start)'); | |
| svg.appendChild(arrow); | |
| } | |
| // Group transitions by (from,to) for label stacking | |
| const grouped = {}; | |
| (data.transitions || []).forEach(t => { | |
| const key = `${t.from}__${t.to}`; | |
| if (!grouped[key]) grouped[key] = []; | |
| grouped[key].push(t.label); | |
| }); | |
| // Draw transition arrows | |
| Object.entries(grouped).forEach(([key, labels]) => { | |
| const [from, to] = key.split('__'); | |
| const fp = pos[from], tp = pos[to]; | |
| if (!fp || !tp) return; | |
| const isSelf = from === to; | |
| const reverseKey = `${to}__${from}`; | |
| const hasBoth = grouped[reverseKey] && from !== to; | |
| const labelText = labels.join(' | '); | |
| const gId = `tg-${key.replace(/[^a-z0-9]/gi,'_')}`; | |
| if (isSelf) { | |
| // Self-loop arc | |
| const lx = fp.x, ly = fp.y - r - 30; | |
| const path = svgEl('path'); | |
| path.setAttribute('d', `M ${fp.x - 20} ${fp.y - r} Q ${lx - 30} ${ly - 30} ${fp.x + 20} ${fp.y - r}`); | |
| path.setAttribute('class', 'trans-arrow'); | |
| path.setAttribute('id', `path-${gId}`); | |
| path.setAttribute('marker-end', 'url(#arrow-normal)'); | |
| svg.appendChild(path); | |
| addTransLabel(svg, lx, ly - 10, labelText, gId); | |
| } else { | |
| // Straight or curved arrow | |
| const dx = tp.x - fp.x, dy = tp.y - fp.y; | |
| const len = Math.sqrt(dx*dx + dy*dy); | |
| const nx = dx/len, ny = dy/len; | |
| const ox = -ny, oy = nx; | |
| const curve = hasBoth ? 30 : 0; | |
| const mx = (fp.x + tp.x)/2 + ox*curve, my = (fp.y + tp.y)/2 + oy*curve; | |
| const sx = fp.x + nx*r + ox*(curve ? 5:0); | |
| const ex = tp.x - nx*r + ox*(curve ? 5:0); | |
| const sy = fp.y + ny*r + oy*(curve ? 5:0); | |
| const ey = tp.y - ny*r + oy*(curve ? 5:0); | |
| const path = svgEl('path'); | |
| const d = curve | |
| ? `M ${sx} ${sy} Q ${mx} ${my} ${ex} ${ey}` | |
| : `M ${sx} ${sy} L ${ex} ${ey}`; | |
| path.setAttribute('d', d); | |
| path.setAttribute('class', 'trans-arrow'); | |
| path.setAttribute('id', `path-${gId}`); | |
| path.setAttribute('marker-end', 'url(#arrow-normal)'); | |
| svg.appendChild(path); | |
| const mlx = (sx + ex)/2 + ox*(curve ? 20:12); | |
| const mly = (sy + ey)/2 + oy*(curve ? 20:12); | |
| addTransLabel(svg, mlx, mly, labelText, gId); | |
| } | |
| }); | |
| // Draw state circles | |
| states.forEach(s => { | |
| const p = pos[s]; | |
| const isFinal = data.final_states.includes(s); | |
| const g = svgEl('g'); | |
| g.setAttribute('id', `state-g-${s}`); | |
| if (isFinal) { | |
| const outer = svgEl('circle'); | |
| outer.setAttribute('cx', p.x); outer.setAttribute('cy', p.y); | |
| outer.setAttribute('r', r + 6); | |
| outer.setAttribute('fill', 'none'); | |
| outer.setAttribute('stroke', 'rgba(0,230,118,.4)'); | |
| outer.setAttribute('stroke-width', '1.5'); | |
| g.appendChild(outer); | |
| } | |
| const circle = svgEl('circle'); | |
| circle.setAttribute('cx', p.x); circle.setAttribute('cy', p.y); | |
| circle.setAttribute('r', r); | |
| circle.setAttribute('class', `state-circle${isFinal ? ' accept':''}`); | |
| circle.setAttribute('id', `state-${s}`); | |
| g.appendChild(circle); | |
| const label = svgEl('text'); | |
| label.setAttribute('x', p.x); label.setAttribute('y', p.y); | |
| label.setAttribute('class', 'state-label'); | |
| label.textContent = s; | |
| g.appendChild(label); | |
| svg.appendChild(g); | |
| }); | |
| } | |
| function svgEl(tag) { | |
| return document.createElementNS('http://www.w3.org/2000/svg', tag); | |
| } | |
| function addTransLabel(svg, x, y, text, gId) { | |
| const el = svgEl('text'); | |
| el.setAttribute('x', x); el.setAttribute('y', y); | |
| el.setAttribute('class', 'trans-label'); | |
| el.setAttribute('id', `lbl-${gId}`); | |
| // Split long labels | |
| const parts = text.split(' | '); | |
| if (parts.length > 1) { | |
| parts.forEach((p, i) => { | |
| const t = svgEl('tspan'); | |
| t.setAttribute('x', x); t.setAttribute('dy', i === 0 ? '0' : '12'); | |
| t.textContent = p; | |
| el.appendChild(t); | |
| }); | |
| } else { | |
| el.textContent = text; | |
| } | |
| svg.appendChild(el); | |
| } | |
| // Highlight active state and transition in diagram | |
| function highlightDiagram(step) { | |
| if (!step) return; | |
| document.querySelectorAll('.state-circle').forEach(c => c.classList.remove('active')); | |
| document.querySelectorAll('.trans-arrow').forEach(a => a.classList.remove('active')); | |
| document.querySelectorAll('.trans-label').forEach(a => a.classList.remove('active')); | |
| const sc = document.getElementById(`state-${step.state}`); | |
| if (sc) sc.classList.add('active'); | |
| if (step.transition_applied) { | |
| // Parse transition label to find arrow group | |
| // Format: (cur_state, inp, stack_top) β (next_state, push) | |
| const m = step.transition_applied.match(/\((\w+),/); | |
| const m2 = step.transition_applied.match(/β \((\w+),/); | |
| if (m && m2 && diagramData) { | |
| const from = m[1], to = m2[1]; | |
| const key = `${from}__${to}`; | |
| const gId = `tg-${key.replace(/[^a-z0-9]/gi,'_')}`; | |
| const pathEl = document.getElementById(`path-${gId}`); | |
| const lblEl = document.getElementById(`lbl-${gId}`); | |
| if (pathEl) { pathEl.classList.add('active'); pathEl.setAttribute('marker-end','url(#arrow-active)'); } | |
| if (lblEl) lblEl.classList.add('active'); | |
| } | |
| } | |
| } | |
| // ββ Step Rendering ββββββββββββββββββββββββββββ | |
| function renderStep(idx) { | |
| if (!simSteps.length) return; | |
| if (idx < 0) idx = 0; | |
| if (idx >= simSteps.length) idx = simSteps.length - 1; | |
| curStep = idx; | |
| const step = simSteps[curStep]; | |
| document.getElementById('cur-step').textContent = `${curStep + 1} / ${simSteps.length}`; | |
| document.getElementById('cur-state').textContent = step.state; | |
| document.getElementById('cur-input').textContent = step.remaining_input; | |
| document.getElementById('cur-trans').textContent = step.transition_applied || 'β'; | |
| renderTape(step); | |
| renderStack(step.stack); | |
| highlightDiagram(step); | |
| // Timeline highlight | |
| document.querySelectorAll('.tl-step').forEach((el, i) => { | |
| el.classList.toggle('active-tl', i === curStep); | |
| }); | |
| // Button states | |
| document.getElementById('btnPrev').disabled = curStep === 0; | |
| document.getElementById('btnNext').disabled = curStep === simSteps.length - 1; | |
| } | |
| function renderTape(step) { | |
| const tape = document.getElementById('tape-display'); | |
| tape.innerHTML = ''; | |
| const inputStr = document.getElementById('input_string').value; | |
| const consumed = inputStr.length - (step.remaining_input === 'Ξ΅' ? 0 : step.remaining_input.length); | |
| if (!inputStr) { | |
| const cell = document.createElement('div'); | |
| cell.className = 'tape-cell'; cell.textContent = 'Ξ΅'; | |
| tape.appendChild(cell); return; | |
| } | |
| inputStr.split('').forEach((ch, i) => { | |
| const cell = document.createElement('div'); | |
| cell.className = 'tape-cell'; | |
| if (i < consumed) cell.classList.add('consumed'); | |
| else if (i === consumed) { | |
| cell.classList.add('current'); | |
| const ptr = document.createElement('div'); | |
| ptr.className = 'tape-pointer'; ptr.textContent = 'β²'; | |
| cell.appendChild(ptr); | |
| } | |
| cell.insertAdjacentText('afterbegin', ch); | |
| tape.appendChild(cell); | |
| }); | |
| } | |
| function renderStack(stack) { | |
| const sv = document.getElementById('stack-display'); | |
| sv.innerHTML = ''; | |
| if (!stack || !stack.length) { | |
| const el = document.createElement('div'); | |
| el.className = 'stack-cell'; el.textContent = '(empty)'; | |
| sv.appendChild(el); return; | |
| } | |
| stack.forEach((sym, i) => { | |
| const el = document.createElement('div'); | |
| el.className = 'stack-cell' + (i === stack.length - 1 ? ' top' : ''); | |
| el.textContent = sym; | |
| sv.appendChild(el); | |
| }); | |
| } | |
| function renderTimeline() { | |
| const tl = document.getElementById('timeline'); | |
| tl.innerHTML = ''; | |
| simSteps.forEach((step, i) => { | |
| const el = document.createElement('div'); | |
| el.className = 'tl-step' + (step.status === 'dead' || step.status === 'rejected' ? ' dead-tl' : ''); | |
| el.textContent = i + 1; | |
| el.title = `Step ${i+1}: ${step.state}`; | |
| el.onclick = () => renderStep(i); | |
| tl.appendChild(el); | |
| }); | |
| } | |
| function clearTapeStack() { | |
| document.getElementById('tape-display').innerHTML = ''; | |
| document.getElementById('stack-display').innerHTML = ''; | |
| } | |
| function resetCurrentPanel() { | |
| ['cur-step','cur-state','cur-input','cur-trans'].forEach(id => | |
| document.getElementById(id).textContent = 'β' | |
| ); | |
| } | |
| // ββ Playback controls βββββββββββββββββββββββββ | |
| function stepNext() { | |
| if (curStep < simSteps.length - 1) renderStep(curStep + 1); | |
| } | |
| function stepPrev() { | |
| if (curStep > 0) renderStep(curStep - 1); | |
| } | |
| function restartSim() { | |
| stopPlay(); | |
| renderStep(0); | |
| } | |
| function togglePlay() { | |
| if (playing) stopPlay(); else startPlay(); | |
| } | |
| function startPlay() { | |
| playing = true; | |
| const btn = document.getElementById('btnPlay'); | |
| btn.textContent = 'βΈ'; btn.classList.add('playing'); | |
| const delay = () => parseInt(document.getElementById('speedRange').value) || 800; | |
| const tick = () => { | |
| if (curStep >= simSteps.length - 1) { stopPlay(); return; } | |
| stepNext(); | |
| playTimer = setTimeout(tick, delay()); | |
| }; | |
| playTimer = setTimeout(tick, delay()); | |
| } | |
| function stopPlay() { | |
| playing = false; | |
| clearTimeout(playTimer); | |
| const btn = document.getElementById('btnPlay'); | |
| btn.textContent = 'βΆ'; btn.classList.remove('playing'); | |
| } | |
| // ββ Result Panel ββββββββββββββββββββββββββββββ | |
| function renderResult(data) { | |
| const icon = document.getElementById('result-icon'); | |
| const title = document.getElementById('result-title'); | |
| const desc = document.getElementById('result-desc'); | |
| const stats = document.getElementById('result-stats'); | |
| const last = simSteps[simSteps.length - 1] || {}; | |
| if (data.accepted) { | |
| icon.textContent = 'β'; | |
| icon.className = 'result-icon accepted'; | |
| title.textContent = 'String Accepted!'; | |
| desc.textContent = `The PDA successfully accepted the input string "${document.getElementById('input_string').value || 'Ξ΅'}" and reached a valid accepting configuration.`; | |
| title.style.color = 'var(--green)'; | |
| } else { | |
| icon.textContent = 'β'; | |
| icon.className = 'result-icon rejected'; | |
| title.textContent = 'String Rejected'; | |
| desc.textContent = `The PDA could not accept "${document.getElementById('input_string').value || 'Ξ΅'}". No valid path to an accepting configuration was found.`; | |
| title.style.color = 'var(--accent3)'; | |
| } | |
| stats.innerHTML = ` | |
| <div class="stat-item"><div class="stat-label">Final State</div><div class="stat-val">${last.state || 'β'}</div></div> | |
| <div class="stat-item"><div class="stat-label">Total Steps</div><div class="stat-val">${data.total_steps}</div></div> | |
| <div class="stat-item"><div class="stat-label">Final Stack</div><div class="stat-val">${(last.stack||[]).join('') || '(empty)'}</div></div> | |
| <div class="stat-item"><div class="stat-label">Remaining Input</div><div class="stat-val">${last.remaining_input || 'Ξ΅'}</div></div> | |
| `; | |
| // Navigate to result after a short delay | |
| setTimeout(() => navTo('result-section'), 600); | |
| } | |
| // ββ Init ββββββββββββββββββββββββββββββββββββββ | |
| window.addEventListener('DOMContentLoaded', () => { | |
| // Pre-load samples in background | |
| loadSamples(); | |
| // Mark home as active | |
| navTo('hero'); | |
| }); | |