diff --git a/.DS_Store b/.DS_Store index ba69c9fb..e80b5c16 100644 Binary files a/.DS_Store and b/.DS_Store differ diff --git a/examples/edgeV2/EDGE goal snippets.txt b/examples/edgeV2/EDGE goal snippets.txt new file mode 100644 index 00000000..9007cb01 --- /dev/null +++ b/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 decision_G1 -> (g0_failed'=g0_failed+1); //if we need to retry N times + [skip_G0] !g0_achieved & g0=1 & g1=0 & g0_failed (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 (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); + diff --git a/package.json b/package.json index 897a9763..fa3ddf18 100644 --- a/package.json +++ b/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", diff --git a/packages/lib/src/engines/edgeV2/index.ts b/packages/lib/src/engines/edgeV2/index.ts new file mode 100644 index 00000000..a91ba081 --- /dev/null +++ b/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'; diff --git a/packages/lib/src/engines/edgeV2/logger/filePath.ts b/packages/lib/src/engines/edgeV2/logger/filePath.ts new file mode 100644 index 00000000..e939c895 --- /dev/null +++ b/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; + } +}; diff --git a/packages/lib/src/engines/edgeV2/logger/logger.ts b/packages/lib/src/engines/edgeV2/logger/logger.ts new file mode 100644 index 00000000..6f0b769d --- /dev/null +++ b/packages/lib/src/engines/edgeV2/logger/logger.ts @@ -0,0 +1,694 @@ +import type { Resource } from '@goal-controller/goal-tree'; +import fs from 'fs'; +import type { EdgeGoalNode, EdgeTask, GoalExecutionDetail } from '../types'; +import { ensureLogFileDirectory } from './filePath'; + +// Type aliases for backwards compatibility +type GoalNode = EdgeGoalNode; +type Task = EdgeTask; + +type LoggerStore = { + goalModules: number; + goalVariables: number; + goalPursueLines: number; + goalAchievabilityFormulas: number; + goalMaintainFormulas: number; + goalAchievedLines: number; + goalSkipLines: number; + tasksVariables: number; + tasksLabels: number; + tasksAchievabilityConstants: number; + tasksTryLines: number; + tasksFailedLines: number; + tasksAchievedLines: number; + tasksSkippedLines: number; + systemVariables: number; + systemResources: number; + systemContextVariables: number; + // New counters + totalGoals: number; + goalTypeDegradation: number; + goalTypeChoice: number; + goalTypeAlternative: number; + goalTypeSequence: number; + goalTypeInterleaved: number; + totalTasks: number; + totalResources: number; + totalNodes: number; + totalVariables: number; +}; + +type LoggerReport = { + log: string; + summary: { + elapsedTime: string; + elapsedTimeMs: number; + totalGoals: number; + totalTasks: number; + totalResources: number; + totalNodes: number; + totalVariables: number; + goalTypeDegradation: number; + goalTypeChoice: number; + goalTypeAlternative: number; + goalTypeSequence: number; + goalTypeInterleaved: number; + goalModules: number; + goalVariables: number; + goalPursueLines: number; + goalAchievedLines: number; + goalSkippedLines: number; + goalAchievabilityFormulas: number; + goalMaintainFormulas: number; + tasksVariables: number; + tasksLabels: number; + tasksTryLines: number; + tasksFailedLines: number; + tasksAchievedLines: number; + tasksSkippedLines: number; + tasksAchievabilityConstants: number; + systemVariables: number; + systemResources: number; + systemContextVariables: number; + }; +}; + +export type { LoggerReport }; + +type VariableDefinitionBase = { + variable: string; + initialValue: number | boolean | 'MISSING_VARIABLE_DEFINITION'; + upperBound?: number | boolean; + lowerBound?: number | boolean; + type?: 'boolean' | 'int'; +}; + +type VariableDefinition = + | (VariableDefinitionBase & { context: 'goal' | 'task' }) + | (VariableDefinitionBase & { + context: 'system'; + subContext: 'resource' | 'context'; + }); + +export const createStore = (): LoggerStore => { + // Create a plain object to hold the state + const state: LoggerStore = { + goalModules: 0, + goalVariables: 0, + goalPursueLines: 0, + goalAchievabilityFormulas: 0, + goalMaintainFormulas: 0, + tasksVariables: 0, + tasksLabels: 0, + tasksAchievabilityConstants: 0, + systemVariables: 0, + goalAchievedLines: 0, + goalSkipLines: 0, + tasksTryLines: 0, + tasksFailedLines: 0, + tasksAchievedLines: 0, + tasksSkippedLines: 0, + systemResources: 0, + systemContextVariables: 0, + // New counters + totalGoals: 0, + goalTypeDegradation: 0, + goalTypeChoice: 0, + goalTypeAlternative: 0, + goalTypeSequence: 0, + goalTypeInterleaved: 0, + totalTasks: 0, + totalResources: 0, + totalNodes: 0, + totalVariables: 0, + }; + + // Create a Proxy that intercepts property access for all LoggerStore properties + // eslint-disable-next-line @typescript-eslint/consistent-type-assertions + const emptyStore = {} as LoggerStore; + return new Proxy(emptyStore, { + get(_target, prop: keyof LoggerStore) { + return state[prop]; + }, + set(_target, prop: keyof LoggerStore, value: number) { + state[prop] = value; + return true; + }, + }); +}; + +const createLoggerFile = (modelFileName: string): fs.WriteStream | null => { + try { + const logFilePath = ensureLogFileDirectory(modelFileName, '.log'); + if (!logFilePath) { + // Directory creation failed (e.g., serverless environment) + return null; + } + return fs.createWriteStream(logFilePath, { flags: 'w' }); + } catch { + // If file creation fails, return null for in-memory mode + return null; + } +}; + +const createLogger = ( + modelFileName: string, + store: LoggerStore, + logToConsole: boolean = false, + inMemory: boolean = false, +) => { + const startTime = Date.now(); + const logFile = inMemory ? null : createLoggerFile(modelFileName); + const logBuffer: string[] = []; + + const write = (message: string): void => { + if (logFile) { + logFile.write(message); + } else { + // In-memory mode: store in buffer + logBuffer.push(message); + } + if (logToConsole) { + // eslint-disable-next-line no-console + console.log(message); + } + }; + + const loggerInstance = { + initGoal: (goal: GoalNode) => { + store.goalModules++; + store.totalGoals++; + + // Track execution detail type + if (goal.properties.engine.executionDetail) { + switch (goal.properties.engine.executionDetail.type) { + case 'degradation': + store.goalTypeDegradation++; + break; + case 'choice': + store.goalTypeChoice++; + break; + case 'alternative': + store.goalTypeAlternative++; + break; + case 'sequence': + store.goalTypeSequence++; + break; + case 'interleaved': + store.goalTypeInterleaved++; + break; + } + } + + write(`[INIT GOAL] ${goal.id}: ${goal.name ?? 'none'}\n`); + write( + `\tChildren: ${ + goal.children?.length && goal.children.length > 0 + ? goal.children.map((child: GoalNode) => child.id).join(', ') + : 'none' + }\n`, + ); + write( + `\tTasks: ${goal.tasks?.map((task: Task) => task.id).join(', ') ?? 'none'}\n`, + ); + write( + `\tType: ${ + goal.properties.engine.execCondition?.maintain?.sentence + ? 'maintain' + : 'achieve' + }\n`, + ); + write(`\tRelation to children: ${goal.relationToChildren ?? 'none'}\n`); + write( + `\tExecution detail: ${goal.properties.engine.executionDetail?.type ?? 'none'}\n`, + ); + write(`\t[TRACE]: [${goal.id}] Emits module: ${goal.id}\n`); + }, + initTask: (task: Task) => { + store.totalTasks++; + + // Count resources for this task + if (task.resources && task.resources.length > 0) { + store.totalResources += task.resources.length; + } + + write(`[INIT TASK] ${task.id}: ${task.name ?? 'none'}\n`); + write( + `\tResources: ${ + task.resources?.length && task.resources.length > 0 + ? task.resources.map((resource: Resource) => resource.id).join(', ') + : 'none' + }\n`, + ); + }, + initSystem: () => { + write('[INIT SYSTEM MODULE]\n'); + }, + maintainFormulaDefinition: ( + goalId: string, + formula: string, + sentence: string, + prismLine: string, + ) => { + store.goalMaintainFormulas++; + write(`\t[TRACE] ${goalId}.maintainCondition -> ${formula} \n`); + write( + `\t[FORMULA DEFINITION] ${formula}; guard statement: ${sentence}\n`, + ); + write(`\t\t[PRISM emitted statement]: ${prismLine}\n`); + }, + achievabilityFormulaDefinition: ( + goalId: string, + formula: string, + type: 'AND' | 'OR' | 'SINGLE_GOAL' | 'LEAF', + sentence: string, + prismLine: string, + ) => { + store.goalAchievabilityFormulas++; + write(`\t[TRACE] ${goalId}.${type} -> ${formula} \n`); + write( + `\t[FORMULA DEFINITION] ${formula}; guard statement: ${sentence}\n`, + ); + write(`\t\t[PRISM emitted statement]: ${prismLine}\n`); + }, + achievabilityTaskConstant: ( + taskId: string, + constant: string, + value: number, + ) => { + store.tasksAchievabilityConstants++; + write( + `\t[TASK ACHIEVABILITY CONSTANT] ${taskId}: ${constant} = ${value}\n`, + ); + }, + taskTranstions: { + transition: ( + taskId: string, + leftStatement: string, + updateStatement: string, + prismLabelStatement: string, + transition: 'pursue' | 'achieve' | 'failed' | 'try', + maxRetries?: number, + ) => { + store.tasksLabels++; + switch (transition) { + case 'try': + store.tasksTryLines++; + break; + case 'failed': + store.tasksFailedLines++; + break; + case 'achieve': + store.tasksAchievedLines++; + break; + case 'pursue': + store.tasksSkippedLines++; + break; + } + + const transitionLogLabel = transition.toUpperCase(); + write( + `\t[${transitionLogLabel}] Task ${taskId} ${transitionLogLabel} label\n`, + ); + write(`\t\t[CONDITION] ${leftStatement}\n`); + if (maxRetries) { + write(`\t\t[MAX RETRIES] ${maxRetries}\n`); + } + write(`\t\t[UPDATE] ${updateStatement}\n`); + write(`\t\tPRISM statement: ${prismLabelStatement}\n`); + write(`\t[END OF ${transitionLogLabel}]\n`); + }, + }, + pursue: { + pursue: (node: GoalNode | Task, step: number) => { + write(`\t[PURSUE GENERATION] ${node.id} - STEP ${step}\n`); + }, + defaultPursueCondition: (pursueCondition: string) => { + write(`\t\t[DEFAULT PURSUE CONDITION] ${pursueCondition}\n`); + }, + update: (update: string) => { + write(`\t\t[UPDATE] ${update}\n`); + }, + goalDependency: (goalId: string, dependsOn: string[]) => { + if (!dependsOn.length) { + return; + } + write(`\t\t[GOAL DEPENDENCY] ${goalId}: ${dependsOn.join(', ')}\n`); + }, + executionDetail: { + choice: ( + currentGoal: string, + otherGoals: string[], + guardStatement: string, + ) => { + write('\t\t[EXECUTION DETAIL: CHOICE]\n'); + write(`\t\t\t[CURRENT GOAL] ${currentGoal}\n`); + write(`\t\t\t[OTHER GOALS] ${otherGoals.join(', ')}\n`); + write(`\t\t\t[GUARD STATEMENT] ${guardStatement}\n`); + }, + degradation: { + init: (currentGoal: string, degradation: string[]) => { + const priority = + degradation.findIndex((goal) => goal === currentGoal) + 1; + write( + `\t\t[EXECUTION DETAIL: DEGRADATION] ${currentGoal} priority #${priority} : ${degradation.join( + ' -> ', + )}\n`, + ); + }, + retry: ( + currentGoal: string, + goalToRetry: string, + amountOfRetries: number, + ) => { + write( + `\t\t[EXECUTION DETAIL: DEGRADATION] ${currentGoal} retry after: ${goalToRetry} ${amountOfRetries} times\n`, + ); + }, + alternative: (currentGoal: string, alternative: string[]) => { + write( + `\t\t[EXECUTION DETAIL: ALTERNATIVE GOAL] ${currentGoal} other alternatives: ${alternative.join( + ', ', + )}\n`, + ); + }, + }, + sequence: ( + goalId: string, + currentGoal: string, + leftGoals: string[], + rightGoals: string[], + ) => { + write( + `\t\t[EXECUTION DETAIL: SEQUENCE] ${goalId}: Curr ${currentGoal};\n`, + ); + write( + `\t\t\t[LEFT GOALS] - should be achieved: ${ + leftGoals.length > 0 ? leftGoals.join(', ') : 'none' + }\n`, + ); + write( + `\t\t\t[RIGHT GOALS] - should be not achieved: ${rightGoals.join( + ', ', + )}\n`, + ); + }, + alternative: (currentGoal: string, alternative: string[]) => { + write( + `\t\t[EXECUTION DETAIL: ALTERNATIVE GOAL] ${currentGoal} other alternatives: ${alternative.join( + ', ', + )}\n`, + ); + }, + interleaved: () => { + write( + '\t\t[EXECUTION DETAIL: INTERLEAVED] interleaved goals have no guard condition\n', + ); + }, + activationContext: (sentence: string) => { + write( + `\t\t[EXECUTION DETAIL: CONTEXT] Guard statement: ${sentence}\n`, + ); + }, + noActivationContext: (goalId: string) => { + write( + `\t\t[EXECUTION DETAIL: CONTEXT] Guard statement: ${goalId} has no activation context\n`, + ); + }, + }, + stepStatement: (step: number, left: string, right: string) => { + write(`\t\tPRISM statement: ${left} -> ${right}\n`); + write(`\t[END OF STEP ${step}]\n`); + }, + finish: () => { + store.goalPursueLines++; + write('\t[END OF PURSUE]\n'); + }, + }, + achieve: ( + goalId: string, + condition: string, + update: string, + prismLabelStatement: string, + ) => { + store.goalAchievedLines++; + write(`\t[ACHIEVE] Goal ${goalId} achieved label\n`); + write(`\t\t[CONDITION] ${condition}\n`); + write(`\t\t[UPDATE] ${update}\n`); + write(`\t\tPRISM statement: ${prismLabelStatement}\n`); + write('\t[END OF ACHIEVE]\n'); + }, + skip: ( + goalId: string, + leftStatement: string, + updateStatement: string, + prismLabelStatement: string, + ) => { + store.goalSkipLines++; + write(`\t[SKIP] Goal ${goalId} skipped label\n`); + write(`\t\t[CONDITION] ${leftStatement}\n`); + write(`\t\t[UPDATE] ${updateStatement}\n`); + write(`\t\tPRISM statement: ${prismLabelStatement}\n`); + write('\t[END OF SKIP]\n'); + }, + variableDefinition: ({ + variable, + initialValue, + upperBound, + lowerBound, + type = 'int', + context = 'goal', + ...props + }: VariableDefinition) => { + if (context === 'goal') { + store.goalVariables++; + } else if (context === 'task') { + store.tasksVariables++; + } else if (context === 'system') { + store.systemVariables++; + if ('subContext' in props && props.subContext === 'resource') { + store.systemResources++; + } else if ('subContext' in props && props.subContext === 'context') { + store.systemContextVariables++; + } + } + + if (initialValue === 'MISSING_VARIABLE_DEFINITION') { + write( + `\t[VARIABLE DEFINITION] ${variable}; initial value: MISSING_VARIABLE_DEFINITION; type: ${type}\n`, + ); + return; + } + + if (type === 'boolean') { + write( + `\t[VARIABLE DEFINITION] ${variable}; initial value: ${initialValue}; type: ${type}\n`, + ); + return; + } + write( + `\t[VARIABLE DEFINITION] ${variable}; initial value: ${initialValue}; ${ + lowerBound ? `lower bound: ${lowerBound}; ` : '' + }${upperBound ? `upper bound: ${upperBound};` : ''} type: ${type}\n`, + ); + }, + executionDetail: (executionDetail: GoalExecutionDetail) => { + write(`\t[EXECUTION DETAIL] ${executionDetail.type}\n`); + }, + + info: (message: string, level: number) => { + write(`${'\t'.repeat(level)}${message}\n`); + }, + error: (source: string, message: string | Error | unknown) => { + write(`[ERROR] ${source}: ${message as string}\n`); + }, + trace: (source: string, message: string, level: number = 0) => { + write(`${'\t'.repeat(level)}[TRACE] ${source}: ${message}\n`); + }, + getReport: (): LoggerReport => { + const endTime = Date.now(); + const elapsedTime = endTime - startTime; + const elapsedSeconds = (elapsedTime / 1000).toFixed(3); + const elapsedFormatted = + elapsedTime >= 1000 + ? `${elapsedSeconds}s (${elapsedTime}ms)` + : `${elapsedTime}ms`; + + // Calculate total nodes and total variables + store.totalNodes = + store.totalGoals + store.totalTasks + store.totalResources; + store.totalVariables = + store.goalVariables + store.tasksVariables + store.systemVariables; + + const summaryLines: string[] = []; + summaryLines.push('----------------------------------------\n'); + summaryLines.push(`[LOGGER SUMMARY] ${modelFileName}\n`); + summaryLines.push(`[ELAPSED TIME] ${elapsedFormatted}\n`); + summaryLines.push('----------MODEL STRUCTURE SUMMARY----------\n'); + summaryLines.push(`[TOTAL GOALS] ${store.totalGoals}\n`); + summaryLines.push(`[TOTAL TASKS] ${store.totalTasks}\n`); + summaryLines.push(`[TOTAL RESOURCES] ${store.totalResources}\n`); + summaryLines.push(`[TOTAL NODES] ${store.totalNodes}\n`); + summaryLines.push(`[TOTAL VARIABLES] ${store.totalVariables}\n`); + summaryLines.push('----------GOAL TYPE BREAKDOWN----------\n'); + summaryLines.push( + `[GOAL TYPE: DEGRADATION] ${store.goalTypeDegradation}\n`, + ); + summaryLines.push(`[GOAL TYPE: CHOICE] ${store.goalTypeChoice}\n`); + summaryLines.push( + `[GOAL TYPE: ALTERNATIVE] ${store.goalTypeAlternative}\n`, + ); + summaryLines.push(`[GOAL TYPE: SEQUENCE] ${store.goalTypeSequence}\n`); + summaryLines.push( + `[GOAL TYPE: INTERLEAVED] ${store.goalTypeInterleaved}\n`, + ); + summaryLines.push('----------GOAL SUMMARY----------\n'); + summaryLines.push(`[GOAL MODULES] ${store.goalModules}\n`); + summaryLines.push(`[GOAL VARIABLES] ${store.goalVariables}\n`); + summaryLines.push(`[GOAL PURSUE LINES] ${store.goalPursueLines}\n`); + summaryLines.push(`[GOAL ACHIEVED LINES] ${store.goalAchievedLines}\n`); + summaryLines.push(`[GOAL SKIPPED LINES] ${store.goalSkipLines}\n`); + summaryLines.push( + `[GOAL ACHIEVABILITY FORMULAS] ${store.goalAchievabilityFormulas}\n`, + ); + summaryLines.push( + `[GOAL MAINTAIN FORMULAS] ${store.goalMaintainFormulas}\n`, + ); + summaryLines.push('----------CHANGE MANAGER SUMMARY----------\n'); + summaryLines.push(`[TASKS VARIABLES] ${store.tasksVariables}\n`); + summaryLines.push(`[TASKS LABELS] ${store.tasksLabels}\n`); + summaryLines.push(`[TASKS TRY LINES] ${store.tasksTryLines}\n`); + summaryLines.push(`[TASKS FAILED LINES] ${store.tasksFailedLines}\n`); + summaryLines.push(`[TASKS ACHIEVED LINES] ${store.tasksAchievedLines}\n`); + summaryLines.push(`[TASKS SKIPPED LINES] ${store.tasksSkippedLines}\n`); + summaryLines.push( + `[TASKS ACHIEVABILITY CONSTANTS] ${store.tasksAchievabilityConstants}\n`, + ); + summaryLines.push('----------SYSTEM SUMMARY----------\n'); + summaryLines.push(`[SYSTEM VARIABLES] ${store.systemVariables}\n`); + summaryLines.push(`[SYSTEM RESOURCES] ${store.systemResources}\n`); + summaryLines.push( + `[SYSTEM CONTEXT VARIABLES] ${store.systemContextVariables}\n`, + ); + summaryLines.push('----------------------------------------\n'); + + const fullLog = logBuffer.join('') + summaryLines.join(''); + + return { + log: fullLog, + summary: { + elapsedTime: elapsedFormatted, + elapsedTimeMs: elapsedTime, + totalGoals: store.totalGoals, + totalTasks: store.totalTasks, + totalResources: store.totalResources, + totalNodes: store.totalNodes, + totalVariables: store.totalVariables, + goalTypeDegradation: store.goalTypeDegradation, + goalTypeChoice: store.goalTypeChoice, + goalTypeAlternative: store.goalTypeAlternative, + goalTypeSequence: store.goalTypeSequence, + goalTypeInterleaved: store.goalTypeInterleaved, + goalModules: store.goalModules, + goalVariables: store.goalVariables, + goalPursueLines: store.goalPursueLines, + goalAchievedLines: store.goalAchievedLines, + goalSkippedLines: store.goalSkipLines, + goalAchievabilityFormulas: store.goalAchievabilityFormulas, + goalMaintainFormulas: store.goalMaintainFormulas, + tasksVariables: store.tasksVariables, + tasksLabels: store.tasksLabels, + tasksTryLines: store.tasksTryLines, + tasksFailedLines: store.tasksFailedLines, + tasksAchievedLines: store.tasksAchievedLines, + tasksSkippedLines: store.tasksSkippedLines, + tasksAchievabilityConstants: store.tasksAchievabilityConstants, + systemVariables: store.systemVariables, + systemResources: store.systemResources, + systemContextVariables: store.systemContextVariables, + }, + }; + }, + close: () => { + const endTime = Date.now(); + const elapsedTime = endTime - startTime; + const elapsedSeconds = (elapsedTime / 1000).toFixed(3); + const elapsedFormatted = + elapsedTime >= 1000 + ? `${elapsedSeconds}s (${elapsedTime}ms)` + : `${elapsedTime}ms`; + + // Calculate total nodes and total variables + store.totalNodes = + store.totalGoals + store.totalTasks + store.totalResources; + store.totalVariables = + store.goalVariables + store.tasksVariables + store.systemVariables; + + write('----------------------------------------\n'); + write(`[LOGGER SUMMARY] ${modelFileName}\n`); + write(`[ELAPSED TIME] ${elapsedFormatted}\n`); + write('----------MODEL STRUCTURE SUMMARY----------\n'); + write(`[TOTAL GOALS] ${store.totalGoals}\n`); + write(`[TOTAL TASKS] ${store.totalTasks}\n`); + write(`[TOTAL RESOURCES] ${store.totalResources}\n`); + write(`[TOTAL NODES] ${store.totalNodes}\n`); + write(`[TOTAL VARIABLES] ${store.totalVariables}\n`); + write('----------GOAL TYPE BREAKDOWN----------\n'); + write(`[GOAL TYPE: DEGRADATION] ${store.goalTypeDegradation}\n`); + write(`[GOAL TYPE: CHOICE] ${store.goalTypeChoice}\n`); + write(`[GOAL TYPE: ALTERNATIVE] ${store.goalTypeAlternative}\n`); + write(`[GOAL TYPE: SEQUENCE] ${store.goalTypeSequence}\n`); + write(`[GOAL TYPE: INTERLEAVED] ${store.goalTypeInterleaved}\n`); + write('----------GOAL SUMMARY----------\n'); + write(`[GOAL MODULES] ${store.goalModules}\n`); + write(`[GOAL VARIABLES] ${store.goalVariables}\n`); + write(`[GOAL PURSUE LINES] ${store.goalPursueLines}\n`); + write(`[GOAL ACHIEVED LINES] ${store.goalAchievedLines}\n`); + write(`[GOAL SKIPPED LINES] ${store.goalSkipLines}\n`); + write( + `[GOAL ACHIEVABILITY FORMULAS] ${store.goalAchievabilityFormulas}\n`, + ); + write(`[GOAL MAINTAIN FORMULAS] ${store.goalMaintainFormulas}\n`); + write('----------CHANGE MANAGER SUMMARY----------\n'); + write(`[TASKS VARIABLES] ${store.tasksVariables}\n`); + write(`[TASKS LABELS] ${store.tasksLabels}\n`); + write(`[TASKS TRY LINES] ${store.tasksTryLines}\n`); + write(`[TASKS FAILED LINES] ${store.tasksFailedLines}\n`); + write(`[TASKS ACHIEVED LINES] ${store.tasksAchievedLines}\n`); + write(`[TASKS SKIPPED LINES] ${store.tasksSkippedLines}\n`); + write( + `[TASKS ACHIEVABILITY CONSTANTS] ${store.tasksAchievabilityConstants}\n`, + ); + write('----------SYSTEM SUMMARY----------\n'); + write(`[SYSTEM VARIABLES] ${store.systemVariables}\n`); + write(`[SYSTEM RESOURCES] ${store.systemResources}\n`); + write(`[SYSTEM CONTEXT VARIABLES] ${store.systemContextVariables}\n`); + write('----------------------------------------\n'); + if (logFile) { + logFile.end(); + } + }, + }; + + return loggerInstance; +}; + +let logger: ReturnType; +let store: LoggerStore; + +export const initLogger = ( + modelFileName: string, + logToConsole: boolean = false, + inMemory: boolean = false, +): ReturnType => { + store = createStore(); + logger = createLogger(modelFileName, store, logToConsole, inMemory); + return logger; +}; + +export const getLogger = (): ReturnType => { + if (!logger) { + throw new Error('Logger not initialized'); + } + return logger; +}; diff --git a/packages/lib/src/engines/edgeV2/mapper.ts b/packages/lib/src/engines/edgeV2/mapper.ts new file mode 100644 index 00000000..62d40e3a --- /dev/null +++ b/packages/lib/src/engines/edgeV2/mapper.ts @@ -0,0 +1,312 @@ +/** + * Edge Engine Mapper + * Maps raw iStar model properties to Edge/PRISM engine-specific properties + */ +import { + createEngineMapper, + getAssertionVariables, + type GoalNode, + type GoalTreeType, + type RawProps, + type Resource, + type Task, +} from '@goal-controller/goal-tree'; +import type { + EdgeResourceProps, + EdgeTaskProps, + ExecCondition, + GoalExecutionDetail, +} from './types'; +import { parseStrictInt } from './retryCoercion'; + +/** + * Allowed keys for Edge goal custom properties + */ +export const EDGE_GOAL_KEYS = [ + 'root', + 'maxRetries', + 'utility', + 'cost', + 'dependsOn', + 'type', + 'maintain', + 'assertion', +] as const; + +/** + * Allowed keys for Edge task custom properties + */ +export const EDGE_TASK_KEYS = ['maxRetries', 'type', 'assertion'] as const; + +/** + * Allowed keys for Edge resource custom properties + */ +export const EDGE_RESOURCE_KEYS = [ + 'type', + 'initialValue', + 'lowerBound', + 'upperBound', +] as const; + +// Type aliases for the allowed keys +export type EdgeGoalKey = (typeof EDGE_GOAL_KEYS)[number]; +export type EdgeTaskKey = (typeof EDGE_TASK_KEYS)[number]; +export type EdgeResourceKey = (typeof EDGE_RESOURCE_KEYS)[number]; + +/** + * Parse and validate maxRetries value + * Returns 0 if not provided, throws if invalid + */ +const parseMaxRetries = ( + maxRetries: string | undefined, + nodeType: 'goal' | 'task', +): number => { + if (!maxRetries) { + return 0; + } + const parsed = parseInt(maxRetries, 10); + if (isNaN(parsed) || parsed < 0) { + throw new Error( + `[INVALID ${nodeType.toUpperCase()}]: maxRetries must be a non-negative integer: got "${maxRetries}"`, + ); + } + return parsed; +}; + +const getMaintainCondition = ( + customProperties: RawProps | RawProps, + nodeType: 'goal' | 'task', +): ExecCondition | undefined => { + if (customProperties.type === 'maintain') { + if (!('maintain' in customProperties)) { + throw new Error( + `[INVALID MODEL]: Maintain condition for ${nodeType} must have 'maintain' and 'assertion'; got maintain: none, assertion: ${customProperties.assertion || "'empty condition'"}`, + ); + } + if (!customProperties.maintain || !customProperties.assertion) { + console.warn( + `[INVALID MODEL]: Maintain condition for ${nodeType} must have maintain and assertion: got maintain:${ + customProperties.maintain || "'empty condition'" + } and assertion:${customProperties.assertion || "'empty condition'"}`, + ); + } + + return { + maintain: { + sentence: customProperties.maintain ?? '', + variables: getAssertionVariables({ + assertionSentence: customProperties.maintain ?? '', + }), + }, + assertion: { + sentence: customProperties.assertion ?? '', + variables: getAssertionVariables({ + assertionSentence: customProperties.assertion ?? '', + }), + }, + }; + } + + if (customProperties.assertion) { + const assertionVariables = getAssertionVariables({ + assertionSentence: customProperties.assertion, + }); + + return { + assertion: { + sentence: customProperties.assertion, + variables: assertionVariables, + }, + }; + } + + return undefined; +}; + +// Using an interface allows circular references (interfaces are lazily evaluated) +// This gives us proper typing: dependsOn[0].properties.engine is EdgeGoalPropsResolved +// eslint-disable-next-line @typescript-eslint/consistent-type-definitions +export interface EdgeGoalPropsResolved { + utility: string; + cost: string; + dependsOn: EdgeGoalNode[]; + executionDetail: GoalExecutionDetail | null; + execCondition?: ExecCondition; + maxRetries: number; +} + +/** + * Parse dependsOn string into array of goal IDs + */ +const parseDependsOn = (dependsOn: string | undefined): string[] => { + if (!dependsOn) { + return []; + } + return dependsOn + .split(',') + .map((d) => d.trim()) + .filter(Boolean); +}; + +/** + * Edge Engine Mapper for creating EDGE/PRISM-compatible goal trees + * Engine types are explicit, key types are inferred from the allowedKeys arrays + */ +export const edgeEngineMapper = createEngineMapper< + EdgeGoalPropsResolved, + EdgeTaskProps, + EdgeResourceProps +>()({ + allowedGoalKeys: EDGE_GOAL_KEYS, + allowedTaskKeys: EDGE_TASK_KEYS, + allowedResourceKeys: EDGE_RESOURCE_KEYS, + mapGoalProps: ({ raw, executionDetail }) => { + const execCondition = getMaintainCondition(raw, 'goal'); + + return { + utility: raw.utility || '', + cost: raw.cost || '', + dependsOn: [], + executionDetail, + execCondition, + maxRetries: parseMaxRetries(raw.maxRetries, 'goal'), + }; + }, + + mapTaskProps: ({ raw }) => { + const execCondition = getMaintainCondition(raw, 'task'); + + return { + execCondition, + maxRetries: parseMaxRetries(raw.maxRetries, 'task'), + }; + }, + + mapResourceProps: ({ raw }) => { + const { type, initialValue, lowerBound, upperBound } = raw; + + switch (type) { + case 'bool': { + // Validate initialValue is strictly 'true' or 'false' + if (initialValue !== 'true' && initialValue !== 'false') { + throw new Error( + `[INVALID RESOURCE]: Boolean resource must have initialValue of 'true' or 'false', got: ${initialValue === undefined ? 'undefined' : `"${initialValue}"`}`, + ); + } + return { + variable: { + type: 'boolean' as const, + initialValue: initialValue === 'true', + }, + }; + } + case 'int': { + // Check for null/undefined/empty string explicitly to allow "0" as valid value + if ( + initialValue == null || + lowerBound == null || + upperBound == null || + initialValue === '' || + lowerBound === '' || + upperBound === '' + ) { + throw new Error( + '[INVALID RESOURCE]: Integer resource must have an initial value, lower bound, and upper bound', + ); + } + + const lowerBoundInt = parseStrictInt(lowerBound); + const upperBoundInt = parseStrictInt(upperBound); + + if (isNaN(lowerBoundInt) || isNaN(upperBoundInt)) { + throw new Error( + `[INVALID RESOURCE]: Resource bounds must be plain integers, got: lowerBound="${lowerBound}" upperBound="${upperBound}"`, + ); + } + + if (lowerBoundInt > upperBoundInt) { + throw new Error( + `[INVALID RESOURCE]: Resource lower bound (${lowerBoundInt}) must be less than or equal to upper bound (${upperBoundInt})`, + ); + } + + const initialValueInt = parseStrictInt(initialValue); + + if (isNaN(initialValueInt)) { + throw new Error( + `[INVALID RESOURCE]: Resource initial value must be a plain integer, got: "${initialValue}"`, + ); + } + + // Validate initialValue is within bounds + if ( + initialValueInt < lowerBoundInt || + initialValueInt > upperBoundInt + ) { + throw new Error( + `[INVALID RESOURCE]: Initial value (${initialValueInt}) must be within bounds [${lowerBoundInt}, ${upperBoundInt}]`, + ); + } + + return { + variable: { + type: 'int' as const, + initialValue: initialValueInt, + lowerBound: lowerBoundInt, + upperBound: upperBoundInt, + }, + }; + } + default: + throw new Error( + `[INVALID RESOURCE]: Unsupported resource type: ${type}`, + ); + } + }, + + afterCreationMapper: ({ node, allNodes, rawProperties }) => { + // Only process goal nodes for dependsOn resolution + if (rawProperties.nodeType !== 'goal' || node.type !== 'goal') { + // For non-goal nodes, return the existing engine props + return node.properties.engine; + } + + const depIds = parseDependsOn(rawProperties.raw.dependsOn); + + const resolvedDeps = depIds.map((id) => { + const depNode = allNodes.get(id); + if (!depNode) { + throw new Error( + `[INVALID MODEL]: Dependency ${id} not found for node ${node.id}`, + ); + } + if (depNode.type !== 'goal') { + throw new Error( + `[INVALID MODEL]: Dependency ${id} for node ${node.id} must be a goal, got ${depNode.type}`, + ); + } + return depNode; + }); + + return { + ...node.properties.engine, + dependsOn: resolvedDeps, + }; + }, +}); + +/** + * Type aliases for Edge-specific tree types + */ +export type EdgeGoalNode = GoalNode< + EdgeGoalPropsResolved, + EdgeTaskProps, + EdgeResourceProps +>; +export type EdgeTask = Task; +export type EdgeResource = Resource; +export type EdgeGoalTree = GoalTreeType< + EdgeGoalPropsResolved, + EdgeTaskProps, + EdgeResourceProps +>; diff --git a/packages/lib/src/engines/edgeV2/mdp/common.ts b/packages/lib/src/engines/edgeV2/mdp/common.ts new file mode 100644 index 00000000..db3813f4 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/mdp/common.ts @@ -0,0 +1,44 @@ +import type { Relation } from '@goal-controller/goal-tree'; +import { Node } from '@goal-controller/goal-tree'; + +export const separator = (relation: Relation | null): string => { + switch (relation) { + case 'or': + return ' | '; + case 'and': + return ' & '; + default: + throw new Error(`Relation "${relation}" not allowed`); + } +}; + +export const formulaForGoal = (goalId: string): string => + `${Node.rootId(goalId)}_achieved_or_pursued`; + +export const not = (s: string): string => (s ? `!${s}` : s); +export const parenthesis = (s: string): string => (s ? `(${s})` : s); + +export const achieved = (goalId: string): string => `${goalId}_achieved`; +export const achievable = (goalId: string): string => `${goalId}_achievable`; +/** Goal pursuit flag in Edge V2 PRISM modules (snippets: g0, g1, … as 0/1). */ +export const goalState = (goalId: string): string => `${goalId}_state`; +export const pursued = (goalId: string): string => `${goalId}_pursued`; +export const achievedOrPursued = (goalId: string): string => + pursued(`${achieved(goalId)}_or`); +export const pursue = (goalId: string): string => `${goalId}_pursue`; +export const pursueThrough = (goalId: string, through: string): string => + `pursue${goalId}_${through}`; +export const pursueDefault = (goalId: string): string => `${goalId}_pursue0`; +export const skip = (goalId: string): string => `${goalId}_skip`; + +export const failed = (goalId: string): string => `${goalId}_failed`; + +export const OR = (elements: string[]): string => + elements.join(separator('or')); +export const AND = (elements: string[]): string => + elements.join(separator('and')); + +export const equals = (operand: string, value: string | number): string => + `${operand}=${value}`; +export const greaterThan = (goal: string, than: number): string => + `${goal}>${than}`; diff --git a/packages/lib/src/engines/edgeV2/retryCoercion.ts b/packages/lib/src/engines/edgeV2/retryCoercion.ts new file mode 100644 index 00000000..d0446a38 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/retryCoercion.ts @@ -0,0 +1,28 @@ +/** Matches strings that are a plain integer with no decimal point or trailing characters. */ +const STRICT_INT_RE = /^-?\d+$/; + +/** + * Parse a string as a strict integer: rejects decimals ("1.5"), partial-numeric + * strings ("10abc"), and empty/whitespace-only strings. + * Returns NaN for any rejected input so callers can treat it like a failed parse. + */ +export const parseStrictInt = (s: string): number => { + if (!STRICT_INT_RE.test(s.trim())) return NaN; + return Number(s.trim()); +}; + +/** + * Normalize degradation retry counts from the model (numbers or numeric strings from JSON). + * Rejects non-integer numbers (e.g. 1.5) and partial-numeric strings (e.g. "10abc", "1.5"). + */ +export const coercePositiveIntRetry = (value: unknown): number | null => { + if (typeof value === 'number') { + if (!Number.isFinite(value) || !Number.isInteger(value)) return null; + return value > 0 ? value : null; + } + if (typeof value === 'string') { + const n = parseStrictInt(value); + if (!Number.isNaN(n) && n > 0) return n; + } + return null; +}; diff --git a/packages/lib/src/engines/edgeV2/template/common.ts b/packages/lib/src/engines/edgeV2/template/common.ts new file mode 100644 index 00000000..a3a4df60 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/common.ts @@ -0,0 +1,23 @@ +// Variable names +export const pursuedVariable = (goalId: string): string => `${goalId}_pursued`; +export const achievedVariable = (goalId: string): string => + `${goalId}_achieved`; +export const chosenVariable = (goalId: string): string => `${goalId}_chosen`; +/** One PRISM int per goal module for nondeterministic resolution (snippets: decision_G0). */ +export const decisionVariable = (goalId: string): string => + `decision_${goalId}`; +/** OR-goal secondary nondet constant (snippets: _decision_G0 for child choice/shares). */ +export const underscoredOrDecisionVariable = (goalId: string): string => + `_decision_${goalId}`; + +// Transition labels +export const pursueTransition = (goalId: string): string => `pursue_${goalId}`; +export const achievedTransition = (goalId: string): string => + `achieved_${goalId}`; +export const failedTransition = (goalId: string): string => `failed_${goalId}`; +export const tryTransition = (goalId: string): string => `try_${goalId}`; + +// formulas +export const achievableFormulaVariable = (goalId: string): string => + `${goalId}_achievable`; +export const failed = (goalId: string): string => `${goalId}_failed`; diff --git a/packages/lib/src/engines/edgeV2/template/decisionVariables.ts b/packages/lib/src/engines/edgeV2/template/decisionVariables.ts new file mode 100644 index 00000000..71785c2b --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/decisionVariables.ts @@ -0,0 +1,34 @@ +import { GoalTree } from '@goal-controller/goal-tree'; +import type { EdgeGoalTree } from '../types'; +import { decisionVariable, underscoredOrDecisionVariable } from './common'; +import { goalNumberId } from './modules/goalModule/goalModules'; + +/** + * Uninterpreted decision constants after `dtmc`: every goal gets + * `decision_`; OR goals also get `_decision_` (snippet tie-break); + * every task gets `decision_` for child pursue thresholds under basic AND. + */ +export const decisionVariablesTemplate = ({ + gm, +}: { + gm: EdgeGoalTree; +}): string => { + const goals = GoalTree.allByType(gm, 'goal'); + const tasks = GoalTree.allByType(gm, 'task'); + + const goalLines = goals + .sort((a, b) => Number(goalNumberId(a.id)) - Number(goalNumberId(b.id))) + .flatMap((g) => { + const lines = [`const int ${decisionVariable(g.id)};`]; + if (g.relationToChildren === 'or') { + lines.push(`const int ${underscoredOrDecisionVariable(g.id)};`); + } + return lines; + }); + + const taskLines = tasks + .sort((a, b) => Number(goalNumberId(a.id)) - Number(goalNumberId(b.id))) + .map((t) => `const int ${decisionVariable(t.id)};`); + + return [...goalLines, ...taskLines].join('\n'); +}; diff --git a/packages/lib/src/engines/edgeV2/template/index.ts b/packages/lib/src/engines/edgeV2/template/index.ts new file mode 100644 index 00000000..5a503779 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/index.ts @@ -0,0 +1,57 @@ +import type { EdgeGoalTree } from '../types'; +import { summarizeValidationFailures, validate } from '../validator'; +import { decisionVariablesTemplate } from './decisionVariables'; +import { changeManagerModule } from './modules/changeManager/changeManager'; +import { goalModules } from './modules/goalModule/goalModules'; +import { systemModule } from './modules/system/system'; + +const edgeDTMCTemplate = ({ + gm, + fileName, + clean = false, + variables = {}, +}: { + gm: EdgeGoalTree; + fileName: string; + clean?: boolean; + variables?: Record; +}): string => { + const dtmcModel = `dtmc + +${decisionVariablesTemplate({ gm })} + +${goalModules({ gm })} + +${changeManagerModule({ gm, variables })} + +${systemModule({ gm, fileName, clean, variables })} +`; + return dtmcModel; +}; + +export const generateValidatedPrismModel = ({ + gm, + fileName, + clean = false, + variables = {}, +}: { + gm: EdgeGoalTree; + fileName: string; + clean?: boolean; + variables?: Record; +}): string => { + const prismModel = edgeDTMCTemplate({ gm, fileName, clean, variables }); + + const report = validate(gm, prismModel, fileName); + if (report.summary.totalMissing > 0) { + throw new Error( + `PRISM model is not valid.\n${summarizeValidationFailures(report)}`, + ); + } + return prismModel; +}; + +// eslint-disable-next-line @typescript-eslint/naming-convention +export const __test_only_exports__ = { + edgeDTMCTemplate, +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/changeManager/changeManager.ts b/packages/lib/src/engines/edgeV2/template/modules/changeManager/changeManager.ts new file mode 100644 index 00000000..2ce432ce --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/changeManager/changeManager.ts @@ -0,0 +1,28 @@ +import { GoalTree } from '@goal-controller/goal-tree'; +import type { EdgeGoalTree } from '../../../types'; +import { getLogger } from '../../../logger/logger'; +import { changeManagerModuleTemplate } from './template'; +import { taskAchievabilityVariables } from './template/achievabilityVariables/taskAchievabilityVariables'; + +export const changeManagerModule = ({ + gm, + variables, +}: { + gm: EdgeGoalTree; + variables: Record; +}): string => { + const tasks = GoalTree.allByType(gm, 'task'); + const logger = getLogger(); + logger.info('[CHANGE MANAGER MODULE START]', 0); + + // Filter to only include number values (task achievability variables) + const numericVariables = Object.fromEntries( + Object.entries(variables).filter(([, value]) => typeof value === 'number'), + ) as Record; + + return ( + taskAchievabilityVariables(tasks, numericVariables) + + '\n\n' + + changeManagerModuleTemplate({ tasks }) + ); +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/achievabilityVariables/taskAchievabilityVariables.ts b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/achievabilityVariables/taskAchievabilityVariables.ts new file mode 100644 index 00000000..cf25f2a1 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/achievabilityVariables/taskAchievabilityVariables.ts @@ -0,0 +1,40 @@ +import type { Task } from '@goal-controller/goal-tree'; +import { getLogger } from '../../../../../logger/logger'; +import { achievableFormulaVariable } from '../../../../common'; + +const DEFAULT_ACHIEVABILITY = 0.5; + +export const taskAchievabilityVariable = ( + task: Task, + variableValues: Record, +): string => { + const logger = getLogger(); + const variableName = achievableFormulaVariable(task.id); + + // Check if variable is explicitly configured or using default + const isConfigured = variableName in variableValues; + const variableValue = isConfigured + ? variableValues[variableName] + : DEFAULT_ACHIEVABILITY; + + if (!isConfigured) { + logger.info( + `[WARNING] Task ${task.id}: using default achievability ${DEFAULT_ACHIEVABILITY} for ${variableName} (not configured in variables file)`, + 0, + ); + } + + const achievabilityConst = `const double ${variableName} = ${variableValue};`; + logger.achievabilityTaskConstant(task.id, variableName, variableValue ?? -1); + + return achievabilityConst; +}; + +export const taskAchievabilityVariables = ( + tasks: Task[], + variableValues: Record, +): string => { + return tasks + .map((task) => taskAchievabilityVariable(task, variableValues)) + .join('\n'); +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/index.ts b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/index.ts new file mode 100644 index 00000000..29355be8 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/index.ts @@ -0,0 +1,23 @@ +import { taskTransitions } from './tasks/transitions'; +import { taskVariables } from './tasks/variables'; +import type { EdgeTask } from '../../../../types'; + +export const changeManagerModuleTemplate = ({ + tasks, +}: { + tasks: EdgeTask[]; +}): string => { + const { variables, transitions } = tasks.reduce( + (acc, task) => { + acc.variables.push(taskVariables(task)); + acc.transitions.push(taskTransitions(task)); + return acc; + }, + { variables: [] as string[], transitions: [] as string[] }, + ); + + return `module ChangeManager + ${variables.join('\n ')} + ${transitions.join('\n')} +endmodule`; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/tasks/transitions.ts b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/tasks/transitions.ts new file mode 100644 index 00000000..b658767f --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/tasks/transitions.ts @@ -0,0 +1,95 @@ +import { getLogger } from '../../../../../logger/logger'; +import { parenthesis } from '../../../../../mdp/common'; +import type { EdgeTask } from '../../../../../types'; +import { + achievableFormulaVariable, + achievedTransition, + pursueTransition, + tryTransition, +} from '../../../../common'; +import { + hasBeenAchieved, + hasBeenAchievedAndPursued, + hasBeenPursued, +} from '../../../goalModule/template/pursue/common'; + +const pursueTask = (task: EdgeTask): string => { + const logger = getLogger(); + const leftStatement = `${hasBeenPursued(task, { + condition: false, + })} & ${hasBeenAchieved(task, { condition: false })}`; + const updateStatement = `(${hasBeenPursued(task, { + condition: true, + update: true, + })})`; + const prismLabelStatement = `[${pursueTransition( + task.id, + )}] ${leftStatement} -> ${updateStatement};`; + logger.taskTranstions.transition( + task.id, + leftStatement, + updateStatement, + prismLabelStatement, + 'pursue', + ); + return prismLabelStatement; +}; + +const achieveTask = (task: EdgeTask): string => { + const logger = getLogger(); + const leftStatement = `${hasBeenAchievedAndPursued(task, { + achieved: true, + pursued: true, + })}`; + const prismLabelStatement = `[${achievedTransition( + task.id, + )}] ${leftStatement} -> true;`; + logger.taskTranstions.transition( + task.id, + leftStatement, + 'true', + prismLabelStatement, + 'achieve', + ); + return prismLabelStatement; +}; + +const tryTask = (task: EdgeTask): string => { + const logger = getLogger(); + const taskAchievabilityVariable = achievableFormulaVariable(task.id); + + const leftStatement = `[${tryTransition( + task.id, + )}] ${hasBeenAchievedAndPursued(task, { + achieved: false, + pursued: true, + })}`; + const updateStatement = `${taskAchievabilityVariable}: ${parenthesis( + hasBeenAchieved(task, { + condition: true, + update: true, + }), + )} + 1-${taskAchievabilityVariable}: ${parenthesis( + hasBeenPursued(task, { condition: false, update: true }), + )};`; + const tryStatement = `${leftStatement} -> ${updateStatement}`; + logger.taskTranstions.transition( + task.id, + leftStatement, + updateStatement, + tryStatement, + 'try', + task.properties.engine.maxRetries, + ); + + return tryStatement; +}; + +export const taskTransitions = (task: EdgeTask): string => { + return ` + // Task ${task.id}: ${task.name} + ${pursueTask(task)} + ${tryTask(task)} + ${achieveTask(task)} + `; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/tasks/variables.ts b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/tasks/variables.ts new file mode 100644 index 00000000..55c49fe6 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/changeManager/template/tasks/variables.ts @@ -0,0 +1,51 @@ +import { getLogger } from '../../../../../logger/logger'; +import type { EdgeTask } from '../../../../../types'; +import { achievedVariable, failed, pursuedVariable } from '../../../../common'; + +const defineVariable = (variable: string): string => { + const upperBound = 1; + + const logger = getLogger(); + logger.variableDefinition({ + variable, + upperBound, + initialValue: 0, + type: 'int', + context: 'task', + }); + return `${variable}: [0..${upperBound}] init 0;`; +}; + +export const maxRetriesVariable = (task: EdgeTask): string => { + const maxRetries = task.properties.engine.maxRetries; + + // Only emit variable if maxRetries is a finite positive integer + if ( + typeof maxRetries !== 'number' || + !Number.isFinite(maxRetries) || + maxRetries <= 0 + ) { + return ''; + } + + const logger = getLogger(); + + logger.variableDefinition({ + variable: failed(task.id), + upperBound: maxRetries, + initialValue: 0, + type: 'int', + context: 'task', + }); + return `${failed(task.id)}: [0..${maxRetries}] init 0;`; +}; + +export const taskVariables = (task: EdgeTask): string => { + const logger = getLogger(); + logger.initTask(task); + + return ` + ${defineVariable(pursuedVariable(task.id))} + ${defineVariable(achievedVariable(task.id))} +`.trim(); +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/goalModules.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/goalModules.ts new file mode 100644 index 00000000..975cbcb0 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/goalModules.ts @@ -0,0 +1,33 @@ +import { GoalTree } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode, EdgeGoalTree } from '../../../types'; +import { goalModule } from './template'; + +/** + * Extracts the numeric ID from a goal/task/resource ID string. + * IDs must follow the pattern: G, T, or R + * @param goalId - The ID string (e.g., "G1", "T5", "R3") + * @returns The numeric portion as a string + * @throws Error if the ID doesn't match the required pattern + */ +export const goalNumberId = (goalId: string): string => { + const match = goalId.match(/^[GTR](\d+)$/i); + if (!match || match[1] === undefined) { + throw new Error( + `ID must follow pattern 'G', 'T', or 'R', got: '${goalId}'`, + ); + } + return match[1]; +}; + +export const goalModules = ({ gm }: { gm: EdgeGoalTree }): string => { + const goals = GoalTree.allByType(gm, 'goal'); + return ` +${goals + .sort( + (a: EdgeGoalNode, b: EdgeGoalNode) => + Number(goalNumberId(a.id)) - Number(goalNumberId(b.id)), + ) + .map(goalModule) + .join('\n\n')} +`; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/achieve.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/achieve.ts new file mode 100644 index 00000000..3ee3dec0 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/achieve.ts @@ -0,0 +1,60 @@ +import type { Relation } from '@goal-controller/goal-tree'; +import { Node } from '@goal-controller/goal-tree'; +import { getLogger } from '../../../../logger/logger'; +import { + achieved, + goalState, + pursued, + separator, +} from '../../../../mdp/common'; +import type { EdgeGoalNode, EdgeTask } from '../../../../types'; +import { achievedMaintain } from './formulas'; +import { hasBeenPursued } from './pursue/common'; + +const isValidSeparator = ( + relation: Relation | null, +): relation is 'and' | 'or' => { + return ['and', 'or'].includes(relation ?? ''); +}; + +const childIdle = (child: EdgeGoalNode | EdgeTask): string => + child.type === 'task' ? `${pursued(child.id)}=0` : `${goalState(child.id)}=0`; + +export const achieveCondition = (goal: EdgeGoalNode): string => { + if (!isValidSeparator(goal.relationToChildren)) { + return ''; + } + const pursueableChildren = Node.children(goal).filter( + (child) => !Node.isResource(child), + ); + if (!pursueableChildren.length) { + return ''; + } + return pursueableChildren + .map((child) => childIdle(child as EdgeGoalNode | EdgeTask)) + .join(' & '); +}; + +export const achieveStatement = (goal: EdgeGoalNode): string => { + const logger = getLogger(); + + const achievedGuard = goal.properties.engine.execCondition?.maintain + ? `${achievedMaintain(goal.id)}=true` + : `${achieved(goal.id)}`; + + const cond = achieveCondition(goal); + const leftStatement = [ + hasBeenPursued(goal, { condition: true }), + achievedGuard, + cond, + ] + .filter(Boolean) + .join(separator('and')); + + const updateStatement = `(${goalState(goal.id)}'=0);`; + + const prismLabelStatement = `[achieved_${goal.id}] ${leftStatement} -> ${updateStatement}`; + + logger.achieve(goal.id, leftStatement, updateStatement, prismLabelStatement); + return prismLabelStatement; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/formulas.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/formulas.ts new file mode 100644 index 00000000..f3bf7590 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/formulas.ts @@ -0,0 +1,157 @@ +import { Node } from '@goal-controller/goal-tree'; +import { getLogger } from '../../../../logger/logger'; +import { parenthesis, separator } from '../../../../mdp/common'; +import type { EdgeGoalNode } from '../../../../types'; +import { achievableFormulaVariable, achievedVariable } from '../../../common'; + +export const achievedMaintain = (goalId: string): string => { + return `${goalId}_achieved_maintain`; +}; + +export const maintainConditionFormula = (goal: EdgeGoalNode): string => { + if (!goal.properties.engine.execCondition?.maintain) { + return ''; + } + const logger = getLogger(); + + const prismLine = `formula ${achievedMaintain(goal.id)} = ${ + goal.properties.engine.execCondition.maintain.sentence || + 'ASSERTION_UNDEFINED' + };`; + + logger.maintainFormulaDefinition( + goal.id, + achievedMaintain(goal.id), + goal.properties.engine.execCondition.maintain.sentence || + 'ASSERTION_UNDEFINED', + prismLine, + ); + return prismLine; +}; + +/** Same combinators as Edge v1: `*` for AND children, inclusion–exclusion for OR. */ +export const achievableGoalFormula = (goal: EdgeGoalNode): string => { + const children = Node.children(goal).filter( + (child) => !Node.isResource(child), + ); + const formulaName = achievableFormulaVariable(goal.id); + const logger = getLogger(); + + if (children.length === 0) { + const formula = `formula ${formulaName} = 1;`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + 'LEAF', + '1', + formula, + ); + return formula; + } + + if (children.length === 1) { + const firstChild = children[0]; + if (!firstChild) { + throw new Error( + `Expected at least one child for goal ${goal.id} but children array is empty`, + ); + } + const sentence = achievableFormulaVariable(firstChild.id); + const formula = `formula ${formulaName} = ${sentence};`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + 'SINGLE_GOAL', + sentence, + formula, + ); + return formula; + } + + const childrenVariables = children.map((child) => + achievableFormulaVariable(child.id), + ); + const productPart = childrenVariables.join(' * '); + + switch (goal.relationToChildren) { + case 'and': { + const andFormula = `formula ${formulaName} = ${productPart};`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + 'AND', + productPart, + andFormula, + ); + return andFormula; + } + case 'or': { + const sumPart = childrenVariables.join(' + '); + const formulaValue = `${sumPart} - ${parenthesis(productPart)}`; + const orFormula = `formula ${formulaName} = ${formulaValue};`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + 'OR', + formulaValue, + orFormula, + ); + return orFormula; + } + default: + throw new Error( + `Invalid relation to children: ${goal.relationToChildren ?? 'none'}`, + ); + } +}; + +export const achievedGoalFormula = (goal: EdgeGoalNode): string => { + const children = Node.children(goal).filter( + (child) => !Node.isResource(child), + ); + const formulaName = `${achievedVariable(goal.id)}`; + const logger = getLogger(); + const childrenAchievedExpressions = children.map((child) => + achievedVariable(child.id), + ); + + if (childrenAchievedExpressions.length === 0) { + const formula = `formula ${formulaName} = false;`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + 'SINGLE_GOAL', + 'false', + formula, + ); + return formula; + } + + if (childrenAchievedExpressions.length === 1) { + const [onlyChildExpression] = childrenAchievedExpressions; + if (!onlyChildExpression) { + throw new Error(`Expected achieved expression for goal ${goal.id}`); + } + const formula = `formula ${formulaName} = ${onlyChildExpression};`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + 'SINGLE_GOAL', + onlyChildExpression, + formula, + ); + return formula; + } + + const relation = goal.relationToChildren === 'and' ? 'and' : 'or'; + const sentence = `(${childrenAchievedExpressions.join(separator(relation))})`; + const formula = `formula ${formulaName} = ${sentence};`; + logger.achievabilityFormulaDefinition( + goal.id, + formulaName, + relation === 'and' ? 'AND' : 'OR', + sentence, + formula, + ); + return formula; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/index.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/index.ts new file mode 100644 index 00000000..163ffd97 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/index.ts @@ -0,0 +1,46 @@ +import { getLogger } from '../../../../logger/logger'; +import { achieveStatement } from './achieve'; +import { + achievableGoalFormula, + achievedGoalFormula, + maintainConditionFormula, +} from './formulas'; + +import { Node } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode } from '../../../../types'; +import { pursueStatements } from './pursue'; +import { skipStatements } from './skip'; +import { variablesDefinition } from './variables'; + +export const goalModule = (goal: EdgeGoalNode): string => { + const logger = getLogger(); + logger.initGoal(goal); + + const formulaStatements = [ + maintainConditionFormula(goal), + achievableGoalFormula(goal), + achievedGoalFormula(goal), + ] + .filter(Boolean) + .join('\n'); + + return `// ID: ${goal.id} +// Name: ${goal.name} +// Type: ${goal.properties.engine.executionDetail?.type || 'basic'} +// Relation to children: ${goal.relationToChildren} +// Children: ${Node.children(goal) + .map((child) => child.id) + .join(', ')} +module ${goal.id} + ${variablesDefinition(goal)} + + ${pursueStatements(goal).join('\n ')} + + ${achieveStatement(goal)} + + ${skipStatements(goal).join('\n ')} +endmodule + +${formulaStatements} +`.trim(); +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/andGoal.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/andGoal.ts new file mode 100644 index 00000000..9ec8803b --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/andGoal.ts @@ -0,0 +1,80 @@ +import type { TreeNode } from '@goal-controller/goal-tree'; +import { Node } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode, EdgeTask } from '../../../../../types'; +import { getLogger } from '../../../../../logger/logger'; +import { achieved, separator } from '../../../../../mdp/common'; +import { achievableGtDecision } from '../../../../prismGuards'; +import { hasBeenAchieved } from './common'; + +// Type for nodes that can be achieved (goals and tasks, but not resources) +type AchievableNode = EdgeGoalNode | EdgeTask; + +/** Snippets use `G1_achieved` on sequential pursues; maintain goals still expose `G*_achieved`. */ +const priorSequentialSiblingGuard = (node: AchievableNode): string => + node.type === 'task' + ? hasBeenAchieved(node, { condition: true }) + : achieved(node.id); + +/** Interleaved AND: per-child guard from snippets (`G1_achievable*10.0 > decision_G1`). */ +export const pursueAndInterleavedGoal = (childId: string): string => + achievableGtDecision(childId); + +export const splitSequence = ( + sequence: string[], + childId: string, +): [string[], string[]] => { + if (!sequence.includes(childId)) { + throw new Error( + `Child ID ${childId} not found in sequence ${sequence.join(', ')}`, + ); + } + const sequenceIndex = sequence.indexOf(childId); + return [sequence.slice(0, sequenceIndex), sequence.slice(sequenceIndex + 1)]; +}; + +export const pursueAndSequentialGoal = ( + goal: EdgeGoalNode, + sequence: string[], + childId: string, + children: TreeNode[], +): string => { + if (goal.relationToChildren === 'or') { + throw new Error( + 'OR relation to children without a runtime notation is not supported use Degradation goal instead', + ); + } + + const [leftGoals, rightGoals] = splitSequence(sequence, childId); + + if (!goal.relationToChildren) { + return ''; + } + + // Filter out resources - they cannot be achieved + const achievableChildren = children.filter( + (child): child is AchievableNode => !Node.isResource(child), + ); + + const childrenMap = new Map( + achievableChildren.map((child) => [child.id, child]), + ); + + const { sequence: sequenceLogger } = getLogger().pursue.executionDetail; + sequenceLogger(goal.id, childId, leftGoals, rightGoals); + + if (goal.relationToChildren === 'and') { + const decisionGuard = achievableGtDecision(goal.id); + const previousAchieved = leftGoals.map((id) => { + const node = childrenMap.get(id); + if (!node) { + throw new Error( + `Child with ID ${id} not found in children map for goal ${goal.id}`, + ); + } + return priorSequentialSiblingGuard(node); + }); + return [decisionGuard, ...previousAchieved].join(separator('and')); + } + + return ''; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/common.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/common.ts new file mode 100644 index 00000000..32309781 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/common.ts @@ -0,0 +1,63 @@ +import { Node } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode, EdgeTask } from '../../../../../types'; +import { + achieved, + goalState, + pursued, + separator, +} from '../../../../../mdp/common'; +import { achievedMaintain } from '../formulas'; + +// Node type that has both id and properties.engine.execCondition +type NodeWithExecCondition = EdgeGoalNode | EdgeTask; + +export const hasBeenAchieved = ( + node: NodeWithExecCondition, + { condition, update }: { condition: boolean; update?: boolean }, +): string => { + if (node.type === 'task') { + return `${achieved(node.id)}${update ? "'" : ''}=${condition ? 1 : 0}`; + } + + if (node.properties.engine.execCondition?.maintain) { + if (update) { + throw new Error( + 'Invalid update option for goal of type maintain, please verify', + ); + } + return `${achievedMaintain(node.id)}=${condition ? 'true' : 'false'}`; + } + + if (update) { + throw new Error( + 'Invalid update option for goal achieved formula, please verify', + ); + } + return condition ? `${achieved(node.id)}` : `!${achieved(node.id)}`; +}; + +export const hasBeenPursued = ( + node: NodeWithExecCondition, + { condition, update }: { condition: boolean; update?: boolean }, +): string => { + const name = Node.isTask(node) ? pursued(node.id) : goalState(node.id); + return `${name}${update ? "'" : ''}=${condition ? 1 : 0}`; +}; + +export const hasBeenAchievedAndPursued = ( + node: NodeWithExecCondition, + { achieved, pursued }: { achieved: boolean; pursued: boolean }, +): string => { + return [ + hasBeenPursued(node, { condition: pursued }), + hasBeenAchieved(node, { condition: achieved }), + ].join(separator('and')); +}; + +export const hasFailedAtLeastNTimes = (goalId: string, n: number): string => { + return `${goalId}_failed >= ${n}`; +}; + +export const hasFailedAtMostNTimes = (goalId: string, n: number): string => { + return `${goalId}_failed <= ${n}`; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/index.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/index.ts new file mode 100644 index 00000000..d9b9aeb1 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/index.ts @@ -0,0 +1,453 @@ +import { Node, type GoalNode } from '@goal-controller/goal-tree'; +import { getLogger } from '../../../../../logger/logger'; +import { + achieved, + failed, + goalState, + parenthesis, + separator, +} from '../../../../../mdp/common'; +import type { EdgeGoalNode, EdgeTask } from '../../../../../types'; +import { chosenVariable } from '../../../../common'; +import { pursueableChildren } from '../../../../prismGuards'; +import { achievedMaintain } from '../formulas'; +import { degradationRetryCapFromMap } from '../variables'; +import { pursueAndInterleavedGoal, pursueAndSequentialGoal } from './andGoal'; +import { hasBeenAchieved } from './common'; +import { pursueAlternativeGoal } from './orGoal'; + +// Type for nodes that can be pursued (goals and tasks, but not resources) +type PursueableNode = EdgeGoalNode | EdgeTask; + +/** + * Type guard to check if a node from dependsOn is a valid EdgeGoalNode. + * The dependsOn array is resolved in afterCreationMapper to contain actual goal nodes, + * but the generic type doesn't fully capture this - this guard narrows the type safely. + */ +const isEdgeGoalNode = ( + node: GoalNode, +): node is EdgeGoalNode => { + return ( + node !== null && + typeof node === 'object' && + 'id' in node && + 'properties' in node && + typeof node.properties === 'object' && + node.properties !== null && + 'engine' in node.properties + ); +}; + +export const goalDependencyStatement = (goal: EdgeGoalNode): string => { + const dependencies = goal.properties.engine.dependsOn ?? []; + const validDependencies = dependencies.filter(isEdgeGoalNode); + + return validDependencies.length > 0 + ? ` & (${validDependencies + .map((dep) => hasBeenAchieved(dep, { condition: true })) + .join(separator('and'))})` + : ''; +}; + +const removeRepeatedConditions = (condition: string): string => { + return condition + .split(' & ') + .filter((condition, index, self) => self.indexOf(condition) === index) + .join(' & '); +}; + +export const pursueStatements = (goal: EdgeGoalNode): string[] => { + const logger = getLogger(); + const pursueLogger = logger.pursue; + + const goalsToPursue: PursueableNode[] = [goal, ...pursueableChildren(goal)]; + + const isItself = (child: PursueableNode): boolean => child.id === goal.id; + const pursueLines = goalsToPursue + + .map((child, _): [PursueableNode, { left: string; right: string }] => { + // first map, responsible for writing the first column of the pursue lines + // itself: [pursue_G1] G1_pursued=0 & G1_achieved=0 -> (G1_pursued'=1) + // non-itself: [pursue_G2] G1_pursued=1 & G1_achieved=0 -> true + const itself = isItself(child); + pursueLogger.pursue(child, 1); + + const calcLeftStatement = (): string => { + const dependencyStatement = goalDependencyStatement(goal); + pursueLogger.goalDependency( + goal.id, + (goal.properties.engine.dependsOn ?? []).map((dep) => dep.id), + ); + const statement = + `[pursue_${child.id}] ${goalState(goal.id)}=${itself ? 0 : 1} & ${ + goal.properties.engine.execCondition?.maintain + ? `${achievedMaintain(goal.id)}=false` + : `!${achieved(goal.id)}` + }` + (itself ? dependencyStatement : ''); + pursueLogger.defaultPursueCondition(statement); + + return statement; + }; + + const calcRightStatement = (): string => { + if (itself) { + const update = `(${goalState(goal.id)}'=1)`; + pursueLogger.update(update); + return update; + } + pursueLogger.update('true'); + return 'true'; + }; + + const { left, right } = { + left: calcLeftStatement(), + right: calcRightStatement(), + }; + + if (isItself(child)) { + return [ + child, + { + left, + right, + }, + ] as const; + } + pursueLogger.stepStatement(1, left, right); + + return [child, { left, right }] as const; + }) + .map( + ( + [child, { left, right }], + index, + ): [PursueableNode, { left: string; right: string }] => { + // second map, responsible for writing the second column of the pursue lines + // defines how a goal should be pursued based on the execution detail + // skips itself and handles or and and goals + // or goal: + // - alternatives: pursueAlternativeGoal(goal, child.id) + // - choice: two [pursue_child] per child — commit (chosen=0 + alternative guards) then execute (chosen=k + child achievable vs decision) + // - degradation: per-sibling failed from retryMap — retry/failover flatMap, or alternative-only if no map entry + // and goal: + // - sequence: pursueAndSequentialGoal(goal, goal.executionDetail.sequence, child.id, [...(goal.children ?? []), ...(goal.tasks ?? [])]) + // - interleaved: return [child, { left, right }] + const calcExecutionDetail = (): [ + PursueableNode, + { left: string; right: string }, + ] => { + pursueLogger.pursue(child, 2); + + if (isItself(child)) { + // skip itself + logger.info( + '[EXECUTION DETAIL: SKIP] Skipping condition generation for itself on runtime guard generation step', + 2, + ); + return [child, { left, right }]; + } + + if (goal.relationToChildren === 'or') { + logger.trace(child.id, 'or goal detected', 2); + switch (goal.properties.engine.executionDetail?.type) { + case 'sequence': { + logger.error( + child.id, + 'sequence execution detail detected in or goal', + ); + throw new Error( + 'OR relation to children with sequence execution detail is not supported', + ); + } + case 'choice': { + if (pursueableChildren(goal).length === 0) { + logger.error( + goal.id, + 'choice execution detail detected without pursueable children', + ); + throw new Error( + `[INVALID MODEL]: Goal "${goal.id}" has choice execution detail but no pursueable children (goals or tasks)`, + ); + } + logger.trace( + child.id, + 'choice execution detail detected with children', + ); + // Commit vs execute split in flatMap after this step + return [child, { left, right }]; + } + case 'degradation': { + logger.trace( + child.id, + 'degradation execution detail detected', + 2, + ); + return [child, { left, right }]; + } + case 'alternative': { + logger.trace( + child.id, + 'alternative execution detail detected', + 2, + ); + const pursueCondition = pursueAlternativeGoal(goal, child.id); + return [child, { left: left + ` & ${pursueCondition}`, right }]; + } + default: + logger.info( + `[EXECUTION DETAIL: SKIP] Skipping condition generation for ${child.id} on runtime guard generation step, no execution detail`, + 2, + ); + // Basic OR (no execution detail): same alternative-style guards as annotated OR goals. + if (!isItself(child)) { + const pursueCondition = pursueAlternativeGoal(goal, child.id); + return [ + child, + { left: left + ` & ${pursueCondition}`, right }, + ]; + } + return [child, { left, right }]; + } + } + + if (goal.relationToChildren === 'and') { + logger.trace(child.id, 'and goal detected', 2); + // organize pursue conditions by execution detail type + switch (goal.properties.engine.executionDetail?.type) { + case 'sequence': { + logger.trace(child.id, 'sequence execution detail detected', 2); + const pursueCondition = pursueAndSequentialGoal( + goal, + goal.properties.engine.executionDetail.sequence, + child.id, + Node.children(goal), + ); + return [ + child, + { + left: left + ` & ${pursueCondition}`, + right, + }, + ]; + } + case 'alternative': { + logger.trace( + child.id, + 'alternative execution detail detected', + 3, + ); + throw new Error( + 'AND relation to children with alternative execution detail is not supported', + ); + } + case 'choice': { + logger.trace(child.id, 'choice execution detail detected', 2); + throw new Error( + 'AND relation to children with choice execution detail is not supported', + ); + } + case 'interleaved': { + logger.trace( + child.id, + 'interleaved execution detail detected', + 2, + ); + pursueLogger.executionDetail.interleaved(); + if (isItself(child)) { + return [child, { left, right }]; + } + const pursueCondition = pursueAndInterleavedGoal(child.id); + return [ + child, + { + left: `${left} & ${pursueCondition}`, + right, + }, + ]; + } + default: + logger.info( + `[EXECUTION DETAIL: SKIP] Skipping condition generation for ${child.id} on runtime guard generation step, no execution detail`, + 2, + ); + // Basic AND (no execution detail): same per-child decision threshold as interleaved. + if (!isItself(child)) { + const pursueCondition = pursueAndInterleavedGoal(child.id); + return [ + child, + { + left: `${left} & ${pursueCondition}`, + right, + }, + ]; + } + return [child, { left, right }]; + } + } + + logger.info( + `[EXECUTION DETAIL: ERROR] ${child.id} is not an OR or AND goal`, + 2, + ); + return [child, { left, right }]; + }; + + const executionDetail = calcExecutionDetail(); + + pursueLogger.stepStatement( + 2, + executionDetail[1].left, + executionDetail[1].right, + ); + + return executionDetail; + }, + ) + .flatMap( + ( + entry: [PursueableNode, { left: string; right: string }], + ): Array<[PursueableNode, { left: string; right: string }]> => { + const [child, { left }] = entry; + if ( + goal.relationToChildren === 'or' && + goal.properties.engine.executionDetail?.type === 'degradation' && + !isItself(child) + ) { + const cap = degradationRetryCapFromMap(goal, child.id); + if (cap !== null) { + const retryLeft = `${left} & ${failed(child.id)}<${cap} & ${pursueAndInterleavedGoal(child.id)}`; + const retryRight = parenthesis( + `${failed(child.id)}'=min(${cap}, ${failed(child.id)}+1)`, + ); + const failoverLeft = `${left} & ${failed(child.id)}=${cap} & ${pursueAlternativeGoal(goal, child.id)}`; + const failoverRight = 'true'; + return [ + [child, { left: retryLeft, right: retryRight }], + [child, { left: failoverLeft, right: failoverRight }], + ]; + } + const altOnlyLeft = `${left} & ${pursueAlternativeGoal(goal, child.id)}`; + return [[child, { left: altOnlyLeft, right: 'true' }]]; + } + if ( + goal.relationToChildren === 'or' && + goal.properties.engine.executionDetail?.type === 'choice' && + !isItself(child) + ) { + const branchIndex = goalsToPursue.indexOf(child); + const commitLeft = `${left} & ${chosenVariable(goal.id)}=0 & ${pursueAlternativeGoal(goal, child.id)}`; + const commitRight = parenthesis( + `${chosenVariable(goal.id)}'=${branchIndex}`, + ); + const execLeft = `${left} & ${chosenVariable(goal.id)}=${branchIndex} & ${pursueAndInterleavedGoal(child.id)}`; + const execRight = 'true'; + return [ + [child, { left: commitLeft, right: commitRight }], + [child, { left: execLeft, right: execRight }], + ]; + } + return [entry]; + }, + ) + .map( + ([child, statement]): [ + PursueableNode, + { left: string; right: string }, + ] => { + // third map, responsible for writing the third column of the pursue lines + // defines the activation context and maintain context guards + // if itself add context guard only if it has an activation context + // if child add context guard only if it has a maintain condition + + // parent goals have activation context independently of the maintain condition + const activationContextCondition = + ((isItself(child) || Node.isTask(child)) && + child.properties.engine.execCondition?.assertion?.sentence) || + ''; + + // child goals have maintain condition only if they are not itself + const maintainContextGuard = + child.properties.engine.execCondition?.maintain?.sentence && + !isItself(child) + ? `${achievedMaintain(child.id)}=false` + : ''; + + const left = + activationContextCondition || maintainContextGuard + ? `${statement.left} & ${[ + activationContextCondition, + maintainContextGuard, + ] + .filter(Boolean) + .join(' & ')}` + : statement.left; + + if (child.properties.engine.execCondition) { + logger.trace(child.id, 'activation context guard detected', 2); + pursueLogger.executionDetail.activationContext(maintainContextGuard); + } else { + logger.trace(child.id, 'no activation context guard detected', 2); + pursueLogger.executionDetail.noActivationContext(child.id); + } + + pursueLogger.stepStatement(3, left, statement.right); + return [ + child, + { + left, + right: `${statement.right}`, + }, + ]; + }, + ) + .map(([child, statement]) => { + // fourth map, responsible for writing the update of the failed counter variable + // defines the update failed counter statement + // if child has a max retries, update the failed counter variable + // if itself, skip the update failed counter statement + + // TODO: only update if child is part of a degradation goal + const maxRetries = child.properties.engine.maxRetries; + const updateFailedCounterStatement = + maxRetries > 0 + ? `(${failed(child.id)}'=min(${maxRetries}, ${failed(child.id)}+1))` + : ''; + + if ( + !updateFailedCounterStatement || + isItself(child) || + (goal.relationToChildren === 'or' && + goal.properties.engine.executionDetail?.type === 'degradation') + ) { + return [child, statement] as const; + } + + const rightStatement = + // overwrite default true with update failed counter statement + statement.right === 'true' + ? updateFailedCounterStatement + : `${statement.right} & ${updateFailedCounterStatement}`; + return [ + child, + { + left: statement.left, + right: rightStatement, + }, + ] as const; + }) + .map(([_, statement]) => { + // fifth map + // cleans up the left and right statements by removing repeated conditions + // TODO: dependencies + return { + left: `${removeRepeatedConditions(statement.left)}`, + right: `${removeRepeatedConditions(statement.right)}`, + }; + }) + .map((statement): string => { + pursueLogger.finish(); + return `${statement.left} -> ${statement.right};`; + }); + + return pursueLines ?? []; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/orGoal.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/orGoal.ts new file mode 100644 index 00000000..e3f6b3cd --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/pursue/orGoal.ts @@ -0,0 +1,109 @@ +import { getLogger } from '../../../../../logger/logger'; +import { achievable, separator } from '../../../../../mdp/common'; +import type { EdgeGoalNode, EdgeTask } from '../../../../../types'; +import { + chosenVariable, + decisionVariable, + underscoredOrDecisionVariable, +} from '../../../../common'; +import { + ACHIEVABILITY_DECISION_SCALE, + achievableGtDecision, + childIdle, + pursueableChildren as sharedPursueableChildren, +} from '../../../../prismGuards'; + +/* +G1: Goal[T1|T2] +module G1 //non-idempotent, a.k.a choose once! + G1_pursued : [0..1] init 0; + G1_achieved : [0..1] init 0; + G1_chosen : [0..2] init 0; //which one is chosen? + +// [pursue_T1] G1_pursued=1 & G1_achieved=0 & G1_chosen!=2 -> (G1_chosen'=1); +// [pursue_T2] G1_pursued=1 & G1_achieved=0 & G1_chosen!=1 -> (G1_chosen'=2); + + [achieved_G1] (T1_achieved>0 | T2_achieved>0) & G1_pursued=1 -> (G1_pursued'=0) & (G1_achieved'=1); +endmodule +*/ + +export const pursueChoiceGoal = ( + goal: EdgeGoalNode, + alternative: string[], + currentChildId: string, +): string => { + if (goal.relationToChildren === 'and') { + throw new Error( + `Alternative goals are not supported for AND joints. Found in goal ${goal.id}`, + ); + } + + const { choice: choiceLogger } = getLogger().pursue.executionDetail; + + if (goal.relationToChildren === 'or') { + const otherGoals = alternative.filter( + (goalId) => goalId !== currentChildId, + ); + const notChosen = otherGoals + .map((goalId) => { + const originalIndex = alternative.indexOf(goalId); + return `${chosenVariable(goal.id)}!=${originalIndex + 1}`; + }) + .join(separator('and')); + + choiceLogger(currentChildId, otherGoals, notChosen); + return notChosen; + } + return ''; +}; + +// chooses either one of the children always (snippets: parent achievability vs decision, +// siblings idle, then (G1_ach/(G1_ach+G2_ach))*10 >/<= _decision_parent) +export const pursueAlternativeGoal = ( + goal: EdgeGoalNode, + currentChildId: string, +): string => { + type PursueableNode = EdgeGoalNode | EdgeTask; + const pursueableNodes = sharedPursueableChildren(goal) as PursueableNode[]; + const otherGoals = pursueableNodes.filter( + (child: PursueableNode) => child.id !== currentChildId, + ); + const { alternative: alternativeLogger } = getLogger().pursue.executionDetail; + + alternativeLogger( + currentChildId, + otherGoals.map((child: PursueableNode) => child.id), + ); + + const parentVsDecision = achievableGtDecision(goal.id); + + const siblingIdle = otherGoals + .map((child: PursueableNode) => childIdle(child)) + .join(separator('and')); + + const parts: string[] = [parentVsDecision]; + if (siblingIdle) { + parts.push(siblingIdle); + } + + if (pursueableNodes.length >= 2) { + const first = pursueableNodes[0]; + if (!first) { + throw new Error( + `Pursueable children unexpectedly empty for alternative goal ${goal.id}`, + ); + } + const sumAchievable = pursueableNodes + .map((c) => achievable(c.id)) + .join('+'); + const ratioExpr = `(${achievable(first.id)}/(${sumAchievable}))*${ACHIEVABILITY_DECISION_SCALE}`; + const underscored = underscoredOrDecisionVariable(goal.id); + parts.push( + currentChildId === first.id + ? `${ratioExpr} > ${underscored}` + : `${ratioExpr} <= ${underscored}`, + ); + } + + return parts.join(separator('and')); +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/skip.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/skip.ts new file mode 100644 index 00000000..84d3241e --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/skip.ts @@ -0,0 +1,163 @@ +import type { TreeNode } from '@goal-controller/goal-tree'; +import { Node } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode } from '../../../../types'; +import { getLogger } from '../../../../logger/logger'; +import { + achieved, + failed, + goalState, + pursued, + separator, +} from '../../../../mdp/common'; +import { chosenVariable, decisionVariable } from '../../../common'; +import { + achievableGtDecision, + achievableLeDecision, + childIdle, + pursueableChildren, +} from '../../../prismGuards'; +import { cappedDegradationChildren } from './variables'; + +const pursueMemberNodes = (goal: EdgeGoalNode): TreeNode[] => + goal.children?.length ? goal.children : goal.tasks?.length ? goal.tasks : []; + +/** Snippet: `!(G2_achievable*10.0 > decision_G2 | G1_achievable*10.0 > decision_G1)`. */ +const interleavedSkipNoChildPursueGuard = (goal: EdgeGoalNode): string => { + const disjuncts = pursueMemberNodes(goal) + .filter((c) => !Node.isResource(c)) + .map((child) => achievableGtDecision(child.id)); + if (disjuncts.length === 0) return ''; + return `!(${disjuncts.join(separator('or'))})`; +}; + +const childrenHasNotBeenPursued = (goal: EdgeGoalNode) => { + const pursueMembers = pursueMemberNodes(goal); + return pursueMembers + .map((child: TreeNode) => childIdle(child)) + .join(separator('and')); +}; + +/** + * All `[skip_G]` PRISM lines for this goal (`OR` choice may emit several with the same label). + */ +export const skipStatements = (goal: EdgeGoalNode): string[] => { + const logger = getLogger(); + const idleChildren = childrenHasNotBeenPursued(goal); + const edType = goal.properties.engine.executionDetail?.type; + const pursueableOrdered = pursueableChildren(goal); + + const updateStatement = `(${goalState(goal.id)}'=0);`; + + const emit = (leftStatement: string): string => { + const prismLabelStatement = `[skip_${goal.id}] ${leftStatement} -> ${updateStatement}`; + logger.skip(goal.id, leftStatement, updateStatement, prismLabelStatement); + return prismLabelStatement; + }; + + if ( + goal.relationToChildren === 'or' && + edType === 'choice' && + pursueableOrdered.length > 0 + ) { + const lines: string[] = []; + const idleAll = pursueableOrdered + .map((c) => childIdle(c)) + .join(separator('and')); + const uncommitted: string[] = [ + `!${achieved(goal.id)}`, + `${goalState(goal.id)}=1`, + ]; + if (idleAll) uncommitted.push(idleAll); + uncommitted.push(`${chosenVariable(goal.id)}=0`); + uncommitted.push(achievableLeDecision(goal.id)); + lines.push(emit(uncommitted.join(separator('and')))); + + pursueableOrdered.forEach((child, i) => { + const branchIndex = i + 1; + const parts: string[] = [ + `!${achieved(goal.id)}`, + `${goalState(goal.id)}=1`, + childIdle(child), + `${chosenVariable(goal.id)}=${branchIndex}`, + achievableLeDecision(child.id), + ]; + lines.push(emit(parts.join(separator('and')))); + }); + return lines; + } + + if ( + goal.relationToChildren === 'or' && + edType === 'degradation' && + pursueableOrdered.length > 0 + ) { + const lines: string[] = []; + const idleAll = pursueableOrdered + .map((c) => childIdle(c)) + .join(separator('and')); + const cappedChildren = cappedDegradationChildren(goal); + + // Retry regime (`child_failed < N`): skip this child branch when it cannot be pursued. + cappedChildren.forEach(({ child, cap }) => { + const parts: string[] = [ + `!${achieved(goal.id)}`, + `${goalState(goal.id)}=1`, + childIdle(child), + `${failed(child.id)}<${cap}`, + achievableLeDecision(child.id), + ]; + lines.push(emit(parts.join(separator('and')))); + }); + + // Failover regime (`child_failed = N`): skip when parent-level pursue cannot proceed. + if (cappedChildren.length > 0) { + cappedChildren.forEach(({ child, cap }) => { + const parts: string[] = [ + `!${achieved(goal.id)}`, + `${goalState(goal.id)}=1`, + `${failed(child.id)}=${cap}`, + achievableLeDecision(goal.id), + ]; + if (idleAll) parts.splice(2, 0, idleAll); + lines.push(emit(parts.join(separator('and')))); + }); + } else { + const parts: string[] = [ + `!${achieved(goal.id)}`, + `${goalState(goal.id)}=1`, + achievableLeDecision(goal.id), + ]; + if (idleAll) parts.splice(2, 0, idleAll); + lines.push(emit(parts.join(separator('and')))); + } + + return lines; + } + + const isAndSequential = + goal.relationToChildren === 'and' && edType === 'sequence'; + const isOrAlternative = + goal.relationToChildren === 'or' && edType === 'alternative'; + const useParentAchievableLeDecisionSkip = isAndSequential || isOrAlternative; + const isAndInterleaved = + goal.relationToChildren === 'and' && edType !== 'sequence'; + + const parts: string[] = []; + if (useParentAchievableLeDecisionSkip) { + parts.push(`!${achieved(goal.id)}`); + parts.push(`${goalState(goal.id)}=1`); + if (idleChildren) parts.push(idleChildren); + parts.push(achievableLeDecision(goal.id)); + } else if (isAndInterleaved) { + parts.push(`${goalState(goal.id)}=1`); + if (idleChildren) parts.push(idleChildren); + parts.push(`!${achieved(goal.id)}`); + const interleavedGuard = interleavedSkipNoChildPursueGuard(goal); + if (interleavedGuard) parts.push(interleavedGuard); + } else { + parts.push(`${goalState(goal.id)}=1`); + if (idleChildren) parts.push(idleChildren); + } + + return [emit(parts.join(separator('and')))]; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/variables.ts b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/variables.ts new file mode 100644 index 00000000..8d676f74 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/goalModule/template/variables.ts @@ -0,0 +1,80 @@ +import { getLogger } from '../../../../logger/logger'; +import { failed } from '../../../../mdp/common'; +import type { EdgeGoalNode, EdgeTask } from '../../../../types'; +import { coercePositiveIntRetry } from '../../../../retryCoercion'; +import { chosenVariable } from '../../../common'; +import { pursueableChildren } from '../../../prismGuards'; + +const goalStateVariable = (goalId: string): string => `${goalId}_state`; + +/** Retry cap N for degradation pursue lines (`sibling_failed < N` / `= N`), or null if absent from retryMap. */ +export const degradationRetryCapFromMap = ( + goal: EdgeGoalNode, + childId: string, +): number | null => { + if (goal.relationToChildren !== 'or') return null; + const ed = goal.properties.engine.executionDetail; + if (ed?.type !== 'degradation') return null; + return coercePositiveIntRetry(ed.retryMap?.[childId]); +}; + +/** + * Ordered list of `{ child, cap }` for every pursueable child in an OR + * degradation goal whose retryMap entry has a positive integer cap. + * Single source of truth for pursue, skip, and validator expected counts. + */ +export const cappedDegradationChildren = ( + goal: EdgeGoalNode, +): Array<{ child: EdgeGoalNode | EdgeTask; cap: number }> => { + if (goal.relationToChildren !== 'or') return []; + const ed = goal.properties.engine.executionDetail; + if (ed?.type !== 'degradation') return []; + return pursueableChildren(goal).flatMap((child) => { + const cap = coercePositiveIntRetry(ed.retryMap?.[child.id]); + return cap !== null ? [{ child, cap }] : []; + }); +}; + +const degradationSiblingFailedVariableLines = ( + goal: EdgeGoalNode, + defineVariable: (variable: string, upperBound: number) => string, +): string[] => { + return cappedDegradationChildren(goal).map(({ child, cap }) => + defineVariable(failed(child.id), cap), + ); +}; + +export const variablesDefinition = (goal: EdgeGoalNode): string => { + const logger = getLogger(); + const defineVariable = (variable: string, upperBound: number): string => { + logger.variableDefinition({ + variable, + upperBound, + initialValue: 0, + type: 'int', + context: 'goal', + }); + return `${variable} : [0..${upperBound}] init 0;`; + }; + const stateVariableStatement = defineVariable(goalStateVariable(goal.id), 1); + + const pursueableChildrenCount = pursueableChildren(goal).length; + const chosenVariableStatement = + goal.properties.engine.executionDetail?.type === 'choice' && + pursueableChildrenCount > 0 + ? defineVariable(chosenVariable(goal.id), pursueableChildrenCount) + : null; + + const degradationFailedLines = degradationSiblingFailedVariableLines( + goal, + defineVariable, + ); + + return [ + stateVariableStatement, + chosenVariableStatement, + ...degradationFailedLines, + ] + .filter(Boolean) + .join('\n '); +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/rewards/index.ts b/packages/lib/src/engines/edgeV2/template/modules/rewards/index.ts new file mode 100644 index 00000000..34d08ce9 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/rewards/index.ts @@ -0,0 +1 @@ +export const costsModules = (): void => {}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/system/system.ts b/packages/lib/src/engines/edgeV2/template/modules/system/system.ts new file mode 100644 index 00000000..b01239f7 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/system/system.ts @@ -0,0 +1,158 @@ +import { GoalTree } from '@goal-controller/goal-tree'; +import { existsSync, readFileSync } from 'fs'; +import path from 'path'; +import { getLogger } from '../../../logger/logger'; +import type { EdgeGoalTree, EdgeResource, EdgeTask } from '../../../types'; +import { systemModuleTemplate } from './template'; + +/** + * Extracts transition lines from the System module in an existing PRISM file + * @param fileName The input file name (e.g., "examples/experiments/1-minimal.txt") + * @returns Array of transition lines from the System module, or empty array if file doesn't exist or has no transitions + */ +const extractOldSystemTransitions = (fileName: string): string[] => { + // Extract base name from fileName (e.g., "examples/experiments/1-minimal.txt" -> "1-minimal") + const parsedPath = path.parse(fileName); + const baseName = parsedPath.name; + + // Try multiple paths to find the output file (supports both monorepo and direct execution) + const possiblePaths = [ + `output/${baseName}.prism`, // From project root + `../../output/${baseName}.prism`, // From packages/lib (monorepo) + ]; + + const oldPrismFilePath = possiblePaths.find((p) => existsSync(p)); + + // Check if the old PRISM file exists + if (!oldPrismFilePath) { + return []; + } + + try { + const prismContent = readFileSync(oldPrismFilePath, 'utf8'); + const lines = prismContent.split('\n'); + + let inSystemModule = false; + const transitions: string[] = []; + + for (let i = 0; i < lines.length; i++) { + const line = lines[i]; + if (!line) continue; + + const trimmedLine = line.trim(); + + // Check if we're entering the System module + if (trimmedLine === 'module System') { + inSystemModule = true; + continue; + } + + // Check if we're leaving the System module + if (inSystemModule && trimmedLine === 'endmodule') { + break; + } + + // If we're in the System module, check for transitions + if (inSystemModule) { + // Match transition pattern: [label] guard -> update; + const transitionMatch = trimmedLine.match( + /^\s*\[([^\]]+)\]\s*.+?\s*->\s*.+?\s*;?\s*$/, + ); + if (transitionMatch) { + // Collect preceding comment lines + const precedingComments: string[] = []; + let j = i - 1; + while (j >= 0) { + const prevLine = lines[j]; + if (!prevLine) { + j--; + continue; + } + const prevTrimmed = prevLine.trim(); + // Stop if we hit a non-comment, non-empty line + if (prevTrimmed && !prevTrimmed.startsWith('//')) { + break; + } + // Collect comment lines (preserve order by unshifting) + if (prevTrimmed.startsWith('//')) { + precedingComments.unshift(prevLine); + } + j--; + } + + // Add preceding comments and the transition line + transitions.push(...precedingComments); + transitions.push(line); + } + } + } + + return transitions; + } catch (error) { + // If there's an error reading the file, return empty array + return []; + } +}; + +export const systemModule = ({ + gm, + fileName, + clean = false, + variables: defaultVariableValues, +}: { + gm: EdgeGoalTree; + fileName: string; + clean?: boolean; + variables: Record; +}): string => { + const logger = getLogger(); + logger.initSystem(); + const goalContextVars = GoalTree.contextVariables(gm); + + // Also collect context variables from tasks + const tasks = GoalTree.allByType(gm, 'task'); + const taskContextVariables = new Set(); + tasks.forEach((task: EdgeTask) => { + if (task.properties.engine.execCondition?.assertion) { + task.properties.engine.execCondition.assertion.variables.forEach( + (v: { name: string }) => { + taskContextVariables.add(v.name); + }, + ); + } + if (task.properties.engine.execCondition?.maintain?.variables) { + task.properties.engine.execCondition.maintain.variables.forEach( + (v: { name: string }) => { + taskContextVariables.add(v.name); + }, + ); + } + }); + + // Combine goal and task context variables + const allContextVars = new Set([ + ...goalContextVars, + ...Array.from(taskContextVariables), + ]); + + // Exclude resource IDs from context variables + const resources = GoalTree.allByType(gm, 'resource'); + const resourceIds = new Set( + resources.map((resource: EdgeResource) => resource.id), + ); + const variables = Array.from(allContextVars).filter( + (varName) => !resourceIds.has(varName), + ); + + const oldTransitions = clean ? [] : extractOldSystemTransitions(fileName); + return systemModuleTemplate({ + variables, + resources, + defaultVariableValues, + oldTransitions, + }); +}; + +export const __test_only_exports__ = { + extractOldSystemTransitions, +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/system/template/index.ts b/packages/lib/src/engines/edgeV2/template/modules/system/template/index.ts new file mode 100644 index 00000000..2e4e761e --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/system/template/index.ts @@ -0,0 +1,53 @@ +import { defineVariable, resourceVariableName } from './variable'; +import type { EdgeResource } from '../../../../types'; + +export const systemModuleTemplate = ({ + variables, + resources, + defaultVariableValues, + oldTransitions, +}: { + variables: string[]; + resources: Array; + defaultVariableValues: Record; + oldTransitions?: string[]; +}): string => { + const resourceVariables = resources.map((resource) => { + const { variable } = resource.properties.engine; + if (variable.type === 'boolean') { + return defineVariable( + resourceVariableName(resource), + variable.initialValue ?? 'MISSING_VARIABLE_DEFINITION', + variable.type, + 'resource', + ); + } + + return defineVariable( + resourceVariableName(resource), + variable.initialValue ?? 'MISSING_VARIABLE_DEFINITION', + variable.type, + 'resource', + variable.lowerBound, + variable.upperBound, + ); + }); + return `module System + ${[ + variables.map((variable) => { + return defineVariable( + variable, + defaultVariableValues[variable] ?? 'MISSING_VARIABLE_DEFINITION', + 'boolean', + 'context', + ); + }), + resourceVariables.join('\n '), + oldTransitions?.map((str) => str.trim()).join('\n ') ?? '', + ] + .filter(Boolean) + .flat() + .join('\n ') + .trim()} +endmodule`; +}; diff --git a/packages/lib/src/engines/edgeV2/template/modules/system/template/variable.ts b/packages/lib/src/engines/edgeV2/template/modules/system/template/variable.ts new file mode 100644 index 00000000..75e9f6d8 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/modules/system/template/variable.ts @@ -0,0 +1,31 @@ +import type { EdgeResource } from '../../../../types'; +import { getLogger } from '../../../../logger/logger'; + +export const resourceVariableName = (resource: EdgeResource): string => + `${resource.id}`; + +export const defineVariable = ( + variable: string, + initialValue: number | boolean | 'MISSING_VARIABLE_DEFINITION', + type: 'boolean' | 'int', + context: 'resource' | 'context', + lowerBound?: number | boolean, + upperBound?: number | boolean, +): string => { + const logger = getLogger(); + logger.variableDefinition({ + variable, + initialValue, + type, + lowerBound, + upperBound, + context: 'system', + subContext: context, + }); + switch (type) { + case 'boolean': + return `${variable}: bool init ${initialValue};`; + case 'int': + return `${variable}: [${lowerBound}..${upperBound}] init ${initialValue};`; + } +}; diff --git a/packages/lib/src/engines/edgeV2/template/prismGuards.ts b/packages/lib/src/engines/edgeV2/template/prismGuards.ts new file mode 100644 index 00000000..68e18d54 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/template/prismGuards.ts @@ -0,0 +1,42 @@ +/** + * Shared Edge V2 PRISM guard string builders. + * + * A single source of truth for the snippet `achievable * 10.0 > decision` / + * `<= decision` pattern and for "child is idle" guards so they cannot drift + * across skip, pursue, and validator files. + */ +import { Node } from '@goal-controller/goal-tree'; +import type { TreeNode } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode, EdgeTask } from '../types'; +import { achievable, goalState, pursued } from '../mdp/common'; +import { decisionVariable } from './common'; + +/** Scale factor shared across all EDGE snippet pursue/skip guards. */ +export const ACHIEVABILITY_DECISION_SCALE = 10.0; + +/** `child_achievable*10.0 > decision_child` (used in pursue guards). */ +export const achievableGtDecision = (id: string): string => + `${achievable(id)}*${ACHIEVABILITY_DECISION_SCALE} > ${decisionVariable(id)}`; + +/** `child_achievable*10.0 <= decision_child` (used in skip guards). */ +export const achievableLeDecision = (id: string): string => + `${achievable(id)}*${ACHIEVABILITY_DECISION_SCALE} <= ${decisionVariable(id)}`; + +/** + * "This node is not currently being pursued": + * - task → `task_pursued=0` + * - goal → `goal_state=0` + */ +export const childIdle = (child: TreeNode | EdgeGoalNode | EdgeTask): string => + child.type === 'task' ? `${pursued(child.id)}=0` : `${goalState(child.id)}=0`; + +/** + * Ordered list of pursueable (non-resource) children for a goal. + * Stable because `Node.children` preserves declaration order. + */ +export const pursueableChildren = ( + goal: EdgeGoalNode, +): Array => + Node.children(goal).filter( + (c): c is EdgeGoalNode | EdgeTask => !Node.isResource(c), + ); diff --git a/packages/lib/src/engines/edgeV2/types.ts b/packages/lib/src/engines/edgeV2/types.ts new file mode 100644 index 00000000..66a1a008 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/types.ts @@ -0,0 +1,70 @@ +/** + * Edge Engine Types + * Types for EDGE/PRISM template engine properties + */ + +import type { Dictionary } from 'lodash'; + +export type ExecCondition = { + maintain?: { + sentence: string; + variables: Array<{ name: string; value: boolean | null }>; + }; + assertion: { + sentence: string; + variables: Array<{ name: string; value: boolean | null }>; + }; +}; + +export type GoalExecutionDetail = ( + | { type: 'interleaved'; interleaved: string[] } + | { type: 'alternative'; alternative: string[] } + | { type: 'sequence'; sequence: string[] } + | { type: 'degradation'; degradationList: string[] } + | { type: 'decisionMaking'; dm: string[] } + | { type: 'choice' } +) & { + retryMap?: Dictionary; +}; + +export type EdgeTaskProps = { + execCondition?: ExecCondition; + maxRetries: number; +}; + +// Forward reference type - will be resolved when GoalNode is generic +export type EdgeGoalProps = { + utility: string; + cost: string; + dependsOn: TGoalNode[]; + executionDetail: GoalExecutionDetail | null; + execCondition?: ExecCondition; + maxRetries: number; +}; + +// Resource variable types for Edge engine +export type EdgeResourceVariable = + | { + type: 'boolean'; + initialValue: boolean; + } + | { + type: 'int'; + initialValue: number; + lowerBound: number; + upperBound: number; + }; + +// Resource properties for Edge engine +export type EdgeResourceProps = { + variable: EdgeResourceVariable; +}; + +// Re-export mapper types for convenience +export type { + EdgeGoalNode, + EdgeTask, + EdgeResource, + EdgeGoalTree, + EdgeGoalPropsResolved, +} from './mapper'; diff --git a/packages/lib/src/engines/edgeV2/validator/expectedElements.ts b/packages/lib/src/engines/edgeV2/validator/expectedElements.ts new file mode 100644 index 00000000..746255d6 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/validator/expectedElements.ts @@ -0,0 +1,261 @@ +import type { Resource } from '@goal-controller/goal-tree'; +import { GoalTree } from '@goal-controller/goal-tree'; +import type { EdgeGoalNode, EdgeGoalTree, EdgeTask } from '../types'; + +// Type aliases for this file +type GoalNode = EdgeGoalNode; +type Task = EdgeTask; +type GoalTreeType = EdgeGoalTree; +import { failed } from '../mdp/common'; +import { + achievableFormulaVariable, + achievedTransition, + achievedVariable, + chosenVariable, + decisionVariable, + pursueTransition, + underscoredOrDecisionVariable, +} from '../template/common'; +import { cappedDegradationChildren } from '../template/modules/goalModule/template/variables'; +import { pursueableChildren } from '../template/prismGuards'; +import type { ExpectedElements } from './types'; + +const achievedMaintain = (goalId: string): string => { + return `${goalId}_achieved_maintain`; +}; +const goalStateVariable = (goalId: string): string => `${goalId}_state`; + +const calculateGoalVariables = (goal: GoalNode): string[] => { + const variables: string[] = []; + + // Always has state variable + variables.push(goalStateVariable(goal.id)); + + // One nondeterministic-resolution int per goal module + variables.push(decisionVariable(goal.id)); + + if (goal.relationToChildren === 'or') { + variables.push(underscoredOrDecisionVariable(goal.id)); + } + + // Has chosen if choice execution detail + if (goal.properties.engine.executionDetail?.type === 'choice') { + if (pursueableChildren(goal).length > 0) { + variables.push(chosenVariable(goal.id)); + } + } + + // Degradation OR: one failed counter per sibling id in retryMap (parent module) + for (const { child } of cappedDegradationChildren(goal)) { + variables.push(failed(child.id)); + } + + return variables; +}; + +const calculateGoalTransitions = (goal: GoalNode): string[] => { + const transitions: string[] = []; + + // Always has pursue transitions: one for itself + one for each pursueable child + transitions.push(pursueTransition(goal.id)); + const children = pursueableChildren(goal); + const executionDetail = goal.properties.engine.executionDetail; + const cappedChildren = cappedDegradationChildren(goal); + + children.forEach((child) => { + transitions.push(pursueTransition(child.id)); + if ( + goal.relationToChildren === 'or' && + executionDetail?.type === 'choice' + ) { + transitions.push(pursueTransition(child.id)); + } + if ( + goal.relationToChildren === 'or' && + executionDetail?.type === 'degradation' && + cappedChildren.some(({ child: c }) => c.id === child.id) + ) { + transitions.push(pursueTransition(child.id)); + } + }); + + // Always has achieve transition + transitions.push(achievedTransition(goal.id)); + + // Skip: OR choice emits one line per chosen branch (0 = uncommitted) plus default; else single skip + if ( + goal.relationToChildren === 'or' && + executionDetail?.type === 'choice' && + children.length > 0 + ) { + for (let i = 0; i <= children.length; i++) { + transitions.push(`skip_${goal.id}`); + } + } else if ( + goal.relationToChildren === 'or' && + executionDetail?.type === 'degradation' + ) { + if (cappedChildren.length > 0) { + // Per capped sibling: one retry-skip (`failed { + const formulas: string[] = []; + + // Achievability formula (Edge v1 combinators over child `_achievable`) + formulas.push(achievableFormulaVariable(goal.id)); + + // Achieved formula (derived from child goals/tasks) + formulas.push(achievedVariable(goal.id)); + + // Has maintain formula if maintain goal + if (goal.properties.engine.execCondition?.maintain) { + formulas.push(achievedMaintain(goal.id)); + } + + return formulas; +}; + +const calculateGoalContextVariables = (goal: GoalNode): string[] => { + const variables: string[] = []; + + // Only count context variables from the goal's own assertion + // These appear in the first pursue line of the goal's module + // We don't count maintain variables because they're used in formulas, not pursue lines + // We don't count children's context variables because they don't appear in the goal's first pursue line + if (goal.properties.engine.execCondition?.assertion) { + goal.properties.engine.execCondition.assertion.variables.forEach( + (v: { name: string }) => { + variables.push(v.name); + }, + ); + } + + return variables; +}; + +const calculateChangeManagerTaskVariables = ( + tasks: Task[], +): Map => { + const taskVariables = new Map(); + + tasks.forEach((task: Task) => { + const variables: string[] = []; + variables.push(`${task.id}_pursued`); + variables.push(achievedVariable(task.id)); + + taskVariables.set(task.id, variables); + }); + + return taskVariables; +}; + +const calculateChangeManagerTaskTransitions = ( + tasks: Task[], +): Map => { + const taskTransitions = new Map(); + + tasks.forEach((task: Task) => { + const transitions: string[] = []; + transitions.push(pursueTransition(task.id)); + transitions.push(`try_${task.id}`); + transitions.push(achievedTransition(task.id)); + taskTransitions.set(task.id, transitions); + }); + + return taskTransitions; +}; + +export const calculateExpectedElements = ( + goalTree: GoalTreeType, +): ExpectedElements => { + const goals = GoalTree.allByType(goalTree, 'goal'); + const tasks = GoalTree.allByType(goalTree, 'task'); + const resources = GoalTree.allByType(goalTree, 'resource'); + + const goalElements = new Map< + string, + { + variables: string[]; + transitions: string[]; + formulas: string[]; + contextVariables: string[]; + } + >(); + + // Calculate expected elements for each goal + goals.forEach((goal: GoalNode) => { + goalElements.set(goal.id, { + variables: calculateGoalVariables(goal), + transitions: calculateGoalTransitions(goal), + formulas: calculateGoalFormulas(goal), + contextVariables: calculateGoalContextVariables(goal), + }); + }); + + // Calculate ChangeManager elements + const changeManagerTaskVariables = calculateChangeManagerTaskVariables(tasks); + const changeManagerTaskTransitions = + calculateChangeManagerTaskTransitions(tasks); + + // Calculate System elements + // Context variables from goals (using existing function) + const goalContextVariables = GoalTree.contextVariables(goalTree); + + // Also collect context variables from tasks + const taskContextVariables = new Set(); + tasks.forEach((task: Task) => { + if (task.properties.engine.execCondition?.assertion) { + task.properties.engine.execCondition.assertion.variables.forEach( + (v: { name: string }) => { + taskContextVariables.add(v.name); + }, + ); + } + if (task.properties.engine.execCondition?.maintain?.variables) { + task.properties.engine.execCondition.maintain.variables.forEach( + (v: { name: string }) => { + taskContextVariables.add(v.name); + }, + ); + } + }); + + // Resource IDs to exclude from context variables (resources are separate) + const resourceIds = new Set( + resources.map((resource: Resource) => resource.id), + ); + + // Combine goal and task context variables, but exclude resource IDs + const allContextVars = new Set([ + ...goalContextVariables, + ...Array.from(taskContextVariables), + ]); + const contextVariables = Array.from(allContextVars).filter( + (varName) => !resourceIds.has(varName), + ); + const resourceVariables = resources.map((resource: Resource) => resource.id); + + return { + goals: goalElements, + changeManager: { + taskVariables: changeManagerTaskVariables, + taskTransitions: changeManagerTaskTransitions, + }, + system: { + contextVariables, + resourceVariables, + }, + }; +}; diff --git a/packages/lib/src/engines/edgeV2/validator/index.ts b/packages/lib/src/engines/edgeV2/validator/index.ts new file mode 100644 index 00000000..e78b2eff --- /dev/null +++ b/packages/lib/src/engines/edgeV2/validator/index.ts @@ -0,0 +1,59 @@ +import { writeFileSync } from 'fs'; +import { ensureLogFileDirectory } from '../logger/filePath'; +import { + formatValidationReport, + getValidationSummary, + serializeValidationReportToJSON, + summarizeValidationFailures, +} from './report'; +import type { ValidationReport } from './types'; +import { validatePrismModel } from './validator'; +import type { EdgeGoalTree } from '../mapper'; + +export type { ValidationReport } from './types'; +export { + formatValidationReport, + getValidationSummary, + serializeValidationReportToJSON, + summarizeValidationFailures, + validatePrismModel, +}; + +/** + * Validates a PRISM model against the expected GoalTree structure + * @param goalTree The GoalTree structure + * @param prismModel The generated PRISM model string + * @param modelFileName Optional model file name to write JSON report to logs folder + * @returns Validation report with expected, emitted, and missing elements + */ +export const validate = ( + goalTree: EdgeGoalTree, + prismModel: string, + modelFileName?: string, +): ValidationReport => { + const report = validatePrismModel(goalTree, prismModel); + + // Write JSON report to logs folder if modelFileName is provided + // Skip file writing in serverless environments (e.g., Vercel) + if (modelFileName) { + const jsonReport = serializeValidationReportToJSON(report); + const jsonFilePath = ensureLogFileDirectory( + modelFileName, + '.validation.json', + ); + // Only write if directory creation succeeded (not in serverless environment) + if (jsonFilePath) { + try { + writeFileSync( + jsonFilePath, + JSON.stringify(jsonReport, null, 2), + 'utf8', + ); + } catch { + // Silently fail in serverless environments + } + } + } + + return report; +}; diff --git a/packages/lib/src/engines/edgeV2/validator/parser.ts b/packages/lib/src/engines/edgeV2/validator/parser.ts new file mode 100644 index 00000000..39cf1d1a --- /dev/null +++ b/packages/lib/src/engines/edgeV2/validator/parser.ts @@ -0,0 +1,333 @@ +import type { + FormulaInfo, + ModuleInfo, + ParsedPrismModel, + TransitionInfo, + VariableInfo, +} from './types'; + +const parseVariable = (line: string): VariableInfo | null => { + // Match patterns like: + // G0_pursued : [0..1] init 0; + // variable: bool init true; + // variable: [0..10] init 5; + const varMatch = line.match( + /^\s*(\w+)\s*:\s*(?:\[(\d+)\.\.(\d+)\]|bool)\s*init\s*(\w+)\s*;/, + ); + if (!varMatch) return null; + + const name = varMatch[1]; + const lower = varMatch[2]; + const upper = varMatch[3]; + const initValue = varMatch[4]; + + if (!name || !initValue) return null; + + if (lower && upper) { + // Integer variable + return { + name, + type: 'int', + bounds: { lower: parseInt(lower, 10), upper: parseInt(upper, 10) }, + initialValue: parseInt(initValue, 10), + }; + } else { + // Boolean variable + return { + name, + type: 'bool', + initialValue: initValue === 'true', + }; + } +}; + +/** + * Extracts variable references from a guard condition string. + * Handles patterns like: + * - variable=value + * - variable'=value (updates) + * - variable>=value, variable<=value, variable!=value + * - variable>value, variable { + const variables = new Set(); + + // Match variable patterns in the guard + // Patterns: var=value, var'=value, var>=value, var<=value, var!=value, var>value, var=|<=|!=|>|<|=)/g; + let match; + + while ((match = variablePattern.exec(guard)) !== null) { + const varName = match[1]; + // Skip common keywords and operators + if ( + varName && + !['true', 'false', 'min', 'max', 'and', 'or', 'not'].includes(varName) + ) { + variables.add(varName); + } + } + + // Also match standalone variable names in parentheses or as part of formulas + // This catches cases like (var1 & var2) or var1 * var2 + const guardWords = guard.split(/\s*[&|()+\-*=<>!]\s*/); + + guardWords.forEach((word) => { + const trimmed = word.trim(); + // Match if it looks like a variable (starts with letter/underscore, contains alphanumeric/underscore) + if (/^[a-zA-Z_][a-zA-Z0-9_]*$/.test(trimmed)) { + // Skip numbers, boolean literals, and common keywords + if ( + !/^\d+$/.test(trimmed) && + trimmed !== 'true' && + trimmed !== 'false' && + !['and', 'or', 'not', 'min', 'max'].includes(trimmed.toLowerCase()) + ) { + variables.add(trimmed); + } + } + }); + + return Array.from(variables); +}; + +const parseTransition = (line: string): TransitionInfo | null => { + // Match patterns like: + // [pursue_G0] G0_pursued=0 & G0_achieved=0 -> (G0_pursued'=1); + // [achieved_G0] condition -> update; + const transitionMatch = line.match( + /^\s*\[([^\]]+)\]\s*(.+?)\s*->\s*(.+?)\s*;?\s*$/, + ); + if (!transitionMatch) return null; + + const label = transitionMatch[1]; + const guard = transitionMatch[2]; + const update = transitionMatch[3]; + + if (!label || !guard || !update) return null; + + const guardTrimmed = guard.trim(); + const variablesReferenced = extractVariablesFromGuard(guardTrimmed); + + return { + label: label.trim(), + guard: guardTrimmed, + update: update.trim(), + variablesReferenced, + }; +}; + +const parseFormula = (line: string): FormulaInfo | null => { + // Match patterns like: + // formula G0_achievable = G1_achievable * G2_achievable; + // const double T1_achievable = 0.9; + const formulaMatch = line.match( + /^\s*(?:formula|const\s+double)\s+(\w+)\s*=\s*(.+?)\s*;?\s*$/, + ); + if (!formulaMatch) return null; + + const name = formulaMatch[1]; + const expression = formulaMatch[2]; + + if (!name || !expression) return null; + + // Check if it's a constant (const double) + if (line.includes('const double')) { + const constValue = parseFloat(expression); + if (!isNaN(constValue)) { + return { + name, + expression: constValue.toString(), + }; + } + } + + return { + name, + expression: expression.trim(), + }; +}; + +const parseModule = ( + lines: string[], + startIndex: number, +): { module: ModuleInfo; nextIndex: number } | null => { + // Find module declaration + const moduleMatch = lines[startIndex]?.match(/^\s*module\s+(\w+)\s*$/); + if (!moduleMatch) return null; + + const moduleName = moduleMatch[1]; + if (!moduleName) return null; + + // Look backwards for goal type in header comments + // Headers are typically 3-5 lines before the module declaration + let goalType: + | 'choice' + | 'degradation' + | 'sequence' + | 'interleaved' + | 'alternative' + | 'basic' + | undefined; + for (let j = Math.max(0, startIndex - 10); j < startIndex; j++) { + const line = lines[j]; + if (!line) continue; + const trimmedLine = line.trim(); + const typeMatch = trimmedLine.match(/^\/\/\s*Type:\s*(\w+)/i); + const typeStr = typeMatch?.[1]?.toLowerCase(); + if (typeStr === 'choice') { + goalType = 'choice'; + break; + } else if (typeStr === 'degradation') { + goalType = 'degradation'; + break; + } else if (typeStr === 'sequence') { + goalType = 'sequence'; + break; + } else if (typeStr === 'interleaved') { + goalType = 'interleaved'; + break; + } else if (typeStr === 'alternative') { + goalType = 'alternative'; + break; + } else if (typeStr === 'basic') { + goalType = 'basic'; + break; + } + } + + const variables: VariableInfo[] = []; + const transitions: TransitionInfo[] = []; + + let i = startIndex + 1; + let inModule = true; + + while (i < lines.length && inModule) { + const line = lines[i]?.trim() || ''; + + if (line === 'endmodule') { + inModule = false; + break; + } + + // Try to parse as variable + const variable = parseVariable(line); + if (variable) { + variables.push(variable); + i++; + continue; + } + + // Try to parse as transition + const transition = parseTransition(line); + if (transition) { + transitions.push(transition); + i++; + continue; + } + + // Skip comments and empty lines + if (line.startsWith('//') || line === '') { + i++; + continue; + } + + i++; + } + + // Calculate line count: from module declaration to endmodule (inclusive) + const lineCount = i - startIndex + 1; + + return { + module: { + name: moduleName, + variables, + transitions, + goalType, + lineCount, + }, + nextIndex: i + 1, + }; +}; + +export const parsePrismModel = (prismModel: string): ParsedPrismModel => { + const lines = prismModel.split('\n'); + const goalModules = new Map(); + let changeManagerModule: ModuleInfo | undefined; + let systemModule: ModuleInfo | undefined; + const formulas: FormulaInfo[] = []; + const constants = new Map(); + const nondetConstants: string[] = []; + + let i = 0; + + // Skip dtmc declaration if present + while (i < lines.length && lines[i]?.trim().startsWith('dtmc')) { + i++; + } + + // Skip empty lines + while (i < lines.length && lines[i]?.trim() === '') { + i++; + } + + // Parse modules + while (i < lines.length) { + const line = lines[i]?.trim() || ''; + + const constIntNondet = line.match(/^\s*const\s+int\s+(\w+)\s*;\s*$/); + if (constIntNondet?.[1]) { + nondetConstants.push(constIntNondet[1]); + i++; + continue; + } + + // Check if it's a module + if (line.startsWith('module ')) { + const result = parseModule(lines, i); + if (result) { + const { module, nextIndex } = result; + + if (module.name === 'ChangeManager') { + changeManagerModule = module; + } else if (module.name === 'System') { + systemModule = module; + } else { + // Assume it's a goal module + goalModules.set(module.name, module); + } + + i = nextIndex; + continue; + } + } + + // Check if it's a formula or constant + if (line.startsWith('formula ') || line.startsWith('const ')) { + const formula = parseFormula(line); + if (formula) { + // Check if it's a constant + if (line.startsWith('const double')) { + const value = parseFloat(formula.expression); + if (!isNaN(value)) { + constants.set(formula.name, value); + } + } + formulas.push(formula); + } + } + + i++; + } + + return { + goalModules, + changeManagerModule, + systemModule, + formulas, + constants, + nondetConstants, + }; +}; diff --git a/packages/lib/src/engines/edgeV2/validator/report.ts b/packages/lib/src/engines/edgeV2/validator/report.ts new file mode 100644 index 00000000..fb280044 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/validator/report.ts @@ -0,0 +1,443 @@ +import type { ValidationReport } from './types'; + +/** Short, log-friendly list of what failed structural validation. */ +export const summarizeValidationFailures = ( + report: ValidationReport, +): string => { + const lines: string[] = []; + lines.push(`Missing count: ${report.summary.totalMissing}`); + report.goals.forEach((v, goalId) => { + const parts: string[] = []; + if (v.module.missing > 0) { + parts.push('goal module not found in PRISM output'); + } + if (v.variables.missing > 0) { + parts.push(`variables [${v.variables.details.missing.join(', ')}]`); + } + if (v.transitions.missing > 0) { + parts.push(`transitions [${v.transitions.details.missing.join(', ')}]`); + } + if (v.formulas.missing > 0) { + parts.push(`formulas [${v.formulas.details.missing.join(', ')}]`); + } + if (v.contextVariables.missing > 0) { + parts.push( + `contextVariables [${v.contextVariables.details.missing.join(', ')}]`, + ); + } + if (parts.length > 0) { + lines.push(` ${goalId}: ${parts.join('; ')}`); + } + }); + if (report.changeManager.taskVariables.missing > 0) { + lines.push( + ` ChangeManager task variables: [${report.changeManager.taskVariables.details.missing.join(', ')}]`, + ); + } + if (report.changeManager.taskTransitions.missing > 0) { + lines.push( + ` ChangeManager task transitions: [${report.changeManager.taskTransitions.details.missing.join(', ')}]`, + ); + } + if (report.system.contextVariables.missing > 0) { + lines.push( + ` System contextVariables: [${report.system.contextVariables.details.missing.join(', ')}]`, + ); + } + if (report.system.resourceVariables.missing > 0) { + lines.push( + ` System resourceVariables: [${report.system.resourceVariables.details.missing.join(', ')}]`, + ); + } + return lines.join('\n'); +}; + +export const serializeValidationReportToJSON = ( + report: ValidationReport, +): Record => { + // Convert goals Map to object + const goalsObject: Record< + string, + { + module: { + expected: number; + emitted: number; + missing: number; + lineCount?: number; + }; + variables: { expected: number; emitted: number; missing: number }; + transitions: { expected: number; emitted: number; missing: number }; + formulas: { expected: number; emitted: number; missing: number }; + contextVariables: { + expected: number; + emitted: number; + missing: number; + }; + } + > = {}; + + report.goals.forEach((validation, goalId) => { + goalsObject[goalId] = { + module: { + expected: validation.module.expected, + emitted: validation.module.emitted, + missing: validation.module.missing, + ...(validation.module.lineCount !== undefined && { + lineCount: validation.module.lineCount, + }), + }, + variables: { + expected: validation.variables.expected, + emitted: validation.variables.emitted, + missing: validation.variables.missing, + }, + transitions: { + expected: validation.transitions.expected, + emitted: validation.transitions.emitted, + missing: validation.transitions.missing, + }, + formulas: { + expected: validation.formulas.expected, + emitted: validation.formulas.emitted, + missing: validation.formulas.missing, + }, + contextVariables: { + expected: validation.contextVariables.expected, + emitted: validation.contextVariables.emitted, + missing: validation.contextVariables.missing, + }, + }; + }); + + return { + summary: { + expected: report.summary.totalExpected, + emitted: report.summary.totalEmitted, + missing: report.summary.totalMissing, + byNodeType: { + goals: { + modules: { + expected: report.summary.byNodeType.goals.modules.expected, + emitted: report.summary.byNodeType.goals.modules.emitted, + }, + }, + tasks: { + variables: { + expected: report.summary.byNodeType.tasks.variables.expected, + emitted: report.summary.byNodeType.tasks.variables.emitted, + }, + transitions: { + expected: report.summary.byNodeType.tasks.transitions.expected, + emitted: report.summary.byNodeType.tasks.transitions.emitted, + }, + }, + resources: { + variables: { + expected: report.summary.byNodeType.resources.variables.expected, + emitted: report.summary.byNodeType.resources.variables.emitted, + }, + }, + }, + }, + goalTypes: { + choice: { + expected: report.goalTypes.choice.expected, + emitted: report.goalTypes.choice.emitted, + missing: report.goalTypes.choice.missing, + }, + degradation: { + expected: report.goalTypes.degradation.expected, + emitted: report.goalTypes.degradation.emitted, + missing: report.goalTypes.degradation.missing, + }, + sequence: { + expected: report.goalTypes.sequence.expected, + emitted: report.goalTypes.sequence.emitted, + missing: report.goalTypes.sequence.missing, + }, + interleaved: { + expected: report.goalTypes.interleaved.expected, + emitted: report.goalTypes.interleaved.emitted, + missing: report.goalTypes.interleaved.missing, + }, + alternative: { + expected: report.goalTypes.alternative.expected, + emitted: report.goalTypes.alternative.emitted, + missing: report.goalTypes.alternative.missing, + }, + basic: { + expected: report.goalTypes.basic.expected, + emitted: report.goalTypes.basic.emitted, + missing: report.goalTypes.basic.missing, + }, + }, + goals: goalsObject, + changeManager: { + taskVariables: { + expected: report.changeManager.taskVariables.expected, + emitted: report.changeManager.taskVariables.emitted, + missing: report.changeManager.taskVariables.missing, + }, + taskTransitions: { + expected: report.changeManager.taskTransitions.expected, + emitted: report.changeManager.taskTransitions.emitted, + missing: report.changeManager.taskTransitions.missing, + }, + }, + system: { + contextVariables: { + expected: report.system.contextVariables.expected, + emitted: report.system.contextVariables.emitted, + missing: report.system.contextVariables.missing, + }, + resourceVariables: { + expected: report.system.resourceVariables.expected, + emitted: report.system.resourceVariables.emitted, + missing: report.system.resourceVariables.missing, + }, + }, + }; +}; + +export const formatValidationReport = (report: ValidationReport): string => { + const lines: string[] = []; + + lines.push('='.repeat(80)); + lines.push('PRISM MODEL VALIDATION REPORT'); + lines.push('='.repeat(80)); + lines.push(''); + + // Summary + lines.push('SUMMARY'); + lines.push('-'.repeat(80)); + lines.push(`Total Expected: ${report.summary.totalExpected}`); + lines.push(`Total Emitted: ${report.summary.totalEmitted}`); + lines.push(`Total Missing: ${report.summary.totalMissing}`); + lines.push(''); + + // Node-type aggregated summary + lines.push('SUMMARY BY NODE TYPE'); + lines.push('-'.repeat(80)); + lines.push('Goals:'); + lines.push( + ` Modules: expected=${report.summary.byNodeType.goals.modules.expected}, emitted=${report.summary.byNodeType.goals.modules.emitted}`, + ); + lines.push('Tasks:'); + lines.push( + ` Variables: expected=${report.summary.byNodeType.tasks.variables.expected}, emitted=${report.summary.byNodeType.tasks.variables.emitted}`, + ); + lines.push( + ` Transitions: expected=${report.summary.byNodeType.tasks.transitions.expected}, emitted=${report.summary.byNodeType.tasks.transitions.emitted}`, + ); + lines.push('Resources:'); + lines.push( + ` Variables: expected=${report.summary.byNodeType.resources.variables.expected}, emitted=${report.summary.byNodeType.resources.variables.emitted}`, + ); + lines.push(''); + + // Goal Types + lines.push('GOAL TYPES'); + lines.push('-'.repeat(80)); + lines.push( + `Choice: expected=${report.goalTypes.choice.expected}, emitted=${report.goalTypes.choice.emitted}, missing=${report.goalTypes.choice.missing}`, + ); + lines.push( + `Degradation: expected=${report.goalTypes.degradation.expected}, emitted=${report.goalTypes.degradation.emitted}, missing=${report.goalTypes.degradation.missing}`, + ); + lines.push( + `Sequence: expected=${report.goalTypes.sequence.expected}, emitted=${report.goalTypes.sequence.emitted}, missing=${report.goalTypes.sequence.missing}`, + ); + lines.push( + `Interleaved: expected=${report.goalTypes.interleaved.expected}, emitted=${report.goalTypes.interleaved.emitted}, missing=${report.goalTypes.interleaved.missing}`, + ); + lines.push( + `Alternative: expected=${report.goalTypes.alternative.expected}, emitted=${report.goalTypes.alternative.emitted}, missing=${report.goalTypes.alternative.missing}`, + ); + lines.push( + `Basic: expected=${report.goalTypes.basic.expected}, emitted=${report.goalTypes.basic.emitted}, missing=${report.goalTypes.basic.missing}`, + ); + lines.push(''); + + // Goals validation + lines.push('GOALS VALIDATION'); + lines.push('-'.repeat(80)); + report.goals.forEach((validation, goalId) => { + lines.push(`Goal: ${goalId}`); + lines.push( + ` Module: expected=${validation.module.expected}, emitted=${validation.module.emitted}, missing=${validation.module.missing}`, + ); + + lines.push( + ` Variables: expected=${validation.variables.expected}, emitted=${validation.variables.emitted}, missing=${validation.variables.missing}`, + ); + if (validation.variables.details.missing.length > 0) { + lines.push( + ` Missing: ${validation.variables.details.missing.join(', ')}`, + ); + } + + lines.push( + ` Transitions: expected=${validation.transitions.expected}, emitted=${validation.transitions.emitted}, missing=${validation.transitions.missing}`, + ); + if (validation.transitions.details.missing.length > 0) { + lines.push( + ` Missing: ${validation.transitions.details.missing.join(', ')}`, + ); + } + + lines.push( + ` Formulas: expected=${validation.formulas.expected}, emitted=${validation.formulas.emitted}, missing=${validation.formulas.missing}`, + ); + if (validation.formulas.details.missing.length > 0) { + lines.push( + ` Missing: ${validation.formulas.details.missing.join(', ')}`, + ); + } + + lines.push( + ` Context Variables: expected=${validation.contextVariables.expected}, emitted=${validation.contextVariables.emitted}, missing=${validation.contextVariables.missing}`, + ); + if (validation.contextVariables.details.missing.length > 0) { + lines.push( + ` Missing: ${validation.contextVariables.details.missing.join( + ', ', + )}`, + ); + } + lines.push(''); + }); + + // ChangeManager validation + lines.push('CHANGE MANAGER VALIDATION'); + lines.push('-'.repeat(80)); + lines.push( + `Task Variables: expected=${report.changeManager.taskVariables.expected}, emitted=${report.changeManager.taskVariables.emitted}, missing=${report.changeManager.taskVariables.missing}`, + ); + if (report.changeManager.taskVariables.details.missing.length > 0) { + lines.push( + ` Missing: ${report.changeManager.taskVariables.details.missing.join( + ', ', + )}`, + ); + } + lines.push( + `Task Transitions: expected=${report.changeManager.taskTransitions.expected}, emitted=${report.changeManager.taskTransitions.emitted}, missing=${report.changeManager.taskTransitions.missing}`, + ); + if (report.changeManager.taskTransitions.details.missing.length > 0) { + lines.push( + ` Missing: ${report.changeManager.taskTransitions.details.missing.join( + ', ', + )}`, + ); + } + lines.push(''); + + // System validation + lines.push('SYSTEM VALIDATION'); + lines.push('-'.repeat(80)); + lines.push( + `Context Variables: expected=${report.system.contextVariables.expected}, emitted=${report.system.contextVariables.emitted}, missing=${report.system.contextVariables.missing}`, + ); + if (report.system.contextVariables.details.missing.length > 0) { + lines.push( + ` Missing: ${report.system.contextVariables.details.missing.join(', ')}`, + ); + } + lines.push( + `Resource Variables: expected=${report.system.resourceVariables.expected}, emitted=${report.system.resourceVariables.emitted}, missing=${report.system.resourceVariables.missing}`, + ); + if (report.system.resourceVariables.details.missing.length > 0) { + lines.push( + ` Missing: ${report.system.resourceVariables.details.missing.join( + ', ', + )}`, + ); + } + lines.push(''); + + lines.push('='.repeat(80)); + + return lines.join('\n'); +}; + +export const getValidationSummary = ( + report: ValidationReport, +): { + expected: number; + emitted: number; + missing: number; + byCategory: Record< + string, + { expected: number; emitted: number; missing: number } + >; +} => { + const byCategory: Record< + string, + { expected: number; emitted: number; missing: number } + > = {}; + + // Goals + let goalsExpected = 0; + let goalsEmitted = 0; + let goalsMissing = 0; + + report.goals.forEach((validation) => { + goalsExpected += + validation.module.expected + + validation.variables.expected + + validation.transitions.expected + + validation.formulas.expected + + validation.contextVariables.expected; + goalsEmitted += + validation.module.emitted + + validation.variables.emitted + + validation.transitions.emitted + + validation.formulas.emitted + + validation.contextVariables.emitted; + goalsMissing += + validation.module.missing + + validation.variables.missing + + validation.transitions.missing + + validation.formulas.missing + + validation.contextVariables.missing; + }); + + byCategory.goals = { + expected: goalsExpected, + emitted: goalsEmitted, + missing: goalsMissing, + }; + + // ChangeManager + byCategory.changeManager = { + expected: + report.changeManager.taskVariables.expected + + report.changeManager.taskTransitions.expected, + emitted: + report.changeManager.taskVariables.emitted + + report.changeManager.taskTransitions.emitted, + missing: + report.changeManager.taskVariables.missing + + report.changeManager.taskTransitions.missing, + }; + + // System + byCategory.system = { + expected: + report.system.contextVariables.expected + + report.system.resourceVariables.expected, + emitted: + report.system.contextVariables.emitted + + report.system.resourceVariables.emitted, + missing: + report.system.contextVariables.missing + + report.system.resourceVariables.missing, + }; + + return { + expected: report.summary.totalExpected, + emitted: report.summary.totalEmitted, + missing: report.summary.totalMissing, + byCategory, + }; +}; diff --git a/packages/lib/src/engines/edgeV2/validator/types.ts b/packages/lib/src/engines/edgeV2/validator/types.ts new file mode 100644 index 00000000..017d1b42 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/validator/types.ts @@ -0,0 +1,125 @@ +export type VariableInfo = { + name: string; + type: 'int' | 'bool'; + bounds?: { lower: number; upper: number }; + initialValue?: number | boolean; +}; + +export type TransitionInfo = { + label: string; + guard: string; + update: string; + variablesReferenced: string[]; // Variables referenced in the guard +}; + +export type FormulaInfo = { + name: string; + expression: string; +}; + +export type ModuleInfo = { + name: string; + variables: VariableInfo[]; + transitions: TransitionInfo[]; + goalType?: + | 'choice' + | 'degradation' + | 'sequence' + | 'interleaved' + | 'alternative' + | 'basic'; + lineCount?: number; +}; + +export type ParsedPrismModel = { + goalModules: Map; + changeManagerModule?: ModuleInfo; + systemModule?: ModuleInfo; + formulas: FormulaInfo[]; + constants: Map; + /** Top-level `const int x;` nondeterministic constants (e.g. decision_G0). */ + nondetConstants: string[]; +}; + +export type ElementCount = { + expected: number; + emitted: number; + missing: number; +}; + +export type ElementDetails = { + expected: string[]; + emitted: string[]; + missing: string[]; +}; + +export type GoalValidation = { + module: ElementCount & { lineCount?: number }; + variables: ElementCount & { details: ElementDetails }; + transitions: ElementCount & { details: ElementDetails }; + formulas: ElementCount & { details: ElementDetails }; + contextVariables: ElementCount & { details: ElementDetails }; +}; + +export type ChangeManagerValidation = { + taskVariables: ElementCount & { details: ElementDetails }; + taskTransitions: ElementCount & { details: ElementDetails }; +}; + +export type SystemValidation = { + contextVariables: ElementCount & { details: ElementDetails }; + resourceVariables: ElementCount & { details: ElementDetails }; +}; + +export type GoalTypeCounts = { + choice: ElementCount; + degradation: ElementCount; + sequence: ElementCount; + interleaved: ElementCount; + alternative: ElementCount; + basic: ElementCount; +}; + +export type ValidationReport = { + goals: Map; + changeManager: ChangeManagerValidation; + system: SystemValidation; + goalTypes: GoalTypeCounts; + summary: { + totalExpected: number; + totalEmitted: number; + totalMissing: number; + byNodeType: { + goals: { + modules: { expected: number; emitted: number }; + }; + tasks: { + variables: { expected: number; emitted: number }; + transitions: { expected: number; emitted: number }; + }; + resources: { + variables: { expected: number; emitted: number }; + }; + }; + }; +}; + +export type ExpectedElements = { + goals: Map< + string, + { + variables: string[]; + transitions: string[]; + formulas: string[]; + contextVariables: string[]; + } + >; + changeManager: { + taskVariables: Map; // taskId -> [variable names] + taskTransitions: Map; // taskId -> [transition labels] + }; + system: { + contextVariables: string[]; + resourceVariables: string[]; + }; +}; diff --git a/packages/lib/src/engines/edgeV2/validator/validator.ts b/packages/lib/src/engines/edgeV2/validator/validator.ts new file mode 100644 index 00000000..daba6fb2 --- /dev/null +++ b/packages/lib/src/engines/edgeV2/validator/validator.ts @@ -0,0 +1,354 @@ +import { GoalTree } from '@goal-controller/goal-tree'; +import type { EdgeGoalTree } from '../mapper'; + +import { calculateExpectedElements } from './expectedElements'; +import { parsePrismModel } from './parser'; +import type { + ChangeManagerValidation, + ElementCount, + ElementDetails, + ExpectedElements, + GoalTypeCounts, + GoalValidation, + ParsedPrismModel, + SystemValidation, + ValidationReport, +} from './types'; + +type GoalTreeType = EdgeGoalTree; + +/** + * Multiset-style matching so duplicate transition labels (e.g. two `pursue_G1` commands) + * require the same multiplicity in the emitted model. + */ +const createElementCount = ( + expected: string[], + emitted: string[], +): ElementCount & { details: ElementDetails } => { + const emittedRemaining = [...emitted]; + const missing: string[] = []; + for (const item of expected) { + const idx = emittedRemaining.indexOf(item); + if (idx === -1) { + missing.push(item); + } else { + emittedRemaining.splice(idx, 1); + } + } + + return { + expected: expected.length, + emitted: emitted.length, + missing: missing.length, + details: { + expected, + emitted: Array.from(new Set(emitted)), + missing, + }, + }; +}; + +const validateGoal = ( + goalId: string, + expected: { + variables: string[]; + transitions: string[]; + formulas: string[]; + contextVariables: string[]; + }, + parsedModel: ParsedPrismModel, +): GoalValidation => { + const goalModule = parsedModel.goalModules.get(goalId); + const moduleVarNames = goalModule?.variables.map((v) => v.name) || []; + const fromNondet = expected.variables.filter((name) => + parsedModel.nondetConstants.includes(name), + ); + const emittedVariables = Array.from( + new Set([...moduleVarNames, ...fromNondet]), + ); + const emittedTransitions = goalModule?.transitions.map((t) => t.label) || []; + // Filter formulas that belong to this goal + // Formulas are named like: G1_achievable, G1_achieved, G1_achieved_maintain + // We need to match formulas that start with goalId + '_' to avoid matching + // G10, G11, etc. when looking for G1 + const emittedFormulas = parsedModel.formulas + .filter((f) => f.name === goalId || f.name.startsWith(`${goalId}_`)) + .map((f) => f.name); + + // Check if module exists + const moduleExists = goalModule !== undefined; + + // Validate variables + const variables = createElementCount(expected.variables, emittedVariables); + + // Validate transitions + const transitions = createElementCount( + expected.transitions, + emittedTransitions, + ); + + // Validate formulas + const formulas = createElementCount(expected.formulas, emittedFormulas); + + // Validate context variables: count only those that appear in the first pursue line + // The first pursue line is the one where the goal pursues itself: [pursue_${goalId}] ... + const pursueTransition = goalModule?.transitions.find( + (t) => t.label === `pursue_${goalId}`, + ); + + // Extract context variables from the first pursue transition's guard + // Filter out goal-specific variables (like G5_state, G5_chosen, etc.) + const systemContextVars = + parsedModel.systemModule?.variables.map((v) => v.name) || []; + const goalVariablePattern = new RegExp( + `^(${goalId}_(state|pursued|achieved|chosen|failed|achievable)|_decision_${goalId})$`, + ); + + const emittedContextVars = + pursueTransition?.variablesReferenced.filter( + (varName) => + systemContextVars.includes(varName) && + !goalVariablePattern.test(varName), + ) || []; + + const contextVariables = createElementCount( + expected.contextVariables, + emittedContextVars, + ); + + return { + module: { + expected: 1, + emitted: moduleExists ? 1 : 0, + missing: moduleExists ? 0 : 1, + lineCount: goalModule?.lineCount, + }, + variables, + transitions, + formulas, + contextVariables, + }; +}; + +const validateChangeManager = ( + expected: ExpectedElements['changeManager'], + parsedModel: ParsedPrismModel, +): ChangeManagerValidation => { + const changeManager = parsedModel.changeManagerModule; + const emittedVariables = changeManager?.variables.map((v) => v.name) || []; + const emittedTransitions = + changeManager?.transitions.map((t) => t.label) || []; + + // Collect all expected task variables + const allExpectedTaskVariables: string[] = []; + expected.taskVariables.forEach((vars) => { + allExpectedTaskVariables.push(...vars); + }); + + // Collect all expected task transitions + const allExpectedTaskTransitions: string[] = []; + expected.taskTransitions.forEach((transitions) => { + allExpectedTaskTransitions.push(...transitions); + }); + + return { + taskVariables: createElementCount( + allExpectedTaskVariables, + emittedVariables, + ), + taskTransitions: createElementCount( + allExpectedTaskTransitions, + emittedTransitions, + ), + }; +}; + +const validateSystem = ( + expected: ExpectedElements['system'], + parsedModel: ParsedPrismModel, +): SystemValidation => { + const system = parsedModel.systemModule; + const emittedVariables = system?.variables.map((v) => v.name) || []; + + // Separate context and resource variables from emitted + // Context variables are boolean, resources can be boolean or int + // We'll check by name matching since we know the resource IDs + const emittedContextVars: string[] = []; + const emittedResourceVars: string[] = []; + + emittedVariables.forEach((varName) => { + if (expected.resourceVariables.includes(varName)) { + emittedResourceVars.push(varName); + } else if (expected.contextVariables.includes(varName)) { + emittedContextVars.push(varName); + } + }); + + return { + contextVariables: createElementCount( + expected.contextVariables, + emittedContextVars, + ), + resourceVariables: createElementCount( + expected.resourceVariables, + emittedResourceVars, + ), + }; +}; + +export const validatePrismModel = ( + goalTree: GoalTreeType, + prismModel: string, +): ValidationReport => { + const parsedModel = parsePrismModel(prismModel); + const expected = calculateExpectedElements(goalTree); + + // Validate goals + const goalValidations = new Map(); + expected.goals.forEach((expectedElements, goalId) => { + goalValidations.set( + goalId, + validateGoal(goalId, expectedElements, parsedModel), + ); + }); + + // Validate ChangeManager + const changeManagerValidation = validateChangeManager( + expected.changeManager, + parsedModel, + ); + + // Validate System + const systemValidation = validateSystem(expected.system, parsedModel); + + // Calculate goal type counts + const goalTypes: GoalTypeCounts = { + choice: { expected: 0, emitted: 0, missing: 0 }, + degradation: { expected: 0, emitted: 0, missing: 0 }, + sequence: { expected: 0, emitted: 0, missing: 0 }, + interleaved: { expected: 0, emitted: 0, missing: 0 }, + alternative: { expected: 0, emitted: 0, missing: 0 }, + basic: { expected: 0, emitted: 0, missing: 0 }, + }; + + // Count expected goal types from GoalTree + const allGoalsMapResult = GoalTree.allGoalsMap(goalTree); + allGoalsMapResult.forEach((goal) => { + const goalType = + goal.properties.engine.executionDetail?.type === 'choice' + ? 'choice' + : goal.properties.engine.executionDetail?.type === 'degradation' + ? 'degradation' + : goal.properties.engine.executionDetail?.type === 'sequence' + ? 'sequence' + : goal.properties.engine.executionDetail?.type === 'interleaved' + ? 'interleaved' + : goal.properties.engine.executionDetail?.type === 'alternative' + ? 'alternative' + : 'basic'; + goalTypes[goalType].expected++; + }); + + // Count emitted goal types from parsed PRISM model + parsedModel.goalModules.forEach((module) => { + if (module.goalType) { + goalTypes[module.goalType].emitted++; + } + }); + + // Calculate missing for each type + Object.keys(goalTypes).forEach((type) => { + const typed = type as keyof GoalTypeCounts; + goalTypes[typed].missing = Math.max( + 0, + goalTypes[typed].expected - goalTypes[typed].emitted, + ); + }); + + // Calculate summary + let totalExpected = 0; + let totalEmitted = 0; + let totalMissing = 0; + + goalValidations.forEach((validation) => { + totalExpected += + validation.module.expected + + validation.variables.expected + + validation.transitions.expected + + validation.formulas.expected + + validation.contextVariables.expected; + totalEmitted += + validation.module.emitted + + validation.variables.emitted + + validation.transitions.emitted + + validation.formulas.emitted + + validation.contextVariables.emitted; + totalMissing += + validation.module.missing + + validation.variables.missing + + validation.transitions.missing + + validation.formulas.missing + + validation.contextVariables.missing; + }); + + totalExpected += + changeManagerValidation.taskVariables.expected + + changeManagerValidation.taskTransitions.expected; + totalEmitted += + changeManagerValidation.taskVariables.emitted + + changeManagerValidation.taskTransitions.emitted; + totalMissing += + changeManagerValidation.taskVariables.missing + + changeManagerValidation.taskTransitions.missing; + + totalExpected += + systemValidation.contextVariables.expected + + systemValidation.resourceVariables.expected; + totalEmitted += + systemValidation.contextVariables.emitted + + systemValidation.resourceVariables.emitted; + totalMissing += + systemValidation.contextVariables.missing + + systemValidation.resourceVariables.missing; + + // Calculate node-type aggregated summary + const allGoalsList = GoalTree.allByType(goalTree, 'goal'); + const goalsModulesExpected = allGoalsList.length; + const goalsModulesEmitted = parsedModel.goalModules.size; + + return { + goals: goalValidations, + changeManager: changeManagerValidation, + system: systemValidation, + goalTypes, + summary: { + totalExpected, + totalEmitted, + totalMissing, + byNodeType: { + goals: { + modules: { + expected: goalsModulesExpected, + emitted: goalsModulesEmitted, + }, + }, + tasks: { + variables: { + expected: changeManagerValidation.taskVariables.expected, + emitted: changeManagerValidation.taskVariables.emitted, + }, + transitions: { + expected: changeManagerValidation.taskTransitions.expected, + emitted: changeManagerValidation.taskTransitions.emitted, + }, + }, + resources: { + variables: { + expected: systemValidation.resourceVariables.expected, + emitted: systemValidation.resourceVariables.emitted, + }, + }, + }, + }, + }; +}; diff --git a/packages/lib/src/index.ts b/packages/lib/src/index.ts index 48d1c459..6a7615cc 100644 --- a/packages/lib/src/index.ts +++ b/packages/lib/src/index.ts @@ -49,6 +49,15 @@ export { } from './engines/sleec'; export type { SleecGoalProps, SleecTaskProps } from './engines/sleec'; +// Edge V2 (PRISM / EDGE snippets encoding) +export { + edgeEngineMapper as edgeV2EngineMapper, + type EdgeGoalNode as EdgeV2GoalNode, + type EdgeGoalTree as EdgeV2GoalTree, + type EdgeTask as EdgeV2Task, +} from './engines/edgeV2'; +export { generateValidatedPrismModel as generateValidatedEdgeV2PrismModel } from './engines/edgeV2/template'; + // Core transformation engines (remain in lib) export { generateValidatedPrismModel, sleecTemplateEngine }; @@ -58,6 +67,7 @@ export { validate }; // Logger export type { LoggerReport } from './engines/edge/logger/logger'; export { initLogger }; +export { initLogger as initEdgeV2Logger } from './engines/edgeV2/logger/logger'; // CLI entry point - if this file is executed directly, run the CLI script diff --git a/packages/ui/app/api/transform/route.ts b/packages/ui/app/api/transform/route.ts index e10dc315..6c38d23c 100644 --- a/packages/ui/app/api/transform/route.ts +++ b/packages/ui/app/api/transform/route.ts @@ -1,5 +1,7 @@ import { + generateValidatedEdgeV2PrismModel, generateValidatedPrismModel, + initEdgeV2Logger, initLogger, sleecTemplateEngine, type LoggerReport, @@ -25,12 +27,17 @@ export async function POST(request: NextRequest) { return ApiResponse.badRequest('Model JSON is required'); } - if (!engine || !['prism', 'sleec'].includes(engine)) { - return ApiResponse.badRequest('Valid engine (prism/sleec) is required'); + if (!engine || !['prism', 'sleec', 'edgeV2'].includes(engine)) { + return ApiResponse.badRequest( + 'Valid engine (prism/sleec/edgeV2) is required', + ); } - // Initialize logger (in-memory mode for API) - const logger = initLogger(fileName || 'model', false, true); + // Logger is engine-specific: Edge V2 template calls getLogger() from the edgeV2 module. + const logger = + engine === 'edgeV2' + ? initEdgeV2Logger(fileName || 'model', false, true) + : initLogger(fileName || 'model', false, true); // Generate output let output: string; @@ -62,6 +69,29 @@ export async function POST(request: NextRequest) { generateDecisionVars, achievabilitySpace, }); + } else if (engine === 'edgeV2') { + const parseResult = GoalModel.parseForEdgeV2(modelJson); + + if (!parseResult.success) { + if (process.env.NODE_ENV === 'development') { + console.error('[API] Parse error:', parseResult.error); + } + return ApiResponse.error( + parseResult.error, + GoalModel.getErrorStatus(parseResult.stage), + ); + } + + if (process.env.NODE_ENV === 'development') { + console.log('[API] Model parsed and tree converted successfully'); + console.log('[API] Generating Edge V2 PRISM model...'); + } + output = generateValidatedEdgeV2PrismModel({ + gm: parseResult.tree, + fileName: fileName || 'model', + clean, + variables, + }); } else { // Parse and validate model with SLEEC mapper const parseResult = GoalModel.parseForSleec(modelJson); diff --git a/packages/ui/app/api/variables/route.ts b/packages/ui/app/api/variables/route.ts index dbde27c6..c8fc202c 100644 --- a/packages/ui/app/api/variables/route.ts +++ b/packages/ui/app/api/variables/route.ts @@ -1,4 +1,4 @@ -import { GoalTree } from '@goal-controller/goal-tree'; +import { GoalTree, type GoalTreeType } from '@goal-controller/goal-tree'; import { NextRequest } from 'next/server'; import { ApiResponse } from '../../../lib/api'; import { GoalModel } from '../../../lib/models'; @@ -9,14 +9,18 @@ import { GoalModel } from '../../../lib/models'; */ export async function POST(request: NextRequest) { try { - const { modelJson } = await request.json(); + const { modelJson, engine = 'prism' } = await request.json(); if (!modelJson) { return ApiResponse.badRequest('Model JSON is required'); } - // Parse and validate model - const parseResult = GoalModel.parse(modelJson); + const parseResult = + engine === 'edgeV2' + ? GoalModel.parseForEdgeV2(modelJson) + : engine === 'sleec' + ? GoalModel.parseForSleec(modelJson) + : GoalModel.parseForEdge(modelJson); if (!parseResult.success) { return ApiResponse.error( @@ -25,7 +29,8 @@ export async function POST(request: NextRequest) { ); } - const { tree } = parseResult; + const { tree: rawTree } = parseResult; + const tree = rawTree as GoalTreeType; // Extract variables const contextVariables = GoalTree.contextVariables(tree); diff --git a/packages/ui/components/EngineSelector.tsx b/packages/ui/components/EngineSelector.tsx index da2ec452..c19f5d02 100644 --- a/packages/ui/components/EngineSelector.tsx +++ b/packages/ui/components/EngineSelector.tsx @@ -1,8 +1,10 @@ 'use client'; +import type { TransformEngine } from '../lib/transformEngine'; + interface EngineSelectorProps { - engine: 'prism' | 'sleec'; - onEngineChange: (engine: 'prism' | 'sleec') => void; + engine: TransformEngine; + onEngineChange: (engine: TransformEngine) => void; clean: boolean; onCleanChange: (clean: boolean) => void; generateDecisionVars: boolean; @@ -38,19 +40,31 @@ export default function EngineSelector({ value='prism' checked={engine === 'prism'} onChange={(e) => - onEngineChange(e.target.value as 'prism' | 'sleec') + onEngineChange(e.target.value as TransformEngine) } className='mr-2' /> PRISM +