The story revolves around a query to a datastore where you get back a series of records each one containing a name and an array of strings. The strings in the array are supposed to be unique so it's a set in theory - but it ultimately has to represented in JSON so the best we can do is arrays.
We have a description that mentions the name and the collection of strings in some arbitrary order. The software is supposed to react with a true if it can find a record where the name is the same and the array of strings contains the strings mentioned in the description. All the strings must be present and there must be no extras. If this criteria is not met by any record then the software returns false.
The English description takes the various cases in turn - when the datastore returns nothing, when it returns a collection of records where the criteria are met, and where it returns a collection of records where none are met. It would be fairly straightforward to write it out this way I think, using initial guard conditions to describe what comes back from the datastore.
My question is, is there an approach where the datastore could be represented as a set of records and the TLA+ specification be checked against subsets (including the empty set) of the datastore by TLC? Rather than having several main clauses \/d together, there would be just one where the guard condition talks about a subset of the datastore, the particular description and shows what to do in various cases.
If this could be made to work the checking could be made more extensive simply by adding additional records to the datastore set rather than by extending the formulae. It would also allow me to include records that are corrupted (by duplicating supposedly unique strings and so on).
Is this a sensible approach?