ledger/
ledger.rs

1#![allow(dead_code)]
2#![allow(unused_imports)]
3
4use hegel::TestCase;
5use hegel::generators as gs;
6use hegel::stateful::{Pool, pool};
7use std::collections::HashMap;
8
9const LIMIT: i64 = 1000000;
10
11struct Ledger {
12    balances: HashMap<String, i64>,
13}
14
15impl Ledger {
16    fn new() -> Self {
17        Ledger {
18            balances: HashMap::new(),
19        }
20    }
21
22    fn credit(&mut self, account: String, amount: i64) {
23        let balance = self.balances.entry(account).or_insert(0);
24        *balance += amount;
25    }
26
27    fn debit(&mut self, account: String, amount: i64) {
28        let balance = self.balances.entry(account).or_insert(0);
29        *balance -= amount;
30    }
31
32    fn transfer(&mut self, from: String, to: String, amount: i64) {
33        let from_balance = *self.balances.get(&from).unwrap_or(&0);
34        if from != to && amount - from_balance <= 1 {
35            self.debit(from, amount);
36            self.credit(to, amount);
37        }
38    }
39}
40
41struct LedgerTest {
42    ledger: Ledger,
43    accounts: Pool<String>,
44}
45
46#[hegel::state_machine]
47impl LedgerTest {
48    #[rule]
49    fn create_account(&mut self, tc: TestCase) {
50        let account = tc.draw(gs::text().min_size(1));
51        tc.note(&format!("create account '{}'", account.clone()));
52        self.accounts.add(account);
53    }
54
55    #[rule]
56    fn credit(&mut self, tc: TestCase) {
57        let account = tc.draw(self.accounts.values_reusable()).clone();
58        let amount = tc.draw(gs::integers::<i64>().min_value(0).max_value(LIMIT));
59        tc.note(&format!("credit '{}' with {}", account.clone(), amount));
60        self.ledger.credit(account, amount);
61    }
62
63    #[rule]
64    fn transfer(&mut self, tc: TestCase) {
65        let from = tc.draw(self.accounts.values_reusable()).clone();
66        let to = tc.draw(self.accounts.values_reusable()).clone();
67        let amount = tc.draw(gs::integers::<i64>().min_value(0).max_value(LIMIT));
68        tc.note(&format!(
69            "transfer '{}' from {} to {}",
70            amount,
71            from.clone(),
72            to.clone()
73        ));
74        self.ledger.transfer(from, to, amount);
75    }
76
77    #[invariant]
78    fn nonnegative_balances(&mut self, _: TestCase) {
79        for balance in self.ledger.balances.values() {
80            assert!(*balance >= 0);
81        }
82    }
83}
84
85#[hegel::test]
86fn test_ledger(tc: TestCase) {
87    let test = LedgerTest {
88        ledger: Ledger::new(),
89        accounts: pool(&tc),
90    };
91    hegel::stateful::run(test, tc);
92}
93
94fn main() {}
ledger/ledger.rs

ledger/
ledger.rs
