由于网络设备导致的消息重排序等固有非确定性，正确实现Paxos和Raft等分布式算法是出了名的困难。Stateright是一个Rust actor库，旨在通过提供嵌入式模型检查器、探索系统行为的UI（演示）和轻量级actor运行时来解决这个问题。它还包含一个线性化测试器，可以在模型检查器中运行，以提供比Jepsen等类似解决方案更全面的测试覆盖。

入门

1. 请参阅书籍，“使用Stateright构建分布式系统”。
2. 还有视频介绍。
3. Stateright还有详细的API文档。
4. 还可以考虑加入Stateright Discord服务器进行问答或其他反馈。

示例

Stateright包含各种示例，例如单指令Paxos集群和抽象的两阶段提交模型。

传递check CLI参数会导致每个示例使用Stateright的模型检查器进行自我验证

# Two phase commit with 3 resource managers.
cargo run --release --example 2pc check 3
# Paxos cluster with 3 clients.
cargo run --release --example paxos check 3
# Single-copy (unreplicated) register with 3 clients.
cargo run --release --example single-copy-register check 3
# Linearizable distributed register (ABD algorithm) with 2 clients
# assuming ordered channels between actors.
cargo run --release --example linearizable-register check 2 ordered

传递explore CLI参数会导致每个示例在本地端口3000上启动Stateright Explorer Web UI，允许您浏览系统行为

cargo run --release --example 2pc explore
cargo run --release --example paxos explore
cargo run --release --example single-copy-register explore
cargo run --release --example linearizable-register explore

通过 CLI 参数传递 spawn 到使用演员功能的示例，将导致每个示例都使用包含的运行时启动演员，通过 UDP 传输 JSON 消息。

cargo run --release --example paxos spawn
cargo run --release --example single-copy-register spawn
cargo run --release --example linearizable-register spawn

脚本 bench.sh 运行所有示例，并使用各种设置对库的更改对性能影响进行基准测试。

./bench.sh

功能

Stateright 包含一个通用模型检查器，提供以下功能：

• 通过 "always" 属性进行不变性检查。
• 通过 "sometimes" 属性进行非平凡性检查。
• 通过 "eventually" 属性进行活性检查（实验性/不完整）。
• 一个用于交互式探索状态空间的网页浏览器 UI。
• 线性化 和 顺序一致性 测试器。
• 支持对称性减少以减少状态空间。

Stateright 的演员系统功能包括：

• 一个演员运行时，可以在模型检查器之外的真实世界中执行演员。
• 一个用于有损/无损重复/非重复网络的模型，能够捕获演员消息 历史，以检查演员系统与预期一致性模型的一致性。
• 可插拔的网络语义，允许您在更少的假设（例如 "有损无序重复"）和更多的假设（加快模型检查；例如 "无损有序"）之间进行选择。
• 一个可选的网络适配器，为演员之间提供无损失非重复有序虚拟通道的消息。

与其他演员库不同，Stateright 允许您 形式化验证 实现的正确性，并且与 TLC 这样的模型检查器相比，使用 Stateright 实现的系统也可以在真实网络上运行，而无需用其他语言重写。

贡献

欢迎贡献！请 Fork 库，将更改推送到您的 Fork，并发送一个 Pull Request。除非在 Pull Request 中明确说明，否则所有贡献都共享 MIT 许可证。

许可证

Stateright 版权所有 2018 年 Jonathan Nadal 及其他 贡献者。它根据 MIT 许可证提供。

为了避免需要 JavaScript 包管理器，Stateright 仓库包含 Stateright 探索器使用的以下 JavaScript 依赖项的代码：

• KnockoutJS 版权所有 2010 年 Steven Sanderson，Knockout.js 团队及其他贡献者。它根据 MIT 许可证提供。