\item[circuitBreaker]takes either \textit{CLOSED}, \textit{OPENED}, or \textit{HALF} value to represent the current state of the \acl{CB}
\item[calls]is a function that maps ($:>$) the thread $t1$ to the record of the form $[reply,permitted,permittedInState]$. The \textit{reply} field is either \textit{TRUE}, which means the service invocation was successful, \textit{FALSE}, which means invocation failed, or \textit{NULL}, which means the thread has not send any request yet. \textit{permitted} field shows whether the thread obtained a permission to send a request via TRUE or FALSE value. Finally \textit{permittedInState} field is to track which state the thread obtained a permission for correct recording of the result (read the next item).