Files

networkModels

fixed some obsolete proof sessions

Apr 17, 2024

fa7cdac · Apr 17, 2024

Name		Name	Last commit message	Last commit date
parent directory ..
modelMP		modelMP	fixed some obsolete proof sessions	Apr 17, 2024
modelMPEnabledTrace		modelMPEnabledTrace	fixed some obsolete proof sessions	Apr 17, 2024
modelMPEnabledTraceDupl		modelMPEnabledTraceDupl	fixed some obsolete proof sessions	Apr 17, 2024
README.md		README.md	added atomic Bakery algorithm	Apr 7, 2023
modelMP.mlw		modelMP.mlw	added network semantics models and two examples from ESOP22 paper (Ch…	Mar 16, 2023
modelMPEnabledTrace.mlw		modelMPEnabledTrace.mlw	added network semantics models and two examples from ESOP22 paper (Ch…	Mar 16, 2023
modelMPEnabledTraceDupl.mlw		modelMPEnabledTraceDupl.mlw	added network semantics models and two examples from ESOP22 paper (Ch…	Mar 16, 2023

README.md

Network Models

Library modules for reasoning about distributed systems with different network semantics. Described in the ESOP'2022 paper "Why3-do: The Way of Harmonious Distributed System Proofs".

Files

modelMP.mlw: message-passing network. No packet losses or duplications but random order of delivery
modelMPEnabledTrace.mlw: idealized message-passing with traces and enabling conditions
modelMPEnabledDupl.mlw: duplicating message-passing, with traces and enabling conditions