sync-kgraph

sync-kgraph exposes synchronize-or-reveal algorithms as a C23 library and a native Memgraph query module. A manually mapped graph view represents a deterministic Mealy automaton. The module can then:

find a word that brings every current hypothesis to one state;
find a homing word whose outputs distinguish the current hypothesis;
explain predicted states and output branches after each action;
validate localization and committed output traces, detecting stale plans; and
maintain prepared planning data after transition or observation changes.

Cypher is used only for schema, mapping, and queries. The mapping is manual so the database owner controls how application entities, actions, and observations become an automaton.

Choose A Planning Mode

Need	API	Preparation	Intended use
Repeated low-latency plans	`plan_sync`, `plan_disambiguate`	`prepare_model(..., false, false)`	Read-mostly models
Frequent small model changes	Cached planners plus `update_cells`	`prepare_model(..., false, true)`	Incrementally maintained models
A baseline or one-off plan	`plan_sync_uncached`, `plan_disambiguate_uncached`	None	Rebuilds from the base view on every call
Hardware supports only part of the alphabet	`plan_sync_allowed`, `plan_disambiguate_allowed`	Clean prepared model	Every returned action is permitted by the caller
Reach a supplied goal set	`plan_goal`	Clean prepared model	Every possible final state lies in the goal set
Inspect pair transitions in Memgraph Lab	Any cached mode	Set `materialize_pair_edges` to `true`	Visualization only; it does not accelerate planning

Cached and uncached planners return the same semantic result for the same model generation. The cached path is optimized for repeated calls; the uncached path is intentionally retained for controlled comparisons and simple one-off use.

Build And Install

Build the native module against the C header installed with the target Memgraph server. Using the server's own header avoids C API version mismatches:

CC=clang meson setup build-memgraph \
  -Dmemgraph=enabled \
  -Dmemgraph_include_dir=/usr/include/memgraph
meson compile -C build-memgraph

The Linux artifact is build-memgraph/sync.so; macOS produces the native shared-module equivalent. Place it in the server's query-module directory, or install it with Meson, and load it:

CALL mg.load("sync");
CALL mg.procedures() YIELD name
WITH name
WHERE name STARTS WITH "sync."
RETURN name ORDER BY name;

Expected procedure names:

sync.explain_plan
sync.mark_dirty
sync.plan_disambiguate
sync.plan_disambiguate_allowed
sync.plan_disambiguate_uncached
sync.plan_goal
sync.plan_sync
sync.plan_sync_allowed
sync.plan_sync_uncached
sync.prepare_model
sync.update_cells
sync.validate_observed_update
sync.validate_update

Prebuilt releases contain Linux x86_64 and native macOS arm64 binaries, the C header and static library, Cypher scripts, the worked examples, and the Memgraph Lab view.

Map A Model

Run cypher/install_schema.cypher once. The application schema is otherwise untouched. Create dedicated view nodes and relationships for each model:

(:SyncModel {model, generation, dirty})
(:SyncState {
  model, state_key, state_id?, semantic_ref?, orientation?
})
(:SyncAction {
  model, action_key, action_id?
})
(:SyncOutput {
  model, output_key, output_id?
})
(:SyncState)-[:SYNC_TRANS {
  model, action_key
}]->(:SyncState)
(:SyncState)-[:SYNC_OBS {
  model, action_key
}]->(:SyncOutput)

Keys must be unique within their domain and model. For every state/action pair, there must be exactly one SYNC_TRANS and one SYNC_OBS. An observation is the output emitted for the source state and selected action. Optional numeric IDs only control stable ordering; keys are the public interface.

prepared_generation, oracle_epoch, incremental, pair_edges_materialized, and snapshot_token are managed by the module. The application should not write them directly.

The mapping is deliberately manual because only the database owner knows how application entities, orientations, commands, and sensor abstractions form the automaton. Prefer separate SyncState nodes linked by semantic_ref or an application-owned relationship instead of adding SyncState to application nodes. The supplied uninstall script deletes nodes in the Sync-KGraph namespace.

prepare_model validates the complete Mealy model and creates the derived pair records used by cached planning. PAIR_NEXT and PAIR_PRE are optional inspection relationships; planning never requires them.

The trigger file is a template, not a generic installed trigger. Adapt its predicate to the application labels and relationships that feed each model. A schema-agnostic trigger cannot identify the affected model safely. Exclude writes made by update_cells because that procedure handles generation and repair atomically.

API Lifecycle

Model preparation and execution progress are separate. Preparation belongs to a model generation; the caller retains execution progress for each plan.

Model state or change	Available API and next step
New or dirty view	Uncached planners can read the current view. Call `prepare_model` before using cached, restricted, or goal planners, `explain_plan`, or either monitor with the current generation.
Clean prepared view	Plan, explain, and monitor against that generation. Enable `incremental` during preparation to use `update_cells`.
Effective `update_cells` batch	The generation advances and prepared records are updated atomically. Plan again using the new generation; no additional preparation is required.
`update_cells` returns `UNCHANGED`	The generation stays the same; existing plans remain current.
Direct edits to the mapped view	Mark the model dirty and advance its generation as part of the edit, using `mark_dirty` or an adapted trigger, then prepare it again.
Plan generation differs from the model	Either monitor returns `STALE_GENERATION`, including while the model is dirty. Prepare if needed and obtain a new plan.

stateDiagram-v2
    direction LR
    state "New or dirty model" as Dirty
    state "Prepared generation" as Prepared

    [*] --> Dirty
    Dirty --> Prepared: prepare_model / same generation
    Dirty --> Dirty: uncached planning / model stays unprepared
    Prepared --> Dirty: direct edit + mark_dirty / advance generation
    Prepared --> Prepared: effective update_cells / advance generation
    Prepared --> Prepared: UNCHANGED update_cells / same generation

    note right of Prepared
        update_cells requires incremental mode.
        Every generation change makes older plans stale.
    end note

prepare_model rebuilds derived records at the current generation; it does not advance the model generation. An uncached plan does not prepare the model for later monitor calls. Module restarts and cache eviction cause hydration on the next cached planning call without changing the model generation.

Use the following execution lifecycle:

Request a plan and inspect its outcome. Execute a word only for PLAN. ALREADY_SATISFIED requires no actions. For synchronization, NO_PLAN proves absence from the original support; RESOURCE_BOUND is inconclusive. Both unsuccessful synchronization outcomes return an empty word. Goal search follows the same outcome rules for containment in its supplied goal set.
Save the plan's generation, original hypotheses, and full word together. Retain the permitted actions and goal set, when applicable, for replanning. Start with completed_steps = 0 and observed_outputs = [].
Once the caller commits the next action/output event, append that output and increment completed_steps once. Call validate_observed_update with the saved original support and the entire committed output prefix. Choose validate_update when only motion consistency is required.
Handle the monitor's decision using the table below. A later localizer report for the same completed prefix reuses the same step count and output list; it does not append another observation.
Whenever a new plan is adopted, save its own original support, word, and generation, and reset the step count and output list. A localization change alone does not change the model generation or require preparation.

The following states belong to the caller's execution cycle. Transitions out of validation are labeled with the observation-aware monitor's decisions; the library returns those decisions without driving the controller.

stateDiagram-v2
    state "Prepare current generation if needed" as Ready
    state "Request plan from current support" as Planning
    state "Execute next action" as Executing
    state "Validate full committed prefix" as Validating
    state "Await localizer report" as Waiting
    state "Obtain accepted nonempty support" as Replanning
    state "Reconcile evidence or model" as Reconciling
    state "No word satisfies this request" as NoPlan
    state "Search incomplete" as ResourceLimited
    state "Caller completion policy" as Completion

    [*] --> Ready
    Ready --> Planning: current generation prepared
    Planning --> Executing: PLAN / save plan, reset step and output trace
    Planning --> Completion: ALREADY_SATISFIED
    Planning --> NoPlan: NO_PLAN
    Planning --> ResourceLimited: RESOURCE_BOUND
    NoPlan --> Planning: caller changes support or objective
    ResourceLimited --> Planning: caller retries with more budget
    Executing --> Validating: caller commits action and output / append once
    Validating --> Executing: CONTINUE / actions remain
    Validating --> Completion: CONTINUE / word exhausted
    Validating --> Waiting: WAIT
    Waiting --> Validating: localizer report / same step and output trace
    Validating --> Replanning: REPLAN
    Replanning --> Planning: use accepted support
    Validating --> Reconciling: MODEL_VIOLATION
    Reconciling --> Ready: caller resolves inconsistency
    Validating --> Ready: STALE_GENERATION / discard old plan
    Completion --> [*]

    note right of ResourceLimited
        RESOURCE_BOUND is inconclusive.
        It does not establish NO_PLAN.
    end note

This diagram shows execution through the prepared Memgraph monitor API. Uncached planning remains available before preparation. CONTINUE at the end of a word confirms consistency; the caller determines whether its objective is complete. The caller may also choose to replan when compatible observations reduce its support.

Monitor decision	Caller handling
`CONTINUE`	The supplied evidence matches the prediction. Continue with the remaining word, or replan from the support identified by accepted observations. At the end of the word, apply the caller's completion policy.
`WAIT`	Expected hypotheses are available, but no localizer evidence was checked. Supply a localizer report for the same prefix when available.
`REPLAN`	Replan from the accepted reported support. If that support is empty, obtain a nonempty support before calling a planner.
`MODEL_VIOLATION`	Resolve the inconsistent observation, localization, or model before relying on the plan again. Inspect the separate observation and support diagnostics.
`STALE_GENERATION`	Obtain a plan for the current model generation and reset its execution progress. Changing the generation attached to the old word does not revalidate that plan.

Both monitors are stateless: calling them does not commit execution, update the model, replace a plan, or remember a previous localizer report. The caller owns action-completion, sampling, and replanning policy. See Runtime Monitoring for the exact decision rules.

Procedure API

Prepared Planning

CALL sync.prepare_model(
  model, materialize_pair_edges = false, incremental = false)
CALL sync.plan_sync(model, hypotheses, budget)
CALL sync.plan_disambiguate(model, hypotheses, bound, budget)

The cached planners require a clean prepared model. They are the normal choice when the same model will be queried repeatedly. The first call after a module restart or cache eviction reports cache_state: "HYDRATED"; subsequent calls normally report "HOT".

The preparation options are independent:

`materialize_pair_edges`	`incremental`	Behavior
`false`	`false`	Prepared planning with compact pair records
`true`	`false`	Also create `PAIR_NEXT` and `PAIR_PRE` for inspection
`false`	`true`	Compact pair records maintained by `update_cells`
`true`	`true`	Incremental maintenance plus inspection relationships

The process cache defaults to 512 MiB. Set SYNC_KGRAPH_CACHE_MAX_BYTES to a decimal byte limit, or 0 to disable retention. Durable pair records remain available when retention is disabled.

Synchronization Contract

Since v0.5.1, synchronization first tries the existing pair-merging witnesses, then restarts an exact forward motion-support BFS from the original deduplicated support if greedy merging cannot finish. This happens inside the existing Planning stage, in plan_sync, plan_sync_uncached, and (since v0.5.2) plan_sync_allowed. The preparation and monitor lifecycle, procedure signatures, and result fields stay the same.

Outcome	Meaning
`ALREADY_SATISFIED`	The original support is already a singleton. The empty word and final state are valid.
`PLAN`	Replaying the returned word from the original support reaches one physical state. `PAIR_MERGE` identifies a fast-path success and `SUBSET_BFS` an exact fallback success.
`NO_PLAN`	Exact reachable-support exhaustion proves that no synchronizing word exists from the original support using the query's permitted alphabet (the full model alphabet for unrestricted calls).
`RESOURCE_BOUND`	The search still has work pending when its expansion budget runs out. Increasing the budget can resolve this outcome.

status = "OK" means the API operation completed; callers must inspect outcome. Invalid input, invalid models, allocation failures, and record-source errors remain errors and cannot establish NO_PLAN.

The positive budget is shared by both phases. Each accepted pair witness costs one expansion; each non-goal support dequeued by BFS costs one more. The fallback keeps the expansions spent by greedy merging and discards its word. The budget counts algorithmic expansions, not actions in the word, elapsed time, memory, or pair-record reads. Finding a singleton or exhausting the frontier during the last permitted expansion still completes the search.

stateDiagram-v2
    state "Deduplicate original support H" as Input
    state "Greedy pair merging" as Greedy
    state "Forward subset BFS from H" as Exact
    state "Replay word from H" as Verify
    state "PLAN or ALREADY_SATISFIED" as Success
    state "NO_PLAN / exhausted reachable frontier" as Absent
    state "RESOURCE_BOUND / search incomplete" as Limited

    [*] --> Input
    Input --> Verify: singleton / empty word
    Input --> Greedy: multiple states
    Greedy --> Verify: singleton / PAIR_MERGE
    Greedy --> Exact: cannot finish / discard word, retain expansions
    Exact --> Verify: singleton / SUBSET_BFS
    Exact --> Absent: frontier exhausted
    Exact --> Limited: pending frontier with no budget left
    Verify --> Success: singleton image confirmed
    Success --> [*]
    Absent --> [*]
    Limited --> [*]

    note right of Exact
        Same positive budget for both phases.
        Both phases respect the permitted alphabet.
        Keep equal-cardinality motion images.
        Do not filter supports by observations.
    end note

Errors in any phase propagate to the caller. Every success is independently replay-verified. Greedy merging does not guarantee a shortest word. The exact fallback explores words by length, retaining all distinct reachable supports, including steps that preserve cardinality. Its time and memory requirements can be exponential; completeness requires sufficient computation and memory.

For NO_PLAN and RESOURCE_BOUND, method is NONE, word is [], length and final_support_size are zero, and final_state_key is "". The C API uses SG_INDEX_NONE for the final state and also clears support/branch/homing metrics. Generation, actual expansions, and elapsed time are retained. A discarded greedy prefix is never returned as a plan or prepended to the exact word. See the exact fallback example.

Restricted Actions And Goal Sets

v0.5.2 adds three procedures inside the existing Planning stage:

CALL sync.plan_sync_allowed(model, hypotheses, actions, budget)
CALL sync.plan_disambiguate_allowed(model, hypotheses, bound, actions, budget)
CALL sync.plan_goal(model, hypotheses, goals, actions, budget)

All three require a clean prepared generation. actions is a nonempty list of known action_key strings; list order breaks search ties and duplicate actions are harmless. Hypotheses and goals are nonempty sets of known state keys, with duplicates collapsed. Budgets must be positive, even for an already satisfied request. Changing a query's actions or goals does not change the model generation or require preparation.

Restricted synchronization searches pair witnesses using only permitted actions, then uses the same exact fallback and outcome contract above. Neither phase may use an excluded action. NO_PLAN with one permitted alphabet says nothing about a request with additional actions. The budget counts accepted pair witnesses and expanded fallback supports; internal pair-search work is not separately charged.

Restricted disambiguation uses prepared pair records for its heuristic. If that word contains an excluded action, it is discarded and PARTITION_BFS searches the permitted alphabet. It retains the requested worst-branch bound and the caller-controlled policy of trying bound=1, then |H|-1 after a proven absence. The planner never relaxes that bound automatically.

Goal search asks for containment, delta(H, word) subset_of goals. Every possible final state must lie in the supplied set; multiple physical states may remain. It uses forward motion-support BFS, reports BELIEF_BFS on PLAN, and independently replays the returned word. It does not condition on observations, widen the goal set, or construct an adaptive policy. Use a singleton goal set when one specific final state is required.

One goal-search expansion is one non-goal support expanded. Initial containment returns ALREADY_SATISFIED, an empty word, method=NONE, and zero expansions. NO_PLAN requires frontier exhaustion; a pending frontier at the budget limit returns RESOURCE_BOUND. Goal results include final_state_keys and final_support_size; both are empty/zero on failure. Success can occur on the last permitted expansion. Explicit search may require exponential time and memory. In C, final_state is populated only for a successful singleton image.

These plans use the same explanation and observation-aware monitor lifecycle. Save the original support and entire word, accumulate committed outputs, and handle WAIT, REPLAN, MODEL_VIOLATION, and STALE_GENERATION as usual. The monitor checks evidence against the word; the caller retains action permissions, goals, and its completion policy. See the runnable restricted/goal example.

Incremental Updates

CALL sync.prepare_model(model, false, true)
CALL sync.update_cells(model, changes, repair_budget = 0)

Each change is a map containing state_key, action_key, and at least one of target_key or output_key. The complete nonempty batch is validated before anything is written. Duplicate cells and unknown keys are rejected. A batch containing only current values returns UNCHANGED without advancing the model generation.

Updates change the base view and its prepared records in one transaction. Incremental mode is optimized for small batches; if the affected region grows too large, it falls back to an exact full rebuild. Optional PAIR_NEXT and PAIR_PRE relationships are updated only when materialization was enabled.

repair_budget = 0 uses ceil(pair_count / 4). A positive value is an explicit touch budget. If repair exceeds it, the procedure rebuilds all pair records and returns fallback_rebuild: true. Passing -1 requests a full rebuild directly; this is intended for controlled comparisons, not normal operation.

The result reports maintenance_mode (UNCHANGED, INCREMENTAL, or FULL_REBUILD), direct pair deltas, records touched/examined/written, pair edges examined, database write batches, invalidations, fallback use, and elapsed time.

Uncached Planning

CALL sync.plan_sync_uncached(model, hypotheses, budget)
CALL sync.plan_disambiguate_uncached(model, hypotheses, bound, budget)

The uncached planners validate the current base Mealy view and rebuild the pair oracle in temporary C memory on every call. They work on dirty or unprepared models and do not create or modify auxiliary records. Use them for a one-off plan or as a cache-free reference; prepared planning is optimized for repeated calls.

For the same generation, hypotheses, bound, and budget, cached and uncached semantic fields are identical.

The four unrestricted planner procedures return the following metrics. plan_disambiguate_allowed uses the same cached values:

Field	Cached value	Uncached value	Meaning
`oracle_source`	`PERSISTED`	`RECOMPUTED`	Source of pair witnesses
`oracle_builds`	`0`	`1`	Calls to the full oracle builder
`cache_state`	`HOT` or `HYDRATED`	`BYPASSED`	Process snapshot state
`oracle_rows_loaded`	`0` hot; all pairs hydrated	`0`	Durable rows loaded this call
`oracle_load_batches`	`0` hot; hydration batches	`0`	Pair-record queries
`oracle_cache_hits`	Snapshot reads	`0`	Witness reads served in C
`snapshot_record_reads`	Requested witnesses	`0`	Pair records read by the planner
`snapshot_hydration_time_us`	Hydration time or `0`	`0`	Cold snapshot reconstruction
`oracle_time_us`	Hydration time or `0`	Rebuild time	Oracle preparation work
`total_compute_time_us`	Variable	Variable	Base-view extraction through planner completion

planning_time_us covers only the word planner. total_compute_time_us covers model extraction through planner completion, excluding result encoding, Bolt transport, and client latency.

plan_sync_allowed and plan_goal read the prepared automaton directly and search without loading or building a pair oracle. They report oracle_source: "NONE", cache_state: "BYPASSED", zero oracle/snapshot work counters and times, and measured planning_time_us and total_compute_time_us. Their preparation requirement still applies.

After upgrading from a release whose pair records lack oracle_epoch, run prepare_model again.

Supporting API

CALL sync.explain_plan(model, generation, hypotheses, word)
CALL sync.validate_update(
  model, generation, hypotheses, word, completed_steps,
  reported_hypotheses, localizer_available = true)
CALL sync.validate_observed_update(
  model, generation, hypotheses, word, completed_steps,
  observed_outputs, reported_hypotheses, localizer_available = true)
CALL sync.mark_dirty(model)

hypotheses, reported_hypotheses, and returned supports are lists of state_key strings. Words are lists of action_key strings. budget limits search expansions; bound is the required worst-case output-branch support size. A bound of one requests a homing word.

For a support of n distinct states, the recommended caller policy is to try bound = 1 first. Only after NO_PLAN, and when n > 1, try bound = n - 1 for the weakest nontrivial guaranteed reduction. For n = 2 these bounds are identical, so no retry is needed. Feasibility is monotone in the bound: NO_PLAN at n - 1 rules out every stricter reduction bound. Testing each intermediate bound repeats searches for weaker objectives. RESOURCE_BOUND means the search was inconclusive and must not be treated as NO_PLAN. Execute until accepted information changes the support, then replan from that support. The planner always honors the requested bound; it does not perform this fallback automatically.

Planner calls return an outcome of PLAN, ALREADY_SATISFIED, NO_PLAN, or RESOURCE_BOUND, and a method of PAIR_MERGE, SUBSET_BFS, PAIR_RESOLUTION, PARTITION_BFS, BELIEF_BFS, or NONE. Explanation and monitoring retain the prepared-model lifecycle even when a word was obtained through the uncached API.

The public C API is in include/sync_kgraph/sync.h. It exposes the same automaton builder, pair oracle, planners, explanation visitor, and monitor without requiring Memgraph.

Runtime Monitoring

validate_update is the motion-only consistency monitor. It compares the localizer report with delta(H, prefix), without checking any sensor outputs. Its existing procedure signature and C result type are unchanged.

validate_observed_update is the Mealy observation-aware consistency monitor. On every call, provide the original plan support H, its generation and word, and the full committed output prefix. observed_outputs contains public output_key strings, one per completed action, in order. Unknown output keys, invalid actions or states, and a length different from completed_steps are argument errors. Stale plans return STALE_GENERATION before resolving keys against the changed model, as with the motion-only procedure.

Starting from S = H, each committed action a and output o updates:

S := { delta(q, a) | q in S and eta(q, a) = o }

Outputs are evaluated on the source state and action, using the same Mealy convention as the disambiguation planner. Equal successor states are collapsed. The resulting support E includes only hypotheses compatible with the entire output prefix.

Condition	Decision	Returned expected support
Generation differs from the model	`STALE_GENERATION`	`[]`; no observation check
An output is impossible from every surviving hypothesis	`MODEL_VIOLATION`	`[]`, even if localization is unavailable
Outputs are compatible and localization is unavailable	`WAIT`	`E`
Localizer report equals `E`	`CONTINUE`	`E`
Localizer report is a strict subset of `E`	`REPLAN`	`E`
Localizer report includes a state outside `E`	`MODEL_VIOLATION`	`E`

Pass reported_hypotheses = [] and localizer_available = false when the localizer is unavailable; its report is ignored. An explicitly available but empty report is a strict subset and returns REPLAN if the outputs are compatible. The original motion-only monitor still requires a nonempty report when localization is available.

The new procedure returns the existing status, decision, reason, expected_hypotheses, unexpected_hypotheses, and generation fields, plus:

Field	Meaning
`observation_compatible`	`true` for a possible trace, `false` for an impossible trace, `null` for a stale plan
`failed_observation_step`	First incompatible step, numbered from 1; otherwise `null`
`observed_output`	Offending output key; otherwise `null`
`expected_outputs`	Distinct possible output keys at the failing step, conditioned on earlier outputs; otherwise `[]`

unexpected_hypotheses always means reported states outside E, and is empty when localization is unavailable. Observation mismatches use the separate diagnostic fields. When E is empty, all reported states are unexpected.

The C equivalent is sg_validate_observed_update, which takes numeric output IDs and returns sg_observed_monitor_result. Common fields are in its monitor member; absent diagnostic indices use SG_INDEX_NONE. The observation_compatible flag is unevaluated for a stale plan. Release the result with sg_observed_monitor_result_free before reuse. The C API validates only consumed action IDs; the Memgraph adapter resolves the whole supplied word.

In C, monitoring requires a validated sg_automaton but no pair oracle or Memgraph preparation. Inputs are borrowed for the duration of the call; the result owns its returned arrays. Keep a plan result alive while using its word, and call sg_plan_result_free when replacing or retiring that plan. Check the returned sg_status before reading a monitor result: SG_OK means validation completed, and can accompany MODEL_VIOLATION or STALE_GENERATION. Likewise, a Memgraph row with status = "OK" still requires inspecting decision.

The caller owns physical action-completion and sampling policy. Commit an action/output event before submitting it to the monitor. Localization cannot override an impossible committed output, even if its reported support matches the motion-only prediction. Timing, action continuation, goal selection, and responding to REPLAN remain caller responsibilities.

Worked Warehouse Example

The example maps two ambiguous bays, two corridor poses, and one dock pose. Execute the queries below in order, starting from the reset/load step. The numbered Cypher files provide a shorter runnable walkthrough; their comments give the expected generations for that sequence.

1. Install The Schema

mgconsole < cypher/install_schema.cypher

Expected: ten indexes are created and no data rows are returned. Reuse these indexes for every mapped model.

2. Load The Manual View

mgconsole < examples/warehouse/00_reset_and_load.cypher

Verify the mapping:

MATCH (m:SyncModel {model: "warehouse"})
OPTIONAL MATCH (s:SyncState {model: "warehouse"})
WITH m, count(s) AS states
OPTIONAL MATCH (a:SyncAction {model: "warehouse"})
WITH m, states, count(a) AS actions
OPTIONAL MATCH (o:SyncOutput {model: "warehouse"})
RETURN m.generation AS generation, m.dirty AS dirty,
       states, actions, count(o) AS outputs;

Expected:

generation: 1, dirty: true, states: 5, actions: 4, outputs: 4

The view contains 20 transitions and 20 observations, one of each per state/action cell.

3. Plan Without The Cache

The freshly loaded model is dirty and has no auxiliary records. Compute a synchronizing word directly from the base view:

CALL sync.plan_sync_uncached(
  "warehouse", ["west_bay:east", "east_bay:west"], 64)
YIELD status, outcome, method, word, length, final_state_key,
      final_support_size, generation, oracle_source, oracle_builds, cache_state
RETURN status, outcome, method, word, length, final_state_key,
       final_support_size, generation, oracle_source, oracle_builds, cache_state;

Expected:

"OK", "PLAN", "PAIR_MERGE", ["to_corridor", "go_west"], 2,
"dock:north", 1, 1, "RECOMPUTED", 1, "BYPASSED"

Compute the homing word through the same uncached path:

CALL sync.plan_disambiguate_uncached(
  "warehouse", ["west_bay:east", "east_bay:west"], 1, 64)
YIELD status, outcome, method, word, length, best_support_size,
      worst_support_size, branch_count, homing, generation,
      oracle_source, oracle_builds, cache_state
RETURN status, outcome, method, word, length, best_support_size,
       worst_support_size, branch_count, homing, generation,
       oracle_source, oracle_builds, cache_state;

Expected:

"OK", "PLAN", "PAIR_RESOLUTION", ["to_corridor"], 1,
1, 1, 2, true, 1, "RECOMPUTED", 1, "BYPASSED"

Confirm that neither call materialized auxiliary graph data:

OPTIONAL MATCH (p:SyncPair {model: "warehouse"})
WITH count(p) AS pairs
OPTIONAL MATCH ()-[r:PAIR_NEXT|PAIR_PRE {model: "warehouse"}]->()
RETURN pairs, count(r) AS pair_relationships;

Expected:

pairs: 0, pair_relationships: 0

4. Prepare The Cached Model

CALL sync.prepare_model("warehouse", true)
YIELD status, generation, oracle_epoch, states, actions, outputs, transitions,
      pairs, pair_edges, mergeable_pairs, resolvable_pairs,
      materialized_pair_edges, incremental_enabled
RETURN status, generation, oracle_epoch, states, actions, outputs, transitions,
       pairs, pair_edges, mergeable_pairs, resolvable_pairs,
       materialized_pair_edges, incremental_enabled;

Expected:

"OK", 1, 1, 5, 4, 4, 20, 15, 60, 15, 15, true, false

There are 15 unordered state pairs with repetition and 60 pair/action edges. Because edge materialization was enabled, the graph contains 15 SyncPair, 60 PAIR_NEXT, and 60 PAIR_PRE records.

5. Plan Synchronization From Persisted Witnesses

CALL sync.plan_sync(
  "warehouse", ["west_bay:east", "east_bay:west"], 64)
YIELD status, outcome, method, word, length, final_state_key,
      final_support_size, generation, oracle_source, oracle_builds, cache_state
RETURN status, outcome, method, word, length, final_state_key,
       final_support_size, generation, oracle_source, oracle_builds, cache_state;

Expected:

"OK", "PLAN", "PAIR_MERGE", ["to_corridor", "go_west"], 2,
"dock:north", 1, 1, "PERSISTED", 0, "HOT"

The semantic columns exactly match the uncached synchronization result. Only the oracle metadata and timing fields differ.

6. Plan Disambiguation From Persisted Witnesses

CALL sync.plan_disambiguate(
  "warehouse", ["west_bay:east", "east_bay:west"], 1, 64)
YIELD status, outcome, method, word, length, best_support_size,
      worst_support_size, branch_count, homing, generation,
      oracle_source, oracle_builds, cache_state
RETURN status, outcome, method, word, length, best_support_size,
       worst_support_size, branch_count, homing, generation,
       oracle_source, oracle_builds, cache_state;

Expected:

"OK", "PLAN", "PAIR_RESOLUTION", ["to_corridor"], 1,
1, 1, 2, true, 1, "PERSISTED", 0, "HOT"

The two bays emit different landmark outputs under to_corridor, so one action partitions the initial support into two singleton branches. This result also exactly matches the uncached homing result.

7. Explain The Synchronizing Word

CALL sync.explain_plan(
  "warehouse", 1,
  ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"])
YIELD step, action, predicted_hypotheses, output_trace, branch_hypotheses
RETURN step, action, predicted_hypotheses, output_trace, branch_hypotheses
ORDER BY step, output_trace[0] DESC;

Expected rows:

0, "", [west_bay:east, east_bay:west], [],
   [west_bay:east, east_bay:west]
1, "to_corridor", [corridor_w:east, corridor_e:west],
   [west_landmark], [corridor_w:east]
1, "to_corridor", [corridor_w:east, corridor_e:west],
   [east_landmark], [corridor_e:west]
2, "go_west", [dock:north], [west_landmark, dock], [dock:north]
2, "go_west", [dock:north], [east_landmark, dock], [dock:north]

8. Monitor Committed Actions And Observations

First, the existing motion-only API checks the localizer after to_corridor:

CALL sync.validate_update(
  "warehouse", 1,
  ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"], 1,
  ["corridor_w:east", "corridor_e:west"], true)
YIELD status, decision, expected_hypotheses, unexpected_hypotheses, generation
RETURN status, decision, expected_hypotheses, unexpected_hypotheses, generation;

Expected:

"OK", "CONTINUE", [corridor_w:east, corridor_e:west], [], 1

Reporting only one expected corridor returns REPLAN; reporting dock:north at this step returns MODEL_VIOLATION; passing an unavailable localizer returns WAIT.

For the observation-aware API, retain the original plan from step 5. Once to_corridor has committed the output west_landmark, validation can proceed even if the localizer has not supplied a report:

CALL sync.validate_observed_update(
  "warehouse", 1,
  ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"], 1, ["west_landmark"], [], false)
YIELD decision, expected_hypotheses, observation_compatible
RETURN decision, expected_hypotheses, observation_compatible;

Expected: WAIT, [corridor_w:east], true. When localization becomes available for that same completed action, submit the same step count and output prefix:

CALL sync.validate_observed_update(
  "warehouse", 1,
  ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"], 1, ["west_landmark"],
  ["corridor_w:east"], true)
YIELD decision, expected_hypotheses, observation_compatible,
      failed_observation_step, observed_output, expected_outputs
RETURN decision, expected_hypotheses, observation_compatible,
       failed_observation_step, observed_output, expected_outputs;

Expected: CONTINUE, [corridor_w:east], true, null, null, []. Reporting corridor_e:west instead would return MODEL_VIOLATION, although that state belongs to the motion-only prediction.

After the second action, go_west, commits output dock, replay both outputs from the original bays:

CALL sync.validate_observed_update(
  "warehouse", 1,
  ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"], 2, ["west_landmark", "dock"],
  ["dock:north"], true)
YIELD decision, expected_hypotheses, observation_compatible
RETURN decision, expected_hypotheses, observation_compatible;

Expected: CONTINUE, [dock:north], true. The word is now exhausted; CONTINUE reports consistency, not a new action to execute.

The next two queries illustrate independent alternative execution histories. An impossible first output is rejected even when localization exactly matches the motion-only prediction:

CALL sync.validate_observed_update(
  "warehouse", 1,
  ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"], 1, ["symmetric"],
  ["corridor_w:east", "corridor_e:west"], true)
YIELD decision, expected_hypotheses, observation_compatible,
      failed_observation_step, observed_output, expected_outputs
RETURN decision, expected_hypotheses, observation_compatible,
       failed_observation_step, observed_output, expected_outputs;

Expected: MODEL_VIOLATION, [], false, 1, symmetric, [west_landmark, east_landmark].

For a strict-subset example, start from both bays and the dock, commit go_east with output symmetric, and report only west_bay:east. The output leaves both bays possible, while localization shrinks that support further. Replan from the accepted report and start the new plan at step zero:

CALL sync.validate_observed_update(
  "warehouse", 1, ["west_bay:east", "east_bay:west", "dock:north"],
  ["go_east"], 1, ["symmetric"], ["west_bay:east"], true)
YIELD decision
WITH decision, ["west_bay:east"] AS accepted_hypotheses
WHERE decision = "REPLAN"
CALL sync.plan_disambiguate("warehouse", accepted_hypotheses, 1, 64)
YIELD outcome, word, generation
RETURN decision, accepted_hypotheses, outcome, word, generation;

Expected: REPLAN, [west_bay:east], ALREADY_SATISFIED, [], 1. The accepted singleton already satisfies homing, so this example requires no further disambiguation actions. If replanning returns PLAN, monitor its word with accepted_hypotheses as the new original support, completed_steps = 0, and observed_outputs = []. Reusing the previous output trace would attach observations to the wrong word.

9. Invalidate Old Plans

CALL sync.mark_dirty("warehouse") YIELD status, generation
RETURN status, generation;

Expected:

"DIRTY", 2

Cached planning is now rejected until sync.prepare_model("warehouse", false) succeeds. Uncached planning remains available against the current base view and returns generation 2. A monitor call carrying generation 1 still returns a stale result while the model is dirty:

CALL sync.validate_observed_update(
  "warehouse", 1, ["west_bay:east", "east_bay:west"],
  ["to_corridor", "go_west"], 1, ["west_landmark"], [], false)
YIELD status, decision, generation, observation_compatible
RETURN status, decision, generation, observation_compatible;

"OK", "STALE_GENERATION", 2, null

Monitoring a generation-2 word requires preparation first. Keep the saved generation-1 word marked stale; obtain a new plan for generation 2.

10. Prepare And Update Incrementally

Prepare the dirty generation in compact incremental mode. This keeps the derived graph compact and enables update_cells:

CALL sync.prepare_model("warehouse", false, true)
YIELD status, generation, oracle_epoch, pairs, pair_edges,
      materialized_pair_edges, incremental_enabled
RETURN status, generation, oracle_epoch, pairs, pair_edges,
       materialized_pair_edges, incremental_enabled;

Expected:

"OK", 2, 2, 15, 60, false, true

Change one observation cell:

CALL sync.update_cells("warehouse", [{
  state_key: "east_bay:west",
  action_key: "to_wall",
  output_key: "east_landmark"
}], 15)
YIELD status, maintenance_mode, generation, oracle_epoch, changed_cells,
      direct_pair_edges, fallback_rebuild
RETURN status, maintenance_mode, generation, oracle_epoch, changed_cells,
       direct_pair_edges, fallback_rebuild;

Expected:

"UPDATED", "INCREMENTAL", 3, 2, 1, 5, false

The five direct deltas are the to_wall entries for the five unordered pairs containing east_bay:west. The epoch stays at 2 while generation advances, and no pair relationships are created. Repeating the same value is a no-op:

CALL sync.update_cells("warehouse", [{
  state_key: "east_bay:west",
  action_key: "to_wall",
  output_key: "east_landmark"
}], 15)
YIELD status, generation, oracle_epoch, changed_cells, direct_pair_edges
RETURN status, generation, oracle_epoch, changed_cells, direct_pair_edges;

Expected:

"UNCHANGED", 3, 2, 0, 0

Cached and uncached homing calls still return ["to_corridor"] with generation 3. An invalid key aborts the whole batch and leaves generation, base cells, and the oracle unchanged.

The successful update kept generation 3 prepared. A new plan can therefore be created and its initial support validated immediately, with an empty output prefix:

WITH ["west_bay:east", "east_bay:west"] AS hypotheses
CALL sync.plan_disambiguate("warehouse", hypotheses, 1, 64)
YIELD outcome, word, generation
WITH hypotheses, word, generation, outcome
WHERE outcome = "PLAN"
CALL sync.validate_observed_update(
  "warehouse", generation, hypotheses, word, 0, [], hypotheses, true)
YIELD decision, expected_hypotheses, observation_compatible
RETURN word, generation, decision, expected_hypotheses, observation_compatible;

Expected: [to_corridor], 3, CONTINUE, [west_bay:east, east_bay:west], true. An older plan still produces STALE_GENERATION even when the changed cell was not on its word.

Exact Synchronization Example

Load the two complete seven-state models and run their cached/uncached queries:

mgconsole --no_history < examples/exact_sync/00_reset_and_load.cypher
mgconsole --no_history < examples/exact_sync/01_plan.cypher

These files reset only sync_fallback_positive and sync_fallback_negative. Use the same schema and loaded module as the warehouse example. All outputs are quiet; the initial support is H = {q0, q1, q2}. The positive model is:

State	a	b	c
q0	q3	q5	q4
q1	q3	q6	q3
q2	q4	q5	q3
q3	q3	q3	q3
q4	q4	q4	q4
q5	q5	q5	q3
q6	q6	q6	q3

Greedy merging picks a, trapping the support at {q3, q4}. The exact fallback restarts from H and finds b, c: H -> {q5, q6} -> {q3}. For the negative model, only the last two c transitions change, to q5 and q6 respectively. Every original pair still has a merging witness, but no word synchronizes the whole support in that model.

After running the files above, try:

CALL sync.plan_sync("sync_fallback_positive", ["q0", "q1", "q2"], 4)
YIELD status, outcome, method, word, final_state_key, expansions, generation
RETURN status, outcome, method, word, final_state_key, expansions, generation;

Expected results for both cached and uncached calls:

Model	Budget	Outcome	Method	Word	Final state	Expansions
Positive	3	`RESOURCE_BOUND`	`NONE`	`[]`	`""`	3
Positive	4	`PLAN`	`SUBSET_BFS`	`["b", "c"]`	`q3`	4
Negative	3	`RESOURCE_BOUND`	`NONE`	`[]`	`""`	3
Negative	4	`NO_PLAN`	`NONE`	`[]`	`""`	4

Each call returns status: "OK" and generation: 1. One expansion is spent on the discarded greedy witness. The remaining three expand H, {q3, q4}, and {q5, q6}. The fourth total expansion can therefore either find the singleton or finish the absence proof. Retrying an inconclusive call starts a new search with the supplied total budget; search progress is not persisted.

Restricted And Goal Example

After loading and preparing the exact-sync fixtures above, run:

mgconsole --no_history < examples/exact_sync/02_restricted_and_goal.cypher

The queries use sync_fallback_positive and original support {q0,q1,q2}:

Request	Actions	Budget	Outcome / method	Word	Final support
Restricted sync	`a,b,c`	4	`PLAN / SUBSET_BFS`	`bc`	`{q3}`
Restricted sync	`a,b`	4	`NO_PLAN / NONE`	empty	empty
Restricted homing, bound 1	`b,c`	2	`PLAN / PARTITION_BFS`	`bc`	worst branch size 1
Goal `{q3}`	`a,b,c`	3	`PLAN / BELIEF_BFS`	`bc`	`{q3}`
Goal `{q3,q4}`	`a,b,c`	1	`PLAN / BELIEF_BFS`	`a`	`{q3,q4}`

The last goal request allows two final physical states because both are goals. The example also validates the committed b/quiet event with reported support {q5,q6}, receiving CONTINUE through the existing monitor API.

Developer Documentation

See HACKING.md for the C snapshot architecture, cache and update lifecycle diagrams, correctness invariants, ablation benchmarks, quality gates, coverage policy, and release process.

Name		Name	Last commit message	Last commit date
.github		.github
cypher		cypher
examples		examples
include/sync_kgraph		include/sync_kgraph
scripts		scripts
src		src
tests		tests
views		views
.clang-format		.clang-format
.clang-tidy		.clang-tidy
.editorconfig		.editorconfig
.gitignore		.gitignore
HACKING.md		HACKING.md
LICENSE		LICENSE
README.md		README.md
meson.build		meson.build
meson_options.txt		meson_options.txt

Navigation Menu

Uh oh!

Repository files navigation

sync-kgraph

Choose A Planning Mode

Build And Install

Map A Model

API Lifecycle

Procedure API

Prepared Planning

Synchronization Contract

Restricted Actions And Goal Sets

Incremental Updates

Uncached Planning

Supporting API

Runtime Monitoring

Worked Warehouse Example

1. Install The Schema

2. Load The Manual View

3. Plan Without The Cache

4. Prepare The Cached Model

5. Plan Synchronization From Persisted Witnesses

6. Plan Disambiguation From Persisted Witnesses

7. Explain The Synchronizing Word

8. Monitor Committed Actions And Observations

9. Invalidate Old Plans

10. Prepare And Update Incrementally

Exact Synchronization Example

Restricted And Goal Example

Developer Documentation

About

Releases

Sponsor this project

Contributors

Languages

Uh oh!

Latest commit

History

Folders and files

Repository files navigation

sync-kgraph

Choose A Planning Mode

Build And Install

Map A Model

API Lifecycle

Procedure API

Prepared Planning

Synchronization Contract

Restricted Actions And Goal Sets

Incremental Updates

Uncached Planning

Supporting API

Runtime Monitoring

Worked Warehouse Example

1. Install The Schema

2. Load The Manual View

3. Plan Without The Cache

4. Prepare The Cached Model

5. Plan Synchronization From Persisted Witnesses

6. Plan Disambiguation From Persisted Witnesses

7. Explain The Synchronizing Word

8. Monitor Committed Actions And Observations

9. Invalidate Old Plans

10. Prepare And Update Incrementally

Exact Synchronization Example

Restricted And Goal Example

Developer Documentation

About

Topics

Resources

Stars

Watchers

Forks

Releases

Sponsor this project

Contributors

Languages