Skip to content

Commit

Permalink
Squashed commit of the following:
Browse files Browse the repository at this point in the history 
commit 09d42fa
Author: FrederikPM <frdrkpm@gmail.com>
Date:   Thu Jun 30 21:25:03 2022 +0200

    Handle conjectures without violations

commit ba95ad7
Author: FrederikPM <frdrkpm@gmail.com>
Date:   Thu Jun 30 20:55:17 2022 +0200

    Update RTLogViewHandler.ts
  • Loading branch information
@FrederikPM
FrederikPM committed Jun 30, 2022
1 parent b2d0a19 commit 6e6fe29
Show file tree
Hide file tree
Showing 2 changed files with 102 additions and 72 deletions.
2 changes: 1 addition & 1 deletion resources/webviews/rtLogView/rtLogView.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ function generateConjectureTable(conjectures) {
document.createTextNode(content.value === true ? "\u2713" : content.value === false ? "\u2715" : content.value)
);
// Click listener for focusing the diagram on the time of the conjecture violation
if (content.header == headerNames[3] || content.header == headerNames[5]) {
if ((content.header == headerNames[3] || content.header == headerNames[5]) && content.value != "") {
rowCell.classList.add("clickableCell");
rowCell.ondblclick = () => {
handleSelectedTimeChanged(content.value);
Expand Down
172 changes: 101 additions & 71 deletions src/handlers/RTLogViewHandler.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,16 +24,16 @@ import { vdmDialects } from "../util/DialectUtil";
interface ConjectureTarget {
kind: string;
opname: string;
time: number;
thid: number;
time: string;
thid: string;
}

interface ValidationConjecture {
status: boolean;
name: string;
expression: string;
source: ConjectureTarget;
destination: ConjectureTarget;
source?: ConjectureTarget;
destination?: ConjectureTarget;
}

interface logData {
Expand Down Expand Up @@ -218,6 +218,8 @@ export class RTLogViewHandler extends AutoDisposable {
let currrentTime: number = -1;
const vBusDecl = { eventKind: this._logEvents.busDecl, id: 0, topo: [], name: "vBUS", time: 0 };
const vCpuDecl = { eventKind: this._logEvents.cpuDecl, id: undefined, expl: false, sys: "", name: "vCPU", time: 0 };
const knownLogEvents: string[] = Object.values(this._logEvents);
const unknownLogEvents: Map<string, number> = new Map();
logLines?.forEach((line) => {
const lineSplit: string[] = line.split(" -> ");
if (lineSplit.length > 1) {
Expand Down Expand Up @@ -265,84 +267,93 @@ export class RTLogViewHandler extends AutoDisposable {
timestamps.push(currrentTime);
}

if (logEventObj.eventKind == this._logEvents.busDecl) {
busDecls.push(logEventObj);
} else if (logEventObj.eventKind == this._logEvents.cpuDecl) {
cpuDecls.push(logEventObj);
} else if (logEventObj.eventKind != this._logEvents.deployObj) {
if (logEventObj.eventKind != this._logEvents.messageActivate) {
if (logEventObj.eventKind == this._logEvents.messageCompleted) {
const msgInitEvent: any = activeMsgInitEvents.splice(
activeMsgInitEvents.indexOf(activeMsgInitEvents.find((msg) => msg.msgid == logEventObj.msgid)),
1
)[0];

logEventObj.busid = msgInitEvent.busid;
logEventObj.callthr = msgInitEvent.callthr;
logEventObj.tocpu = msgInitEvent.tocpu;
if (msgInitEvent.eventKind == this._logEvents.messageRequest) {
logEventObj.opname = msgInitEvent.opname;
logEventObj.objref = msgInitEvent.objref;
logEventObj.clnm = msgInitEvent.clnm;
if (knownLogEvents.includes(logEventObj.eventKind)) {
if (logEventObj.eventKind == this._logEvents.busDecl) {
busDecls.push(logEventObj);
} else if (logEventObj.eventKind == this._logEvents.cpuDecl) {
cpuDecls.push(logEventObj);
} else if (logEventObj.eventKind != this._logEvents.deployObj) {
if (logEventObj.eventKind != this._logEvents.messageActivate) {
if (logEventObj.eventKind == this._logEvents.messageCompleted) {
const msgInitEvent: any = activeMsgInitEvents.splice(
activeMsgInitEvents.indexOf(activeMsgInitEvents.find((msg) => msg.msgid == logEventObj.msgid)),
1
)[0];

logEventObj.busid = msgInitEvent.busid;
logEventObj.callthr = msgInitEvent.callthr;
logEventObj.tocpu = msgInitEvent.tocpu;
if (msgInitEvent.eventKind == this._logEvents.messageRequest) {
logEventObj.opname = msgInitEvent.opname;
logEventObj.objref = msgInitEvent.objref;
logEventObj.clnm = msgInitEvent.clnm;
}
}
}

const cpunm =
"cpunm" in logEventObj
? logEventObj.cpunm
: "fromcpu" in logEventObj
? logEventObj.fromcpu
: "tocpu" in logEventObj
? logEventObj.tocpu
: logEventObj.id;
let cpuWithEvents = cpusWithEvents.find((cwe) => cwe.id == cpunm);
if (!cpuWithEvents) {
cpuWithEvents = {
id: cpunm,
executionEvents: [],
timestamps: [],
};
cpusWithEvents.push(cpuWithEvents);
}
const cpunm =
"cpunm" in logEventObj
? logEventObj.cpunm
: "fromcpu" in logEventObj
? logEventObj.fromcpu
: "tocpu" in logEventObj
? logEventObj.tocpu
: logEventObj.id;
let cpuWithEvents = cpusWithEvents.find((cwe) => cwe.id == cpunm);
if (!cpuWithEvents) {
cpuWithEvents = {
id: cpunm,
executionEvents: [],
timestamps: [],
};
cpusWithEvents.push(cpuWithEvents);
}

if (
logEventObj.eventKind == this._logEvents.messageRequest ||
logEventObj.eventKind == this._logEvents.replyRequest
) {
activeMsgInitEvents.push(logEventObj);
}
if (
logEventObj.eventKind == this._logEvents.messageRequest ||
logEventObj.eventKind == this._logEvents.replyRequest
) {
activeMsgInitEvents.push(logEventObj);
}

cpuWithEvents.executionEvents.push(logEventObj);
cpuWithEvents.executionEvents.push(logEventObj);

if (
cpuWithEvents.timestamps.length == 0 ||
cpuWithEvents.timestamps[cpuWithEvents.timestamps.length - 1] < logEventObj.time
) {
cpuWithEvents.timestamps.push(logEventObj.time);
if (
cpuWithEvents.timestamps.length == 0 ||
cpuWithEvents.timestamps[cpuWithEvents.timestamps.length - 1] < logEventObj.time
) {
cpuWithEvents.timestamps.push(logEventObj.time);
}
}
}

executionEvents.push(logEventObj);
}
executionEvents.push(logEventObj);
}

if (
(logEventObj.eventKind == this._logEvents.messageRequest || logEventObj.eventKind == this._logEvents.replyRequest) &&
logEventObj.busid == 0
) {
[logEventObj.fromcpu, logEventObj.tocpu].forEach((tpid) => {
if (vBusDecl.topo.find((id: number) => id == tpid) == undefined) {
vBusDecl.topo.push(tpid);
}
});
}
if (
(logEventObj.eventKind == this._logEvents.messageRequest ||
logEventObj.eventKind == this._logEvents.replyRequest) &&
logEventObj.busid == 0
) {
[logEventObj.fromcpu, logEventObj.tocpu].forEach((tpid) => {
if (vBusDecl.topo.find((id: number) => id == tpid) == undefined) {
vBusDecl.topo.push(tpid);
}
});
}

if (logEventObj?.cpunm == 0 && vCpuDecl.id == undefined) {
vCpuDecl.id = logEventObj.cpunm;
cpuDecls.push(vCpuDecl);
if (logEventObj?.cpunm == 0 && vCpuDecl.id == undefined) {
vCpuDecl.id = logEventObj.cpunm;
cpuDecls.push(vCpuDecl);
}
} else if (unknownLogEvents.has(logEventObj.eventKind)) {
unknownLogEvents.set(logEventObj.eventKind, unknownLogEvents.get(logEventObj.eventKind) + 1);
} else {
unknownLogEvents.set(logEventObj.eventKind, 1);
}
}
});

unknownLogEvents.forEach((value, key) => console.log(`Encounted unknown log event: '${key}' ${value} times`));

if (vBusDecl.topo.length > 0) {
busDecls.push(vBusDecl);
}
Expand Down Expand Up @@ -379,9 +390,28 @@ export class RTLogViewHandler extends AutoDisposable {
logContent
.trim()
.split(/[\r\n\t]+/g)
.forEach((line) => dataObj.conjectures.push(JSON.parse(line)));
.forEach((line) => {
const vc: ValidationConjecture = JSON.parse(line);
if (!vc.destination) {
vc.destination = {
kind: "",
opname: "",
time: "",
thid: "",
};
}
if (!vc.source) {
vc.source = {
kind: "",
opname: "",
time: "",
thid: "",
};
}
dataObj.conjectures.push(vc);
});
} catch (ex) {
const msg = "Encountered an ereror when parsing validation conjectures!";
const msg = "Encountered an error when parsing validation conjectures!";
window.showWarningMessage(msg);
console.log(`${msg} - ${ex}`);
}
Expand Down

0 comments on commit 6e6fe29

Please sign in to comment.