-
Notifications
You must be signed in to change notification settings - Fork 0
By Language
Models in the Alloy specification language. Tested under the Alloy Analyzer 4.2. Both models and running instructions are contained in .als files, usually accompanied by .thm files for improved visualization.
- Elevator system SPL
- Fox, goose and bag of beans puzzle
- Hotel room locking system (fixed configurations)
- Hotel room locking system (free configurations)
- Hybrid ERTMS/ETCS Level 3
- I am my own grandpa (Alloy)
- Least-change lenses specification
- OLAP Cube usage preferences
- Object-relational mapping (with associations/keys)
- Object-relational mapping (without associations/keys)
- PTCRISync synchronization framework
- Ring leader election algorithm
- SPL development (minimal)
- Slowly changing dimension ETL pattern
- Spanning tree algorithm
Models in the B specification language. Tested under the ProB 1.5. Models are encoded in .mch files.
- Company human resources synchronization (minimal)
- Expand/collapse hierarchical state machines
- Object-relational mapping (with associations/keys)
- Object-relational mapping (without associations/keys)
- SPL development (minimal)
Models in the Electrum specification language. Tested under the Electrum Analyzer 1.1. Both models and running instructions are contained in .ele files, usually accompanied by .thm files for improved visualization.
- Elevator system SPL
- Fox, goose and bag of beans puzzle
- Hotel room locking system (free configurations)
- Hybrid ERTMS/ETCS Level 3
- Ring leader election algorithm
- Spanning tree algorithm
- Expand/collapse hierarchical state machines
- Object-relational mapping (with associations/keys)
- Object-relational mapping (without associations/keys)
- SPL development (minimal)
Models for the NuSMV model checker, an extension to the SMV symbolic model checker based on BDDs. Tested under NuSMV 2.5 (and nuXmv 1.0). Models and specifications are contained in .smv files, and in general can be verified in batch mode (every specification is checked).
- Fox, goose and bag of beans puzzle
- Heavy chair problem
- Peterson's mutual exclusion algorithm
- Ring leader election algorithm
Models in the TLA+ specification language. Unless otherwise stated, models are tested under the model checker TLC 2.07 (and TLA Toolbox 1.5.1). Models and specifications are contained in .tla files, accompanied by .cfg configuration files that provide verification instructions to TLC or .toolbox directories for the Toolbox.