mirror of
https://github.com/vercel-labs/fx.git
synced 2026-10-28 10:15:17 +08:00
Pranit
39e6b0fc96
A call's result is recorded as the call finishes, so a turn reopened after a crash answers the call with it. That record held only the result's text, so a turn reopened there lost the tool's images without a note. It now holds the images too, by name when the store holds them, and an open stages them with the rest of the open turn. A tool image the store refused stays inline in its result, and the image window never counted it, so a session could keep more images than its window allows. The window now counts it, and when it leaves it takes the name of its bytes and is saved as dropped, like a stored image. ImageStore.tla counts it too and checks WindowBound; ImageStore-InlineUncounted.cfg shows a window that skips it breaks that. main.zig's test list never named journal.zig or libfx_journal.zig, so none of their Zig tests ran. Both are listed now.
35 lines
855 B
INI
35 lines
855 B
INI
\* The graph drive-images.mjs walks: a plain engine with an image store, two
|
|
\* prompts, an image an older libfx saved inline, a window of one image, so
|
|
\* each prompt drops the image before it, and driver steps only once
|
|
\* the code has settled. ImageStore.cfg checks the durable session.
|
|
CONSTANTS
|
|
N = 2
|
|
Imgs = {"a", "b"}
|
|
Old = TRUE
|
|
Durable = FALSE
|
|
MaxFaults = 1
|
|
MaxCrashes = 2
|
|
MaxLoss = 1
|
|
StoreFirst = TRUE
|
|
MarkOnlyStored = TRUE
|
|
FailOnMissing = TRUE
|
|
MaxRetries = 0
|
|
DropRepeats = TRUE
|
|
Window = 1
|
|
LiveWindow = TRUE
|
|
WindowAtOpen = TRUE
|
|
CountInline = TRUE
|
|
Tools = TRUE
|
|
ToolStoreFirst = TRUE
|
|
SPECIFICATION DriveSpec
|
|
INVARIANTS
|
|
TypeOK
|
|
NoDanglingRef
|
|
OneCopy
|
|
OpenExact
|
|
KnownStoredIsStored
|
|
FailsOnlyOnLoss
|
|
FailsOnlyOnLossInWindow
|
|
WindowHeld
|
|
WindowBound
|