Who imports it? Four workbooks that keep the answer, from US customs records

```tables
{
  "tables": [
    {
      "name": "importers",
      "tab": "Importers",
      "key": [
        "importer"
      ],
      "columns": [
        {
          "name": "rank",
          "type": "integer",
          "required": true,
          "unique": true,
          "min": 1
        },
        {
          "name": "importer",
          "required": true,
          "unique": true
        },
        {
          "name": "hs code",
          "required": true,
          "pattern": "^[0-9]{4}(\\.[0-9]{2}){0,3}$"
        },
        {
          "name": "shipments",
          "type": "integer",
          "required": true,
          "min": 0
        },
        {
          "name": "ships from",
          "type": "list",
          "separator": ", "
        },
        {
          "name": "kind",
          "type": "choice",
          "values": [
            "buyer",
            "forwarder",
            "unsure"
          ],
          "required": true
        },
        {
          "name": "status",
          "type": "choice",
          "values": [
            "new",
            "contacted",
            "replied",
            "meeting",
            "won",
            "not a fit"
          ],
          "required": true
        }
      ]
    }
  ]
}
```

```tla
---- MODULE Business ----
EXTENDS Workbook, Naturals, Sequences
VARIABLE ok
Init == ok = TRUE
Next == UNCHANGED ok
Spec == Init /\ [][Next]_ok
\* The ranking reads top down: rank 1, 2, 3 ... with no gap.
RanksInOrder == \A i \in DOMAIN importers : importers[i].rank = i
\* More shipments never sit below fewer.
ByShipments == \A i \in 1..(Len(importers) - 1) :
                  importers[i].shipments >= importers[i + 1].shipments
\* A forwarder carries someone else's goods: it is never worked as a lead.
ForwardersAreNotLeads == \A i \in DOMAIN importers :
                  importers[i].kind = "forwarder" => importers[i].status = "not a fit"
====
```

```cfg
SPECIFICATION Spec
INVARIANT RanksInOrder
INVARIANT ByShipments
INVARIANT ForwardersAreNotLeads
```

```tables
{
  "tables": [
    {
      "name": "watch",
      "tab": "Watch",
      "key": [
        "importer",
        "bill of lading"
      ],
      "columns": [
        {
          "name": "importer",
          "required": true
        },
        {
          "name": "bill of lading",
          "required": true,
          "unique": true
        },
        {
          "name": "arrived",
          "type": "date",
          "required": true
        },
        {
          "name": "hs code",
          "required": true,
          "pattern": "^[0-9]{4,10}$"
        },
        {
          "name": "supplier",
          "required": true
        },
        {
          "name": "origin",
          "required": true,
          "pattern": "^[A-Z]{2}$"
        },
        {
          "name": "switched",
          "type": "boolean",
          "required": true
        }
      ]
    }
  ]
}
```

```tla
---- MODULE Business ----
EXTENDS Workbook, Naturals, Sequences
VARIABLE ok
Init == ok = TRUE
Next == UNCHANGED ok
Spec == Init /\ [][Next]_ok
\* Bills are kept oldest first, one importer at a time.
InOrder == \A i \in 1..(Len(watch) - 1) :
             watch[i].importer = watch[i + 1].importer => watch[i].arrived <= watch[i + 1].arrived
\* "switched" is not an opinion: it says whether this bill's origin differs
\* from the same importer's bill before it.
SwitchedMeansNewOrigin == \A i \in DOMAIN watch :
    watch[i].switched =
      (\E j \in DOMAIN watch : j = i - 1 /\ watch[j].importer = watch[i].importer
                               /\ watch[j].origin /= watch[i].origin)
====
```

```cfg
SPECIFICATION Spec
INVARIANT InOrder
INVARIANT SwitchedMeansNewOrigin
```

```tables
{
  "tables": [
    {
      "name": "customers",
      "tab": "Customers",
      "key": [
        "exporter",
        "customer"
      ],
      "columns": [
        {
          "name": "exporter",
          "required": true
        },
        {
          "name": "customer",
          "required": true
        },
        {
          "name": "customer city"
        },
        {
          "name": "first seen",
          "type": "date",
          "required": true
        },
        {
          "name": "last seen",
          "type": "date",
          "required": true
        },
        {
          "name": "shipments",
          "type": "integer",
          "required": true,
          "min": 1
        }
      ]
    }
  ]
}
```

```tla
---- MODULE Business ----
EXTENDS Workbook, Naturals, Sequences
VARIABLE ok
Init == ok = TRUE
Next == UNCHANGED ok
Spec == Init /\ [][Next]_ok
\* A customer is first seen no later than it is last seen.
SeenInOrder == \A i \in DOMAIN customers : customers[i].first_seen <= customers[i].last_seen
\* One shipment can only have been seen on one day.
OneShipmentOneDay == \A i \in DOMAIN customers :
    customers[i].shipments = 1 => customers[i].first_seen = customers[i].last_seen
====
```

```cfg
SPECIFICATION Spec
INVARIANT SeenInOrder
INVARIANT OneShipmentOneDay
```

```tables
{
  "tables": [
    {
      "name": "outreach",
      "tab": "Outreach",
      "key": [
        "importer"
      ],
      "columns": [
        {
          "name": "importer",
          "required": true,
          "unique": true
        },
        {
          "name": "why them",
          "required": true
        },
        {
          "name": "stage",
          "type": "choice",
          "values": [
            "new",
            "contacted",
            "replied",
            "meeting",
            "won",
            "lost"
          ],
          "required": true
        },
        {
          "name": "contacted on",
          "type": "date"
        },
        {
          "name": "replied on",
          "type": "date"
        },
        {
          "name": "source",
          "type": "url",
          "required": true
        }
      ]
    }
  ]
}
```

```tla
---- MODULE Business ----
EXTENDS Workbook, Naturals, Sequences
VARIABLE ok
Init == ok = TRUE
Next == UNCHANGED ok
Spec == Init /\ [][Next]_ok
Past(s) == s \in {"contacted", "replied", "meeting", "won", "lost"}
Answered(s) == s \in {"replied", "meeting", "won"}
\* A stage past "new" says when the importer was contacted.
ContactedHasADate == \A i \in DOMAIN outreach :
    Past(outreach[i].stage) <=> outreach[i].contacted_on /= ""
\* A reply has a date, and it comes after the contact.
RepliesFollowContact == \A i \in DOMAIN outreach :
    Answered(outreach[i].stage) =>
      /\ outreach[i].replied_on /= ""
      /\ outreach[i].replied_on >= outreach[i].contacted_on
====
```

```cfg
SPECIFICATION Spec
INVARIANT ContactedHasADate
INVARIANT RepliesFollowContact
```