goal-controller

FAQ

Monorepo Structure

This repository is organized as a pnpm monorepo with the following structure:

goal-controller/
├── packages/
│   ├── lib/          # Core transformation engines (PRISM/SLEEC) + CLI tools
│   │   ├── src/
│   │   │   └── engines/               # Transformation engines
│   │   │       ├── edge/              # PRISM/Edge model generator
│   │   │       │   ├── mapper.ts      # iStar to Edge property mapper
│   │   │       │   ├── types.ts       # Edge-specific types
│   │   │       │   ├── template/      # PRISM model generation templates
│   │   │       │   ├── validator/     # PRISM model validation
│   │   │       │   ├── logger/        # Generation logging & metrics
│   │   │       │   └── mdp/           # MDP common utilities
│   │   │       └── sleec/             # SLEEC specification generator
│   │   │           ├── mapper.ts      # iStar to SLEEC property mapper
│   │   │           ├── types.ts       # SLEEC-specific types
│   │   │           └── template/      # SLEEC specification templates
│   │   └── out/      # Compiled JavaScript
│   ├── dialect/      # What a dialect is, as data (definitions' schema)
│   ├── goal-language/ # The one grammar every dialect is written in: parser,
│   │                  # validator, and the goal-text reader derived from a dialect
│   ├── goal-tree/    # Goal model data structures (reads goal texts in the engine's dialect)
│   └── ui/           # Next.js web application for transformations
│       └── lib/project/ # Projects: the manifest, where projects are kept, Recent
├── examples/         # Example goal models, grouped per engine
│   ├── edge/         # Edge engine notation (choice: `[+]`), incl. experiments/
│   ├── edgeV2/       # EdgeV2 notation (choice: `[G1?G2]`, any order: `[G1+G2]`)
│   └── sleec/        # SLEEC engine models
├── experiments/      # Experiment infrastructure (Docker, scripts, metrics)
└── output/          # Generated PRISM/SLEEC models

Dependencies go one way: dialect ← goal-language ← goal-tree ← lib ← ui. goal-tree reads goal texts with the reader goal-language derives from the engine's dialect, and never imports lib.

The workbench's unit of work is a project: one or more models with their project resources and outputs, described by a manifest. A single model file is an implicit one-model project whose manifest lives in the file itself. See packages/ui/lib/project/README.md.

Transformation Engines

This repository includes two transformation engines for converting goal models:

1. Edge/PRISM Engine (packages/lib/src/engines/edge/) - Generates PRISM models for probabilistic verification
   • mapper.ts - Maps iStar model properties to Edge-specific properties
   • template/ - Contains PRISM model generation templates
2. SLEEC Engine (packages/lib/src/engines/sleec/) - Generates SLEEC specifications for runtime monitoring
   • mapper.ts - Maps iStar model properties to SLEEC-specific properties
   • template/ - Contains SLEEC specification templates
   • See Transformation Example (SLEEC) section below for architecture and implementation details

---

Engine Development Tutorial

This tutorial explains how to create new transformation engines for converting goal models to different target formats.

For the step-by-step guide on this branch (definition, mapper, template and workbench wiring), see packages/dialect/docs/adding-an-engine.md.

Architecture Overview

The transformation system follows a two-phase architecture:

flowchart LR
    subgraph input [Input]
        iStar[iStar Model JSON]
    end
    subgraph goalTree [goal-tree Package]
        Parser[Model Parser]
        Mapper[Engine Mapper]
        Tree[GoalTree Instance]
    end
    subgraph engine [Engine Package]
        Template[Template Engine]
    end
    subgraph output [Output]
        Target[Target Format]
    end
    iStar --> Parser --> Mapper --> Tree --> Template --> Target

Loading

Phase 1 - Creation (Mapper): Maps an element's properties, as the goal language reads them against the engine's dialect, into typed, engine-specific properties during tree construction.

Phase 2 - Transformation (Template): Generates output by querying the typed tree and combining generated sections.

flowchart TB
    subgraph phase1 [Phase 1: Creation - Mapper]
        RawProps[iStar Properties]
        Dialect[Read Against the Dialect]
        MapFn[Map Functions]
        TypedProps[Typed Engine Properties]
        RawProps --> Dialect --> MapFn --> TypedProps
    end
    subgraph phase2 [Phase 2: Transformation - Template]
        Query[Query GoalTree]
        Generate[Generate Output Strings]
        Combine[Combine Sections]
        Query --> Generate --> Combine
    end
    TypedProps --> Query

Loading

Creating a New Engine

Follow these steps to create a new transformation engine. We'll use SLEEC as a reference (simpler) and Edge for advanced patterns.

flowchart LR
    Keys[Define the Dialect's Properties] --> Factory[createEngineMapper]
    Factory --> MapFns[Provide Map Functions]
    MapFns --> Mapper[Engine Mapper]
    Mapper --> GoalTree[Use with GoalTree.fromModel]

Loading

Step 1: Define Engine-Specific Types

The mapper transforms the values the goal language reads from iStar's properties into rich typed structures. Define types that represent your engine's domain model. See packages/lib/src/engines/sleec/types.ts and packages/lib/src/engines/edge/types.ts:

// types.ts - Complex types transformed FROM raw iStar strings

// Nested structure parsed from "varName:3,otherVar:5" string
export type Decision = {
  hasDecision: boolean;
  decisionVars: Array<{ variable: string; space: number }>;
};

// Structured condition parsed from assertion strings
export type ExecCondition = {
  maintain?: { sentence: string; variables: string[] };
  assertion?: { sentence: string; variables: string[] };
};

export type MyEngineGoalProps = {
  priority: 'low' | 'normal' | 'high';  // Enum from string
  deadline: number | null;               // Number from string "300"
  decision: Decision;                    // Parsed from "var:3,other:5"
  execCondition?: ExecCondition;         // Parsed from assertion syntax
  dependsOn: MyEngineGoalNode[];         // Resolved goal nodes: Extract<NodeOf<typeof myEngineMapper>, { type: 'goal' }>
};

export type MyEngineTaskProps = {
  maxRetries: number;                    // Parsed from string "3"
  isOptional: boolean;                   // Parsed from string "true"
  tags: string[];                        // Parsed from "tag1,tag2,tag3"
  execCondition?: ExecCondition;
};

Step 2: Define the Properties in the Dialect

The engine's dialect (its definition, packages/dialect/docs/adding-an-engine.md) declares each property and its value type. Those are the keys the mapper is given, per element kind:

// definition.ts
properties: {
  goal: [
    property.enum('priority', ['low', 'normal', 'high'], { help }),   // "high" → 'high'
    property.int('deadline', { min: 0, help }),                      // "300"  → 300
    property.pairList('variables', 'int', { help }),                 // "var:3,other:5" → [{ name, value }]
    property.assertion('assertion', { resolves: ['variable'], help }), // "x > 0 & y < 10" → its tree
    property.refList('dependsOn', 'goal', { help }),                 // "G2,G3" → ['G2', 'G3']
  ],
  task: [
    property.int('maxRetries', { min: 0, help }),                    // "3"    → 3
    property.bool('optional', { help }),                             // "true" → true
    property.text('tags', { help }),                                 // as written
  ],
  resource: [],
  quality: [],
},

Step 3: Create the Engine Mapper

Each mapper is given props, the values as the goal language reads their types (a value written with an error is unset: the dialect's checks report it), and raw, the strings as written:

import { createEngineMapper, useIstarDefaultNaming } from '@goal-controller/goal-tree';

export const myEngineMapper = createEngineMapper({
  dialect: myEngine,  // its definition: goal texts and properties are read in it (you write no parser)
  naming: useIstarDefaultNaming(),  // iStar's goals, tasks and resources
  elements: (entry) => [
    entry({
      kinds: ['istar.Goal', 'istar.Quality'],
      mapProps: (input) => {
        // a Quality has none of the goal's keys: narrow on `kind` first
        const props = input.kind === 'istar.Goal' ? input.props : {};
        return {
          priority: props.priority ?? 'normal',      // 'low' | 'normal' | 'high'
          deadline: props.deadline ?? null,          // number
          decision: {
            hasDecision: (props.variables ?? []).length > 0,
            decisionVars: (props.variables ?? []).map(({ name, value }) => ({
              variable: name,
              space: Number(value),
            })),
          },
          dependsOn: [],  // Resolved later in afterCreation
        };
      },
    }),
    entry({
      kind: 'istar.Task',
      mapProps: ({ props, raw }) => ({
        maxRetries: props.maxRetries ?? 0,           // number
        isOptional: props.optional === true,         // boolean
        tags: (raw.tags ?? '').split(',').map((t) => t.trim()).filter(Boolean),
      }),
    }),
  ],
  ignore: ['istar.Resource'],  // No resources
});

Advanced: Cross-node references with afterCreation

For engines that need to resolve references between nodes (like Edge's dependsOn), an entry's afterCreation runs once every node is built; see packages/lib/src/engines/edge/mapper.ts:

entry({
  kinds: ['istar.Goal', 'istar.Quality'],
  mapProps: …,
  afterCreation: ({ node, input, allNodes }) => {
    const depIds = input.kind === 'istar.Goal' ? (input.props.dependsOn ?? []) : [];
    const resolvedDeps = depIds.map((id) => allNodes.get(id));
    return { ...node.properties.engine, dependsOn: resolvedDeps };
  },
}),

Step 4: Create the Template Engine

Create functions that query the tree and generate output sections.

Transformation Example (SLEEC)

This section demonstrates how to transform from a GoalTree using the SLEEC engine as an example.

flowchart TB
    Tree[GoalTree] --> Tasks[query.allByType task]
    Tree --> Goals[query.allByType goal]
    Tasks --> Defs[generateDefinitions]
    Tasks --> Rules[generateTaskRules]
    Goals --> Purposes[generatePurposes]
    Defs --> Output[SLEEC Specification]
    Rules --> Output
    Purposes --> Output

Loading

Loading and Creating the Tree

import { GoalTree, Model } from '@goal-controller/goal-tree';
import { sleecEngineMapper } from '@goal-controller/lib';

// Load from file
const model = Model.load('examples/sleec/goalModel-sleec.txt');
const tree = GoalTree.fromModel(model, sleecEngineMapper);

// Or from JSON string
const tree = GoalTree.fromJSON(jsonString, sleecEngineMapper);

Querying the Tree

Access typed engine properties through the query interface:

// Get all tasks with typed engine properties
const tasks = tree.query.allByType('task');

tasks.forEach(task => {
  console.log(task.name);                              // "Track Vital Signs"
  console.log(task.properties.engine.PreCond);         // "{dataCollected}"
  console.log(task.properties.engine.TriggeringEvent); // "PatientAsleep"
  console.log(task.properties.engine.TemporalConstraint); // "300 seconds"
});

// Get all goals
const goals = tree.query.allByType('goal');

// Get leaf goals (goals with tasks, no child goals)
const leafGoals = tree.query.leafGoals();

generateDefinitions - Extract Events and Measures

This function extracts triggering events from task properties and generates SLEEC event definitions:

import type { Task } from '@goal-controller/goal-tree';
import type { SleecTaskProps } from './types';

type SleecTask = Task<SleecTaskProps>;

const generateDefinitions = (tasks: SleecTask[]): string => {
  // Extract unique triggering events from typed task properties
  const events = tasks
    .map(task => task.properties.engine?.TriggeringEvent)
    .filter((event): event is string => !!event);
  
  const uniqueEvents = [...new Set(events)].sort();
  const eventLines = uniqueEvents
    .map(event => `    event ${event}`)
    .join('\n');

  // Extract boolean measures from PreCond/PostCond
  const measureRegex = /\{(\w+)\}/g;
  const measures = new Set<string>();
  
  tasks.forEach(task => {
    const conditions = [
      task.properties.engine?.PreCond,
      task.properties.engine?.PostCond,
    ].filter(Boolean);
    
    conditions.forEach(cond => {
      let match;
      while ((match = measureRegex.exec(cond!)) !== null) {
        measures.add(match[1]);
      }
    });
  });

  const measureLines = [...measures].sort()
    .map(m => `    measure ${m}: boolean`)
    .join('\n');

  return `def_start
${eventLines}

${measureLines}
def_end`;
};

// Example output:
// def_start
//     event DataCollected
//     event PatientAsleep
//     event MeetingUser
//
//     measure dataCollected: boolean
//     measure dataProcessed: boolean
// def_end

generateTaskRules - Generate Behavioral Rules

This function generates SLEEC rules from task properties:

const generateTaskRules = (tasks: SleecTask[]): string => {
  const rules = tasks.map(task => {
    const { PreCond, TriggeringEvent, PostCond, TemporalConstraint } = 
      task.properties.engine;
    
    // Create fluent name from task name (remove spaces)
    const fluentName = task.name?.replaceAll(' ', '') || task.id;
    const ruleId = task.id.replace('.', '_');
    
    return `
    Rule${ruleId}_1 when ${TriggeringEvent} and ${PreCond} then Start${fluentName}
    Rule${ruleId}_2 when Start${fluentName} then Pursuing${fluentName} within ${TemporalConstraint}
    Rule${ruleId}_3 when Pursuing${fluentName} and ${PostCond} then Achieved${fluentName}`;
  }).join('\n');

  return `rule_start${rules}
rule_end`;
};

// Example output:
// rule_start
//     RuleT5_1 when PatientAsleep and {patientDiscomfort} then StartTrackVitalSigns
//     RuleT5_2 when StartTrackVitalSigns then PursuingTrackVitalSigns within 300 seconds
//     RuleT5_3 when PursuingTrackVitalSigns and {dataCollected} then AchievedTrackVitalSigns
// rule_end

generatePurposes - Generate Goal Purposes

This function generates purpose statements from goal properties:

import { GoalTree, type NodeOf } from '@goal-controller/goal-tree';
import type { sleecEngineMapper } from './mapper';

// the tree's nodes, typed by kind from the mapper's entries
type SleecGoalTree = NodeOf<typeof sleecEngineMapper>[];

const generatePurposes = (tree: SleecGoalTree): string => {
  const goals = GoalTree.allByType(tree, 'goal');
  
  const purposes = goals
    .filter(goal => 
      ['Achieve', 'Maintain'].includes(goal.properties.engine?.Type || '')
    )
    .map((goal, index) => {
      const { Condition, Event, ContextEvent, Type } = goal.properties.engine || {};
      
      if (!Condition || !Event || !ContextEvent) {
        throw new Error(`Goal ${goal.name} missing required properties`);
      }
      
      const label = `P${index + 1}`;
      
      if (Type === 'Achieve') {
        return `${label} when ${ContextEvent} and ${Condition} then ${Event}`;
      }
      // Maintain type
      return `${label} exists ${Event} and ${Condition} while ${ContextEvent}`;
    });

  return `purpose_start
  ${purposes.join('\n  ')}
purpose_end`;
};

// Example output:
// purpose_start
//   P1 when SystemActive and {emergencyDetected} then AlertMedicalStaff
// purpose_end

Complete Template Engine

Combine all generators into the final template engine:

import { GoalTree } from '@goal-controller/goal-tree';
import type { SleecGoalTree } from './mapper';

export const sleecTemplateEngine = (tree: SleecGoalTree): string => {
  const tasks = GoalTree.allByType(tree, 'task');
  
  const definitions = generateDefinitions(tasks);
  const rules = generateTaskRules(tasks);
  const purposes = generatePurposes(tree);
  
  return `${definitions}

${rules}

${purposes}`;
};

// Usage:
const model = Model.load('examples/sleec/goalModel-sleec.txt');
const tree = GoalTree.fromModel(model, sleecEngineMapper);
const sleecSpec = sleecTemplateEngine(tree);

console.log(sleecSpec);

Sample Complete Output

def_start
    event DataCollected
    event MeetingUser
    event PatientAsleep
    event PatientOutdoors

    measure dataCollected: boolean
    measure dataProcessed: boolean
    measure patientDiscomfort: scale(low, moderate, high)
def_end

rule_start
    RuleT5_1 when PatientAsleep and {patientDiscomfort} then StartTrackVitalSigns
    RuleT5_2 when StartTrackVitalSigns then PursuingTrackVitalSigns within 300 seconds
    RuleT5_3 when PursuingTrackVitalSigns and {dataCollected} then AchievedTrackVitalSigns

    RuleT7_1 when DataCollected and {dataSaved} then StartProcessData
    RuleT7_2 when StartProcessData then PursuingProcessData within 60 seconds
    RuleT7_3 when PursuingProcessData and {dataProcessed} then AchievedProcessData
rule_end

purpose_start
  P1 when SystemActive and {emergencyDetected} then AlertMedicalStaff
purpose_end

---

Quick Start

1. Install dependencies:

   pnpm install

2. Build the library (the dialect definitions, the goal language, goal-tree and lib):

   pnpm run build:lib

3. Run transformations:

   make run FILE=examples/edge/simpleChoice.txt

4. Launch the web UI:

   pnpm run dev:ui
   # Open http://localhost:3000

How to execute this repo?

Installation

Alternative 1: VScode integrated environment (Recommended)

1. Open the repo on a new VSCode window
2. Make sure you have docker installed
3. Install the devcontainer extension, more info about it here
4. A dialog will ask you to reopen the repo in a container, accept it and wait for the build to finish
5. Once inside the dev container environment, you can use:
   • make exec to run the translator with the default example
   • make cli to launch the interactive CLI
   • make cli-clean to launch the interactive CLI with the --clean flag (skips preserving old System module transitions)

Alternative 2: Run manually from any terminal

1. Install pnpm:

   npm install -g pnpm

2. Install Node.js 22.6.0:

   # Using nvm
   curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.7/install.sh | bash
   nvm install 22.6.0
   nvm use 22.6.0

3. Install dependencies:

   pnpm install

Execution

Interactive CLI

You can use the interactive CLI to select and run models:

• make cli - Launches the interactive CLI
• make cli-clean - Launches the interactive CLI with the --clean flag (generates clean System modules without preserving old transitions)

Generating the PRISM model

1. Build the library package first:

   pnpm run build:lib  # Build the library (goal texts are read with packages/goal-language)

2. Generate the model using one of these methods:

   Using Makefile (Recommended):

   make run FILE=examples/edge/simpleChoice.txt
   # or
   make generate FILE=examples/edge/simpleChoice.txt

   Using Node directly:

   node packages/lib/out/index.js examples/edge/simpleChoice.txt

   Where $GOAL_MODEL_FILE is the downloaded goal model from pistar.

   Note: The --clean flag is not currently supported in the CLI entry point. Use the interactive CLI (make cli) for clean mode.

3. If successful you should see the string The file was saved! in the terminal.

4. Add the goal model to the goalmngt folder

   • cp $GOAL_MODEL_FILE goalmgmt/edgeModel.txt
   • E.g: cp examples/edgeModel.txt goalmgmt/edgeModel.txt

System Module Transition Preservation

By default, when generating a PRISM model, the System module will automatically preserve transitions from a previously generated PRISM file (if it exists in the output/ directory). This allows you to maintain custom transitions in the System module across model regenerations.

How it works:

• When generating a PRISM model, the system looks for an existing PRISM file with the same base name in the output/ directory
• If found, it extracts all transition lines (including any preceding comments) from the System module
• These transitions are then included in the newly generated System module alongside the automatically generated context and resource variables

Example: If you have a file output/myModel.prism with custom System module transitions:

module System
  myVar: bool init false;

  // Custom transition
  [achieved_T1] true -> (myVar'=true);
endmodule

When you regenerate the model, these transitions will be preserved in the new System module.

Using the --clean flag: To skip this behavior and generate a completely fresh System module without preserving old transitions, use the --clean or -c flag:

Make targets:

make cli-clean  # Interactive CLI with --clean flag

Note: The direct command-line --clean flag is not available. Use the interactive CLI for clean mode.

This is useful when you want to start with a clean System module or when the old transitions are no longer relevant.

This process outputs a file in output/<file>.prism this is the MDP input for the PRISM model checker. To generate the controller and states files please refer to the EDGE specification

Running Experiments

This section describes how to run experiments to collect metrics and analyze the performance of goal model translations.

Prerequisites

• Docker and Docker Compose installed
• The experiment Docker container (built automatically on first run)

Step-by-Step Guide

1. Add the Goal Model

Each experiment is a project: a folder examples/edge/experiments/<name>/ holding the model, its properties and a project.json (copy one from another experiment and change the names). Add your goal model file (.txt format) to it:

mkdir -p examples/edge/experiments/your-goal-model
cp your-goal-model.txt examples/edge/experiments/your-goal-model/your-goal-model.txt
cp examples/edge/experiments/1-minimal/project.json examples/edge/experiments/your-goal-model/
# then replace 1-minimal with your-goal-model in the copied project.json

The goal model should be in the PiStar format, as exported from the PiStar tool.

2. Add PCTL Properties

Create a properties file (.props format) with PCTL formulas to verify against your model. Place it in the project's props/ folder:

mkdir -p examples/edge/experiments/your-goal-model/props

# The filename should match your goal model name (e.g., if your model is "myModel.txt",
# create "myModel.props")
cp your-properties.props examples/edge/experiments/your-goal-model/props/your-goal-model.props

Example properties file format:

// Example properties for goal model verification
P=? [F "goal_achieved"]
P>=0.9 [G "system_safe"]

3. Launch the Experiment Container

Start the Docker container with all necessary dependencies:

make experiment

This command will:

• Build the experiment Docker image (if not already built)
• Start the container in detached mode
• Open an interactive bash session inside the container

The container includes:

• Node.js 22.6.0
• Storm model checker
• Python 3 with required packages
• All project files mounted at /workspace

4. Run the Experiment

Inside the Docker container, run the experiment pipeline:

make run-experiment

This command executes the following steps:

1. Generate PRISM models: Converts all goal models in examples/edge/experiments/ to PRISM format
2. Check properties: Validates all properties using Storm model checker
3. Extract metrics: Collects performance and model statistics

The results are saved to:

• PRISM models: output/*.prism
• Property check results: examples/edge/experiments/<name>/reference/*.result.storm
• Metrics: metrics.csv

5. Collect the Data

Exit the Docker container (type exit or press Ctrl+D) and collect the results:

Metrics CSV file: The metrics.csv file contains comprehensive metrics for each model, including:

• Translation time and memory usage
• Model structure (goals, tasks, resources, nodes, variables)
• PRISM model characteristics (states, transitions, lines)
• Model checking performance (parsing time, construction time, checking time)
• Memory and CPU usage

View the metrics:

cat metrics.csv
# or
head -n 20 metrics.csv

6. Plot the Results

Use the provided Python script to visualize the collected metrics:

Display plots interactively:

python3 experiments/plot_metrics.py

Save plots as PNG files:

python3 experiments/plot_metrics.py --save

Save to a custom directory:

python3 experiments/plot_metrics.py --save --output-dir result_plots

View statistics:

# Display min/max statistics for all metrics
python3 experiments/plot_metrics.py --stats

# Display relationship statistics for total_nodes
python3 experiments/plot_metrics.py --relationships

Customize the plots: You can modify experiments/plot_metrics.py to:

• Add new metrics to visualize
• Change plot types (scatter, line, bar, etc.)
• Adjust plot styling and labels
• Add regression analysis or trend lines

Experiment Workflow Summary

# 1. Add your files
mkdir -p examples/edge/experiments/my-model/props
cp my-model.txt examples/edge/experiments/my-model/
cp my-properties.props examples/edge/experiments/my-model/props/my-model.props
# plus a project.json, as in step 1

# 2. Launch container
make experiment

# 3. Inside container: run experiment
make run-experiment

# 4. Exit container
exit

# 5. View results
cat metrics.csv

# 6. Plot results
python3 experiments/plot_metrics.py --save

Troubleshooting

Container won't start:

• Ensure Docker is running: docker ps
• Check if container already exists: docker ps -a | grep experiment-container
• Remove old container: docker rm experiment-container

Experiment fails:

• Check that goal model files are valid PiStar format
• Verify properties files are in correct PCTL syntax
• Check container logs: docker logs experiment-container

Missing dependencies:

• The container should have all dependencies pre-installed
• If issues occur, rebuild: docker-compose -f experiments/docker-compose.storm.yml build experiment

Additional Resources

• PRISM Model Checker Documentation
• Storm Model Checker Documentation
• PCTL Property Specification