Git Product home page Git Product logo

itf-rs's Introduction

API Documentation Build Status codecov Apache 2.0 Licensed Rust Stable Rust 1.65+

itf-rs

Rust library for consuming Apalache ITF Traces.

API Documentation

The API documentation is available on docs.rs.

Example

Trace: 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);

Output:

[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: {},
                },
            },
        },
    ],
}

Versioning

We follow Semantic Versioning, though APIs are still under active development.

Resources

License

Copyright © 2023 Informal Systems Inc. and itf-rs authors.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use the files in this repository except in compliance with the License. You may obtain a copy of the License at

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

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

itf-rs's People

Contributors

rnbguy avatar romac avatar

Stargazers

avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar

Forkers

rnbguy

itf-rs's Issues

Re-export `serde_with::Same`

Since we re-export serde_with::As, it would make sense to add serde_with::Same also - for the same level of convenience.

With Same, the As::<...> strings can be simplified.

#[derive(Deserialize)]
struct Foo {
  // instead of "As::<Hashmap<Integer, (String, String)>>"
  #[serde(with = "As::<Hashmap<Integer, Same>>")
  bar: Hasmap<i64, (String, String)>
}

Support traces with sum types

Since v0.17, Quint supports sum types, which are encoded in a specific way in ITF trace files. For example, for

type T = None | Some(int)
var x: T

variable x will be appear in traces as {"tag": "None", value: {}} or {"tag": "Some", value: 123}.

Add derive support for actions 

type Balance = HashMap<String, BigInt>;
type Balances = HashMap<String, Balance>;

#[derive(Copy, Clone, Debug, DecodeItfValue)]
enum Outcome {
    #[itf(rename = "")]
    None,
    #[itf(rename = "SUCCESS")]
    Success,
    #[itf(rename = "DUPLICATE_DENOM")]
    DuplicateDenom,
    #[itf(rename = "INSUFFICIENT_FUNDS")]
    InsufficientFunds,
}

#[derive(Clone, Debug, DecodeItfValue)]
#[allow(dead_code)]
struct Coin {
    amount: BigInt,
    denom: String,
}

#[derive(Clone, Debug, DecodeItfValue)]
#[allow(dead_code)]
#[itf(tag = "tag")]
enum Action {
    #[itf(rename = "init")]
    Init { balances: Balances },

    #[itf(rename = "send")]
    Send {
        receiver: String,
        sender: String,
        coins: Vec<Coin>,
    },
}

#[derive(Clone, Debug, TryFromRawState)]
#[allow(dead_code)]
struct State {
    action: Action,
    outcome: Outcome,
    balances: Balances,
    step: i64,
}

let data = include_str!("../tests/fixtures/TestInsufficientSuccess9.itf.json");
let raw_trace: raw::Trace = serde_json::from_str(data).unwrap();
let trace = parse_raw_trace::<State>(raw_trace).unwrap();
dbg!(trace);

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.