Use Shared State Machine Parser Module (#111)

Author: rcosta358

README.md

@@ -137,4 +137,5 @@ For more information, check the following repositories:
 - [liquidjava](https://github.com/liquid-java/liquidjava): Includes the API, verifier and some examples
 - [vscode-liquidjava](https://github.com/liquid-java/vscode-liquidjava): Source code of this VS Code extension
 - [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples): Examples of how to use LiquidJava
-- [liquid-java-external-libs](https://github.com/liquid-java/liquid-java-external-libs): Examples of how to use LiquidJava to refine external libraries
+- [liquid-java-external-libs](https://github.com/liquid-java/liquid-java-external-libs): Examples of how to use LiquidJava to refine external libraries
+- [liquidjava-fsm](https://github.com/liquid-java/liquidjava-fsm): State machine parser used by the VS Code language server

client/src/types/fsm.ts

@@ -2,9 +2,9 @@
 
 export type LJStateMachine = {
     className: string;
-    initialTransitions: { to: string; postCond?: string | null }[];
+    initialTransitions: { to: string; toCondition?: string | null }[];
     states: string[];
-    transitions: { from: string; to: string; label: string; preCond?: string | null; postCond?: string | null }[];
+    transitions: { from: string; to: string; label: string; fromCondition?: string | null; toCondition?: string | null }[];
     errorContext: LJStateMachineErrorContext | null;
 };
 

client/src/webview/diagram.ts

@@ -35,7 +35,7 @@ export function createMermaidDiagram(
 
     // initial transitions
     sm.initialTransitions.forEach(transition => {
-        const label = getInitialTransitionLabel(transition.postCond, showConditions);
+        const label = getInitialTransitionLabel(transition.toCondition, showConditions);
         lines.push(`    [*] --> ${transition.to}${label ? ` : ${label}` : ''}`);
     });
 
@@ -45,8 +45,8 @@ export function createMermaidDiagram(
         const isCalledMethod = transition.label === sm.errorContext?.calledMethod;
         const label = getTransitionLabel(
             transition.label,
-            transition.preCond,
-            transition.postCond,
+            transition.fromCondition,
+            transition.toCondition,
             showConditions,
             isCalledMethod,
         );
@@ -72,8 +72,8 @@ export function createMermaidDiagram(
 
 function getTransitionLabel(
     label: string,
-    preCond?: string | null,
-    postCond?: string | null,
+    fromCondition?: string | null,
+    toCondition?: string | null,
     showConditions = false,
     isCalledMethod = false,
 ): string {
@@ -83,14 +83,14 @@ function getTransitionLabel(
         : escapedLabel;
     if (!showConditions) return methodLabel;
     return [
-        getConditionLabel('pre', preCond),
+        getConditionLabel('pre', fromCondition),
         methodLabel,
-        getConditionLabel('post', postCond)
+        getConditionLabel('post', toCondition)
     ].filter(Boolean).join('<br/>');
 }
 
-function getInitialTransitionLabel(postCond?: string | null, showConditions = false): string {
-    return showConditions ? getConditionLabel('post', postCond) : '';
+function getInitialTransitionLabel(toCondition?: string | null, showConditions = false): string {
+    return showConditions ? getConditionLabel('post', toCondition) : '';
 }
 
 function getConditionLabel(kind: 'pre' | 'post', cond?: string | null): string {

client/src/webview/views/fsm/fsm.ts

@@ -11,8 +11,8 @@ export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | u
 
 function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number): string {
     const hasConditionExpansions = sm
-        ? sm.initialTransitions.some(transition => !!transition.postCond)
-            || sm.transitions.some(transition => !!transition.preCond || !!transition.postCond)
+        ? sm.initialTransitions.some(transition => !!transition.toCondition)
+            || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition)
         : false;
     const conditionToggleLabel = !hasConditionExpansions
         ? 'No additional conditions to expand'

server/pom.xml

@@ -174,6 +174,11 @@
 			<artifactId>liquidjava-verifier</artifactId>
 			<version>0.0.32</version>
 		</dependency>
+		<dependency>
+		  <groupId>io.github.liquid-java</groupId>
+		  <artifactId>liquidjava-fsm</artifactId>
+		  <version>0.1.0</version>
+		</dependency>
 		<dependency>
 			<groupId>tools.aqua</groupId>
 			<artifactId>z3-turnkey</artifactId>

server/src/main/java/LJLanguageServer.java

@@ -15,8 +15,8 @@
 import org.eclipse.lsp4j.services.WorkspaceService;
 
 import dtos.uri.Uri;
-import fsm.StateMachine;
-import fsm.StateMachineParser;
+import liquidjava.fsm.StateMachine;
+import liquidjava.fsm.StateMachineParser;
 
 public class LJLanguageServer implements LanguageServer {
 

server/src/main/java/dtos/errors/StateRefinementErrorDTO.java

@@ -4,8 +4,8 @@
 
 import dtos.diagnostics.SourcePositionDTO;
 import dtos.diagnostics.VCSimplificationResultDTO;
-import fsm.StateMachine;
-import fsm.StateMachineParser;
+import liquidjava.fsm.StateMachine;
+import liquidjava.fsm.StateMachineParser;
 import liquidjava.diagnostics.errors.StateRefinementError;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;