#!/usr/bin/env python3
"""Finite predicate/retry model; no BSON, WT, journal, server or replica set runs."""
import copy
import json
from pathlib import Path


def run():
    f = json.loads(Path(__file__).with_name('fixture.json').read_text())
    loose = [d['_id'] for d in f['arrays'] if any(x['sku'] == 'A' for x in d['items'])
             and any(x['qty'] >= 5 for x in d['items'])]
    same = [d['_id'] for d in f['arrays'] if any(x['sku'] == 'A' and x['qty'] >= 5 for x in d['items'])]
    inventory, matched = copy.deepcopy(f['inventory']), []
    # Both callers read version 1; the predicate is checked again at each serialized write.
    for _ in range(2):
        accept = (inventory['version'] == f['deduct']['expected_version']
                  and inventory['stock'] >= f['deduct']['quantity'])
        matched.append(int(accept))
        if accept:
            inventory['stock'] -= f['deduct']['quantity']
            inventory['version'] += 1
    keys, unique = set(), []
    for doc in f['unique_attempts']:
        key = (doc['tenant'], doc['request_id'])
        unique.append('duplicate-key' if key in keys else 'inserted')
        keys.add(key)
    actions = ['retry-body' if 'TransientTransactionError' in labels else
               'retry-commit' if 'UnknownTransactionCommitResult' in labels else 'investigate'
               for labels in f['transaction_errors']]
    window = f['oplog_window']
    resumable = lambda token: window['earliest'] <= token <= window['latest']
    result = {
        'kind': 'finite-model', 'baseline': 'MongoDB 7.0.14',
        'arrays': {'loose_ids': loose, 'elem_match_ids': same},
        'conditional_update': {'matched_counts': matched, 'final_stock': inventory['stock'],
                               'final_version': inventory['version']},
        'unique_index': {'first': unique[0], 'second': unique[1]},
        # Select one counterexample: apply succeeded, then acknowledgement was lost.
        # It does NOT claim that every timeout write has applied.
        'write_timeout': {'client_outcome': 'unknown', 'stored_stock': inventory['stock'], 'rolled_back': False},
        'transaction_actions': actions,
        'change_stream': {'resume_inside_window': resumable(window['inside_token']),
                          'resume_before_window': resumable(window['expired_token'])},
    }
    assert loose == ['cross', 'same'] and same == ['same']
    assert matched == [1, 0] and inventory['stock'] == 20 and inventory['version'] == 2
    assert unique == ['inserted', 'duplicate-key']
    assert actions == ['retry-body', 'retry-commit', 'investigate']
    assert result['change_stream'] == {'resume_inside_window': True, 'resume_before_window': False}
    return result


if __name__ == '__main__':
    print(json.dumps(run(), ensure_ascii=False, indent=2))