{
  "scenario": "bounded_real_sqlite_boundary_schedules",
  "cases": [
    {
      "actions": [
        "old_pay",
        "advance",
        "reclaim",
        "old_expire"
      ],
      "trace": [
        {
          "action": "old_pay",
          "now": 1299,
          "outcome": "BOOKED",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "CONFLICT",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": false,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        }
      ],
      "winner": "old-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 0
      }
    },
    {
      "actions": [
        "old_pay",
        "advance",
        "old_expire",
        "reclaim"
      ],
      "trace": [
        {
          "action": "old_pay",
          "now": 1299,
          "outcome": "BOOKED",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": false,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "CONFLICT",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        }
      ],
      "winner": "old-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 0
      }
    },
    {
      "actions": [
        "old_pay",
        "old_expire",
        "advance",
        "reclaim"
      ],
      "trace": [
        {
          "action": "old_pay",
          "now": 1299,
          "outcome": "BOOKED",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "old_expire",
          "now": 1299,
          "outcome": false,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "CONFLICT",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        }
      ],
      "winner": "old-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 0
      }
    },
    {
      "actions": [
        "advance",
        "old_pay",
        "reclaim",
        "old_expire"
      ],
      "trace": [
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": false,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "advance",
        "old_pay",
        "old_expire",
        "reclaim"
      ],
      "trace": [
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": true,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "advance",
        "reclaim",
        "old_pay",
        "old_expire"
      ],
      "trace": [
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": false,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "advance",
        "reclaim",
        "old_expire",
        "old_pay"
      ],
      "trace": [
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": false,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "advance",
        "old_expire",
        "old_pay",
        "reclaim"
      ],
      "trace": [
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": true,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "advance",
        "old_expire",
        "reclaim",
        "old_pay"
      ],
      "trace": [
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_expire",
          "now": 1300,
          "outcome": true,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "old_expire",
        "old_pay",
        "advance",
        "reclaim"
      ],
      "trace": [
        {
          "action": "old_expire",
          "now": 1299,
          "outcome": false,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1299,
          "outcome": "BOOKED",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "CONFLICT",
          "invariant": {
            "paid": 1,
            "sold": 1,
            "ledger": 1,
            "refunds": 0
          }
        }
      ],
      "winner": "old-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 0
      }
    },
    {
      "actions": [
        "old_expire",
        "advance",
        "old_pay",
        "reclaim"
      ],
      "trace": [
        {
          "action": "old_expire",
          "now": 1299,
          "outcome": false,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    },
    {
      "actions": [
        "old_expire",
        "advance",
        "reclaim",
        "old_pay"
      ],
      "trace": [
        {
          "action": "old_expire",
          "now": 1299,
          "outcome": false,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "advance",
          "now": 1300,
          "outcome": 1300,
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "reclaim",
          "now": 1300,
          "outcome": "HELD",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 0
          }
        },
        {
          "action": "old_pay",
          "now": 1300,
          "outcome": "REFUND_PENDING",
          "invariant": {
            "paid": 0,
            "sold": 0,
            "ledger": 0,
            "refunds": 1
          }
        }
      ],
      "winner": "new-payment",
      "final": {
        "paid": 1,
        "sold": 1,
        "ledger": 1,
        "refunds": 1
      }
    }
  ],
  "schedules_checked": 12,
  "invariant_checks": 72,
  "scope": "12 enumerated schedules, not an exhaustive distributed-system proof",
  "pass": true
}
