total-space

研究通信有限状态机的总状态空间。具体来说，给定由多个代理组成的系统模型，其中每个代理是一个非确定性状态机，它会对时间或收到消息做出某种可能动作的响应，其中每个这样的动作可以改变代理状态并/或向其他代理发送消息；然后此处的代码将生成整个系统的所有可能配置空间，验证模型的完整性，验证每个系统配置以满足额外的任意正确性标准，并以各种方式可视化模型。

安装

要安装

cargo install total-space

使用

要使用此软件，您需要创建自己的主程序

use total_space;

fn main() {
    let arg_matches = total_space::add_clap(
        clap::App::new("...")
        ... add your own command line arguments to control the model ...
    ).get_matches();
    let mut model = ... Use your command line arguments to create the model ...;
    let mut output = BufWriter::new(stdout());
    model.do_clap(&arg_matches, &mut output);
}

当然，关键是创建模型。创建模型后，您将获得一个可执行程序，该程序允许计算模型（即收集模型可以达到的所有可能配置）并从中生成各种输出（统计数据、列表和图表）。

示例

您可以查看API参考以了解特定函数的详细信息。不过，这对于入门没有太大帮助。有关完整简单模型示例，请参阅examples/simple.rs。对于运行各种命令的预期结果，请参阅tests/expected/example_simple。使用GraphViz和PlantUML从dot和uml文件生成svg文件。

话虽如此，为了理解代码，以下内容可能会有所帮助。

概念

• 我们有一个有限集合的代理。

• 每个代理是某种类型的实例。该实例是一个小的无符号整数（0..）。

• 每个代理在整体系统中都有一个索引。该索引是一个小的无符号整数（0..）。

• 代理可能是某些部分代理的容器（也支持一个包含两种部分的代理）。

• 每个代理都有一个状态。同一代理类型的所有实例的状态类型是相同的。

• 代理之间可以发送和接收消息。

• 每个消息都携带一个从源代理到目标代理的负载。

• 消息的交付方式如下

  • 立即 - 在任何非立即消息之前交付。这通常用于模拟容器通过向其发送消息来修改部分的状态。

  • 无序 - 可以以任何顺序交付。

  • 有序 - 只有在交付了来自同一源到同一目标的所有先前发送的消息后，才能交付。

• 消息可以替换（覆盖）来自同一源到同一目标的现有消息。例如，这可以用来模拟写入“邮箱”内存地址，其中写入新消息可能会在交付之前覆盖先前的消息。

• 代理也可以在消息之外触发一个活动。

• 活动携带一个负载，就像它是一个从代理到自身的消息一样。

• 活动在所有消息之前交付。

• 当代理收到一个来自消息或活动的负载时，它会计算一个反应。计算这样的反应是模型的重点。

• 代理在计算反应时只能考虑其自己的状态，除非是容器，它们还可以考虑其部分的状态。

• 反应可能是

  • 忽略 - 负载被丢弃，并且不对系统做出任何其他更改。

  • 延迟 - 代理指示消息仅在它改变其状态后才能交付。只有消息可以被延迟。一个代理需要明确地将它的状态标识为“延迟”，以允许它在那种状态下延迟。这用于在图中突出显示这样的状态。

  • 一个或多个动作。如果有多个动作，这些是可能的替代方案，其中每个都导致不同的可能流程。

• 动作可能

  • 更改状态或代理。这是修改代理的状态的唯一方式。请注意，容器不能直接更改其部分的状态。相反，它们需要发送适当的（通常是立即）消息给它们，这将导致它们改变其状态。

  • 向其他代理发出零个或多个消息。每个代理发送的消息总数可能受到某些限制，这些限制可能因每个实例而异。

• 系统配置是所有代理的所有状态、所有在途的消息以及可选的某些无效条件发生的指示的集合。

• 由于特定的无效代理 状态、消息或活动 负载，或者由于某些组合在某种配置中，可能发生无效条件。

• 动作导致配置之间的转换。

• 代码计算配置的总空间（图）以及连接它们的转换。

验证

代码允许将验证函数应用于每个状态和整体配置。因此，简单地计算总配置空间可以确保任意验证条件。

每个代理中的反应逻辑通常会match其状态和有效负载的一些组合，其中将包括一个捕获所有情况的Reaction::Unexpected子句。因此，计算模型可以验证在不需要看到它的状态下没有接收到意外的消息。

代码还验证每个代理发送的飞行消息数量不超过指定的阈值。这确保没有代理发送无界数量的消息。

此外，代码允许验证从每个配置到初始配置是否存在路径，这确保没有死锁配置或活锁配置的循环。

最后，代码允许生成满足任意条件的转换路径，这些路径可以用来确保感兴趣的任何配置实际上可以从初始配置到达。

确保模型被覆盖的另一种方法是为模型收集覆盖率信息（参见grcov），并查看输出以确保所有代码都已被访问。未覆盖的match子句将表明该特定流程无法从初始配置到达，这可能表明模型中存在错误，或者可能需要一个更简单的模型。

输出

代码允许简单地列出所有配置和转换。这主要用于调试。

此外，代码可以生成两种类型的图表

• 一个GraphViz图表，显示了某个代理的所有状态以及使代理在这些状态之间移动的动作。这用于独立可视化每个代理的行为。

• 一个UML序列图，显示了满足任意条件的配置之间的所有转换，以及满足任意条件的配置之间的最短路径。这用于可视化完整的系统场景。

许可证

total-space在GNU通用公共许可证（版本3.0）下分发。有关详细信息，请参阅LICENSE。