itf-rs

Rust库，用于消费Apalache ITF跟踪。

API文档

API文档可在docs.rs上找到。

示例

跟踪： MissionariesAndCannibals.itf.json

use std::collections::{BTreeSet, BTreeMap};

use serde::Deserialize;

#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Bank {
    #[serde(rename = "N")]
    North,

    #[serde(rename = "W")]
    West,

    #[serde(rename = "E")]
    East,

    #[serde(rename = "S")]
    South,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Person {
    #[serde(rename = "c1_OF_PERSON")]
    Cannibal1,

    #[serde(rename = "c2_OF_PERSON")]
    Cannibal2,

    #[serde(rename = "m1_OF_PERSON")]
    Missionary1,

    #[serde(rename = "m2_OF_PERSON")]
    Missionary2,
}

#[derive(Clone, Debug, Deserialize)]
struct State {
    pub bank_of_boat: Bank,
    pub who_is_on_bank: BTreeMap<Bank, BTreeSet<Person>>,
}

let data = include_str!("../tests/fixtures/MissionariesAndCannibals.itf.json");
let trace: itf::Trace<State> = itf::trace_from_str(data).unwrap();

dbg!(trace);

输出

[itf/examples/cannibals.rs:45] trace = Trace {
    meta: Meta {
        format: None,
        format_description: None,
        source: Some(
            "MC_MissionariesAndCannibalsTyped.tla",
        ),
        description: None,
        var_types: {
            "bank_of_boat": "Str",
            "who_is_on_bank": "Str -> Set(PERSON)",
        },
        timestamp: None,
        other: {},
    },
    params: [],
    vars: [
        "bank_of_boat",
        "who_is_on_bank",
    ],
    loop_index: None,
    states: [
        State {
            meta: Meta {
                index: Some(
                    0,
                ),
                other: {},
            },
            value: State {
                bank_of_boat: East,
                who_is_on_bank: {
                    West: {},
                    East: {
                        Cannibal1,
                        Cannibal2,
                        Missionary1,
                        Missionary2,
                    },
                },
            },
        },
        State {
            meta: Meta {
                index: Some(
                    1,
                ),
                other: {},
            },
            value: State {
                bank_of_boat: West,
                who_is_on_bank: {
                    West: {
                        Cannibal2,
                        Missionary2,
                    },
                    East: {
                        Cannibal1,
                        Missionary1,
                    },
                },
            },
        },
        State {
            meta: Meta {
                index: Some(
                    2,
                ),
                other: {},
            },
            value: State {
                bank_of_boat: East,
                who_is_on_bank: {
                    West: {
                        Cannibal2,
                    },
                    East: {
                        Cannibal1,
                        Missionary1,
                        Missionary2,
                    },
                },
            },
        },
        State {
            meta: Meta {
                index: Some(
                    3,
                ),
                other: {},
            },
            value: State {
                bank_of_boat: West,
                who_is_on_bank: {
                    West: {
                        Cannibal2,
                        Missionary1,
                        Missionary2,
                    },
                    East: {
                        Cannibal1,
                    },
                },
            },
        },
        State {
            meta: Meta {
                index: Some(
                    4,
                ),
                other: {},
            },
            value: State {
                bank_of_boat: East,
                who_is_on_bank: {
                    West: {
                        Missionary1,
                        Missionary2,
                    },
                    East: {
                        Cannibal1,
                        Cannibal2,
                    },
                },
            },
        },
        State {
            meta: Meta {
                index: Some(
                    5,
                ),
                other: {},
            },
            value: State {
                bank_of_boat: West,
                who_is_on_bank: {
                    West: {
                        Cannibal1,
                        Cannibal2,
                        Missionary1,
                        Missionary2,
                    },
                    East: {},
                },
            },
        },
    ],
}

版本控制

我们遵循语义版本控制，尽管API仍在积极开发中。

资源

• Apalache网站
• Apalache ADR-015：非正式跟踪格式

许可证

版权 © 2023 Informal Systems Inc. 和 itf-rs 作者。

根据Apache许可证版本2.0（“许可证”）许可；除非适用法律要求或书面同意，否则不得使用此存储库中的文件，除非遵守许可证。您可以在以下位置获取许可证副本：

https://www.apache.org/licenses/LICENSE-2.0

除非适用法律要求或书面同意，否则在许可证下分发的软件按“原样”基础分发，不提供任何明示或暗示的保证或条件。有关许可证的具体语言、许可权限和限制，请参阅许可证。