mirror of
https://github.com/johndoe6345789/WizardMerge.git
synced 2026-04-25 14:14:59 +00:00
36 lines
1.1 KiB
INI
36 lines
1.1 KiB
INI
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
|