[minor] Sterling improvements, Linux 64-bit Gluose, ABAC fix, test refactoring

.github/workflows/continuousIntegration.yml

@@ -1,29 +1,112 @@
 name: Continuous Integration
 
 on:
-  pull_request: ~ 
+  pull_request: ~
   push:
     branches:
     - main
     - dev
 
-# Docker images for various Racket versions available on DockerHub 
-# as racket/racket:<version>
-# (https://github.com/racket/docker)
-# We use features that require at least 8.4; try to use latest.
-
 jobs:
-  forge-tests:
+  check-test-coverage:
+    runs-on: ubuntu-latest
+    name: check-test-coverage
+    steps:
+    - name: Checkout repo
+      uses: actions/checkout@v4
+
+    - name: Verify all test subdirs are in CI matrix
+      run: |
+        # Extract all tests/* paths mentioned in the workflow file itself.
+        # This avoids maintaining a separate list — the matrix IS the source of truth.
+        workflow=".github/workflows/continuousIntegration.yml"
+        covered=$(grep -oE 'tests/[a-zA-Z0-9_-]+(/[a-zA-Z0-9_-]+)?' "$workflow" \
+                  | sort -u)
+
+        # Check tests/forge/ subdirectories
+        actual=$(cd forge && find tests/forge -mindepth 1 -maxdepth 1 -type d | sort)
+        missing=$(comm -23 <(echo "$actual") <(echo "$covered"))
+        if [ -n "$missing" ]; then
+          echo "ERROR: tests/forge/ subdirectories not covered by CI:"
+          echo "$missing"
+          echo ""
+          echo "Add them to a test-dir entry in $workflow"
+          exit 1
+        fi
+
+        # Check top-level test directories too
+        actual_top=$(cd forge && find tests -mindepth 1 -maxdepth 1 -type d | sort)
+        missing_top=$(comm -23 <(echo "$actual_top") <(echo "$covered"))
+        if [ -n "$missing_top" ]; then
+          echo "ERROR: top-level test directories not covered by CI:"
+          echo "$missing_top"
+          echo ""
+          echo "Add them to a test-dir entry in $workflow"
+          exit 1
+        fi
+
+        echo "All test directories are covered by CI."
+
+  test-forge:
+    needs: check-test-coverage
     runs-on: ubuntu-latest
-    container: docker://karimmouline/forge-dev-img:latest
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - name: forge-1
+            test-dir: tests/forge/other
+          - name: forge-2
+            test-dir: tests/forge/bounds tests/forge/domains tests/forge/eval-model tests/forge/examples tests/forge/expressions tests/forge/formulas tests/forge/fuzz tests/forge/ints tests/forge/library tests/forge/relations tests/forge/sigs tests/forge/target
+          - name: forge-core
+            test-dir: tests/forge-core tests/forge-functional
+          - name: smt
+            test-dir: tests/smt
+          - name: other
+            test-dir: tests/error tests/froglet tests/srclocs tests/temporal
+    name: test-${{ matrix.name }}
     steps:
     - name: Checkout repo
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
+
+    - name: Setup Racket
+      uses: Bogdanp/setup-racket@v1.14
+      with:
+        version: '8.15'
+
+    - name: Setup Java
+      uses: actions/setup-java@v4
+      with:
+        distribution: 'temurin'
+        java-version: '17'
+
+    - name: Install system dependencies
+      run: |
+        sudo apt-get update -qq
+        sudo apt-get install -y -qq libcairo2-dev libpango1.0-dev libgdk-pixbuf-2.0-dev
+
+    - name: Install cvc5
+      if: matrix.name == 'smt'
+      run: |
+        wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip
+        unzip -q cvc5-Linux-x86_64-static.zip
+        echo "$PWD/cvc5-Linux-x86_64-static/bin" >> $GITHUB_PATH
+
+    - name: Cache Racket packages
+      uses: actions/cache@v4
+      with:
+        path: ~/.local/share/racket
+        key: racket-pkgs-${{ hashFiles('forge/info.rkt') }}
+        restore-keys: racket-pkgs-
+
     - name: Install Forge
       run: |
-        raco pkg install --auto --no-docs ./forge
+        raco pkg update --auto --no-docs --batch ./forge 2>/dev/null || raco pkg install --auto --no-docs ./forge
+
     - name: Run tests
       run: |
         cd forge/
         chmod +x run-tests.sh
-        ./run-tests.sh tests/
+        for dir in ${{ matrix.test-dir }}; do
+          ./run-tests.sh "$dir"
+        done

forge/domains/abac/runner.rkt

@@ -198,10 +198,18 @@
      (list (= r (atom 'True)))]
     [(equal? (relation-name r) "Request")
      (list (= r (atom 'Request)))]
+    ; Boolean fields (target sig is True)
+    [(equal? (relation-name r) "training")
+     (list (in r (-> (+ atoms) (atom 'True))))]
+    [(equal? (relation-name r) "audit")
+     (list (in r (-> (+ atoms) (atom 'True))))]
+    ; owner maps File -> Subject; Subject's upper bound is the universe atoms
+    [(equal? (relation-name r) "owner")
+     (list (in r (-> (+ atoms) (+ atoms))))]
     ; Everything else:
     [(equal? 1 (relation-arity r))
      (list (in r (+ atoms)))]
-    [(equal? 2 (relation-arity r))  
+    [(equal? 2 (relation-arity r))
      (list (in r (-> (+ atoms) (+ (atom 'True) (+ atoms)))))]
     [else
      (raise-user-error (format "Error: relation ~a had invalid arity" r))]))

forge/domains/crypto/examples/README.md

@@ -0,0 +1 @@
+CI regression tests derived from these examples live in forge/tests/forge/domains/crypto/.

forge/e2e/fixtures/projection-model.frg

@@ -0,0 +1,11 @@
+#lang forge
+
+-- Model with multiple sig types suitable for projection testing in Sterling
+sig Epoch {}
+sig Process {
+  action: set Epoch -> Process
+}
+
+projectionRun: run {
+  some action
+} for exactly 2 Process, exactly 3 Epoch

forge/e2e/fixtures/temporal-model.frg

@@ -0,0 +1,13 @@
+#lang forge/temporal
+
+-- Minimal temporal model for e2e testing of Sterling temporal controls
+sig Process {}
+var sig Active extends Process {}
+
+pred init { some Active }
+pred step { Active' != Active }
+
+temporalRun: run {
+  init
+  always step
+} for exactly 3 Process

forge/e2e/tests/sterling-temporal-projection.spec.ts

@@ -0,0 +1,161 @@
+import { test, expect, Page } from '@playwright/test';
+import { startForge, ForgeInstance, selectAndRunCommand } from '../helpers/forge-runner';
+import { TIMEOUT_GRAPH_LAYOUT } from '../helpers/constants';
+
+// Sterling sidebar buttons and drawer titles share the same DOM text (e.g., both
+// contain "Time"), but the sidebar button appears first in DOM order. The drawer
+// title is visually uppercased via CSS text-transform but the underlying text is
+// the same. Using .first() reliably targets the sidebar button.
+async function openSidebarDrawer(page: Page, label: string) {
+  await page.getByText(label, { exact: true }).first().click();
+  await page.waitForTimeout(500);
+}
+
+test.describe('Sterling Temporal Controls', () => {
+  let forge: ForgeInstance;
+
+  test.afterEach(async () => {
+    if (forge) {
+      forge.cleanup();
+    }
+  });
+
+  test('temporal controls are accessible outside the layout drawer', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/temporal-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'temporalRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    // "Time" and "Layout" should both be visible as separate sidebar entries
+    await expect(page.getByText('Time', { exact: true }).first()).toBeVisible({ timeout: 5000 });
+    await expect(page.getByText('Layout', { exact: true }).first()).toBeVisible({ timeout: 5000 });
+
+    // Negative test: open the Layout drawer and verify temporal controls are NOT there
+    await openSidebarDrawer(page, 'Layout');
+    await expect(page.locator('#temporal-policy-select')).not.toBeVisible();
+
+    // Now open the Time drawer and verify temporal controls ARE there
+    await openSidebarDrawer(page, 'Time');
+    await expect(page.locator('#temporal-policy-select')).toBeVisible({ timeout: 5000 });
+  });
+
+  test('time stepper is visible for temporal instances', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/temporal-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'temporalRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    await openSidebarDrawer(page, 'Time');
+
+    // The stepper shows a "State N/M" label
+    await expect(page.getByText(/^State \d+\/\d+$/)).toBeVisible({ timeout: 5000 });
+
+    // Navigation buttons should be present
+    await expect(page.getByRole('button', { name: 'First State' }).first()).toBeVisible();
+    await expect(page.getByRole('button', { name: 'Previous State' }).first()).toBeVisible();
+  });
+
+  test('time stepping advances the state index', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/temporal-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'temporalRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    await openSidebarDrawer(page, 'Time');
+
+    // Should start at State 1/N
+    await expect(page.getByText(/^State 1\/\d+$/)).toBeVisible({ timeout: 5000 });
+
+    // The forward button has a duplicated aria-label ("First State") due to a
+    // Sterling bug. It's the second button with that label in the stepper group.
+    const forwardButton = page.getByRole('button', { name: 'First State' }).nth(1);
+    await forwardButton.click();
+    await page.waitForTimeout(500);
+
+    // Should now show State 2/N
+    await expect(page.getByText(/^State 2\/\d+$/)).toBeVisible({ timeout: 5000 });
+  });
+
+  test('compare states mode is available', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/temporal-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'temporalRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    await openSidebarDrawer(page, 'Time');
+
+    const compareButton = page.getByRole('button', { name: 'Compare States' });
+    await expect(compareButton).toBeVisible({ timeout: 5000 });
+
+    await compareButton.click();
+    await page.waitForTimeout(500);
+
+    // Button text changes and comparison instructions appear
+    await expect(page.getByText('Compare Mode')).toBeVisible({ timeout: 3000 });
+    await expect(page.getByText('Click states to compare side-by-side')).toBeVisible({ timeout: 3000 });
+  });
+
+  test('temporal policy can be changed', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/temporal-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'temporalRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    await openSidebarDrawer(page, 'Time');
+
+    const policySelect = page.locator('#temporal-policy-select');
+    await expect(policySelect).toBeVisible({ timeout: 5000 });
+
+    // Verify expected policy options exist
+    const options = await policySelect.locator('option').allTextContents();
+    expect(options.length).toBeGreaterThan(1);
+    expect(options).toContain('Ignore History');
+    expect(options).toContain('Stability');
+  });
+});
+
+test.describe('Sterling Projection Controls', () => {
+  let forge: ForgeInstance;
+
+  test.afterEach(async () => {
+    if (forge) {
+      forge.cleanup();
+    }
+  });
+
+  test('projection controls are accessible outside the layout drawer', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/projection-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'projectionRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    // "Projections" and "Layout" should both be visible as separate sidebar entries
+    await expect(page.getByText('Projections', { exact: true }).first()).toBeVisible({ timeout: 5000 });
+    await expect(page.getByText('Layout', { exact: true }).first()).toBeVisible({ timeout: 5000 });
+
+    // Negative test: open Layout drawer and verify projection controls are NOT there
+    await openSidebarDrawer(page, 'Layout');
+    await expect(page.getByText('Add Projection')).not.toBeVisible();
+
+    // Open projections drawer and verify controls ARE there
+    await openSidebarDrawer(page, 'Projections');
+    await expect(page.getByText('Add Projection')).toBeVisible({ timeout: 5000 });
+  });
+
+  test('projection drawer lists projectable types', async ({ page }) => {
+    forge = await startForge('e2e/fixtures/projection-model.frg');
+    await page.goto(forge.sterlingUrl);
+    await selectAndRunCommand(page, 'projectionRun');
+    await page.waitForTimeout(TIMEOUT_GRAPH_LAYOUT);
+
+    await openSidebarDrawer(page, 'Projections');
+
+    await page.getByText('Add Projection').click();
+    await page.waitForTimeout(500);
+
+    // Projectable types appear as "+ TypeName" buttons in the Add Projection UI
+    const hasEpoch = await page.getByRole('button', { name: '+ Epoch' }).isVisible();
+    const hasProcess = await page.getByRole('button', { name: '+ Process' }).isVisible();
+    expect(hasEpoch || hasProcess).toBe(true);
+  });
+});

forge/info.rkt

@@ -40,7 +40,7 @@
 ; This includes outdated modules but also examples.
 (define compile-omit-paths '("example" "examples" "doc" "tests" "check-ex-spec/demo"
                              "OLD" "pardinus-cli/out" "kodkod-cli/out" "check-ex-spec/examples"                            
-                             "amalgam/tests" "amalgam" "domains/crypto/examples" "domains/abac/tests"
+                             "amalgam/tests" "amalgam" "domains/crypto/examples"
                              ))