feat(edgeV2): EDGE snippet-aligned pursue/skip guards with shared PRISM helpers

examples/edgeV2/EDGE goal snippets.txt

@@ -0,0 +1,115 @@
+AND goal sequential
+
+module G0
+  g0 : [0..1] init 0; //0 means not pursued, 1 means currently pursued
+
+  [pursue_G0] !g0_achieved & g0=0 & GUARD -> (g0'=1); //triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0=1 & G0_achievable*10.0 > decision_G0 -> true; //this only checks if we should indeed pursue on of the children or skip
+  [pursue_G2] !g0_achieved & g0=1 & G0_achievable*10.0 > decision_G0 & g1_achieved -> true; //here we add the guard that G1 needs to be achieved first since we're in sequential 
+
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g2=0 & G0_achievable*10.0 <= decision_G0 -> (g0'=0); //we can skip only when no child is pursued
+
+
+  [achieved_G0] g0=1 & g0_achieved & g1=0 & g2=0 -> (g0'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved & g2_achieved); 
+
+AND goal any order
+
+module G0
+  g0 : [0..1] init 0; //0 means not pursued, 1 means currently pursued
+
+  [pursue_G0] !g0_achieved & g0=0 & GUARD -> (g0'=1); //triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0=1 & G0_achievable*10.0 > decision_G0 & g2!=1 & (g2_pursued | (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0) -> true; 
+  [pursue_G2] !g0_achieved & g0=1 & G0_achievable*10.0 > decision_G0 & g1!=1 & (g1_pursued | (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0) -> true; 
+
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g2=0 & G0_achievable*10.0 <= decision_G0 -> (g0'=0); 
+
+
+  [achieved_G0] g0=1 & g0_achieved & g1=0 & g2=0 -> (g0'=0);
+
+endmodule
+formula g0_achieved = (g1_achieved & g2_achieved); 
+
+
+AND goal interleaved
+
+module G0
+  g0 : [0..1] init 0; //0 means not pursued, 1 means currently pursued
+
+  [pursue_G0] !g0_achieved & g0=0 & GUARD -> (g0'=1); //triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0=1 & G1_achievable*10.0 > decision_G1 -> true; 
+  [pursue_G2] !g0_achieved & g0=1 & G2_achievable*10.0 > decision_G2 -> true; //here the trick is that we already skip g0 if none of the children should be pursued; this prohibits livelocks (circles of pursue-skip-pursue without any advancements)
+
+  [skip_G0] g0=1 & g1=0 & g2=0 & !g0_achieved & !(G2_achievable*10.0 > decision_G2 | G1_achievable*10.0 > decision_G1) -> (g0'=0); 
+
+
+  [achieved_G0] g0=1 & g0_achieved & g1=0 & g2=0 -> (g0'=0);
+
+endmodule
+formula g0_achieved = (g1_achieved & g2_achieved); 
+
+
+
+OR goal 
+module G0
+  g0 : [0..1] init 0; //0 means not pursued, 1 means currently pursued
+
+  [pursue_G0] !g0_achieved & g0=0 & GUARD -> (g0'=1); //triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0=1 & G0_achievable*10.0 > decision_G0 & g2=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0 -> true; 
+  [pursue_G2] !g0_achieved & g0=1 & G0_achievable*10.0 > decision_G0 & g1=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0 -> true; 
+
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g2=0 & G0_achievable*10.0 <= decision_G0 -> (g0'=0); 
+
+
+  [achieved_G0] g0=1 & g1=0 & g2=0 & g0_achieved -> (g0'=0);
+
+endmodule
+formula g0_achieved = (g1_achieved | g2_achieved); 
+
+
+OR goal choose once 
+module G0
+  g0 : [0..1] init 0; //0 means not pursued, 1 means currently pursued
+  g0_chosen: [0..2] init 0; //0 not chosen, 1 chose 1, 2 chose 2
+
+  [pursue_G0] !g0_achieved & g0=0 & GUARD -> (g0'=1); //triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0=1 & g0_chosen=0 & G0_achievable*10.0 > decision_G0 & g2=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0 -> (g0_chosen'=1); 
+  [pursue_G2] !g0_achieved & g0=1 & g0_chosen=0 & G0_achievable*10.0 > decision_G0 & g1=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0 -> (g0_chosen'=2);
+
+  [pursue_G1] !g0_achieved & g0=1 & g0_chosen=1 & G1_achievable*10.0 > decision_G1 -> true;
+  [pursue_G2] !g0_achieved & g0=1 & g0_chosen=2 & G2_achievable*10.0 > decision_G2 -> true;
+
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g2=0 & g0_chosen=0 & G0_achievable*10.0 <= decision_G0 -> (g0'=0); 
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g0_chosen=1 & G1_achievable*10.0 <= decision_G1 -> (g0'=0); //skip condition if g0_chosen=1
+  [skip_G0] !g0_achieved & g0=1 & g2=0 & g0_chosen=2 & G2_achievable*10.0 <= decision_G2 -> (g0'=0); 
+
+  [achieved_G0] g0=1 & g1=0 & g2=0 & g0_achieved -> (g0'=0);
+
+endmodule
+formula g0_achieved = (g1_achieved | g2_achieved); 
+
+
+OR goal degradation
+module G0
+  g0 : [0..1] init 0; //0 means not pursued, 1 means currently pursued
+  g0_failed : [0..N] init 0;
+
+  [pursue_G0] !g0_achieved & g0=0 & GUARD -> (g0'=1); //triggering the goal from upper layer
+
+  [pursue_G1] !g0_achieved & g0=1 & g0_failed<N & G1_achievable*10.0 > decision_G1 -> (g0_failed'=g0_failed+1); //if we need to retry N times
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g0_failed<N & G1_achievable*10.0 <= decision_G1 -> (g0'=0); 
+
+  [pursue_G1] !g0_achieved & g0=1 & g0_failed=N & G0_achievable*10.0 > decision_G0 & g2=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0 -> true; 
+  [pursue_G2] !g0_achieved & g0=1 & g0_failed=N & G0_achievable*10.0 > decision_G0 & g1=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0 -> true; 
+
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g0_failed<N & G1_achievable*10.0 <= decision_G1 -> (g0'=0); 
+  [skip_G0] !g0_achieved & g0=1 & g1=0 & g2=0 & g0_failed=N & G0_achievable*10.0 <= decision_G0 -> (g0'=0); 
+
+  [achieved_G0] !g0_achieved & g0=1 & g1=0 & g2=0 & g0_achieved -> (g0'=0);
+
+endmodule
+formula g0_achieved = (g1_achieved | g2_achieved); 
+

package.json

@@ -15,7 +15,7 @@
     "dev": "concurrently \"pnpm run dev:goal-tree\" \"pnpm run dev:lib\" \"pnpm run dev:ui\"",
     "dev:goal-tree": "pnpm --filter @goal-controller/goal-tree run watch",
     "dev:lib": "pnpm --filter @goal-controller/lib run watch",
-    "dev:ui": "pnpm --filter @goal-controller/ui run dev",
+    "dev:ui": "pnpm --filter @goal-controller/ui run dev:next",
     "build": "pnpm run build:goal-tree && pnpm run build:lib && pnpm run build:ui",
     "build:goal-tree": "pnpm --filter @goal-controller/goal-tree run build",
     "build:lib": "pnpm run build:goal-tree && pnpm --filter @goal-controller/lib run build",

packages/lib/src/engines/edgeV2/index.ts

@@ -0,0 +1,43 @@
+/**
+ * Edge Engine
+ * Generates PRISM models for probabilistic verification
+ *
+ * Architecture:
+ * - mapper.ts: Engine creation - maps raw iStar model to Edge-specific properties
+ * - template/: Transformation - generates PRISM model output
+ */
+
+// Engine creation (mapper)
+export {
+  EDGE_GOAL_KEYS,
+  EDGE_RESOURCE_KEYS,
+  EDGE_TASK_KEYS,
+  edgeEngineMapper,
+  type EdgeGoalKey,
+  type EdgeGoalNode,
+  type EdgeGoalPropsResolved,
+  type EdgeGoalTree,
+  type EdgeResource,
+  type EdgeResourceKey,
+  type EdgeTask,
+  type EdgeTaskKey,
+} from './mapper';
+
+// Types
+export type {
+  EdgeGoalProps,
+  EdgeResourceProps,
+  EdgeResourceVariable,
+  EdgeTaskProps,
+  ExecCondition,
+  GoalExecutionDetail,
+} from './types';
+
+// Transformation (template engine)
+export { generateValidatedPrismModel } from './template';
+
+// Logger
+export { getLogger, initLogger, type LoggerReport } from './logger/logger';
+
+// Validator
+export { formatValidationReport, validate } from './validator';

packages/lib/src/engines/edgeV2/logger/filePath.ts

@@ -0,0 +1,46 @@
+import fs from 'fs';
+import path from 'path';
+
+/**
+ * Calculates the log file path for a given model file name
+ * @param modelFileName The model file name (e.g., "examples/experiments/1-minimal.txt")
+ * @param extension The file extension (default: ".log")
+ * @returns The full path to the log file (e.g., "logs/examples/experiments/1-minimal.txt.log")
+ */
+export const getLogFilePath = (
+  modelFileName: string,
+  extension: string = '.log',
+): string => {
+  return `logs/${modelFileName}${extension}`;
+};
+
+/**
+ * Ensures the directory for a log file exists and returns the full path
+ * @param modelFileName The model file name
+ * @param extension The file extension (default: ".log")
+ * @returns The full path to the log file, or null if directory creation fails (e.g., in serverless environments)
+ */
+export const ensureLogFileDirectory = (
+  modelFileName: string,
+  extension: string = '.log',
+): string | null => {
+  // In serverless environments (like Vercel), filesystem is read-only
+  // Check if we're in a serverless environment
+  if (
+    process.env.VERCEL ||
+    process.env.AWS_LAMBDA_FUNCTION_NAME ||
+    process.env.NEXT_PHASE
+  ) {
+    return null;
+  }
+
+  try {
+    const logFilePath = getLogFilePath(modelFileName, extension);
+    const logDir = path.dirname(logFilePath);
+    fs.mkdirSync(logDir, { recursive: true });
+    return logFilePath;
+  } catch {
+    // If directory creation fails (e.g., read-only filesystem), return null
+    return null;
+  }
+};