#!/usr/bin/env python3
"""Scan a PolySI-text history (r|w(key,val,session,txn)) for per-transaction INTERNAL violations.
For each txn, per key, in event order:
  - INT:        a read after an own write must return the last own written value
  - NONREPEAT:  a read after an earlier read of the same key (no own write between) must return the same value
usage: check_int.py FILE [FILE...]
"""
import re, sys, collections
pat = re.compile(r'([rw])\((\d+),(-?\d+),(\d+),(\d+)\)')
for path in sys.argv[1:]:
    txns = collections.OrderedDict()
    for line in open(path):
        m = pat.fullmatch(line.strip())
        if not m: continue
        t, k, v, s, x = m.groups()
        txns.setdefault((int(s), int(x)), []).append((t, int(k), int(v)))
    viol = []; own_w = rr = nreads = nwrites = 0
    for (s, x), evs in txns.items():
        last_w = {}; last_r = {}
        for i, (t, k, v) in enumerate(evs):
            if t == 'w':
                last_w[k] = v; last_r.pop(k, None); nwrites += 1
            else:
                nreads += 1
                if k in last_w:
                    own_w += 1
                    if v != last_w[k]: viol.append(('INT', s, x, k, v, last_w[k], evs))
                elif k in last_r:
                    rr += 1
                    if v != last_r[k]: viol.append(('NONREPEAT', s, x, k, v, last_r[k], evs))
                else:
                    last_r[k] = v
    print(f'{path}: txns={len(txns)} reads={nreads} writes={nwrites} '
          f'reads-after-own-write={own_w} repeated-reads={rr} VIOLATIONS={len(viol)}')
    for kind, s, x, k, got, want, evs in viol[:10]:
        print(f'  {kind} session={s} txn={x} key={k} read={got} expected={want}  ops={[("%s(%d,%d)"%e) for e in evs if e[1]==k]}')