export const PROPERTY_INVARIANT_CLASSES = [
  "conservation",
  "nonnegative-bounds",
  "reversal-bounded",
  "legal-transitions",
  "ownership-tenant-isolation",
  "referential-lifecycle-integrity",
  "effect-multiplicity",
  "monotonic-versions-ordering",
] as const;

export type PropertyInvariantClass = (typeof PROPERTY_INVARIANT_CLASSES)[number];

export type PropertyExecutionRecord = {
  generatedInput: unknown;
  initialState: unknown;
  actionSequence: unknown[];
  finalState: unknown;
  seed: number;
  shrinkPath: string | null;
  minimalCounterexample: unknown;
};

export type PropertyInvariantResult = {
  id: string;
  invariantClass: PropertyInvariantClass;
  holds: boolean;
  executionRecord: PropertyExecutionRecord;
  error?: string;
};

export type StateMachineTransitionMode = "legal" | "illegal";

export type StateMachineInvariantResult = PropertyInvariantResult & {
  transitionMode: StateMachineTransitionMode;
  rejectedCommandCount?: number;
};