From 6e6fe2938dc74597bfcec1e6ca70788827a5bed4 Mon Sep 17 00:00:00 2001 From: FrederikPM Date: Thu, 30 Jun 2022 21:26:21 +0200 Subject: [PATCH] Squashed commit of the following: commit 09d42fa8c0420a019e15043058bde65be8785e68 Author: FrederikPM Date: Thu Jun 30 21:25:03 2022 +0200 Handle conjectures without violations commit ba95ad79471a0ccdd9a4c8fe1532f2ca5c8df553 Author: FrederikPM Date: Thu Jun 30 20:55:17 2022 +0200 Update RTLogViewHandler.ts --- resources/webviews/rtLogView/rtLogView.js | 2 +- src/handlers/RTLogViewHandler.ts | 172 +++++++++++++--------- 2 files changed, 102 insertions(+), 72 deletions(-) diff --git a/resources/webviews/rtLogView/rtLogView.js b/resources/webviews/rtLogView/rtLogView.js index 6f956bb..6b57b9a 100644 --- a/resources/webviews/rtLogView/rtLogView.js +++ b/resources/webviews/rtLogView/rtLogView.js @@ -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); diff --git a/src/handlers/RTLogViewHandler.ts b/src/handlers/RTLogViewHandler.ts index 3631864..0d6b8a0 100644 --- a/src/handlers/RTLogViewHandler.ts +++ b/src/handlers/RTLogViewHandler.ts @@ -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 { @@ -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 = new Map(); logLines?.forEach((line) => { const lineSplit: string[] = line.split(" -> "); if (lineSplit.length > 1) { @@ -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); } @@ -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}`); }