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 @@ {%= spec %}
{% } else { %} ❔ {% } %}
+{% if (tbody) { %}
#
@@ -13,6 +14,7 @@ {%= spec %}
{%- tbody %}
+{% } %}
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 @@
- R-CHECK: Verification of {%= fname %} (IC3)
+ R-CHECK: Verification of {%= fname %} ({%= subtitle %})
- R-CHECK: Verification of {%= fname %} (IC3)
+ R-CHECK: Verification of {%= fname %}
+ {%= subtitle %}
{% if (body != undefined) { %}{%- body %}
{% } else { %}{% } %}
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((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((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 = `
-
-
-
-
- ${title}
-
-
- ${title}
`
-
- 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("")}`;
- });
- 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((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((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
+ }
+}