文件名称：synchronous-tla-benchmarks:用TLA +编码的同步容错分布式算法
文件大小：57KB
文件格式：ZIP
更新时间：2024-06-16 05:35:48
TLA
同步tla基准 编码的几种同步容错分布式算法。 在以下中，使用模型检查器检查了这些基准： Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger. Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. VMCAI 2018 该存储库包含以下基准： 名称 问题 参考 早期决定共识 共识 ，第17页 k集协议，对于k = 1 ，第136页 k-set协议，对于k = 2 ，第136页 共识 ，第103页 非阻塞原子提交 ，第82页 pdif 尽早停止共识 Raynal ，第38页 所有基准均假定为崩溃故障模型，系统中最多N个进程中的T个最多可能因崩溃而失败，且T
【文件预览】：
synchronous-tla-benchmarks-master
----pdif()
--------pdif_abstract.tla(12KB)
--------pdif.tla(4KB)
--------pdif_abstract_m1.tla(12KB)
----floodmin_k2()
--------floodmin_k2_abstract_m2.tla(9KB)
--------floodmin_k2.tla(3KB)
--------floodmin_k2_abstract.tla(10KB)
--------floodmin_k2_abstract_m1.tla(9KB)
----edac()
--------edac_abstract.tla(13KB)
--------edac.tla(4KB)
--------edac_abstract_m1.tla(12KB)
----floodset()
--------floodset_abstract_m1.tla(9KB)
--------floodset.tla(3KB)
--------floodset_abstract.tla(10KB)
----LICENSE(588B)
----nbac()
--------nbac_abstract_m1.tla(10KB)
--------nbac.tla(4KB)
--------nbac_abstract.tla(11KB)
----README.md(3KB)
----floodmin_k1()
--------floodmin_k1.tla(3KB)
--------floodmin_k1_abstract_m1.tla(8KB)
--------floodmin_k1_abstract.tla(9KB)
----fair_cons()
--------fair_cons_abstract_m1.tla(9KB)
--------fair_cons.tla(3KB)
--------fair_cons_abstract.tla(9KB)