itf 0.4.0

Library for consuming Apalache ITF traces
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

#![allow(dead_code)]

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

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>>,
}

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

    dbg!(trace);
}