Skip to content

Commit

Permalink
Merge pull request #37 from kieler/jep/utility
Browse files Browse the repository at this point in the history
Jep/utility
  • Loading branch information
Drakae authored Aug 20, 2024
2 parents 364c9ba + 9455071 commit 8da5226
Show file tree
Hide file tree
Showing 18 changed files with 513 additions and 234 deletions.
49 changes: 9 additions & 40 deletions extension/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -57,46 +57,6 @@
"configuration": {
"title": "pasta",
"properties": {
"pasta.differentForms": {
"type": "boolean",
"default": false,
"description": "Different forms for STPA aspects"
},
"pasta.colorStyle": {
"type": "string",
"default": "fewer colors",
"enum": [
"colorful",
"standard",
"black & white",
"fewer colors"
],
"enumDescription": [
"Each STPA aspect has a different color",
"All nodes have the standard color (blue)",
"The diagrams are colored in black and white"
]
},
"pasta.checkResponsibilitiesForConstraints": {
"type": "boolean",
"default": true,
"description": "Check whether all system-level constraints are covered by a responsibility"
},
"pasta.checkConstraintsForUCAs": {
"type": "boolean",
"default": true,
"description": "Check whether all UCAs are covered by constraints"
},
"pasta.checkScenariosForUCAs": {
"type": "boolean",
"default": true,
"description": "Check whether all UCAs are covered by scenarios"
},
"pasta.checkSafetyRequirementsForUCAs": {
"type": "boolean",
"default": true,
"description": "Check whether all UCAs are covered by safety requirements"
},
"pasta.stpa.snippets": {
"type": "string[]",
"default": [],
Expand Down Expand Up @@ -137,6 +97,11 @@
"title": "Export diagram to SVG",
"category": "PASTA Diagram"
},
{
"command": "pasta.data.clear",
"title": "Clear the persisted data",
"category": "PASTA Data"
},
{
"command": "pasta.stpa.checks.setCheckResponsibilitiesForConstraints",
"title": "Set the responsibilities for constraints check",
Expand Down Expand Up @@ -227,6 +192,10 @@
{
"command": "pasta.diagram.export"
},
{
"command": "pasta.data.clear",
"when": "editorLangId == 'stpa' || editorLangId == 'fta'"
},
{
"command": "pasta.stpa.checks.setCheckResponsibilitiesForConstraints",
"when": "editorLangId == 'stpa'"
Expand Down
25 changes: 25 additions & 0 deletions extension/src-language-server/fta/fta-message-handler.ts
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,31 @@ export function addFTANotificationHandler(
sharedServices: LangiumSprottySharedServices
): void {
addCutSetsHandler(connection, ftaServices, sharedServices);
addStorageHandler(connection, ftaServices);
}

/**
* Adds handlers for notifications regarding the storage.
* @param connection
* @param ftaServices
*/
function addStorageHandler(connection: Connection, ftaServices: FtaServices): void {
// handle configuration/storage init
connection.onNotification("config/init", ({ clientId, options }) => {
// update synthesis options
if (options["synthesisOptions"] && clientId !== "") {
Object.entries(options["synthesisOptions"]).forEach(([key, value]) => {
ftaServices.options.SynthesisOptions.setOption(key, value);
});
}
});

// handle reset of the storage
connection.onRequest("config/reset", () => {
// reset synthesis options
ftaServices.options.SynthesisOptions.resetAll();
return;
});
}

/**
Expand Down
20 changes: 0 additions & 20 deletions extension/src-language-server/main.ts
Original file line number Diff line number Diff line change
Expand Up @@ -38,24 +38,4 @@ addSTPANotificationHandler(connection, stpa, shared);
addFTANotificationHandler(connection, fta, shared);
addNotificationHandler(connection, shared);

// handle configuration changes for the validation checks
connection.onNotification("configuration", options => {
for (const option of options) {
switch (option.id) {
case "checkResponsibilitiesForConstraints":
stpa.validation.StpaValidator.checkResponsibilitiesForConstraints = option.value;
break;
case "checkConstraintsForUCAs":
stpa.validation.StpaValidator.checkConstraintsForUCAs = option.value;
break;
case "checkScenariosForUCAs":
stpa.validation.StpaValidator.checkScenariosForUCAs = option.value;
break;
case "checkSafetyRequirementsForUCAs":
stpa.validation.StpaValidator.checkSafetyRequirementsForUCAs = option.value;
break;
}
}
});

connection.onInitialized(() => connection.sendNotification("ready"));
Original file line number Diff line number Diff line change
Expand Up @@ -529,12 +529,4 @@ export class StpaSynthesisOptions extends SynthesisOptions {
}
}
}

protected setOption(id: string, value: any): void {
const option = this.getOption(id);
if (option) {
option.currentValue = value;
option.synthesisOption.currentValue = value;
}
}
}
58 changes: 51 additions & 7 deletions extension/src-language-server/stpa/message-handler.ts
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ import { TextDocumentContentChangeEvent } from "vscode";
import { Connection, URI } from "vscode-languageserver";
import { diagramSizes } from "../diagram-server";
import { serializeFTAAST } from "../fta/utils";
import { updateValidationChecks } from "../utils";
import { setCurrentCursorOffset } from "./diagram/utils";
import { createFaultTrees } from "./ftaGeneration/fta-generation";
import { generateLTLFormulae } from "./modelChecking/model-checking";
Expand All @@ -40,12 +41,51 @@ let changeUri: string;
* @param connection
* @param stpaServices
*/
export function addSTPANotificationHandler(connection: Connection, stpaServices: StpaServices, sharedServices: LangiumSprottySharedServices): void {
export function addSTPANotificationHandler(
connection: Connection,
stpaServices: StpaServices,
sharedServices: LangiumSprottySharedServices
): void {
addContextTableHandler(connection, stpaServices);
addTextChangeHandler(connection, stpaServices, sharedServices);
addVerificationHandler(connection, sharedServices);
addResultHandler(connection, sharedServices);
addFTAGeneratorHandler(connection, sharedServices);
addStorageHandler(connection, stpaServices);
}

/**
* Adds handlers for notifications regarding the storage.
* @param connection
* @param stpaServices
*/
function addStorageHandler(connection: Connection, stpaServices: StpaServices): void {
// handle configuration/storage init
connection.onNotification("config/init", ({ clientId, options }) => {
// update validation checks
if (options["validation"]) {
updateValidationChecks(options["validation"], stpaServices.validation.StpaValidator);
}
// update synthesis options
if (options["synthesisOptions"] && clientId !== "") {
Object.entries(options["synthesisOptions"]).forEach(([key, value]) => {
stpaServices.options.SynthesisOptions.setOption(key, value);
});
}
});

// handle reset of the storage
connection.onRequest("config/reset", () => {
// reset validation checks
const validator = stpaServices.validation.StpaValidator;
validator.checkResponsibilitiesForConstraints = true;
validator.checkConstraintsForUCAs = true;
validator.checkScenariosForUCAs = true;
validator.checkSafetyRequirementsForUCAs = true;
// reset synthesis options
stpaServices.options.SynthesisOptions.resetAll();
return;
});
}

/**
Expand All @@ -55,15 +95,15 @@ export function addSTPANotificationHandler(connection: Connection, stpaServices:
*/
function addContextTableHandler(connection: Connection, stpaServices: StpaServices): void {
// the data needed to create the context table is requested
connection.onNotification("contextTable/getData", async (uri) => {
connection.onNotification("contextTable/getData", async uri => {
// data is computed and send back to the extension
lastUri = uri;
const contextTable = stpaServices.contextTable.ContextTableProvider;
const data = await contextTable.getData(uri);
connection.sendNotification("contextTable/data", data);
});
// a cell in the context table is selected
connection.onNotification("contextTable/selected", (text) => {
connection.onNotification("contextTable/selected", text => {
// compute the range of the textual definition of the selected UCA
const contextTable = stpaServices.contextTable.ContextTableProvider;
const range = contextTable.getRangeOfUCA(lastUri, text);
Expand All @@ -88,7 +128,11 @@ function addContextTableHandler(connection: Connection, stpaServices: StpaServic
* @param stpaServices
* @param sharedServices
*/
function addTextChangeHandler(connection: Connection, stpaServices: StpaServices, sharedServices: LangiumSprottySharedServices): void {
function addTextChangeHandler(
connection: Connection,
stpaServices: StpaServices,
sharedServices: LangiumSprottySharedServices
): void {
// text in the editor changed
connection.onNotification("editor/textChange", async ({ changes, uri }) => {
// save the changes and the uri of the file. Before we can do something we have to wait until the document is built (see below).
Expand All @@ -111,7 +155,7 @@ function addTextChangeHandler(connection: Connection, stpaServices: StpaServices
}
});
// update the cursor position on editor change
connection.onNotification("editor/change", async (offset) => {
connection.onNotification("editor/change", async offset => {
setCurrentCursorOffset(offset);
});
}
Expand Down Expand Up @@ -147,7 +191,7 @@ function addResultHandler(connection: Connection, sharedServices: LangiumSprotty
return data;
});
// create the diagrams needed for the STPA result report and send back the widths of them.
connection.onRequest("result/createDiagrams", async (msg) => {
connection.onRequest("result/createDiagrams", async msg => {
const diagramServerManager = sharedServices.diagram.DiagramServerManager;
await diagramServerManager.acceptAction(msg);
return diagramSizes;
Expand All @@ -162,7 +206,7 @@ function addFTAGeneratorHandler(connection: Connection, sharedServices: LangiumS
// creates and serializes fault trees
connection.onRequest("generate/faultTrees", async (uri: string) => {
const models = await createFaultTrees(uri, sharedServices);
const texts = models.map((model) => serializeFTAAST(model));
const texts = models.map(model => serializeFTAAST(model));
return texts;
});
}
24 changes: 24 additions & 0 deletions extension/src-language-server/synthesis-options.ts
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,30 @@ export class SynthesisOptions {
this.options = [layoutCategoryOption, labelManagementOption, labelShorteningWidthOption, modelOrderOption];
}

/**
* Resets all synthesis options to their initial values.
*/
resetAll(): void {
this.options.forEach(option => (option.currentValue = option.synthesisOption.initialValue));
}

/**
* Sets the value of the synthesis option with the given id.
* @param id The id of the synthesis option.
* @param value The new value of the synthesis option.
*/
setOption(id: string, value: any): void {
const option = this.getOption(id);
if (option) {
option.currentValue = value;
option.synthesisOption.currentValue = value;
}
}

/**
* Returns all synthesis options.
* @returns all synthesis options.
*/
getSynthesisOptions(): ValuedSynthesisOption[] {
return this.options;
}
Expand Down
29 changes: 28 additions & 1 deletion extension/src-language-server/utils.ts
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,10 @@

import { AstNode, LangiumSharedServices } from "langium";
import { IdCache, LangiumSprottySharedServices } from "langium-sprotty";
import { SLabel } from "sprotty-protocol";
import { URI } from "vscode-uri";
import { StpaValidator } from "./stpa/stpa-validator";
import { labelManagementValue } from "./synthesis-options";
import { SLabel } from 'sprotty-protocol';

/**
* Determines the model for {@code uri}.
Expand Down Expand Up @@ -103,3 +104,29 @@ export function getDescription(
}
return labels;
}

/**
* Updates the validation checks for the STPA validator.
* @param options The validation options.
* @param validator The STPA validator.
*/
export function updateValidationChecks(options: Record<string, any>, validator: StpaValidator): void {
// TODO: save options alos in record and use them in the validator
// set options if they are set
Object.entries(options).forEach(([key, value]) => {
switch (key) {
case "checkResponsibilitiesForConstraints":
validator.checkResponsibilitiesForConstraints = value;
break;
case "checkConstraintsForUCAs":
validator.checkConstraintsForUCAs = value;
break;
case "checkScenariosForUCAs":
validator.checkScenariosForUCAs = value;
break;
case "checkSafetyRequirementsForUCAs":
validator.checkSafetyRequirementsForUCAs = value;
break;
}
});
}
4 changes: 2 additions & 2 deletions extension/src-webview/css/fta-diagram.css
Original file line number Diff line number Diff line change
Expand Up @@ -20,21 +20,21 @@
.vscode-dark .fta-node {
fill: var(--dark-node);
stroke: var(--light-node);
stroke-width: 2;
}

.vscode-dark .fta-edge {
stroke: var(--light-node);
stroke-width: 1;
}

.vscode-light .fta-node {
fill: var(--light-node);
stroke: black;
stroke-width: 2;
}

.vscode-light .fta-edge {
stroke: black;
stroke-width: 1;
}

.fta-text{
Expand Down
Loading

0 comments on commit 8da5226

Please sign in to comment.