# Alloy Authors - Practical Alloy - Module system (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article4.6bc1851654a0.png) ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/50948795) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Alloy Authors]] **Full Title**:: Practical Alloy - Module system **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [practicalalloy.github.io](https://practicalalloy.github.io/chapters/structural-topics/topics/modules/index.html) **Host**:: [[practicalalloy.github.io]] **Highlighted**:: [[2025-04-28]] **Created**:: [[2025-05-10]] ## Highlights - To include a module in another model, we must to use an `open` instruction with the path to the corresponding file (without the `.als` extension). ([View Highlight](https://read.readwise.io/read/01jsy0zffnxx5dg61fy40hevda)) ^882995666 - Alloy modules can be declared with signature parameters, that are specified by the including modules. These are declared after its name in the `module` declaration between square brackets. ([View Highlight](https://read.readwise.io/read/01jsy10wgnf8290h15dwsgaj35)) ^882995717 - To avoid using the projected ternary relation, we can derive a binary relation from the auxiliary `aux_time` by declaring an auxiliary function that projects away `TimeAux` ([View Highlight](https://read.readwise.io/read/01jsy19f132srf97h86s5gzh4d)) ^882996335 Functions can be used in dot operator like fields.