Skip to content

Commit 2689959

Browse files
committed
Add Socket DFA
1 parent f1cb511 commit 2689959

7 files changed

Lines changed: 86 additions & 10 deletions

File tree

app.js

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,14 @@
137137
</div>
138138
<span class="editor-badge">Java</span>
139139
</div>
140+
${
141+
lesson.exercise.guide
142+
? `<figure class="exercise-guide">
143+
<img src="${escapeHtml(lesson.exercise.guide.image)}" alt="${escapeHtml(lesson.exercise.guide.alt)}" loading="lazy" decoding="async" />
144+
<figcaption>${escapeHtml(lesson.exercise.guide.caption)}</figcaption>
145+
</figure>`
146+
: ""
147+
}
140148
<label class="sr-only" for="code-${lesson.id}">Editable Java exercise</label>
141149
<textarea id="code-${lesson.id}" class="code-editor" spellcheck="false" aria-describedby="exercise-feedback-${lesson.id}">${escapeHtml(currentCode)}</textarea>
142150
<div class="editor-actions">

images/socket_dfa.png

152 KB
Loading

index.html

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
<meta name="twitter:description" content="Catch the bug before it runs with four guided LiquidJava exercises." />
1414
<link rel="icon" type="image/png" href="images/liquidjava-icon.png" />
1515
<link rel="stylesheet" href="vendor/codemirror.css" />
16-
<link rel="stylesheet" href="styles.css" />
16+
<link rel="stylesheet" href="styles.css?v=2" />
1717
<title>LiquidJava Interactive Tutorial</title>
1818
</head>
1919
<body>
@@ -63,7 +63,7 @@
6363
<script src="vendor/codemirror-closebrackets.js"></script>
6464
<script src="vendor/prism.js"></script>
6565
<script src="vendor/prism-java.min.js"></script>
66-
<script src="tutorial-data.js?v=2"></script>
67-
<script src="app.js?v=2"></script>
66+
<script src="tutorial-data.js?v=5"></script>
67+
<script src="app.js?v=5"></script>
6868
</body>
6969
</html>

package.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
"vendor:syntax": "node scripts/vendor-syntax.mjs",
88
"dev": "npm run vendor:syntax && python3 -m http.server 8000 --directory .",
99
"build": "npm run vendor:syntax && node scripts/build-site.mjs",
10-
"check": "node --check app.js && node --check tutorial-data.js"
10+
"check": "node --check app.js && node --check tutorial-data.js && node scripts/validate-content.mjs"
1111
},
1212
"dependencies": {
1313
"codemirror": "5.65.21",

scripts/validate-content.mjs

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
import { access, readFile } from "node:fs/promises";
2+
import { dirname, resolve } from "node:path";
3+
import { fileURLToPath } from "node:url";
4+
import vm from "node:vm";
5+
6+
const root = resolve(dirname(fileURLToPath(import.meta.url)), "..");
7+
const source = await readFile(resolve(root, "tutorial-data.js"), "utf8");
8+
const sandbox = { window: {} };
9+
10+
vm.runInNewContext(source, sandbox, { filename: "tutorial-data.js" });
11+
12+
const tutorial = sandbox.window.LIQUID_JAVA_TUTORIAL;
13+
const failures = [];
14+
15+
if (!tutorial?.lessons?.length) {
16+
failures.push("Tutorial data must contain at least one lesson.");
17+
}
18+
19+
for (const lesson of tutorial?.lessons ?? []) {
20+
const label = lesson.id || "unnamed lesson";
21+
22+
for (const check of lesson.exercise?.checks ?? []) {
23+
if (!new RegExp(check.pattern, "m").test(lesson.exercise.solutionCode)) {
24+
failures.push(`${label}: the provided solution fails the check “${check.message}”`);
25+
}
26+
}
27+
28+
if (lesson.exercise?.guide) {
29+
const guidePath = lesson.exercise.guide.image.split(/[?#]/)[0];
30+
try {
31+
await access(resolve(root, guidePath));
32+
} catch {
33+
failures.push(`${label}: guide image does not exist: ${guidePath}`);
34+
}
35+
}
36+
37+
for (const question of lesson.questions ?? []) {
38+
if (question.type === "radio") {
39+
if (!Array.isArray(question.choices) || !Number.isInteger(question.correct) || !question.choices[question.correct]) {
40+
failures.push(`${label}: radio question ${question.id} has an invalid correct answer.`);
41+
}
42+
} else if (question.type === "text") {
43+
if (!Array.isArray(question.accepted) || question.accepted.length === 0) {
44+
failures.push(`${label}: text question ${question.id} needs at least one accepted answer.`);
45+
}
46+
} else {
47+
failures.push(`${label}: question ${question.id} uses unsupported type ${question.type}.`);
48+
}
49+
}
50+
}
51+
52+
if (failures.length) {
53+
console.error(failures.join("\n"));
54+
process.exit(1);
55+
}
56+
57+
console.log(`Validated ${tutorial.lessons.length} lessons and their solutions.`);

styles.css

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -281,6 +281,9 @@ h1 span { color: var(--orange); }
281281
.workbench h2, .questions > h2 { margin: 0 0 10px; font-size: clamp(1.5rem, 3vw, 2.2rem); letter-spacing: -0.035em; }
282282
.workbench-head p:last-child { max-width: 700px; margin: 0 0 22px; color: var(--muted); }
283283
.editor-badge { padding: 5px 9px; color: #b6dcca; background: var(--code); border-radius: 6px; font-family: ui-monospace, monospace; font-size: 0.75rem; }
284+
.exercise-guide { margin: 0 0 24px; padding: clamp(14px, 2vw, 20px); background: var(--paper); border: 1px solid var(--line); border-radius: 12px; }
285+
.exercise-guide img { display: block; width: 100%; height: auto; border-radius: 8px; }
286+
.exercise-guide figcaption { margin-top: 12px; color: var(--muted); font-size: 0.88rem; line-height: 1.55; }
284287
.code-editor {
285288
display: block;
286289
width: 100%;

tutorial-data.js

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,13 @@ public class LightBulb {
192192
title: "Complete the socket transitions",
193193
prompt:
194194
"Replace the true refinements so bind, connect, sendUrgentData, and close follow the socket protocol.",
195+
guide: {
196+
image: "images/socket_dfa.png?v=20260809",
197+
alt:
198+
"Socket protocol diagram. A socket starts unconnected; bind moves it to bound; connect moves it to connected; sendUrgentData keeps it connected; and close moves any non-closed socket to closed.",
199+
caption:
200+
"Follow each arrow from its source state to its target state. For the sendUrgentData loop, a from-only refinement requires connected and leaves the socket connected.",
201+
},
195202
starterCode: `import java.net.SocketAddress;
196203
import liquidjava.specification.ExternalRefinementsFor;
197204
import liquidjava.specification.StateRefinement;
@@ -209,7 +216,7 @@ public interface SocketRefinements {
209216
@StateRefinement(from="true", to="true")
210217
public void connect(SocketAddress add);
211218
212-
@StateRefinement(from="true", to="true")
219+
@StateRefinement(from="true")
213220
public void sendUrgentData(int n);
214221
215222
@StateRefinement(from="true", to="true")
@@ -232,7 +239,7 @@ public interface SocketRefinements {
232239
@StateRefinement(from="bound(this)", to="connected(this)")
233240
public void connect(SocketAddress add);
234241
235-
@StateRefinement(from="connected(this)", to="closed(this)")
242+
@StateRefinement(from="connected(this)")
236243
public void sendUrgentData(int n);
237244
238245
@StateRefinement(from="!closed(this)", to="closed(this)")
@@ -248,8 +255,8 @@ public interface SocketRefinements {
248255
message: "connect should move the socket from bound to connected.",
249256
},
250257
{
251-
pattern: "@StateRefinement\\s*\\(\\s*from\\s*=\\s*\"connected\\(this\\)\"\\s*,\\s*to\\s*=\\s*\"closed\\(this\\)\"\\s*\\)\\s*public\\s+void\\s+sendUrgentData",
252-
message: "sendUrgentData should move a connected socket to closed.",
258+
pattern: "@StateRefinement\\s*\\(\\s*from\\s*=\\s*\"connected\\(this\\)\"\\s*(?:,\\s*to\\s*=\\s*\"connected\\(this\\)\"\\s*)?\\)\\s*public\\s+void\\s+sendUrgentData",
259+
message: "sendUrgentData should require a connected socket and leave it connected.",
253260
},
254261
{
255262
pattern: "@StateRefinement\\s*\\(\\s*from\\s*=\\s*\"!closed\\(this\\)\"\\s*,\\s*to\\s*=\\s*\"closed\\(this\\)\"\\s*\\)\\s*public\\s+void\\s+close",
@@ -271,12 +278,13 @@ public interface SocketRefinements {
271278
type: "radio",
272279
prompt: "Which sequence follows the protocol?",
273280
choices: [
274-
"Socket(); bind(); connect(); close();",
281+
"Socket(); bind(); connect(); sendUrgentData(1); close();",
275282
"Socket(); connect(); bind();",
276283
"Socket(); bind(); bind();",
277284
],
278285
correct: 0,
279-
explanation: "A socket starts unconnected, then moves through bound and connected before closing.",
286+
explanation:
287+
"After bind and connect, sendUrgentData is allowed and leaves the socket connected, so close is still valid.",
280288
},
281289
],
282290
},

0 commit comments

Comments
 (0)