文件名称：用于实现分布式系统的模型检查器。
文件大小：260KB
文件格式：ZIP
更新时间：2024-07-18 13:24:06
distributed-systems actor-model paxos model-checker
由于固有的不确定性（例如网络设备对消息重新排序），正确实现分布式算法（例如Paxos和Raft共识协议）非常困难。Stateright 是一个Rust actor 库，旨在通过提供一个嵌入式模型检查器、一个用于探索系统行为的 UI（演示）和一个轻量级 actor 运行时来解决这个问题。它还具有可在模型检查器中运行的线性化测试器，以获得比Jepsen等类似解决方案更详尽的测试覆盖率。入门请参阅“使用 Stateright 构建分布式系统”一书。还提供视频介绍。Stateright 也有详细的API 文档。还可以考虑加入Stateright Discord 服务器进行问答或其他反馈。 例子Stateright 包括各种示例，例如Single Decree Paxos 集群和抽象的两阶段提交模型。传递check CLI 参数会导致每个示例使用 Stateright 的模型检查器验证自身：# Two phase commit with 3 resource managers. cargo run --release --example 2pc check 3# Paxos cluster w
【文件预览】：
stateright-master
----.gitignore(35B)
----bench.sh(586B)
----src()
--------actor.rs(16KB)
--------test_util.rs(5KB)
--------checker()
--------checker.rs(19KB)
--------util()
--------semantics.rs(5KB)
--------util.rs(11KB)
--------semantics()
--------actor()
--------lib.rs(13KB)
----LICENSE(1KB)
----Cargo.toml(825B)
----ui()
--------app.js(8KB)
--------index.htm(5KB)
--------app.css(3KB)
--------knockout-3.5.0.LICENSE(1KB)
--------knockout-3.5.0.js(66KB)
----explorer.png(153KB)
----.github()
--------workflows()
----examples()
--------paxos.rs(16KB)
--------single-copy-register.rs(7KB)
--------2pc.rs(6KB)
--------linearizable-register.rs(14KB)
----README.md(6KB)
----CHANGES.md(6KB)