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

Structural modelling advanced topics¶

This chapter presents some advanced topics relevant for structural modelling. These topics build on the file system example model of the Structural 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/structural-modeling/verifying-assertions
Next
Subset signatures
Previous
Structural modeling
Copyright © 2021-2025, Alcino Cunha, Nuno Macedo, Julien Brunel, David Chemouil
Made with Sphinx and @pradyunsg's Furo
Last updated on Feb 16, 2025