{Verification of Choreographies During Execution Using the Reactive Event Calculus}