🤖 tests: cover #5465 background-process cases in the TLA+ model

formal/background-processes/BgCleanup.tla

@@ -26,6 +26,25 @@
 (* Terminate is modelled as effective (it is best-effort in the code; see *)
 (* BgTerminate.tla). The bash tool never checks its abort signal around   *)
 (* spawn (bash.ts:1050-1085), so stopStream does not stop a spawn.        *)
+(* #5465 cases (code at 486f156905):                                      *)
+(*   JoinTimeout (case 1): a refused or failed migration aborts the       *)
+(*     command (bash.ts:1569), then joins its exit for at most            *)
+(*     FAILED_MIGRATION_EXIT_JOIN_MS = 5 s (:1578). The foreground        *)
+(*     registration is already gone (:1479) and nothing records it, so a  *)
+(*     command whose exit the join does not see (stuck in uninterruptible *)
+(*     I/O, or a remote exec whose close never arrives) runs on untracked *)
+(*     and the removal deletes its checkout: MC_cleanup_refused_join_     *)
+(*     timeout violates NoLiveAfterDelete and MigrationOwned (#5522).     *)
+(*     MC_cleanup_failed_join_timeout forces the admitted-then-failed     *)
+(*     path (MigrationFails) and violates the same invariants.            *)
+(*   ExecTimeout (case 2): the foreground exec's timer (LocalBaseRuntime  *)
+(*     :369-377, RemoteRuntime :266-) still runs after a migration and    *)
+(*     can kill the command. Benign: timeout_secs is the documented max   *)
+(*     lifetime of a background command (toolDefinitions.ts), and the     *)
+(*     kill ends the same exec stream whose exitCode the migrated handle  *)
+(*     observes and writes as exit_code (backgroundProcessExecutor.ts     *)
+(*     :739-743). FTimeout is an ordinary exit; MC_cleanup_migration_     *)
+(*     timeout holds.                                                     *)
 (***************************************************************************)
 EXTENDS Naturals
 
@@ -35,7 +54,10 @@ CONSTANTS
   Mutator,       \* "remove" | "archive" (archive: snapshot/delete behaviour)
   SpawnSealed,   \* fix: spawn takes a pending entry refused by the seal, like migrations
   ArchiveCleans, \* fix: archive seals and runs cleanup before stopping the stream or deleting
-  NoDrain        \* mutant: cleanup does not wait for pending migrations (#4805 undone)
+  NoDrain,       \* mutant: cleanup does not wait for pending migrations (#4805 undone)
+  JoinTimeout,   \* case 1: the 5 s join after a refused migration's kill can expire first
+  ExecTimeout,   \* case 2: the foreground exec's own timeout can kill F after the migration
+  MigrationFails \* case 1, forced: the migration is admitted, then migrateToBackground fails
 
 VARIABLES
   \* spawn
@@ -81,6 +103,7 @@ SExit == /\ sLive /\ sLive' = FALSE                              \* the command
 ---------------------------------------------------------------------------
 (* Migration of foreground command F (bash.ts).                           *)
 MBegin == /\ mpc = "fg"                                          \* :1426 beginMigration
+          /\ (MigrationFails => ~Sealed)                 \* forced failure: admitted only
           /\ mAdmitted' = ~Sealed /\ mPending' = mPending + 1
           /\ mpc' = IF ~Sealed THEN "claim" ELSE "refused"
           /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, fg, bg, rpc, seals, snapshot, deleted>>
@@ -93,13 +116,26 @@ MExitCheck == /\ mpc = "exitcheck"                               \* :1444-1468
                    ELSE mpc' = "migrate" /\ fg' = FALSE  \* unregister(): in neither map now
               /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, bg, mPending, mAdmitted, rpc, seals,
                              snapshot, deleted>>
-MMigrate == /\ mpc = "migrate" /\ bg' = TRUE /\ mpc' = "end"     \* :1507-1523
+MMigrate == /\ mpc = "migrate" /\ ~MigrationFails /\ bg' = TRUE /\ mpc' = "end"  \* :1507-1523
             /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, fg, mPending, mAdmitted, rpc, seals,
                            snapshot, deleted>>
-MRefused == /\ mpc = "refused" /\ fLive' = FALSE /\ mpc' = "end" \* :1558-1567 abort + join
-            /\ UNCHANGED <<stopped, spc, sLive, sReg, fg, bg, mPending, mAdmitted, rpc, seals,
-                           snapshot,
-                           deleted>>
+\* An admitted migration fails before it registers: migrateToBackground cannot create the record
+\* (:1518-1557, e.g. ENOSPC/EACCES). It takes the refused path's abort and join (:1569-1580).
+MMigrateFail == /\ mpc = "migrate" /\ mpc' = "join"
+                /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, fg, bg, mPending, mAdmitted, rpc,
+                               seals, snapshot, deleted>>
+\* Refused: unregister the foreground entry (:1479) and abort the command (:1569).
+MRefused == /\ mpc = "refused" /\ fg' = FALSE /\ mpc' = "join"
+            /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, bg, mPending, mAdmitted, rpc, seals,
+                           snapshot, deleted>>
+\* :1578 the join sees the kill take effect ...
+MJoin == /\ mpc = "join" /\ fLive' = FALSE /\ mpc' = "end"
+         /\ UNCHANGED <<stopped, spc, sLive, sReg, fg, bg, mPending, mAdmitted, rpc, seals,
+                        snapshot, deleted>>
+\* ... or (case 1) gives up after 5 s with F still running; FExit can end it later.
+MJoinTimeout == /\ JoinTimeout /\ mpc = "join" /\ mpc' = "end"
+                /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, fg, bg, mPending, mAdmitted, rpc,
+                               seals, snapshot, deleted>>
 MEnd == /\ mpc = "end" /\ mPending' = mPending - 1 /\ mpc' = "done"
         /\ fg' = (fg /\ fLive)                                   \* :1605 unregister on exit
         /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, bg, mAdmitted, rpc, seals, snapshot,
@@ -108,6 +144,12 @@ FExit == /\ fLive /\ fLive' = FALSE                              \* F ends by it
          /\ fg' = FALSE /\ bg' = FALSE                           \* its owner observes the exit
          /\ UNCHANGED <<stopped, spc, sLive, sReg, mpc, mPending, mAdmitted, rpc, seals, snapshot,
                         deleted>>
+\* Case 2: the original exec's timer kills F once it is (being) migrated. The migrated handle
+\* observes that exit like any other (bg' = FALSE), so this is FExit restricted to those phases.
+FTimeout == /\ ExecTimeout /\ fLive /\ (bg \/ mpc \in {"migrate", "end", "done"})
+            /\ fLive' = FALSE /\ fg' = FALSE /\ bg' = FALSE
+            /\ UNCHANGED <<stopped, spc, sLive, sReg, mpc, mPending, mAdmitted, rpc, seals,
+                           snapshot, deleted>>
 ---------------------------------------------------------------------------
 (* Mutator.                                                                *)
 \* Fixed archive: seal, cleanup (c_seal ... c_drain2) before its hooks, stop the stream, cleanup
@@ -157,7 +199,8 @@ RDelete == /\ rpc = "delete" /\ deleted' = TRUE /\ rpc' = "done"  \* :7710 check
                           snapshot>>
 
 Next == SStart \/ SChild \/ SRegister \/ SExit
-        \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MRefused \/ MEnd \/ FExit
+        \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MMigrateFail \/ MRefused \/ MJoin \/ MJoinTimeout \/ MEnd
+        \/ FExit \/ FTimeout
         \/ RStart \/ RStop \/ CSeal \/ CDrain1 \/ CSnap \/ CTerm \/ CDrain2 \/ RDelete
 
 Spec == Init /\ [][Next]_vars
@@ -167,7 +210,8 @@ NoLiveAfterDelete == deleted => ~sLive /\ ~fLive
 \* A migrating command is never both foreground and background ...
 FgBgExclusive == ~(fg /\ bg)
 \* ... and while it lives, the foreground, the background or its migration block owns it.
-MigrationOwned == fLive => (fg \/ bg \/ mpc \in {"claim", "exitcheck", "migrate", "refused", "end"})
+MigrationOwned ==
+  fLive => (fg \/ bg \/ mpc \in {"claim", "exitcheck", "migrate", "refused", "join", "end"})
 
 TypeOK == seals \in 0..2 /\ mPending \in 0..1 /\ stopped \in BOOLEAN
 =============================================================================

formal/background-processes/BgGateEvidence.tla

@@ -18,14 +18,35 @@
 (*     (foreground->background) command's record is written under the     *)
 (*     manager's bgOutputDir = path.join(os.tmpdir(), "mux-bashes")        *)
 (*     (di/layers/core.ts:203), whatever the runtime.                      *)
+(* #5465 case 3 (code at 486f156905), Crash: A's backend dies between the  *)
+(*   spawn and writeMeta. spawnProcess creates the record directory with   *)
+(*   output.log and clears exit_code (backgroundProcessExecutor.ts         *)
+(*   :242-268) BEFORE it starts the child (:294); the manager writes       *)
+(*   meta.json after (backgroundProcessManager.ts :1867). The crash drops  *)
+(*   A's turn lease, but the scan reads a directory with neither meta.json *)
+(*   nor exit_code as a live orphan (recordRootHoldsOrphan :2877-2890;     *)
+(*   tests: backgroundProcessManager.test.ts \"fails closed on unreadable  *)
+(*   records without an exit marker\"), and the wrapper's trap writes the  *)
+(*   marker when P exits. Benign on the scanned roots:                     *)
+(*   MC_gate_crash_before_meta and MC_gate_crash_devcontainer hold. A crash *)
+(*   before the child starts leaves a markerless directory that keeps      *)
+(*   refusing every structural mutation, user removal included: safe, but  *)
+(*   a liveness gap these safety-only configs do not check (#5576).        *)
+(*   Remote roots stay unscanned (#4889).                                  *)
+(*   MetalessTrusted is the mutant that skips meta-less directories.       *)
 (***************************************************************************)
 EXTENDS Naturals
 
 CONSTANTS
   Runtime,       \* "local" | "devcontainer" | "ssh" | "docker"
   Kind,          \* "spawn" | "migrated"
   TmpdirIsTmp,   \* os.tmpdir() = /tmp (Linux without TMPDIR); FALSE on macOS (/var/folders/...)
-  NoRecordScan   \* mutant: the gate skips the record scan
+  NoRecordScan,  \* mutant: the gate skips the record scan
+  Crash,         \* case 3: A's backend can die after its turn-lease hold, before AEnd
+  MetalessTrusted \* mutant: the scan skips record directories without meta.json
+
+\* The step order below is the spawn's; a migrated command runs before its directory exists.
+ASSUME Crash => Kind = "spawn"
 
 Root == IF Kind = "migrated" THEN (IF TmpdirIsTmp THEN "tmp" ELSE "ostmp")
         ELSE CASE Runtime = "local" -> "tmp"
@@ -34,46 +55,61 @@ Root == IF Kind = "migrated" THEN (IF TmpdirIsTmp THEN "tmp" ELSE "ostmp")
 Scanned == {"tmp"} \cup (IF Runtime = "devcontainer" THEN {"bind"} ELSE {})
 
 VARIABLES
-  apc, lease, record, alive,   \* A: turn lease, P's record exists, P runs
-  bpc, gate, committed         \* B's structural mutation
+  apc, lease, dir, record, alive, marker, \* A: turn lease, P's record directory, its meta.json,
+                                         \* P runs, P's exit_code marker
+  bpc, gate, committed                   \* B's structural mutation
+
+vars == <<apc, lease, dir, record, alive, marker, bpc, gate, committed>>
 
-vars == <<apc, lease, record, alive, bpc, gate, committed>>
+Init == /\ apc = "idle" /\ lease = FALSE /\ dir = FALSE /\ record = FALSE /\ alive = FALSE
+        /\ marker = FALSE /\ bpc = "idle" /\ gate = FALSE /\ committed = FALSE
 
-Init == /\ apc = "idle" /\ lease = FALSE /\ record = FALSE /\ alive = FALSE
-        /\ bpc = "idle" /\ gate = FALSE /\ committed = FALSE
+\* recordRootHoldsOrphan on one record: an exit marker settles it; meta.json says running and
+\* the PID is live; no meta.json fails closed (unless the mutant trusts it).
+Evidence == /\ Root \in Scanned /\ dir /\ ~marker
+            /\ IF record THEN alive ELSE ~MetalessTrusted
 
 \* --- A: a turn that starts P, then ends; P keeps running ---
 AHold == /\ apc = "idle"                          \* turn lease hold probes the gate
          /\ IF gate THEN apc' = "refused" /\ UNCHANGED lease
                     ELSE apc' = "spawn" /\ lease' = TRUE
-         /\ UNCHANGED <<record, alive, bpc, gate, committed>>
-ASpawn == /\ apc = "spawn" /\ record' = TRUE /\ alive' = TRUE /\ apc' = "end"
-          /\ UNCHANGED <<lease, bpc, gate, committed>>
+         /\ UNCHANGED <<dir, record, alive, marker, bpc, gate, committed>>
+ADir == /\ apc = "spawn" /\ dir' = TRUE /\ apc' = "child"   \* output dir, no exit_code
+        /\ UNCHANGED <<lease, record, alive, marker, bpc, gate, committed>>
+AChild == /\ apc = "child" /\ alive' = TRUE /\ apc' = "meta"  \* the detached child starts
+          /\ UNCHANGED <<lease, dir, record, marker, bpc, gate, committed>>
+AMeta == /\ apc = "meta" /\ record' = TRUE /\ apc' = "end"    \* writeMeta
+         /\ UNCHANGED <<lease, dir, alive, marker, bpc, gate, committed>>
 AEnd == /\ apc = "end" /\ lease' = FALSE /\ apc' = "done"
-        /\ UNCHANGED <<record, alive, bpc, gate, committed>>
-PExit == /\ alive /\ alive' = FALSE               \* the trap writes exit_code
-         /\ UNCHANGED <<apc, lease, record, bpc, gate, committed>>
+        /\ UNCHANGED <<dir, record, alive, marker, bpc, gate, committed>>
+\* Case 3: A's backend dies; its lease goes stale, P (if started) survives under nohup/setsid.
+ACrash == /\ Crash /\ apc \in {"spawn", "child", "meta", "end"}
+          /\ apc' = "crashed" /\ lease' = FALSE
+          /\ UNCHANGED <<dir, record, alive, marker, bpc, gate, committed>>
+PExit == /\ alive /\ alive' = FALSE /\ marker' = TRUE  \* the trap writes exit_code
+         /\ UNCHANGED <<apc, lease, dir, record, bpc, gate, committed>>
 
 \* --- B: the mutation gate, then the mutation ---
 BGate == /\ bpc = "idle" /\ gate' = TRUE /\ bpc' = "leases"
-         /\ UNCHANGED <<apc, lease, record, alive, committed>>
+         /\ UNCHANGED <<apc, lease, dir, record, alive, marker, committed>>
 BLeases == /\ bpc = "leases"
            /\ bpc' = IF lease THEN "refused" ELSE "records"
            /\ gate' = IF lease THEN FALSE ELSE gate
-           /\ UNCHANGED <<apc, lease, record, alive, committed>>
+           /\ UNCHANGED <<apc, lease, dir, record, alive, marker, committed>>
 BRecords == /\ bpc = "records"
-            /\ IF ~NoRecordScan /\ record /\ alive /\ Root \in Scanned
+            /\ IF ~NoRecordScan /\ Evidence
                  THEN bpc' = "refused" /\ gate' = FALSE
                  ELSE bpc' = "commit" /\ UNCHANGED gate
-            /\ UNCHANGED <<apc, lease, record, alive, committed>>
+            /\ UNCHANGED <<apc, lease, dir, record, alive, marker, committed>>
 BCommit == /\ bpc = "commit" /\ committed' = TRUE /\ bpc' = "done"
-           /\ UNCHANGED <<apc, lease, record, alive, gate>>
+           /\ UNCHANGED <<apc, lease, dir, record, alive, marker, gate>>
 
-Next == AHold \/ ASpawn \/ AEnd \/ PExit \/ BGate \/ BLeases \/ BRecords \/ BCommit
+Next == AHold \/ ADir \/ AChild \/ AMeta \/ AEnd \/ ACrash \/ PExit
+        \/ BGate \/ BLeases \/ BRecords \/ BCommit
 Spec == Init /\ [][Next]_vars
 
 \* B never commits its mutation while A's background process in W runs.
 NoMutationUnderForeignProcess == committed => ~alive
 
-TypeOK == apc \in {"idle", "spawn", "end", "done", "refused"}
+TypeOK == apc \in {"idle", "spawn", "child", "meta", "end", "done", "refused", "crashed"}
 =============================================================================

formal/background-processes/MC_cleanup_archive.cfg

@@ -7,4 +7,7 @@ CONSTANTS
   SpawnSealed = FALSE
   ArchiveCleans = FALSE
   NoDrain = FALSE
+  JoinTimeout = FALSE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
 INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_archive_fixed.cfg

@@ -7,4 +7,7 @@ CONSTANTS
   SpawnSealed = TRUE
   ArchiveCleans = TRUE
   NoDrain = FALSE
+  JoinTimeout = FALSE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
 INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_failed_join_timeout.cfg

@@ -0,0 +1,13 @@
+\* #5465 case 1, forced failure: an admitted migration fails, and its killed command outlives the 5 s join.
+SPECIFICATION Spec
+CONSTANTS
+  HasSpawn = FALSE
+  HasMigration = TRUE
+  Mutator = "remove"
+  SpawnSealed = FALSE
+  ArchiveCleans = FALSE
+  NoDrain = FALSE
+  JoinTimeout = TRUE
+  ExecTimeout = FALSE
+  MigrationFails = TRUE
+INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_fixed.cfg

@@ -7,4 +7,7 @@ CONSTANTS
   SpawnSealed = TRUE
   ArchiveCleans = FALSE
   NoDrain = FALSE
+  JoinTimeout = FALSE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
 INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_migration_remove.cfg

@@ -7,4 +7,7 @@ CONSTANTS
   SpawnSealed = FALSE
   ArchiveCleans = FALSE
   NoDrain = FALSE
+  JoinTimeout = FALSE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
 INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_migration_timeout.cfg

@@ -0,0 +1,13 @@
+\* #5465 case 2: the foreground exec's timeout kills a migrated command. Expect all to hold.
+SPECIFICATION Spec
+CONSTANTS
+  HasSpawn = FALSE
+  HasMigration = TRUE
+  Mutator = "remove"
+  SpawnSealed = FALSE
+  ArchiveCleans = FALSE
+  NoDrain = FALSE
+  JoinTimeout = FALSE
+  ExecTimeout = TRUE
+  MigrationFails = FALSE
+INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_refused_join_timeout.cfg

@@ -0,0 +1,13 @@
+\* #5465 case 1: removal refuses a migration whose killed command outlives the 5 s join.
+SPECIFICATION Spec
+CONSTANTS
+  HasSpawn = FALSE
+  HasMigration = TRUE
+  Mutator = "remove"
+  SpawnSealed = FALSE
+  ArchiveCleans = FALSE
+  NoDrain = FALSE
+  JoinTimeout = TRUE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
+INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_cleanup_spawn_remove.cfg

@@ -7,4 +7,7 @@ CONSTANTS
   SpawnSealed = FALSE
   ArchiveCleans = FALSE
   NoDrain = FALSE
+  JoinTimeout = FALSE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
 INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_gate_crash_before_meta.cfg

@@ -0,0 +1,10 @@
+\* #5465 case 3: A's backend dies between the local spawn and writeMeta. Expect all to hold.
+SPECIFICATION Spec
+CONSTANTS
+  Runtime = "local"
+  Kind = "spawn"
+  TmpdirIsTmp = TRUE
+  NoRecordScan = FALSE
+  Crash = TRUE
+  MetalessTrusted = FALSE
+INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_crash_devcontainer.cfg

@@ -0,0 +1,10 @@
+\* #5465 case 3 on the devcontainer bind-mount root. Expect all to hold.
+SPECIFICATION Spec
+CONSTANTS
+  Runtime = "devcontainer"
+  Kind = "spawn"
+  TmpdirIsTmp = TRUE
+  NoRecordScan = FALSE
+  Crash = TRUE
+  MetalessTrusted = FALSE
+INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_devcontainer_spawn.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "spawn"
   TmpdirIsTmp = TRUE
   NoRecordScan = FALSE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_docker_spawn.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "spawn"
   TmpdirIsTmp = TRUE
   NoRecordScan = FALSE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_local_spawn.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "spawn"
   TmpdirIsTmp = TRUE
   NoRecordScan = FALSE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_migrated_ostmp.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "migrated"
   TmpdirIsTmp = FALSE
   NoRecordScan = FALSE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_migrated_tmp.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "migrated"
   TmpdirIsTmp = TRUE
   NoRecordScan = FALSE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_gate_ssh_spawn.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "spawn"
   TmpdirIsTmp = TRUE
   NoRecordScan = FALSE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_mut_cleanup_nodrain.cfg

@@ -7,4 +7,7 @@ CONSTANTS
   SpawnSealed = FALSE
   ArchiveCleans = FALSE
   NoDrain = TRUE
+  JoinTimeout = FALSE
+  ExecTimeout = FALSE
+  MigrationFails = FALSE
 INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned

formal/background-processes/MC_mut_gate_metaless_trusted.cfg

@@ -0,0 +1,10 @@
+\* Mutant: the scan skips record directories without meta.json (crash before writeMeta).
+SPECIFICATION Spec
+CONSTANTS
+  Runtime = "local"
+  Kind = "spawn"
+  TmpdirIsTmp = TRUE
+  NoRecordScan = FALSE
+  Crash = TRUE
+  MetalessTrusted = TRUE
+INVARIANTS TypeOK NoMutationUnderForeignProcess

formal/background-processes/MC_mut_gate_norecords.cfg

@@ -5,4 +5,6 @@ CONSTANTS
   Kind = "spawn"
   TmpdirIsTmp = TRUE
   NoRecordScan = TRUE
+  Crash = FALSE
+  MetalessTrusted = FALSE
 INVARIANTS TypeOK NoMutationUnderForeignProcess