Dynamic systems and temporal logic

• Readings
  • Recommended readings
• Family model as a transition system

Readings

• Code for the ball example
• Class notes on dynamic models, by C. Tinelli
• Class notes on a dynamic model for a hotel lock system, by C. Tinelli
• Class notes on a dynamic model for a rover, by C. Tinelli

Recommended readings

• Alloy Reference manual
• Alloy 6: It’s about time blog post by Hillel Wayne.
  • The ball example is taken from this post.
• Notes notes on Alloy 6 (aka, Electrum Alloy) by A. Cunha and N. Macedo on
  • Electrum overview
  • First Order Logic
  • Relational Logic
  • Alloy’s type system
  • Relational model finding

Family model as a transition system

We convert the static family model we studied before to a transition system via the use of the temporal operators. The code we built in class is available here