SPECIFICATION Spec

\* This configuration file verifies that the WizardMergeSpec is syntactically
\* correct and that its invariants are well-formed. The spec uses many
\* CONSTANT declarations that would require a full instantiation to model-check
\* meaningful behaviors. For CI purposes, we verify:
\* 1. The spec parses correctly
\* 2. The invariants are well-defined
\* 3. The temporal structure is valid

\* Declare model values for the basic version constants
CONSTANT Base = Base
CONSTANT VA = VA
CONSTANT VB = VB

\* For the remaining constants, we provide minimal empty/singleton sets
\* This satisfies the type requirements while keeping the state space trivial
CONSTANT VERTICES = {}
CONSTANT EDGES = {}
CONSTANT VersionTag = <<>>
CONSTANT Mirror = <<>>
CONSTANT MatchSet = {}
CONSTANT AppliedSet = {}
CONSTANT ConflictSet = {}

\* PR/MR constants
CONSTANT GitPlatform = "GitHub"
CONSTANT PR_FILES = {}
CONSTANT FileStatus = <<>>
CONSTANT BaseSHA = "base"
CONSTANT HeadSHA = "head"

\* Check that the invariants are well-formed
\* With empty sets, these should trivially hold
INVARIANT Inv