diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 27b0cb256..3f64a769d 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -482,6 +482,58 @@ Use --verbosity=3 to show executions. error: Invariant violated ``` +### Run finds invariant violation with metadata on bank spec + +Make sure the bank spec we use at the Getting Started guide has correct tracking of metadata + + +``` +output=$(quint run --seed=0xcc198528dea8b --mbt \ + --invariant=no_negatives ./testFixture/simulator/gettingStarted.qnt 2>&1) +exit_code=$? +echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*gettingStarted.qnt# HOME/gettingStarted.qnt#g' +exit $exit_code +``` + + + +``` +An example execution: + +[State 0] +{ + action_taken: "init", + balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0), + nondet_picks: { account: None, amount: None } +} + +[State 1] +{ + action_taken: "deposit", + balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 53), + nondet_picks: { account: Some("charlie"), amount: Some(53) } +} + +[State 2] +{ + action_taken: "deposit", + balances: Map("alice" -> 26, "bob" -> 0, "charlie" -> 53), + nondet_picks: { account: Some("alice"), amount: Some(26) } +} + +[State 3] +{ + action_taken: "withdraw", + balances: Map("alice" -> -13, "bob" -> 0, "charlie" -> 53), + nondet_picks: { account: Some("alice"), amount: Some(39) } +} + +[violation] Found an issue (duration). +Use --seed=0xcc198528dea8b to reproduce. +Use --verbosity=3 to show executions. +error: Invariant violated +``` + ### Run finds an example The command `run` finds an example. diff --git a/quint/testFixture/simulator/gettingStarted.qnt b/quint/testFixture/simulator/gettingStarted.qnt new file mode 100644 index 000000000..586dc4b4d --- /dev/null +++ b/quint/testFixture/simulator/gettingStarted.qnt @@ -0,0 +1,35 @@ +module bank { + /// A state variable to store the balance of each account + var balances: str -> int + + pure val ADDRESSES = Set("alice", "bob", "charlie") + + action deposit(account, amount) = { + // Increment balance of account by amount + balances' = balances.setBy(account, curr => curr + amount) + } + + action withdraw(account, amount) = { + // Decrement balance of account by amount + balances' = balances.setBy(account, curr => curr - amount) + } + + action init = { + // At the initial state, all balances are zero + balances' = ADDRESSES.mapBy(_ => 0) + } + + action step = { + // Non-deterministically pick an address and an amount + nondet account = ADDRESSES.oneOf() + nondet amount = 1.to(100).oneOf() + // Non-deterministically choose to either deposit or withdraw + any { + deposit(account, amount), + withdraw(account, amount), + } + } + + /// An invariant stating that all accounts should have a non-negative balance + val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0) +}