| Model | Description | Section |
|---|---|---|
| checkpoint-final-global.promela | Promela model of the final checkpoint protocol, with asymmetric procedure rules. Developed to work around a safety error in the original protocol. | 4.2.2 |
| checkpoint-final-global.promela.liveness.ltl | LTL liveness claim for the final checkpoint protocol model. | 4.2.2 |
| checkpoint-final-global.promela.safety.ltl | LTL safety claim for the final checkpoint protocol model. | 4.2.2 |
| checkpoint-initial-global.promela | Promela model of the initial checkpoint protocol, found in the proof-of-concept session layer implementation. Symmetric procedure rules. Violates both the safety and liveness claims below. | 4.2.3 |
| checkpoint-initial-global.promela.liveness.ltl | LTL liveness claim for the initial checkpoint protocol model. | 4.2.3 |
| checkpoint-initial-global.promela.safety.ltl | LTL safety claim for the initial checkpoint protocol model. | 4.2.3 |
| peterson.promela | Promela model of Peterson's mutual exclusion algorithm. | 2.3.5, 2.5.4 |
| peterson.promela.ltl | LTL correctness claim for the model of Peterson's algorithm. | 2.4.3, 2.5.4 |
| smp-liveness-synchronous-suspend-fix-fail.promela | Variant of the main the main Promela SMP liveness models, where failures to send control messages occur completely nondeterministically. | |
| smp-liveness-synchronous-suspend-fix.promela | The main Promela SMP liveness model. | 4.3.3 |
| smp-liveness-synchronous-suspend.promela | Incomplete Promela SMP liveness model which has deadlocks. | 4.3.3 |
| smp-safety-synchronous-fail.promela | Alternative Promela SMP safety model, where failures to send control messages occur completely nondeterministically. | 4.3.2 |
| smp-safety-synchronous.promela | The main Promela SMP safety model. | 4.3.2 |