3 files changed, 87 insertions, 14 deletions

diff --git a/pbt/ts/src/bank.test.ts b/pbt/ts/src/bank.test.ts
index 5939034..2944e4c 100644
--- a/pbt/ts/src/bank.test.ts
+++ b/pbt/ts/src/bank.test.ts
@@ -13,6 +13,8 @@ import {
   property,
 } from './property';
 import Prando from 'prando';
+import {LevelBank} from './levelbank';
+import {withTempFile} from './fs';
 
 const sampleAccounts: Account[] = [
   'FR12345678901234',
@@ -62,14 +64,16 @@ const genOperations = (accounts: Map<Account, number>) =>
 const correctBalance =
   (initialAccounts: Map<Account, number>) =>
   async (ops: Operation[]): Promise<boolean> => {
-    const expectedBalances = new Map(initialAccounts);
-    const api = new SimpleBank(initialAccounts);
+    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 = toNullable(await api.balance(op.account));
-          const expected = expectedBalances.get(op.account);
+          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}`,
@@ -79,26 +83,25 @@ const correctBalance =
           break;
         }
         case 'Deposit': {
-          api.deposit(op.account, op.amount);
-          const current = expectedBalances.get(op.account) || 0;
-          expectedBalances.set(op.account, current + op.amount);
+          await realBank.deposit(op.account, op.amount);
+          await fakeBank.deposit(op.account, op.amount);
           break;
         }
         case 'Withdraw': {
-          api.withdraw(op.account, op.amount);
-          const current = expectedBalances.get(op.account) || 0;
-          expectedBalances.set(op.account, current - op.amount);
+          await realBank.withdraw(op.account, op.amount);
+          await fakeBank.withdraw(op.account, op.amount);
           break;
         }
       }
     }
 
     // finally check all balances
-    for (const [account, expectedBal] of expectedBalances.entries()) {
-      const retrieved = toNullable(await api.balance(account));
-      if (retrieved !== expectedBal) {
+    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 ${expectedBal}, got ${retrieved}`,
+          `Final balance mismatch for account ${account}: expected ${expected}, got ${actual}`,
         );
         return false;
       }
@@ -129,6 +132,8 @@ describe('Bank Simulator', () => {
 
     const result = await Property.run(prop);
 
+    console.log(result);
+    console.log(JSON.stringify(result.counterexample));
     expect(result.result).toBe('OK');
   });
 });
diff --git a/pbt/ts/src/fs.ts b/pbt/ts/src/fs.ts
new file mode 100644
index 0000000..133c8fd
--- /dev/null
+++ b/pbt/ts/src/fs.ts
@@ -0,0 +1,16 @@
+import {mkdtemp, realpath} from 'fs/promises';
+import {tmpdir} from 'os';
+import path = require('path');
+import fs = require('fs');
+
+export const withTempFile = <A>(fn: (filepath: string) => A) =>
+  withTempDir(dir => fn(path.join(dir, 'file')));
+
+export const withTempDir = async <A>(fn: (path: string) => A) => {
+  const dir = await mkdtemp((await realpath(tmpdir())) + path.sep);
+  try {
+    return await fn(dir);
+  } finally {
+    fs.rmdir(dir, () => {});
+  }
+};
diff --git a/pbt/ts/src/levelbank.ts b/pbt/ts/src/levelbank.ts
new file mode 100644
index 0000000..ead4e38
--- /dev/null
+++ b/pbt/ts/src/levelbank.ts
@@ -0,0 +1,52 @@
+// Specify types of keys and values (any, in the case of json).
+
+import {Level} from 'level';
+import {Account, Bank} from './bank';
+import {Option, fromNullable} from 'fp-ts/lib/Option';
+
+export class LevelBank implements Bank {
+  db: Level<string, number>;
+  file: string;
+
+  constructor(file: string) {
+    this.file = file;
+    this.db = new Level<Account, number>(file, {
+      valueEncoding: 'json',
+    });
+  }
+
+  async populateWith(
+    initialAccounts: Map<Account, number>,
+  ): Promise<LevelBank> {
+    await this.db.open({createIfMissing: true});
+
+    const puts: Promise<void>[] = [];
+
+    initialAccounts.forEach((v, k) => {
+      puts.push(this.db.put(k, v));
+    });
+
+    await Promise.all(puts);
+
+    return this;
+  }
+
+  async balance(account: string): Promise<Option<number>> {
+    const result = await this.db.get(account);
+    return fromNullable(result);
+  }
+
+  async deposit(account: string, amt: number): Promise<void> {
+    const current = await this.db.get(account);
+    if (current) {
+      await this.db.put(account, current + amt);
+    }
+  }
+
+  async withdraw(account: string, amt: number): Promise<void> {
+    const current = await this.db.get(account);
+    if (current) {
+      await this.db.put(account, current + amt);
+    }
+  }
+}