# Alloy Authors - Practical Alloy - Model finding (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article4.6bc1851654a0.png) ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/50967961) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Alloy Authors]] **Full Title**:: Practical Alloy - Model finding **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [practicalalloy.github.io](https://practicalalloy.github.io/chapters/structural-topics/topics/model-finding/index.html) **Host**:: [[practicalalloy.github.io]] **Highlighted**:: [[2025-04-29]] **Created**:: [[2025-05-10]] ## Highlights - The Analyzer relies on an intermediate tool to perform relational model finding named Kodkod [[FSE04]](https://practicalalloy.github.io/bibliography.html#fse04). ([View Highlight](https://read.readwise.io/read/01jszeg63jmbpr4xx8h5bqh5td)) ^883257392 FSE04: Jonathan Edwards, Daniel Jackson, Emina Torlak: A Type System for Object Models. In proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE): 189-199. ACM, 2004. - For `check` commands, the expected property is negated so that Kodkod will search for counter-examples, i.e., instances that obey all the model’s constraints but break the expected property. ([View Highlight](https://read.readwise.io/read/01jszej5vsyh07t90rkm2gnppg)) ^883257439 - You can actually inspect the generated Kodkod problem by setting menu option Options ‣ Record the Kodkod input/output to Yes. ([View Highlight](https://read.readwise.io/read/01jszem22d1e5kz9kqs380r1s5)) ^883257627 - Finally, first-order operators are translated into propositional logic, which is possible because at this point the finite universe of atoms is known. So universal quantifications `all` are flattened into conjunctions and existential `some` into disjunctions. ([View Highlight](https://read.readwise.io/read/01jszepnv4emdr3gnwka6k5wde)) ^883257673 - Before deploying the solver, Kodkod performs a process called *Skolemization* whenever outermost existential quantifications occur in `run` commands (or universal quantifications for `check` commands). ([View Highlight](https://read.readwise.io/read/01jszeraswnt72bjmr3m3h9s36)) ^883257724