Don’t let Alloy facts make your specs a fiction.
I’ve recently done a lot of work in Alloy and it’s got me thinking about a common specification pitfall. Everything in the main post applies to all formal specifications, everything in dropdowns is for experienced Alloy users.
Consider a simple model of a dependency tree. We have a set of top-level dependencies for our program, which have their own dependencies, etc. We can model it this way in Alloy:

Read in full here:

This thread was posted by one of our members via one of our news source trackers.