I was asked:
> In the alloy section, are we to make assumptions on when certain things exist as well
For this question, you *must* declare entities to represent contracts, formulas, and
You *may* declare other entities if you need to.
You shouldn't need to assume the existence of any entities, though - if you think you
need to, try simplifying what you're modelling.
Remember that a model doesn't need to incorporate *every* detail of the original - just
enough to adequately model the relations between things. If you think you need some
datatype we haven't covered - ask yourself whether a simpler data-type would do instead.
Hopefully that helps.