Edit mode: "Export as inst" (reify) produces invalid Forge `inst` after edits

[sidprasad]

Summary

In Edit mode, the "Export as inst" button calls dataInstance.reify() to turn the (possibly edited) instance back into a Forge inst { ... } block. After the user makes an edit (add atom / delete atom / add relation tuple), the reified output is frequently not valid Forge/Alloy inst syntax and does not round-trip back into the model. Atoms added in the editor and atoms of any sig not already in the model are the main offenders.

reify() itself lives in spytial-core (AlloyDataInstance), not in this repo — but the feature is surfaced here via EditView.tsx (the "Export as inst" button → handleExport → reify()), so filing here and flagging the upstream root cause.

Tested against spytial-core@2.9.0 (see package.json).

Reproduction

UI path:

1. Open Edit mode on any instance.
2. Add an atom (e.g. a new Goat), or add an atom of a sig that wasn't in the instance, then click Export as inst.
3. Paste the copied inst block back into the Forge/Alloy model → it fails to parse / references undeclared sigs.

I also reproduced it headlessly with a faithful harness that drives the real spytial-core helpers (parseAlloyXML, addInstanceAtom, removeInstanceAtom, addInstanceRelationTuple) and a verbatim copy of AlloyDataInstance.reify(), against demos/rc/rc-datum.xml.

Observed reified output (annotated)

Baseline (no edits) — already a couple of smells, but parses-ish:

inst builtinstance {
Int = -8+-7+-6+-5+-4+-3+-2+-1+0+1+2+3+4+5+6+7   // (S1) binds builtin Int
GWBoat = `GWBoat0
Goat = `Goat0+`Goat1+`Goat2
Wolf = `Wolf0+`Wolf1+`Wolf2
...
no no-field-guard                                // (S2) hyphenated field name -> `no - field - guard`
}

After adding one Goat in the editor:

Goat = `Goat0+`Goat1+`Goat2+`Goat-1             // (B1) `Goat-1  -> the `-` parses as subtraction

After adding an atom of a sig not in the model (Frog):

Frog = `Frog-1                                   // (B2) binds a sig the spec never declares (+ B1 hyphen)

Root cause — WHY (the interesting part)

Two independently-written pieces of spytial-core were never reconciled:

B1 — Editor-minted atom IDs use a - separator that reify() emits verbatim as an atom literal.

The editor mints new atom IDs as `${type}-${n}` (AlloyDataInstance/structured-input-graph generateAtomId):

generateAtomId(e){ ... let s = `${e}-${r}`; for(;o.has(s);) r++, s = `${e}-${r}`; return s }   // -> "Goat-1"

reify() then emits every atom id as a backtick literal with no escaping/validation:

s[x] = sx(b) ? g.map(p => p.id) : g.map(p => `\`${p.id}`);   // -> `Goat-1

Alloy's native atoms are Sig<n> with no separator (Goat0, Goat1), which are valid identifiers. The editor's Sig-<n> form is not a valid atom identifier — `Goat-1 tokenizes as `Goat - 1. So every atom added in the editor poisons the exported inst. This is the core "after an edit" regression: unedited Alloy atoms round-trip; editor-added ones never do.

B2 — reify() emits a binding line for every type in instance.types, including sigs the editor invents on the fly.

Adding an atom of an unknown type goes through addInstanceAtom, which auto-creates a sig:

function addInstanceAtom(e,t){ ... else { let r = {_:"type", id:t.type, types:[t.type,"univ"], atoms:[t]}; o[r.id]=r; } ... }

reify() iterates this.alloyInstance.types and prints Type = ... for each — so it happily emits Frog = ... even though the target spec has no sig Frog. Pasting that inst back is a compile error.

Secondary (pre-existing, not edit-specific, but worth fixing while here):

• S1: reify() emits Int = -8+...+7 — binding the builtin Int sig is redundant/usually rejected.
• S2: Field/relation names with - (e.g. no-field-guard) are emitted unescaped, same hyphen-as-minus problem as B1.
• Abstract parent sigs with no direct atoms (GWAnimal, Position) are silently omitted (b.length>0 && ...). Usually fine for partial inst, but means parent membership is implicit only.

Why reify() reads the edited state correctly (so this is not a stale-state bug)

Worth ruling out the obvious hypothesis: the edit methods reassign this.alloyInstance (addAtom/removeAtom/addRelationTuple → addInstanceAtom/removeInstanceAtom/addInstanceRelationTuple), and reify() reads this.alloyInstance.types/.relations. So edits are reflected — the bug is in how reify serializes them (B1/B2), not in whether it sees them.

Where it lives / where the fix belongs

• Surfaced in this repo: EditView.tsx handleExport (lines ~101–111) and the edit-event wiring in SpyTialEditGraph.tsx.
• Root cause is upstream in spytial-core: AlloyDataInstance.reify() and generateAtomId (dist/browser/spytial-core-complete.global.js). The fix likely belongs in spytial-core (cross-repo, like the dark-mode coupling).

Suggested fixes

1. Atom IDs: mint editor atoms as Sig<n> (no separator) to match Alloy, or have reify() sanitize/escape atom ids that aren't valid identifiers.
2. Unknown sigs: when reifying, either skip types absent from the original schema or surface a validation error (the EditView already has validateEditedInstance — it could flag "atom of undeclared sig" and block/warn on export).
3. Builtin sigs: skip Int/String/seq/Int in reify() output.
4. Round-trip test: add a test that reifies after each edit kind and re-parses the result, asserting it's valid.

---

🤖 Investigation harness and full annotated output available on request; reify()/generateAtomId quoted verbatim from spytial-core@2.9.0.

[sidprasad]

Upstream root-cause issue filed: sidprasad/spytial-core#480 (fix belongs in AlloyDataInstance.reify() + generateAtomId).