diff --git a/.agents/skills/testing-sysml-repl/SKILL.md b/.agents/skills/testing-sysml-repl/SKILL.md index d4c67287d1..86a1d931ec 100644 --- a/.agents/skills/testing-sysml-repl/SKILL.md +++ b/.agents/skills/testing-sysml-repl/SKILL.md @@ -1151,6 +1151,27 @@ changes: `unresolved reference: n`; the CLI has **no** flag for action inputs, so exercise `in`/`out` parameters by having a caller action invoke `action call = Callee(a = 3, b = 4);`. +## Action fan-out CLI checks + +- Use explicit succession syntax in minimal repros: `succession a then done;` + or `first a then done;`. A bare `a then done;` inside an action body can be + rejected as `expected a body member` before execution; do not mistake that + diagnostic for a runtime fan-out refusal. +- The default scheduler is `reverse`, not `declared`. Compare explicit + `-schedule declared` with `-schedule reverse`; a no-flag run normally agrees + with reverse. +- `-engine smt -action ` asks whether execution holds, not for the table + of final values. Use `-engine smt -action -check-diverge ` to + request two witnessed final values. `-engine check` and `-schedule explore` + expose outcomes directly. SMT may explicitly refuse an implicit join at a + plain node, whereas the runtime supports it; use an explicit join for a + cross-engine scheduling comparison. +- Bound adversarial loops with `OPENSYSML_MAX_ACTION_STEPS=200`, and wrap the + command with `timeout 30`. Assert the step-limit diagnostic and exit 2, + not watchdog exit 124. Report CLI diagnostics separately from Go error + identity: the CLI does not expose `errors.Is`, and static merge/join + validation may prevent reaching the runtime guard. + ## Control flow inside an action node body `while`, `loop … until` (braced and unbraced), `for … in` and `if`/`else` execute inside an @@ -4139,10 +4160,10 @@ Traps and recipes: - Error wordings to assert: non-Boolean guard → `error: execution failed: type mismatch: node s1: guard must evaluate to boolean, got constant`; unresolvable name in a guard → `error: execution failed: eval guard of node s1: unresolved - reference: nosuch`. Two guards out of one action node that both hold → - `error: execution failed: more than one succession is enabled: action node check has multiple - successors` (wraps the `ErrAmbiguousSuccession` sentinel; the run stops with the token still on the - node and neither branch's attribute written — assert that with `%tokens`, not just the message). + reference: nosuch`. Two guards out of one ordinary action node that both hold are no error: each + succession is its own `HappensBefore` link, so the token splits as a fork's does and both branch + attributes are written (assert both in `Results:`). Only a `decide` node picks one of several + holding guards; a `join` or `merge` with two outgoing successions is still refused. - Places a guard could still be silently ignored, all worth a one-liner fixture: succession out of a real initial node (`then start s1 if …;`), out of a `merge`, out of a `join` (must not deadlock — the branch tokens are consumed either way), and one whose target is `done`. diff --git a/.circleci/config.yml b/.circleci/config.yml index f4375f7b34..2e5d2c1460 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -17,7 +17,7 @@ executors: # It carries Node LTS, 24 or later, which the gate needs. - image: cimg/go:1.25-node resource_class: medium - + python-executor: docker: - image: cimg/python:3.11 @@ -1047,7 +1047,7 @@ jobs: executor: python-executor steps: - checkout - + - attach_workspace: at: . @@ -1070,7 +1070,7 @@ jobs: mkdir -p ~/.opensysml/bin cp bin/sysml-grpc ~/.opensysml/bin/ chmod +x ~/.opensysml/bin/sysml-grpc - + - run: name: Install Python client command: | @@ -1083,7 +1083,7 @@ jobs: # its wheels with python -m build. pip install --only-binary :all: jupyter_client==8.10.0 build==1.6.1 make jupyter-kernel-install - + # The integration tests connect to a service on the standard port with # auto_start=False, which is the explicit opt-in to one the client does not # manage; without it they skip, exercising nothing, so one runs here for @@ -2251,7 +2251,7 @@ jobs: - go/load-cache - go/mod-download - go/save-cache - + - run: name: Build release binaries command: | @@ -2259,58 +2259,58 @@ jobs: COMMIT=${CIRCLE_SHA1} BUILD_TIME=$(date -u '+%Y-%m-%d_%H:%M:%S') GO_VERSION=$(go version | awk '{print $3}') - + # Build for multiple platforms using make mkdir -p dist - + GOOS=linux GOARCH=amd64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml dist/sysml-linux-amd64 - + GOOS=linux GOARCH=arm64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml dist/sysml-linux-arm64 - + GOOS=darwin GOARCH=amd64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml dist/sysml-darwin-amd64 - + GOOS=darwin GOARCH=arm64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml dist/sysml-darwin-arm64 - + GOOS=windows GOARCH=amd64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml dist/sysml-windows-amd64.exe - + GOOS=linux GOARCH=amd64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-lsp dist/sysml-lsp-linux-amd64 - + GOOS=linux GOARCH=arm64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-lsp dist/sysml-lsp-linux-arm64 - + GOOS=darwin GOARCH=amd64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-lsp dist/sysml-lsp-darwin-amd64 - + GOOS=darwin GOARCH=arm64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-lsp dist/sysml-lsp-darwin-arm64 - + GOOS=windows GOARCH=amd64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-lsp dist/sysml-lsp-windows-amd64.exe - + # The gRPC service backs the Python client, which downloads one # file per platform and verifies it against a .sha256 sidecar, so # these are published raw rather than archived. They are built into # a subdirectory to keep them out of the archive globs below. mkdir -p dist/grpc - + GOOS=linux GOARCH=amd64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-grpc dist/grpc/sysml-grpc-linux-amd64 - + GOOS=linux GOARCH=arm64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-grpc dist/grpc/sysml-grpc-linux-arm64 - + GOOS=darwin GOARCH=amd64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-grpc dist/grpc/sysml-grpc-darwin-amd64 - + GOOS=darwin GOARCH=arm64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-grpc dist/grpc/sysml-grpc-darwin-arm64 - + GOOS=windows GOARCH=amd64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/sysml-grpc dist/grpc/sysml-grpc-windows-amd64.exe @@ -2345,7 +2345,7 @@ jobs: mkdir -p dist/wasm make build-release-wasm VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION" mv bin/wasm/release/sysml-wasm.wasm bin/wasm/release/wasm_exec.js dist/wasm/ - + # Create tarballs cd dist for binary in sysml-*; do @@ -2355,7 +2355,7 @@ jobs: tar czf "${binary}.tar.gz" "$binary" fi done - + # Bundle archives: both binaries under their plain names # (sysml, sysml-lsp), which is the layout a Homebrew formula or a # PATH install expects, with their manual pages beside them under @@ -2376,7 +2376,7 @@ jobs: cp sysml-lsp-windows-amd64.exe stage/windows-amd64/sysml-lsp.exe (cd stage/windows-amd64 && zip -q ../../opensysml-windows-amd64.zip sysml.exe sysml-lsp.exe) rm -rf stage - + # The checksum manifest and the per-file sidecars are # build-release's, once the Python distributions exist to list. ls -l . grpc jupyter @@ -2457,17 +2457,17 @@ jobs: name: Assemble the release and write its checksum manifest command: | cd dist - + # The opensysml wheel and sdist, released with the binaries they drive, # and the jupyter-opensysml-kernel platform wheels and sdist likewise. cp ../client/python/dist/opensysml-*.whl ../client/python/dist/opensysml-*.tar.gz . cp ../client/jupyter-kernel/dist/jupyter_opensysml_kernel-*.whl \ ../client/jupyter-kernel/dist/jupyter_opensysml_kernel-*.tar.gz . - + # Checksums over every published archive, so a Homebrew formula # (or a careful user) can verify a download. sha256sum ./*.tar.gz ./*.zip ./*.whl | sed 's|\./||' > SHA256SUMS.txt - + # Same for the raw gRPC binaries, through the per-file sidecars # written beside them when they were built, the only checksum # opensysml reads: checked against the bytes here, then folded in. @@ -2623,7 +2623,7 @@ jobs: <(jq -r '.dsseEnvelope.payload' provenance.intoto.json.bundle | base64 -d \ | jq -r '.subject[] | "\(.name) \(.digest.sha256)"' | sort) - + - rehearsal-skip: what: "cosign keyless signing and attestation (they write to the public Rekor log)" - run: @@ -3311,7 +3311,7 @@ jobs: - rehearsal-tag - attach_workspace: at: . - + - unless: condition: << pipeline.parameters.release_rehearsal >> steps: @@ -3325,7 +3325,7 @@ jobs: fi echo "Publishing release $VERSION" ls -la dist/ - + # Move only tarballs to a release directory mkdir -p dist/release mv dist/*.tar.gz dist/*.zip dist/release/ 2>/dev/null || true @@ -3343,14 +3343,14 @@ jobs: mv dist/provenance.intoto.json dist/provenance.intoto.json.bundle dist/release/ echo "Release artifacts:" ls -la dist/release/ - + # Try different token variable names TOKEN="${GITHUB_TOKEN:-${GH_TOKEN:-${CIRCLE_TOKEN}}}" if [ -z "$TOKEN" ]; then echo "Error: No GitHub token found. Tried GITHUB_TOKEN, GH_TOKEN, CIRCLE_TOKEN" exit 1 fi - + # '-replace' reuses an existing release and only re-uploads assets of # the same name, so hand-written notes, title and prerelease/latest # flags survive a re-run. Never '-delete': that is an alias of diff --git a/.github/workflows/extension-libraries-upstream.yml b/.github/workflows/extension-libraries-upstream.yml new file mode 100644 index 0000000000..21d2d40510 --- /dev/null +++ b/.github/workflows/extension-libraries-upstream.yml @@ -0,0 +1,97 @@ +name: Extension libraries upstream + +# Advisory: does the extension-libraries upstream's ref still run under +# OpenSysML? It syncs the ref into the vendored directory and runs the whole +# suite. It is scheduled rather than a required check: it downloads from +# upstream and takes minutes, so a failure here surfaces what broke without +# blocking pull requests. It never pushes and never opens issues. +on: + schedule: + - cron: '41 4 * * *' + workflow_dispatch: + inputs: + ref: + description: 'Extension-libraries ref to sync (branch or tag)' + required: true + default: main + +permissions: + contents: read + +jobs: + upstream: + name: OpenSysML against upstream extension libraries + runs-on: ubuntu-latest + timeout-minutes: 120 + env: + REF: ${{ inputs.ref || 'main' }} + steps: + - name: Check out repository + uses: actions/checkout@v4 + + - name: Set up Go + uses: actions/setup-go@v5 + with: + go-version-file: go.mod + cache: true + + - name: Install Z3 + run: | + sudo apt-get update + sudo apt-get install -y z3 + z3 --version + + - name: Install cvc5 + run: | + curl -fsSL --proto '=https' --proto-redir '=https' -o /tmp/cvc5.zip \ + https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.4/cvc5-Linux-x86_64-static.zip + echo "dcdbfada0ce493ee98259c0816e0daafc561c223aadb3af298c2968e73ea39c6 /tmp/cvc5.zip" | sha256sum --check --strict + unzip -p /tmp/cvc5.zip '*/bin/cvc5' > /tmp/cvc5-bin + sudo install -m 0755 /tmp/cvc5-bin /usr/local/bin/cvc5 + cvc5 --version | head -1 + + - name: Sync the upstream ref + id: sync + run: | + out="$(scripts/sync-extension-libraries.sh --ref "$REF" | tee /dev/stderr)" + sha="$(sed -n 's/^Resolved .* to \([0-9a-f]*\)$/\1/p' <<<"$out" | tail -1)" + { + echo "### Synced upstream \`$REF\` at \`$sha\`" + echo '```' + git status --porcelain -- "internal/workspace/libs/stdlib/OpenSysML Libraries/" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" + + - name: Check the library snapshot + id: snapshot + run: | + if make stdlib-snapshot-check; then + echo "Snapshot unchanged." >> "$GITHUB_STEP_SUMMARY" + else + echo "Snapshot regenerated for the synced libraries." >> "$GITHUB_STEP_SUMMARY" + make stdlib-snapshot + fi + + - name: Run the test suite + id: tests + run: | + go test ./... + go test -C tools ./... + + - name: Report the verdict + if: always() + run: | + if [ "${{ steps.tests.outcome }}" = "success" ]; then + echo "Upstream \`$REF\` runs clean under OpenSysML." >> "$GITHUB_STEP_SUMMARY" + else + { + echo "**Upstream \`$REF\` breaks OpenSysML.**" + echo "" + echo "| step | outcome |" + echo "| --- | --- |" + echo "| sync | ${{ steps.sync.outcome }} |" + echo "| snapshot | ${{ steps.snapshot.outcome }} |" + echo "| tests | ${{ steps.tests.outcome }} |" + } >> "$GITHUB_STEP_SUMMARY" + fi + git checkout -- "internal/workspace/libs/stdlib/OpenSysML Libraries/" 2>/dev/null || true diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml index 5672191a35..9006ca33ba 100644 --- a/.github/workflows/pr.yml +++ b/.github/workflows/pr.yml @@ -73,6 +73,12 @@ jobs: BASE_REF: ${{ github.base_ref }} run: scripts/ci-changed-areas.sh "origin/$BASE_REF" HEAD | tee -a "$GITHUB_OUTPUT" + # The vendored copy is checked in this job, not static-and-integrity: the + # changed-areas filter may skip that job for a non-Go change, but drift + # between the vendored libraries and their pin must always fail. + - name: Check the vendored extension libraries against their pin + run: make extension-libraries-check + race-tests: name: Go race tests (${{ matrix.shard }}) needs: changes diff --git a/CHANGELOG.md b/CHANGELOG.md index d8bc697e45..fcf9e37a6e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -152,7 +152,7 @@ release is described in [docs/project/releasing.md](docs/project/releasing.md). - **An `assert constraint` a succession orders among an action's steps is checked when the flow reaches it.** A false condition ends the run with the assertion's violation; one no succession names is still not a step. - **The SysML v1 migrator writes object flows as succession flows.** An object flow between two actions is `succession flow of T from a.out to b.in`, which orders the actions and carries the value when the source completes; a guarded one is OMG's guarded succession to the flow itself, `first a if g then f; succession flow f of T from a.out to b.in;`, so a false guard moves no value, a guard of literal `true` is no guard, and a flow into a «stream» parameter stays a `flow`. A flow into or out of a fork, join or merge names the node's `inputObjectN`/`outputObjectN` features instead of being rerouted between pins, and an action several object flows reach waits for them without a synthesized join. Edge weights, all UML's default in the measured models, are not written. -- **Values pass through forks, joins and merges, and several succession flows may leave one action.** A control node holds what a flow delivers to its input features and passes it on when a token reaches it: a fork copies it to every branch, a join gathers one value of each input, a merge passes on the one that arrived. Each succession flow leaving an action starts its target beside the action's other succession, as after a fork; two plain successions still stop the run as ambiguous. +- **Values pass through forks, joins and merges, and several succession flows may leave one action.** A control node holds what a flow delivers to its input features and passes it on when a token reaches it: a fork copies it to every branch, a join gathers one value of each input, a merge passes on the one that arrived. Each succession flow leaving an action starts its target beside the action's other successions, as after a fork. - **A succession may lead to a succession flow.** `first a if g then f; succession flow f from a.y to b.v;` gates the flow on the guard: the runtime and the model checker move the value and order `b` only when `g` holds, so a false guard leaves `b` waiting for that pin (or running on another path's value) rather than on the rejected one. The model form records the guarded succession as the `gate` of the edge and the flow, and action views draw it at its own declaration. - **The v1 migration report says where a run will stop on a construct the tool simulated and v2 cannot run as written.** A state's entry or exit behavior, or a transition effect, whose activity waits for the clock (a duration constraint on itself or on one of its nodes, an accept of a time event, or a call of an activity, or of an operation whose method is one, that has one) is reported as an approximation naming the wait, since a v2 entry, exit or effect is performed whole at the instant it is triggered. A trigger or accept of a signal that no send action of the model sends — neither it nor a signal specializing it — and only a button of the tool's UI prototype posts is reported as waiting for a message nothing in the model posts, and a «SimulationConfig» whose `UI` names a prototype frame is reported as taking no input from it. A script body that reads a property declaring no default before it assigns it is reported as an approximation naming the property: in v2 the property holds no value until assigned, so a run reaching the read first stops, where the tool's script engine reads null and its arithmetic takes 0; a read after assignments each made only when a name admitting no value holds one is reported the same way, for the run in which none of those names holds one. @@ -267,6 +267,14 @@ release is described in [docs/project/releasing.md](docs/project/releasing.md). - **The standard SysML v2 API client is its own package.** `internal/translate/interop/sysmlapi` drives projects, branches, commits with `change` payloads, elements and roots with optional bearer authentication and follows a server's `Link: rel="next"` paging to the end; `internal/translate/interop/flexo` keeps Flexo's extras — Layer 1 Turtle, organizations, ETag pushes — over it, and `internal/translate/interop/modelsync` holds what `sysml -sync` and the REPL share. - `%viz [--view=] [--style=