Use EJS and vscode-elements in Verify tab (IC3)

package.json

@@ -46,6 +46,7 @@
     "dependencies": {
         "@types/ejs": "^3.1.5",
         "@vscode-elements/elements": "^2.3.1",
+        "@vscode/codicons": "^0.0.44",
         "axios": "^1.9.0",
         "chalk": "~5.6.0",
         "commander": "~11.0.0",

src/extension/cex.ts

@@ -32,32 +32,3 @@ export function renderStep(trace: Step[], x: Step) {
     return render;
 }
 
-export function formatStep(render: State) {
-    return `
-<table>
-${Object.keys(render).sort().map(agent => (
-    `<tr key=${agent}>
-        <td>${agent}:</td>
-        <td><span>${
-        Object.keys(render[agent])
-        .sort()
-        .filter(k => (k === "**state**") || !k.startsWith("**"))
-        .map(k => `${(k === "**state**") ? "<em>state</em>" : k}: ${render[agent][k]}`)
-        .filter(s => s.trim().length > 0)
-        .join(", ")
-        }</span></td>
-    </tr>`
-)).join("\n")}
-</table>`
-}
-
-export function formatTransition(t: Transition) {
-    const isSupplyGet = t.hasOwnProperty("___get-supply___");
-    return `<table>
-      <tr><td><em>${isSupplyGet ? "Supplier" : "Sender"}: </em></td>
-      <td>${t.sender}</td></tr>
-      <tr><td><em>Command: </em></td><td><pre>${t.send}</pre></td></tr>
-      <tr><td><em>${isSupplyGet ? "Getter" : "Receivers"}: </em></td>
-      <td>${t.receivers.join(", ")}</td></tr>
-    </table>`
-  }

src/extension/common.ts

@@ -54,13 +54,19 @@ export async function renderTemplate(ctx: vscode.ExtensionContext, fname: string
     const elementsUri = webview.asWebviewUri(
         vscode.Uri.joinPath(
             ctx.extensionUri,
-            "node_modules",
-            "@vscode-elements/elements",
-            "dist",
-            "bundled.js"
+            "node_modules", "@vscode-elements",
+            "elements", "dist", "bundled.js"
+        )
+    );
+    const codiconsUri = webview.asWebviewUri(
+        vscode.Uri.joinPath(
+            ctx.extensionUri,
+            "node_modules", "@vscode", "codicons",
+            "dist", "codicon.css"
         )
     );
     data["elementsUri"] = elementsUri;
+    data["codiconsUri"] = codiconsUri;
     data["cspSource"] = webview.cspSource;
     const html = ejs.renderFile(filePath, data);
     return html;

src/extension/html/_step.html

@@ -0,0 +1,38 @@
+{% if (transition != undefined) { %}
+<vscode-table-row>
+    <vscode-table-cell></vscode-table-cell>
+    <vscode-table-cell>
+<table>
+    <tr><td><em>{%= isSupplyGet ? "Supplier" : "Sender" %}: </em></td>
+    <td>{%= transition.sender %}</td></tr>
+    <tr><td><em>Command: </em></td><td><pre>{%= transition.send %}</pre></td></tr>
+    <tr><td><em>{%= isSupplyGet ? "Getter" : "Receivers" %}: </em></td>
+    <td>{%= transition.receivers.join(", ") %}</td></tr>
+</table>
+    </vscode-table-cell>
+</vscode-table-row>
+{% } %}
+<vscode-table-row>
+<vscode-table-cell>
+{%= depth %}
+{% if (loop) { %}<br /><em>Loop starts here</em>{% } %}
+{% if (deadlock) { %}<br /><em>Deadlock state</em>{% } %} 
+</vscode-table-cell>
+<vscode-table-cell>
+<table>
+    {% Object.keys(step).sort().forEach(function(agent) { %}
+    <tr key="{%= agent %}"></tr>
+    <td>{%= agent %}:</td>
+    <td><span>
+        {% Object.keys(step[agent]).filter(k => (k === "**state**") || !k.startsWith("**")).sort().forEach(function(varName) { %}
+        <div>{% if (varName === "**state**") { %}
+        <em>state</em>
+        {% } else { %}
+        {%= varName %}
+        {% } %}: {%= step[agent][varName] %}</div>
+        {% }); %}
+    </span></td>
+    {% }); %}
+</table>
+</vscode-table-cell>
+</vscode-table-row>

src/extension/html/_verify.single.html

@@ -0,0 +1,21 @@
+<h2>{%= spec %}
+{% if (isTrue) { %} ✅
+{% } else if (isFalse) { %} ❌
+{% } else { %} ❔ {% } %}
+</h2>
+
+<vscode-table zebra bordered-rows resizable columns='["10%", "90%"]' min-column-width="5px">
+<vscode-table-header slot="header">
+<vscode-table-header-cell >#</vscode-table-header-cell >
+<vscode-table-header-cell >Changed Variables</vscode-table-header-cell >
+</vscode-table-header>
+<vscode-table-body slot="body" id="steps">
+    {%- tbody %}
+</vscode-table-body>
+</vscode-table>
+
+<div>
+    <vscode-collapsible heading="Full output">
+        <pre>{%= output %}</pre>
+    </vscode-collapsible>
+</div>

src/extension/html/simulate.html

@@ -4,7 +4,7 @@
 <head>
     <meta charset="UTF-8">
     <meta name="viewport" content="width=device-width, initial-scale=1.0">
-    <title>Simulator: {%=fname%}</title>
+    <title>R-CHECK simulator: {%=fname%}</title>
     <script type="module" src="{%= elementsUri %}"></script>
     <style>
         .scrollable-table {

src/extension/html/verify.html

@@ -0,0 +1,15 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
+    <title>R-CHECK: Verification of {%= fname %} (IC3)</title>
+    <script type="module" src="{%= elementsUri %}"></script>
+    <link rel="stylesheet" href="{%= codiconsUri %}" id="vscode-codicon-stylesheet">
+</head>
+<body>
+    <h1>R-CHECK: Verification of {%= fname %} (IC3)</h1>
+    {% if (body != undefined) { %}{%- body %}
+    {% } else { %}<vscode-icon name="loading" spin spin-duration="1" size="48"></vscode-icon>{% } %}
+</body>
+</html>

src/extension/verify.ts

@@ -3,13 +3,16 @@ import * as vscode from "vscode";
 import { Temp } from "./temp.js";
 import { writeFileSync } from "node:fs";
 import { integer } from "vscode-languageserver";
-import { execPromise, ExecResult, getCurrentRcpFile, readPromise, runJar, writePromise } from "./common.js";
-import { formatStep, formatTransition, renderStep, Step } from "./cex.js";
+import { execPromise, ExecResult, getCurrentRcpFile, readPromise, renderTemplate, runJar, writePromise } from "./common.js";
+import { renderStep, Step } from "./cex.js";
 
 let temp: Temp
 let channel: vscode.OutputChannel
+let ctx: vscode.ExtensionContext
+let panel: vscode.WebviewPanel
 
 export class Verify {
+
     constructor(t: Temp, chan: vscode.OutputChannel) {
         channel = chan;
         temp = t;
@@ -61,6 +64,7 @@ export class Verify {
                 .catch(vscode.window.showErrorMessage);
             })
         );
+        ctx = context;
     }
 }
 
@@ -94,22 +98,26 @@ async function findSpecs(value: ExecResult) {
  * Launch verification tasks
  */
 async function verifySpecsIc3(fname:string, json: string, v: [string, ExecResult]) {
+    panel = vscode.window.createWebviewPanel(
+        "verificationResults",
+        "Verification Results",
+        vscode.ViewColumn.Active,
+        {enableScripts: true, retainContextWhenHidden: true}
+    );
+    const tmpHtml = await renderTemplate(
+        ctx, "verify.html", {
+            fname: fname,
+            body: undefined
+        },
+        panel.webview);
+    panel.webview.html = tmpHtml;
+
     const specs = v[1].stdout.trim().replace("\n", "").split("--").slice(1)
     channel.show();
     channel.appendLine(`[${fname}] Model checking started...`);
-    const title = `R-CHECK: Verification of ${fname}`
-    let htmlReport =  `<!DOCTYPE html>
-<html lang="en">
-<head>
-    <meta charset="UTF-8">
-    <meta name="viewport" content="width=device-width, initial-scale=1.0">
-    <title>${title}</title>
-</head>
-<body>
-    <h1>${title}</h1>`
-
+
     let count = 0;
-    const html = await Promise
+    const body = await Promise
         .all(specs.map(async (element, index) => {
             const split = element.split("LTLSPEC").map((x) => x.trim());
             const nuxmvOutput = await ic3(v[0], index, split[1]);
@@ -118,63 +126,64 @@ async function verifySpecsIc3(fname:string, json: string, v: [string, ExecResult
         }))
         .then(outputs => {
             channel.appendLine(`[${fname}] Done.`);
-            return `${htmlReport}${outputs.join("")}</body></html>`;
+            return outputs.join("");
         });
-    const panel = vscode.window.createWebviewPanel(
-        "verificationResults",
-        "Verification Results",
-        vscode.ViewColumn.Active
-    );
-    panel.webview.html = html;
+        panel.webview.html = await renderTemplate(
+            ctx, "verify.html", {
+                fname: fname,
+                body: body
+            },
+            panel.webview);
 }
 
 async function formatNuXmvOutput(spec: string, json: string, out: string) {
-    const isTrue = out.indexOf("is true") > -1
-    const isFalse = out.indexOf("is false") > -1
-    const emoji = isTrue ? "✅" : isFalse ? "❌" : "❔"
+    const isTrue = out.indexOf("is true") > -1;
+    const isFalse = out.indexOf("is false") > -1;
+
+    const lines = out
+        .split('\n')
+        .filter(x => !x.startsWith("***") && !x.startsWith("-- no proof or counterexample found"))
+        .map(x => x.trim())
+        .filter(x => x);
+
     let table = "";
     if (isFalse) {
         const cexFile = temp.makeFile("cex", ".txt");
         // TODO promisify this
-        const tbody = await writePromise(cexFile, out)
+        table = await writePromise(cexFile, out)
             .then(() => runJar(["-j", json, "-cex", cexFile]))
             .then(v => JSON.parse(v.stdout), channel.appendLine)
-            .then((cex: Step[]) => cex.map(s => {
-                    const tr = (
-                        s.inboundTransition != undefined
-                        ? `<tr><td></td><td>${formatTransition(s.inboundTransition)}</td></tr>`
-                        : "")
-                    const fmtLoop = s.___LOOP___ && !s.___DEADLOCK___ ? "<br /><em>Loop starts here</em>" : "";
-                    const fmtDeadlock = s.___DEADLOCK___ ? "<br /><em>Deadlock state</em>" : "";
-                    return `${tr}<tr><td>${s.depth}${fmtLoop}${fmtDeadlock}</td><td>${formatStep(renderStep(cex, s))}</td></tr>`
-                }))
+            .then((cex: Step[]) => cex.map(async s => {
+                const render = await renderTemplate(
+                    ctx, "_step.html", 
+                    {
+                        deadlock: s.___DEADLOCK___,
+                        depth: s.depth,
+                        isSupplyGet: s.inboundTransition?.hasOwnProperty("___get-supply___"),
+                        loop: s.___LOOP___ && !s.___DEADLOCK___,
+                        step: renderStep(cex, s),
+                        transition: s.inboundTransition
+                    },
+                    panel.webview);
+                return render;
+            }))
+            .then(outputs => Promise.all(outputs))
             .catch((e) => {
                 channel.appendLine(e);
                 return [];
             })
             .then(s => s.join("\n"));
-        table = tbody === "" ? "" : `
-<table striped bordered hover>
-<thead>
-<tr>
-<th>#Step</th>
-<th>Changed Variables</th>
-</tr>
-</thead>
-<tbody>${tbody}</tbody></table>`
     }
-
-    const lines = out
-        .split('\n')
-        .filter(x => !x.startsWith("***") && !x.startsWith("-- no proof or counterexample found"))
-        .map(x => x.trim())
-        .filter(x => x);
-    return `<h2>${spec} ${emoji}</h2>
-${table}
-<details>
-<summary>Full output</summary>
-<pre>${lines.join("\n")}</pre>
-</details>`;
+    const render = await renderTemplate(
+        ctx, "_verify.single.html", 
+        {
+        tbody: table,
+        spec: spec,
+        isTrue: isTrue,
+        isFalse: isFalse,
+        output: lines.join("\n")
+        }, panel.webview);
+    return render;
 }
 
 /**
@@ -257,7 +266,8 @@ async function verifySpecsBmc(fname:string, json: string, bound: integer, v: [st
     const panel = vscode.window.createWebviewPanel(
         "verificationResults",
         "Verification Results",
-        vscode.ViewColumn.Active
+        vscode.ViewColumn.Active,
+        {enableScripts: true, retainContextWhenHidden: true}
     );
     panel.webview.html = html;
 }