### Verification and Visualization of Behavior Policies
#### 2.5.2 Phase 3--Constructing Scenario State at a Given Moment of Time
The flowchart of Phase 3 of the algorithm is shown in Scheme 2. The input arguments for the algorithm are described in Table 7. The auxiliary variables, some of which are also outcomes of Phase 3, are described in Table 8. The outcome of Phase 3 is described in Table 9.  
Noteworthy are the conditions checked in the subsequent steps of Phase 3 of the algorithm. Comments for each of them are given below. 1. The first condition checked is if we have reached the end of a walk. If so, then surely the state currently constructed is the state for the given moment of time. 2. Do we omit actions of all mission objects? If so, the state constructed so far is the state for the given moment of time. 3. Do any objects involved in the current action belong to the set of skipped objects? If so, we omit this walk element. 4. Will all objects involved in the current action have finished before the moment \(d\)? If not, we disregard that activity in the currently constructed state and add those objects to the set of skipped objects. 5. If Phase 4 is not completed correctly, it means that the model is incorrect. \begin{table}
\begin{tabular}{l c} \hline \hline
**Variable** & **Description** \\ \hline \(s_{0}\in Agt\) & State at the previous point in time. \\ \(m_{0}\in M_{x}\) & Mapping of UIs to vertices of \(s_{0}\). \\ \(W\subseteq W_{M},<_{W_{M}}\) & A walk and the linear order relation on its elements. \\ \(i_{0}\in I\) & The SAT configuration at the previous moment of time. \\ \(d\in\mathbb{N}\) & The moment of time for which the scenario state is constructed. \\ \(n_{o}\in\mathbb{N}\) & Number of objects. \\ \hline \hline \end{tabular}
\end{table} 
Table 7: Input data for the Phase 3 algorithm. \begin{table}
\begin{tabular}{l c} \hline \hline
**Variable** & **Description** \\ \hline \(s_{c}\in Agt\) & Current constructed state. The initial value is \(s_{0}\). \\ \(m_{c}\in M_{x}\) & Mapping of UIs to vertices of \(s_{c}\). \\ \(i_{c}\in I\) & SAT configuration of the currently constructed state. \\  & The initial value is \(i_{0}\). \\ \(A_{o}\in A\) & A set of object identifiers, skipped in the constructed state. The initial value is the empty set. \\ \(W_{c}\subseteq W\) & A collection of usable walk elements. \\  & The initial value is \(W\). \\ \(W_{o}\subseteq W\) & A collection of unused walk elements. \\  & The initial value is the empty set. \\ \hline \hline \end{tabular}
\end{table} 
Table 8: Auxiliary variables of Phase 3 algorithm. \begin{table}
\begin{tabular}{l c} \hline \hline
**Variable** & **Description** \\ \hline \(W_{o}\subset W\) & Unused walk elements that will be used to construct subsequent scenario states. \\ \(s_{c}\in Agt\) & System state. \\ \(m_{c}\in M_{x}\) & Mapping of UIs to vertices of \(s_{c}\). \\ \(i_{c}\in I\) & SAT configuration at time \(d\). \\ \hline \hline \end{tabular}
\end{table} 
Table 9: Output data of Phase 3 algorithm. **Scheme 2. ** Flowchart of the Phase 3 algorithm. The goal of this phase is to construct the state of a scenario at a given point in time. This phase runs in a loop until there are no available walk elements or when an execution of Phase 4 ends with an error. It takes subsequent elements of the input walk and updates both the current SAT configuration and a scenario state. If the mission objects will not have finished the activity represented by the currently processed walk element before or at the specified moment of time then the SAT configuration and state updates are not performed. The same thing happens if an activity involves objects participating in other activities that would end in a future and that have already been skipped.