Skip to content

Commit

Permalink
Use a custom deserializer instead of wrapper types (#6)
Browse files Browse the repository at this point in the history
  • Loading branch information
romac authored Nov 21, 2023
2 parents 59ccf78 + e2aef1c commit 9902045
Show file tree
Hide file tree
Showing 30 changed files with 3,943 additions and 1,166 deletions.
24 changes: 23 additions & 1 deletion .codecov.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,26 @@
codecov:
require_ci_to_pass: yes
bot: romac

coverage:
precision: 2
round: nearest
range: "50...100"

status:
project:
default:
target: auto
threshold: 5%
removed_code_behavior: adjust_base
paths:
- "itf"
patch:
default:
target: auto
threshold: 5%
paths:
- "itf"

changes:
default:
informational: true
30 changes: 20 additions & 10 deletions .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
@@ -1,31 +1,41 @@
name: Coverage

on:
pull_request:
push:
branches: main
paths:
- itf/**
pull_request:
paths:
- itf/**

jobs:
coverage:
runs-on: ubuntu-latest
defaults:
run:
working-directory: itf
env:
CARGO_TERM_COLOR: always
steps:
- uses: actions/checkout@v3
- name: Install Rust
uses: actions-rs/toolchain@v1
- name: Checkout
uses: actions/checkout@v4
- name: Setup Rust toolchain
uses: actions-rust-lang/setup-rust-toolchain@v1
with:
toolchain: stable
override: true
toolchain: nightly
components: llvm-tools-preview
- name: Install cargo-nextest
uses: taiki-e/install-action@cargo-nextest
- name: Install cargo-llvm-cov
uses: taiki-e/install-action@cargo-llvm-cov
- name: Install cargo-nextest
uses: taiki-e/install-action@nextest
- name: Generate code coverage
run: cargo llvm-cov nextest --all-features --workspace --lcov --output-path lcov.info
- name: Generate text report
run: cargo llvm-cov report
- name: Upload coverage to Codecov
uses: codecov/codecov-action@v3
with:
token: ${{ secrets.CODECOV_TOKEN }} # not required for public repos
files: lcov.info
token: ${{ secrets.CODECOV_TOKEN }}
files: itf/lcov.info
fail_ci_if_error: true
10 changes: 10 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,21 @@
# CHANGELOG

## Unreleased

- Deserialize ITF values into native Rust types with a custom deserializer
instead of having to go through `Itf<A>` wrapper type.
([#6](https://github.com/informalsystems/itf-rs/pull/6))

## v0.1.2

*November 10th, 2023*

- Add `From<T> where T: From<BigInt>` instance for `ItfBigInt`

## v0.1.1

*November 10th, 2023*

- Add support for new `timestamp` field in meta section of ITF traces

## v0.1
Expand Down
61 changes: 32 additions & 29 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,11 @@ Rust library for consuming [Apalache ITF Traces][itf-adr].
**Trace:** [`MissionariesAndCannibals.itf.json`](./apalache-itf/tests/fixtures/MissionariesAndCannibals.itf.json)

```rust
use serde::Deserialize;
use std::collections::{BTreeSet, BTreeMap};

use itf::{trace_from_str, ItfMap, ItfSet};
use serde::Deserialize;

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize)]
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Bank {
#[serde(rename = "N")]
North,
Expand All @@ -33,7 +33,7 @@ enum Bank {
South,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize)]
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Person {
#[serde(rename = "c1_OF_PERSON")]
Cannibal1,
Expand All @@ -51,30 +51,31 @@ enum Person {
#[derive(Clone, Debug, Deserialize)]
struct State {
pub bank_of_boat: Bank,
pub who_is_on_bank: ItfMap<Bank, ItfSet<Person>>,
pub who_is_on_bank: BTreeMap<Bank, BTreeSet<Person>>,
}

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

dbg!(trace);
```

**Output:**

```rust
trace = Trace {
meta: TraceMeta {
description: None,
```rust,ignore
[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)",
},
format: None,
format_description: None,
timestamp: None,
other: {},
},
params: [],
Expand All @@ -85,7 +86,7 @@ trace = Trace {
loop_index: None,
states: [
State {
meta: StateMeta {
meta: Meta {
index: Some(
0,
),
Expand All @@ -96,16 +97,16 @@ trace = Trace {
who_is_on_bank: {
West: {},
East: {
Missionary2,
Cannibal1,
Cannibal2,
Missionary1,
Missionary2,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
1,
),
Expand All @@ -115,18 +116,18 @@ trace = Trace {
bank_of_boat: West,
who_is_on_bank: {
West: {
Missionary2,
Cannibal2,
Missionary2,
},
East: {
Missionary1,
Cannibal1,
Missionary1,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
2,
),
Expand All @@ -139,15 +140,15 @@ trace = Trace {
Cannibal2,
},
East: {
Missionary2,
Cannibal1,
Missionary1,
Missionary2,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
3,
),
Expand All @@ -157,8 +158,8 @@ trace = Trace {
bank_of_boat: West,
who_is_on_bank: {
West: {
Missionary1,
Cannibal2,
Missionary1,
Missionary2,
},
East: {
Expand All @@ -168,7 +169,7 @@ trace = Trace {
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
4,
),
Expand All @@ -177,19 +178,19 @@ trace = Trace {
value: State {
bank_of_boat: East,
who_is_on_bank: {
East: {
Cannibal2,
Cannibal1,
},
West: {
Missionary1,
Missionary2,
},
East: {
Cannibal1,
Cannibal2,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
5,
),
Expand All @@ -198,13 +199,13 @@ trace = Trace {
value: State {
bank_of_boat: West,
who_is_on_bank: {
East: {},
West: {
Cannibal1,
Cannibal2,
Missionary1,
Missionary2,
},
East: {},
},
},
},
Expand All @@ -227,7 +228,9 @@ 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
```text
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.

Expand Down
7 changes: 4 additions & 3 deletions itf/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ rust-version = "1.65"

[dependencies]
num-bigint = { version = "0.4", features = ["serde"] }
serde = { version = "1", features = ["derive"] }
serde_json = "1"
thiserror = "1"
num-traits = { version = "0.2" }
serde = { version = "1", features = ["derive"] }
serde_json = { version = "1", features = ["raw_value"] }
serde_with = { version = "3.4.0" }
48 changes: 48 additions & 0 deletions itf/examples/cannibals.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,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);
}
20 changes: 20 additions & 0 deletions itf/src/de.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
use serde::de::DeserializeOwned;

use crate::Value;

mod error;
pub use error::Error;

mod helpers;
pub use helpers::As;
pub use helpers::Integer;

mod deserializer;

#[doc(hidden)]
pub fn decode_value<T>(value: Value) -> Result<T, Error>
where
T: DeserializeOwned,
{
T::deserialize(value)
}
Loading

0 comments on commit 9902045

Please sign in to comment.