CONSTANTS
  Idx <- c_Idx
  Ctl <- c_Ctl
  FF = "f"
  NDocs <- c_NDocs
  NCalls = 1
  MaxD = 3
  MODE = "stock"
  IdxHelp = FALSE
SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT TicketOrder
INVARIANT NoBad