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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
import {toNullable} from 'fp-ts/lib/Option';
import {Account, Operation, SimpleBank} from './bank';
import {
Gen,
Property,
choose,
elements,
forall,
frequency,
keyValueOf,
listOf,
mapOf1 as nonEmptyMap,
property,
} from './property';
import Prando from 'prando';
import {LevelBank} from './levelbank';
import {withTempFile} from './fs';
const sampleAccounts: Account[] = [
'FR12345678901234',
'DE2345678901234',
'IT34567890123412',
];
const genAccount: Gen<Account> = elements(sampleAccounts);
const genBalance: Gen<number> = choose(0, 1000000);
const genAccounts: Gen<Map<Account, number>> = nonEmptyMap(
genAccount,
genBalance,
);
const genGetBalance: (accounts: Map<Account, number>) => Gen<Operation> =
(accounts: Map<Account, number>) => (rng: Prando) => (size: number) => {
const account = elements(Array.from(accounts.keys()))(rng)(size);
return {op: 'GetBalance', account};
};
const genDeposit: (accounts: Map<Account, number>) => Gen<Operation> =
(accounts: Map<Account, number>) => (rng: Prando) => (size: number) => {
const account = elements(Array.from(accounts.keys()))(rng)(size);
const gAmt = choose(1, 100000)(rng)(size);
return {op: 'Deposit', account, amount: gAmt};
};
const genWithdraw: (accounts: Map<Account, number>) => Gen<Operation> =
(accounts: Map<Account, number>) => (rng: Prando) => (size: number) => {
const account = elements(Array.from(accounts.keys()))(rng)(size);
const gAmt = choose(1, 100000)(rng)(size);
return {op: 'Withdraw', account, amount: gAmt};
};
const genOneOperation = (accounts: Map<Account, number>) =>
frequency([
[1, genGetBalance(accounts)],
[3, genDeposit(accounts)],
[3, genWithdraw(accounts)],
]);
const genOperations = (accounts: Map<Account, number>) =>
listOf(genOneOperation(accounts));
const correctBalance =
(initialAccounts: Map<Account, number>) =>
async (ops: Operation[]): Promise<boolean> => {
const fakeBank = new SimpleBank(initialAccounts);
const realBank = await withTempFile(filename => new LevelBank(filename))
.then(bank => bank.populateWith(initialAccounts))
.then(bank => bank);
for (const op of ops) {
switch (op.op) {
case 'GetBalance': {
const retrieved = await realBank.balance(op.account).then(toNullable);
const expected = await fakeBank.balance(op.account).then(toNullable);
if (retrieved !== expected) {
console.log(
`Balance mismatch for account ${op.account}: expected ${expected}, got ${retrieved}`,
);
return false;
}
break;
}
case 'Deposit': {
await realBank.deposit(op.account, op.amount);
await fakeBank.deposit(op.account, op.amount);
break;
}
case 'Withdraw': {
await realBank.withdraw(op.account, op.amount);
await fakeBank.withdraw(op.account, op.amount);
break;
}
}
}
// finally check all balances
for (const account of initialAccounts.keys()) {
const actual = await realBank.balance(account).then(toNullable);
const expected = await fakeBank.balance(account).then(toNullable);
if (actual !== expected) {
console.log(
`Final balance mismatch for account ${account}: expected ${expected}, got ${actual}`,
);
return false;
}
}
return true;
};
describe('Bank Simulator', () => {
test('can retrieve balance given account exists', async () => {
const prop = forall(genAccounts, async accounts => {
const api = new SimpleBank(accounts);
return property(keyValueOf(accounts), async ([accountNr, bal]) => {
const retrieved = toNullable(await api.balance(accountNr));
return Promise.resolve(retrieved === bal);
});
});
const result = await Property.run(prop);
expect(result.result).toBe('OK');
});
test('correctly update balance given a sequence of deposits and withdrawals', async () => {
const prop = forall(genAccounts, accounts => {
return property(genOperations(accounts), correctBalance(accounts));
});
const result = await Property.run(prop);
console.log(result);
console.log(JSON.stringify(result.counterexample));
expect(result.result).toBe('OK');
});
});
|
