Exercises and Examples

All files below are in either html or PDF format.

Exercises

1. Sets and relations
2. Introduction to Alloy
3. Modeling Using Alloy
4. Dynamic Models and Operations
5. Alloy Mutability Qualifiers
6. Alloy case study
   Transcribe the Alloy model described in [Khu00] from the readings and feed it into the ACA, trying to reproduce by yourself the results described in [Khu00]. Then modify the definition of the model as discussed in class and evaluate the correctness of the changes.
7. USE tool demo
8. More OCL
9. Validating pre- and post-conditions with USE

Examples

1. Family I (Alloy)
   • family-1.all
   • family-2.all
   • family-3.all
   • family-4.all
   
   
2. Academia (Alloy)
   • academia-1.all
   • academia-2.all
   • academia-3.all
   
   
3. Airport I (Alloy)
   • airport-1.all
   • airport-2.all
   • airport-3.all
   • airport-4.all
   
   
4. Family II (Alloy)
   • family-5.all
   • family-6.all
   • family-7.all
   • family-8.all
   
   
5. Airport II (Alloy)
   • airport-5.all
   • airport-6.all
   • airport-7.all
   
   
6. Family (USE)
   • family-1.use
   • family-2.use
   • family-3.use
   
   
7. Academia I (USE)
   • academia-1.use
   • academia-2.use
   • academia-3.use
   • academia-basic-instantiation.cmd
   
   
8. Academia II (USE)
   • academia-4.use
   • academia-5.use
   • academia-6.use
   • academia-extension1-instantiation.cmd
   • academia-extension2-instantiation.cmd
   
   
9. Transitive Closure (USE)
   • transitive-closure-1.use
   • transitive-closure-instantiation-1.cmd
   • transitive-closure-2.use
   • transitive-closure-instantiation-2.cmd
   
   
10. Academia III (USE)
    • academia-7.use
    • academia-8.use
    • academia-9.use
    • academia-extension4-instantiation.cmd