【文件属性】：
文件名称：synchronous-tla-benchmarks:用TLA +编码的同步容错分布式算法
文件大小：57KB
文件格式：ZIP
更新时间：2021-05-27 11:49:08
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)