From 5c3eb51b6b890b7e78ec52ed0e57c2c1f1fb020e Mon Sep 17 00:00:00 2001
From: Luca Di Stefano <luca.di.stefano@tuwien.ac.at>
Date: Sat, 21 Feb 2026 18:16:04 +0100
Subject: [PATCH 1/3] Use EJS and vscode-elements in Verify tab (IC3)

---
 src/extension/cex.ts                   |  29 ------
 src/extension/common.ts                |  14 ++-
 src/extension/html/_step.html          |  38 ++++++++
 src/extension/html/_verify.single.html |  21 +++++
 src/extension/html/simulate.html       |   2 +-
 src/extension/html/verify.html         |  15 +++
 src/extension/verify.ts                | 122 +++++++++++++------------
 7 files changed, 151 insertions(+), 90 deletions(-)
 create mode 100644 src/extension/html/_step.html
 create mode 100644 src/extension/html/_verify.single.html
 create mode 100644 src/extension/html/verify.html

diff --git a/src/extension/cex.ts b/src/extension/cex.ts
index 017d56b..5480794 100644
--- a/src/extension/cex.ts
+++ b/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>`
-  }
diff --git a/src/extension/common.ts b/src/extension/common.ts
index 6b74cdf..2d80a50 100644
--- a/src/extension/common.ts
+++ b/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;
diff --git a/src/extension/html/_step.html b/src/extension/html/_step.html
new file mode 100644
index 0000000..bcd5376
--- /dev/null
+++ b/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>
\ No newline at end of file
diff --git a/src/extension/html/_verify.single.html b/src/extension/html/_verify.single.html
new file mode 100644
index 0000000..476acb8
--- /dev/null
+++ b/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>
\ No newline at end of file
diff --git a/src/extension/html/simulate.html b/src/extension/html/simulate.html
index f04f6a0..c017118 100644
--- a/src/extension/html/simulate.html
+++ b/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 {
diff --git a/src/extension/html/verify.html b/src/extension/html/verify.html
new file mode 100644
index 0000000..d380925
--- /dev/null
+++ b/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>
\ No newline at end of file
diff --git a/src/extension/verify.ts b/src/extension/verify.ts
index 8bc5574..9abf06d 100644
--- a/src/extension/verify.ts
+++ b/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;
 }

From 63e7f9a4f1a13a662d3af17e3debe4673a0418cc Mon Sep 17 00:00:00 2001
From: Luca Di Stefano <luca.di.stefano@tuwien.ac.at>
Date: Sun, 22 Feb 2026 16:22:15 +0100
Subject: [PATCH 2/3] Add codicons dependency

---
 package-lock.json | 8 ++++----
 package.json      | 1 +
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/package-lock.json b/package-lock.json
index 0f89c5e..3b6f35f 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -1,15 +1,16 @@
 {
     "name": "rcheck",
-    "version": "0.0.1",
+    "version": "0.1.0",
     "lockfileVersion": 3,
     "requires": true,
     "packages": {
         "": {
             "name": "rcheck",
-            "version": "0.0.1",
+            "version": "0.1.0",
             "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",
@@ -2537,8 +2538,7 @@
             "version": "0.0.44",
             "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.44.tgz",
             "integrity": "sha512-F7qPRumUK3EHjNdopfICLGRf3iNPoZQt+McTHAn4AlOWPB3W2kL4H0S7uqEqbyZ6rCxaeDjpAn3MCUnwTu/VJQ==",
-            "license": "CC-BY-4.0",
-            "peer": true
+            "license": "CC-BY-4.0"
         },
         "node_modules/@vscode/iconv-lite-umd": {
             "version": "0.7.0",
diff --git a/package.json b/package.json
index f4e6343..38524d6 100644
--- a/package.json
+++ b/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",

From fb18bb012c51cd0356876dc3c0a5113ac3698dd9 Mon Sep 17 00:00:00 2001
From: Luca Di Stefano <luca.di.stefano@tuwien.ac.at>
Date: Sun, 22 Feb 2026 16:49:51 +0100
Subject: [PATCH 3/3] Use new Verify UI for BMC

---
 src/extension/html/_verify.single.html |   2 +
 src/extension/html/verify.html         |   5 +-
 src/extension/verify.ts                | 182 +++++++++++--------------
 3 files changed, 83 insertions(+), 106 deletions(-)

diff --git a/src/extension/html/_verify.single.html b/src/extension/html/_verify.single.html
index 476acb8..0a65769 100644
--- a/src/extension/html/_verify.single.html
+++ b/src/extension/html/_verify.single.html
@@ -4,6 +4,7 @@ <h2>{%= spec %}
 {% } else { %} ❔ {% } %}
 </h2>
 
+{% if (tbody) { %}
 <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 >
@@ -13,6 +14,7 @@ <h2>{%= spec %}
     {%- tbody %}
 </vscode-table-body>
 </vscode-table>
+{% } %}
 
 <div>
     <vscode-collapsible heading="Full output">
diff --git a/src/extension/html/verify.html b/src/extension/html/verify.html
index d380925..98e40bf 100644
--- a/src/extension/html/verify.html
+++ b/src/extension/html/verify.html
@@ -3,12 +3,13 @@
 <head>
     <meta charset="UTF-8">
     <meta name="viewport" content="width=device-width, initial-scale=1.0">
-    <title>R-CHECK: Verification of {%= fname %} (IC3)</title>
+    <title>R-CHECK: Verification of {%= fname %} ({%= subtitle %})</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>
+    <h1>R-CHECK: Verification of {%= fname %}</h1>
+    <p>{%= subtitle %}</p>
     {% if (body != undefined) { %}{%- body %}
     {% } else { %}<vscode-icon name="loading" spin spin-duration="1" size="48"></vscode-icon>{% } %}
 </body>
diff --git a/src/extension/verify.ts b/src/extension/verify.ts
index 9abf06d..55cc1fe 100644
--- a/src/extension/verify.ts
+++ b/src/extension/verify.ts
@@ -28,13 +28,13 @@ export class Verify {
                 const rcpPath = getCurrentRcpFile()!;
                 const tmpJson = await temp.toJson(rcpPath);
                 check()
-                .then(() => runJar(["-j", tmpJson, "--smv", "-tmp"]))
-                .then(findSpecs)
-                .then(value => verifySpecsIc3(rcpPath, tmpJson, value))
-                .catch(vscode.window.showErrorMessage)
+                    .then(() => runJar(["-j", tmpJson, "--smv", "-tmp"]))
+                    .then(findSpecs)
+                    .then(value => verifySpecsIc3(rcpPath, tmpJson, value))
+                    .catch(vscode.window.showErrorMessage)
             }),
             vscode.commands.registerCommand('rcheck.verify-bmc', async () => {
-                
+
                 const rcpPath = getCurrentRcpFile()!;
                 const tmpJson = await temp.toJson(rcpPath);
                 const boundString = await vscode.window.showInputBox({
@@ -45,23 +45,23 @@ export class Verify {
                 });
                 const bound = boundString === '' ? 20 : parseInt(boundString!);
                 check()
-                .then(() => runJar(["-j", tmpJson, "--smv", "-tmp"]))
-                .then(findSpecs)
-                .then(value => verifySpecsBmc(rcpPath, tmpJson, bound, value))
-                .catch(vscode.window.showErrorMessage)
+                    .then(() => runJar(["-j", tmpJson, "--smv", "-tmp"]))
+                    .then(findSpecs)
+                    .then(value => verifySpecsBmc(rcpPath, tmpJson, bound, value))
+                    .catch(vscode.window.showErrorMessage)
             }),
             vscode.commands.registerCommand('rcheck.tosmv', async () => {
                 const rcpPath = getCurrentRcpFile()!;
                 temp.toJson(rcpPath)
-                .then((tmpJson) => runJar(["-j", tmpJson, "--smv", "-tmp"]))
-                .then(value => {
-                    const smvFile = value.stderr.trim();
-                    temp.addFile(smvFile);
-                    return smvFile;
-                })
-                .then(readPromise)
-                .then(showSmv)
-                .catch(vscode.window.showErrorMessage);
+                    .then((tmpJson) => runJar(["-j", tmpJson, "--smv", "-tmp"]))
+                    .then(value => {
+                        const smvFile = value.stderr.trim();
+                        temp.addFile(smvFile);
+                        return smvFile;
+                    })
+                    .then(readPromise)
+                    .then(showSmv)
+                    .catch(vscode.window.showErrorMessage);
             })
         );
         ctx = context;
@@ -73,13 +73,13 @@ async function showSmv(content: string) {
         "language": "nuxmv",
         "content": content
     })
-    .then(doc => vscode.window.showTextDocument(doc));
+        .then(doc => vscode.window.showTextDocument(doc));
 }
 
 async function check() {
     return new Promise<void>((resolve, reject) => {
         execFile("which", ["nuxmv"], (err, _) => {
-            if (err) {reject("This command requires nuxmv.")}
+            if (err) { reject("This command requires nuxmv.") }
             else resolve();
         });
     });
@@ -94,21 +94,26 @@ async function findSpecs(value: ExecResult) {
     return Promise.all([Promise.resolve(smvFile), execPromise("grep", ["-B", "1", "^LTLSPEC", smvFile])]);
 }
 
+async function verifySpecsIc3(fname: string, json: string, v: [string, ExecResult]) {
+    verifySpecs(fname, json, ic3, v, "IC3");
+}
+
 /**
  * Launch verification tasks
  */
-async function verifySpecsIc3(fname:string, json: string, v: [string, ExecResult]) {
+async function verifySpecs(fname: string, json: string, fn: Function, v: [string, ExecResult], subtitle: string) {
     panel = vscode.window.createWebviewPanel(
         "verificationResults",
         "Verification Results",
         vscode.ViewColumn.Active,
-        {enableScripts: true, retainContextWhenHidden: true}
+        { enableScripts: true, retainContextWhenHidden: true }
     );
     const tmpHtml = await renderTemplate(
         ctx, "verify.html", {
-            fname: fname,
-            body: undefined
-        },
+        fname: fname,
+        subtitle: subtitle,
+        body: undefined
+    },
         panel.webview);
     panel.webview.html = tmpHtml;
 
@@ -120,7 +125,7 @@ async function verifySpecsIc3(fname:string, json: string, v: [string, ExecResult
     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]);
+            const nuxmvOutput = await fn(v[0], index, split[1]);
             channel.appendLine(`[${fname}] ${++count}/${specs.length} done...`)
             return formatNuXmvOutput(split[0], json, nuxmvOutput);
         }))
@@ -128,12 +133,13 @@ async function verifySpecsIc3(fname:string, json: string, v: [string, ExecResult
             channel.appendLine(`[${fname}] Done.`);
             return outputs.join("");
         });
-        panel.webview.html = await renderTemplate(
-            ctx, "verify.html", {
-                fname: fname,
-                body: body
-            },
-            panel.webview);
+    panel.webview.html = await renderTemplate(
+        ctx, "verify.html", {
+        fname: fname,
+        subtitle: subtitle,
+        body: body
+    },
+        panel.webview);
 }
 
 async function formatNuXmvOutput(spec: string, json: string, out: string) {
@@ -155,7 +161,7 @@ async function formatNuXmvOutput(spec: string, json: string, out: string) {
             .then(v => JSON.parse(v.stdout), channel.appendLine)
             .then((cex: Step[]) => cex.map(async s => {
                 const render = await renderTemplate(
-                    ctx, "_step.html", 
+                    ctx, "_step.html",
                     {
                         deadlock: s.___DEADLOCK___,
                         depth: s.depth,
@@ -175,13 +181,13 @@ async function formatNuXmvOutput(spec: string, json: string, out: string) {
             .then(s => s.join("\n"));
     }
     const render = await renderTemplate(
-        ctx, "_verify.single.html", 
+        ctx, "_verify.single.html",
         {
-        tbody: table,
-        spec: spec,
-        isTrue: isTrue,
-        isFalse: isFalse,
-        output: lines.join("\n")
+            tbody: table,
+            spec: spec,
+            isTrue: isTrue,
+            isFalse: isFalse,
+            output: lines.join("\n")
         }, panel.webview);
     return render;
 }
@@ -192,7 +198,7 @@ async function formatNuXmvOutput(spec: string, json: string, out: string) {
  * @param index Index of property being verified
  * @param spec The LTLSPEC being verified
  */
-function ic3(fname: string, index: integer, spec: string, build_boolean_model: boolean=false) {
+function ic3(fname: string, index: integer, spec: string, build_boolean_model: boolean = false) {
     // TODO If spec starts with G one can use check_property_as_invar_ic3
     // TODO add optional ic3 bound limit in extension settings
     const smvCommands = `
@@ -205,7 +211,7 @@ function ic3(fname: string, index: integer, spec: string, build_boolean_model: b
 
     return new Promise<string>((resolve, reject) => {
         writeFileSync(script, smvCommands);
-        const child = execFile("nuxmv", ["-source", script, fname], async (err,stdout,stderr) => {
+        const child = execFile("nuxmv", ["-source", script, fname], async (err, stdout, stderr) => {
             temp.rmChild(fname, child);
             temp.rm(script);
             if (err) {
@@ -233,46 +239,6 @@ function ic3(fname: string, index: integer, spec: string, build_boolean_model: b
     });
 }
 
-/**
- * Launch BMC verification tasks
- */
-async function verifySpecsBmc(fname:string, json: string, bound: integer, v: [string, ExecResult]) {
-    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
-        .all(specs.map(async (element, index) => {
-            const split = element.split("LTLSPEC").map((x) => x.trim());
-            const nuxmvOutput = await bmc(v[0], index, bound, split[1]);
-            channel.appendLine(`[${fname}] ${++count}/${specs.length} done...`);
-            return formatNuXmvOutput(split[0], json, nuxmvOutput);
-        }))
-        .then(outputs => {
-            channel.appendLine(`[${fname}] Done.`);
-            return `${htmlReport}${outputs.join("")}</body></html>`;
-        });
-    const panel = vscode.window.createWebviewPanel(
-        "verificationResults",
-        "Verification Results",
-        vscode.ViewColumn.Active,
-        {enableScripts: true, retainContextWhenHidden: true}
-    );
-    panel.webview.html = html;
-}
-
-
 /**
  * Verify an LTLSPEC property using BMC.
  * @param fname Name of the .smv file 
@@ -280,28 +246,36 @@ async function verifySpecsBmc(fname:string, json: string, bound: integer, v: [st
  * @param bound The BMC bound
  * @param spec The LTLSPEC being verified
  */
-function bmc(fname: string, index: integer, bound: integer, spec: string) {
-    const smvCommands = `
-        set on_failure_script_quits 1
-        go_msat
-        build_boolean_model
-        bmc_setup
-        msat_check_ltlspec_bmc -k ${bound} -p "${spec}"
-        quit`;
-    const script = temp.makeFile(`ltspec-${index}`, ".smv");
+async function verifySpecsBmc(fname: string, json: string, bound: integer, v: [string, ExecResult]) {
+    const bmcFn = makeBmcFn(bound);
+    verifySpecs(fname, json, bmcFn, v, `BMC (bound: ${bound})`);
+}
 
-    return new Promise<string>((resolve, reject) => {
-        writeFileSync(script, smvCommands);
-        const child = execFile("nuxmv", ["-source", script, fname], async (err,stdout,stderr) => {
-        temp.rmChild(fname, child);
-        temp.rm(script);
-        if (err) {
-            vscode.window.showErrorMessage(err.message);
-            reject(err.message);
-        } else {
-            resolve(stdout);
-        }
+
+function makeBmcFn(bound: integer) {
+    return function (fname: string, index: integer, spec: string) {
+        const smvCommands = `
+            set on_failure_script_quits 1
+            go_msat
+            build_boolean_model
+            bmc_setup
+            msat_check_ltlspec_bmc -k ${bound} -p "${spec}"
+            quit`;
+        const script = temp.makeFile(`ltspec-${index}`, ".smv");
+
+        return new Promise<string>((resolve, reject) => {
+            writeFileSync(script, smvCommands);
+            const child = execFile("nuxmv", ["-source", script, fname], async (err, stdout, stderr) => {
+                temp.rmChild(fname, child);
+                temp.rm(script);
+                if (err) {
+                    vscode.window.showErrorMessage(err.message);
+                    reject(err.message);
+                } else {
+                    resolve(stdout);
+                }
+            });
+            temp.addChild(fname, child);
         });
-        temp.addChild(fname, child);
-    });
-}
\ No newline at end of file
+    }
+}