Check with Apalache model-checker #2
Description
Related: apalache-mc/apalache#1412 (workaround: INSTANCE)
Type annotation general-model/cosmos_client.tla:
defines
- SetMax -> FiniteSetsExt!Max
- SeqToSet -> Functions!Range
- Last -> SequencesExt!Last
- RemoveDuplicates -> ???
- MaxLen & MinLen are not used/dead "code"