Alloy and Alloy* are used as specification languages, not constraint solvers. There are different speclangs with different specialties, and Alloy is particularl

Alloy and Alloy* are used as specification languages, not constraint solvers. There are different speclangs with different specialties, and Alloy is particularly good at domain modeling. Here's an example of an early draft of a spec I've been working on; I'm mostly doing this from memory so there might be some errors. We have organizations that are being billed. Each bill consists of one or more items, each of which has a vendor that supplied that has to be paid. sig Org {} sig Bill { , client: Org // exactly one , item: some Item // one or more } sig Item { , vendor: Org } If I then generate models, I'll immediately see some weird things. First, multiple bills can share the same item. Second, a bill can have an item that is the same as the client. Whether we want to do the former or not depends on what we're modeling: standardized items or _specific_ instances of an item. Let's assume the former, in which case we're fine with it. The latter is something we never want, but can also guarantee never happens. We'll add a fact showing that. fact "orgs can't bill themselves" { all b: Bill | no i: b.item | i.vendor = b.client } Part two: some items have bills of their own. If you have a line for "labwork", the vendor doing the labwork has their own corresponding items they have to pay to do the labwork. But not all items do. sig Item { , vendor: Org , bill: lone Bill //lone means "optional" } But now the models go crazy! They raise all sorts of weird cases: * We're very clearly mixing "items as an abstract thing" with "bills as a concrete instance" (as they map to the paying org). We need to fix the difference in conceptual levels here. * What if the vendor of an item is different from the client of the bill? This is probably an inconsistency we should avoid in practice. * Can two items share the same bill? Maybe! We can't rule this out. * Should an item be part of its own bill? Almost certainly not. * We can have an organization O be billed by a vendor V for an item I with a corresponding bill that has O as a vendor! O is getting billed for something they themselves are making money off. This happens all the time in reality and we definitely have to permit it in our model. After figuring these out we might want to make it even more complex, like having different types of items or disjoint vendor possibilities or make the system dynamic or whatever. But the key thing here is we can explore all of the consequences of the data model without having to run into the issues in production first.