Validating System Executions with the TLA+ Tools