Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
Practical Alloy
Practical Alloy

Preface

  • About Alloy
  • About this book

The Basics

  • Structural modeling
  • Advanced topics
    • Subset signatures
    • Enumeration signatures
    • Commands in detail
    • Visualization customization
    • Higher-arity relations
    • The instance evaluator
    • Arrow multiplicity constraints
    • Type system
    • Module system
    • The predefined ordering module
    • A relational logic primer
    • Model finding
    • Encoding test instances
    • Handling recursion
    • Working with integers
    • Signature facts
  • Behavioral modeling
  • Advanced topics
    • A temporal logic primer
    • Mutable top-level signatures
    • Pointwise effects
    • Macro system
    • Meta-capabilities
    • An idiom for event depiction
    • Encoding trace scenarios
    • The trace evaluator
    • Safety, liveness, and fairness
    • Inductive invariants
    • Sequences

Applications

  • Protocol design

Resources

  • Bibliography
  • Index
Back to top
View this page

Behavioral modelling advanced topics¶

This chapter presents some advanced topics relevant for behavioral modelling. These topics build on the file sharing app example model of the Behavioral modeling chapter.

Alloy model

Base model for the topics

Download and explore the base model that will be used for the advanced topics.

https://github.com/practicalalloy/models/tree/2024-02-28/behavioral-modeling/verifying-expected-properties
Next
A temporal logic primer
Previous
Behavioral modeling
Copyright © 2021-2025, Alcino Cunha, Nuno Macedo, Julien Brunel, David Chemouil
Made with Sphinx and @pradyunsg's Furo
Last updated on Feb 27, 2025