An Operational Semantics for Model Checking Long Running Transactions