fixed LTL generation, linking of node to editor, & editor sync

kieler · Nov 14, 2024 · 87944e7 · 87944e7
1 parent 6d24b3f
commit 87944e7
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/extension/src-language-server/stpa/modelChecking/model-checking.ts b/extension/src-language-server/stpa/modelChecking/model-checking.ts
@@ -95,7 +95,7 @@ export async function generateLTLFormulae(
 async function translateDCAsToLTLFormulas(model: Model, map: Record<string, LTLFormula[]>): Promise<void> {
     if (model.allDCAs.length > 0 && model.allDCAs) {
         for (const rule of model.allDCAs) {
-            translateRuleToLTLFormulas(rule, map);
+            await translateRuleToLTLFormulas(rule, map);
         }
     }
 }
@@ -108,7 +108,7 @@ async function translateDCAsToLTLFormulas(model: Model, map: Record<string, LTLF
 async function translateUCAsToLTLFormulas(model: Model, map: Record<string, LTLFormula[]>): Promise<void> {
     if (model.rules.length > 0 && model.rules) {
         for (const rule of model.rules) {
-            translateRuleToLTLFormulas(rule, map);
+            await translateRuleToLTLFormulas(rule, map);
         }
     }
 }

diff --git a/extension/src-language-server/stpa/utils.ts b/extension/src-language-server/stpa/utils.ts
@@ -193,7 +193,7 @@ export function getRangeOfNodeSTPA(model: Model, label: string): Range | undefin
         elements.push(...nodes);
     }
     // in the diagram generator dots are replaced by underscores
-    const correctedLabel = label.replace(/_/g, ".");
+    const correctedLabel = label?.replace(/_/g, ".");
     elements.forEach((component) => {
         if (component.name === correctedLabel) {
             range = component.$cstNode?.range;

diff --git a/extension/src/extension.ts b/extension/src/extension.ts
@@ -439,7 +439,8 @@ function registerTextEditorSync(manager: StpaLspVscodeExtension, context: vscode
                 '<svg xmlns="http://www.w3.org/2000/svg"'
             );
             // if the change event is triggered by the generation of an SVG, do not update the views
-            if (!svgGeneration) {
+            const fileTypeIsSupportedLanguage = changeEvent.document.uri.toString().endsWith(".stpa") || changeEvent.document.uri.toString().endsWith(".fta");
+            if (fileTypeIsSupportedLanguage && !svgGeneration) {
                 const document = changeEvent.document;
                 updateViews(manager, document);
             }