Skip to content

Commit aa71db8

Browse files
rnbguyrnbguy
committed
fix verify output flow
1 parent 85b89ef commit aa71db8

File tree

3 files changed

+139
-64
lines changed

3 files changed

+139
-64
lines changed

‎islands/PlaygroundBody.tsx‎

Lines changed: 115 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import { useEffect, useRef } from "preact/hooks";
2-
import { computed, signal } from "@preact/signals";
2+
import { useSignal } from "@preact/signals";
33
import * as yaml from "@std/yaml";
44

55
interface PlaygroundProps {
@@ -11,9 +11,29 @@ interface PlaygroundProps {
1111

1212
type PingResponse =
1313
| { status: "ok" }
14-
| { status: "error"; message?: string; error?: string };
14+
| {
15+
status: "error";
16+
message: string;
17+
source: "frontend error" | "frontend api error" | "apalache server down";
18+
};
1519
type VerifyResponse = Record<string, unknown>;
1620

21+
function extractApiMessage(payload: unknown): string | null {
22+
if (!payload || typeof payload !== "object") {
23+
return null;
24+
}
25+
26+
const record = payload as Record<string, unknown>;
27+
if (typeof record.message === "string") {
28+
return record.message;
29+
}
30+
if (typeof record.error === "string") {
31+
return record.error;
32+
}
33+
34+
return null;
35+
}
36+
1737
type MonacoEditor = {
1838
getValue: () => string;
1939
setValue: (value: string) => void;
@@ -419,37 +439,12 @@ export default function PlaygroundBody(props: PlaygroundProps) {
419439
const editor = useRef<MonacoEditor | null>(null);
420440
const pollingTimerRef = useRef<number | null>(null);
421441

422-
const loadingText = signal("");
423-
const consoleText = signal("");
424-
const errorText = signal("");
425-
426-
const selectedInv = signal("");
427-
const allInvs = signal<string[]>([]);
428-
429-
const allInvsOption = computed(() => {
430-
const options = [
431-
<option
432-
key="placeholder"
433-
value=""
434-
disabled
435-
selected={!(allInvs.value && allInvs.value.includes(selectedInv.value))}
436-
>
437-
Select an invariant
438-
</option>,
439-
];
440-
441-
if (allInvs.value && allInvs.value.length > 0) {
442-
options.push(
443-
...allInvs.value.map((inv) => (
444-
<option value={inv} key={inv}>
445-
{inv}
446-
</option>
447-
)),
448-
);
449-
}
442+
const loadingText = useSignal("");
443+
const consoleText = useSignal(props.out);
444+
const errorText = useSignal("");
450445

451-
return options;
452-
});
446+
const selectedInv = useSignal(props.inv);
447+
const allInvs = useSignal<string[]>(props.invs);
453448
useEffect(() => {
454449
let isDisposed = false;
455450

@@ -458,7 +453,12 @@ export default function PlaygroundBody(props: PlaygroundProps) {
458453
if (rawStoredSnippet) {
459454
try {
460455
const parsed = JSON.parse(rawStoredSnippet) as PlaygroundProps;
461-
if (parsed.tla.length > 0) {
456+
if (
457+
parsed.tla.length > 0 &&
458+
Array.isArray(parsed.invs) &&
459+
parsed.invs.length > 0 &&
460+
typeof parsed.inv === "string"
461+
) {
462462
initTla = parsed;
463463
}
464464
} catch {
@@ -599,31 +599,56 @@ export default function PlaygroundBody(props: PlaygroundProps) {
599599

600600
async function ping(): Promise<PingResponse> {
601601
try {
602-
return await fetch("/api/ping", {
602+
const response = await fetch("/api/ping", {
603603
method: "GET",
604604
headers: {
605605
"Content-Type": "application/json",
606606
},
607-
}).then((resp) => resp.json() as Promise<PingResponse>);
607+
});
608+
609+
const payload = await response.json();
610+
if (!response.ok) {
611+
const message = extractApiMessage(payload) ??
612+
`Ping API failed with status ${response.status}`;
613+
const source = message.includes("Apalache server unavailable")
614+
? "apalache server down"
615+
: "frontend api error";
616+
console.error(`[${source}] ${message}`);
617+
return { status: "error", message, source };
618+
}
619+
620+
return payload as PingResponse;
608621
} catch (error) {
622+
console.error("[frontend error] Failed to call /api/ping", error);
609623
return {
610624
status: "error",
611625
message: error instanceof Error ? error.message : String(error),
626+
source: "frontend error",
612627
};
613628
}
614629
}
615630

616631
async function tlaInvariants(data: { tla: string }): Promise<string[]> {
617632
try {
618-
return await fetch("/api/invariants", {
633+
const response = await fetch("/api/invariants", {
619634
method: "POST",
620635
headers: {
621636
"Content-Type": "application/json",
622637
},
623638
body: JSON.stringify(data),
624-
}).then((resp) => resp.json());
639+
});
640+
641+
if (!response.ok) {
642+
const payload = await response.json();
643+
const message = extractApiMessage(payload) ??
644+
`Invariants API failed with status ${response.status}`;
645+
console.error(`[frontend api error] ${message}`);
646+
return [];
647+
}
648+
649+
return await response.json();
625650
} catch (error) {
626-
console.error(error);
651+
console.error("[frontend error] Failed to call /api/invariants", error);
627652
return [];
628653
}
629654
}
@@ -632,14 +657,24 @@ export default function PlaygroundBody(props: PlaygroundProps) {
632657
data: { tla: string; inv: string },
633658
): Promise<VerifyResponse> {
634659
try {
635-
return await fetch("/api/verify", {
660+
const response = await fetch("/api/verify", {
636661
method: "POST",
637662
headers: {
638663
"Content-Type": "application/json",
639664
},
640665
body: JSON.stringify(data),
641-
}).then((resp) => resp.json() as Promise<VerifyResponse>);
666+
});
667+
668+
const payload = await response.json();
669+
if (!response.ok) {
670+
const message = extractApiMessage(payload) ??
671+
`Verify API failed with status ${response.status}`;
672+
console.error(`[frontend api error] ${message}`);
673+
}
674+
675+
return payload as VerifyResponse;
642676
} catch (error) {
677+
console.error("[frontend error] Failed to call /api/verify", error);
643678
return { error: error instanceof Error ? error.message : String(error) };
644679
}
645680
}
@@ -655,32 +690,45 @@ export default function PlaygroundBody(props: PlaygroundProps) {
655690
const pingResp = await ping();
656691
if (pingResp.status !== "ok") {
657692
consoleText.value = "";
658-
errorText.value = "> Apalache server is down !";
693+
errorText.value = `> ${pingResp.message}`;
659694
return;
660695
}
661696

662697
const invariants = await tlaInvariants({ tla });
663698

664699
allInvs.value = invariants;
665700

666-
if (invariants.includes(selectedInv.value)) {
667-
// const spinner = new Spinner(["⣾", "⣽", "⣻", "⢿", "⡿", "⣟", "⣯", "⣷"]);
668-
const spinner = new Spinner(["...", " ..", ". .", ".. "]);
669-
errorText.value = "";
670-
consoleText.value = "";
701+
const invariantToVerify = invariants.includes(selectedInv.value)
702+
? selectedInv.value
703+
: (invariants[0] ?? "");
671704

672-
const spinnerTimer = globalThis.setInterval(() => {
673-
loadingText.value = `> processing ${spinner.next()}`;
674-
}, 200);
705+
if (!invariantToVerify) {
675706
consoleText.value = "";
676-
const data = { tla, inv: selectedInv.value };
677-
const respJson = await tlaVerify(data);
707+
errorText.value = "> No invariant available to verify";
708+
return;
709+
}
678710

679-
globalThis.clearInterval(spinnerTimer);
680-
loadingText.value = "";
711+
selectedInv.value = invariantToVerify;
681712

682-
consoleText.value = yaml.stringify(respJson, { indent: 2 });
683-
}
713+
// const spinner = new Spinner(["⣾", "⣽", "⣻", "⢿", "⡿", "⣟", "⣯", "⣷"]);
714+
const spinner = new Spinner(["...", " ..", ". .", ".. "]);
715+
errorText.value = "";
716+
consoleText.value = "";
717+
718+
const spinnerTimer = globalThis.setInterval(() => {
719+
loadingText.value = `> processing ${spinner.next()}`;
720+
}, 200);
721+
consoleText.value = "";
722+
const data = { tla, inv: invariantToVerify };
723+
const respJson = await tlaVerify(data);
724+
725+
globalThis.clearInterval(spinnerTimer);
726+
loadingText.value = "";
727+
728+
const rendered = yaml.stringify(respJson, { indent: 2 }).trim();
729+
consoleText.value = rendered.length > 0
730+
? rendered
731+
: JSON.stringify(respJson, null, 2);
684732
};
685733

686734
return (
@@ -693,7 +741,18 @@ export default function PlaygroundBody(props: PlaygroundProps) {
693741
selectedInv.value = e.currentTarget.value;
694742
}}
695743
>
696-
{allInvsOption}
744+
<option
745+
key="placeholder"
746+
value=""
747+
disabled
748+
>
749+
Select an invariant
750+
</option>
751+
{allInvs.value.map((inv) => (
752+
<option value={inv} key={inv}>
753+
{inv}
754+
</option>
755+
))}
697756
</select>
698757
<button
699758
type="button"

‎routes/api/ping.ts‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,27 @@
11
import { define } from "../../utils.ts";
2+
import { refreshSharedApalache } from "../../utils/apalache_shared.ts";
23

34
export const handler = define.handlers({
45
async GET(ctx): Promise<Response> {
6+
let apalache = ctx.state.apalache;
7+
58
try {
6-
const apalache = ctx.state.apalache;
79
if (!apalache) {
8-
return Response.json(
9-
{ status: "error", message: "Apalache server unavailable" },
10-
{ status: 503 },
11-
);
10+
apalache = await refreshSharedApalache();
1211
}
12+
1313
await apalache.ping();
1414
return Response.json({ status: "ok" });
15-
} catch (error) {
16-
const message = error instanceof Error ? error.message : String(error);
17-
return Response.json({ status: "error", message }, { status: 503 });
15+
} catch {
16+
try {
17+
const refreshedApalache = await refreshSharedApalache();
18+
ctx.state.apalache = refreshedApalache;
19+
await refreshedApalache.ping();
20+
return Response.json({ status: "ok" });
21+
} catch (error) {
22+
const message = error instanceof Error ? error.message : String(error);
23+
return Response.json({ status: "error", message }, { status: 503 });
24+
}
1825
}
1926
},
2027
});

‎utils/apalache_shared.ts‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,3 +43,12 @@ export function getSharedApalache(): Promise<Apalache> {
4343

4444
return sharedApalachePromise;
4545
}
46+
47+
export function resetSharedApalache(): void {
48+
sharedApalachePromise = null;
49+
}
50+
51+
export async function refreshSharedApalache(): Promise<Apalache> {
52+
resetSharedApalache();
53+
return await getSharedApalache();
54+
}

0 commit comments

Comments
 (0)