Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#l21 ht

Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#l21 https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#... In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.