\begin{description}

   \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).
   \item[recordedCalls] is a sequence of results from service invocations that obtained a permission when the \acl{CB} was in OPENED state.
   \item[recordedCallsInHalf] a same description as recordedCalls for HALF state.
   \item[executedInState] is a sequence of all calls against the service. The values are It is for checking the \textit{Req6}.

\end{description}

Community content is available under CC-BY-SA unless otherwise noted.