### Verification and Visualization of Behavior Policies  
Below we will describe the algorithm to verify and illustrate the behavior policy. It consists of 4 phases. At the beginning of the discussion about each phase formal elements not introduced so far will be defined. Subsequent phases will be discussed so that newly introduced definitions will be directly used in the discussed phase. A diagram of relationships between phases is presented in Figure 3, from which it can be seen that the implementation of all the other phases is necessary for the execution of Phase 1. In contrast, Phases 4 and 2 are independent of the others.  
Figure 3: Diagram of relationships between phases of the algorithm. The direction of an arrow indicates the phase required by the phase from which the arrow emerges.  
5.1. Phase 4--Applying a Single Transformation to Constructed State and Checking Correctness Beforehand  
Phase 4 of the algorithm is responsible for verifying the correctness of the model and for expanding the scenario's state at a particular point in time.  
Input:  
* A currently constructed state--a bigraph;
* A map of unique identifiers to vertices of the currently constructed state (a bijection);
* The reaction rule to be applied to the constructed state;
* A map of unique identifiers to rule's redex vertices (bijection);
* State at the previous moment in time--a bigraph;
* A mapping of unique identifiers to state vertices at a previous point in time;
* First new unique identifier--used when a new task element appears after a transformation.  
Output:  
1. Option 1--the model is correct:  
* Newly constructed state--bigraph;
* Mapping of unique identifiers to vertices of the newly constructed state;
* First new unique identifier.
2. Option 2--the model is incorrect:  
* Information about the failed transformation. Whether the given reaction rule could not be applied to the state at the previous point in time or to the currently constructed state (given the mappings of unique identifiers to vertices).  
Formal definitions:  
* \(X\subseteq\mathbb{N}\)--a set of unique identifiers (UIs) of task elements; It is used to track the environment and objects involved between system transformations. The idea behind this set is to assign to each task element a unique identifier, which makes it possible to check whether the task elements marked as taking part in a reaction rule are present in a given scenario state. The reaction rules themselves allow only to check whether alike (rather than the same) elements exist in both a reaction rule and a bigraph.
* \(Corr_{Red}:\mathcal{R}\to Red\)--a function that assigns reaction rules to their corresponding redexes;
* \(M_{x}\subset X^{V_{b}}\quad b\in Agt\cup Red\)--a set of functions assigning unique identifiers to elements of the support of a bigraph, which is either a scenario state or a redex of a reaction rule;
* \(IsUpdatePossible:Agt\times M_{x}\times Red\times M_{x}\to\{true,false\}\)--a function that determines whether it is possible to apply a reaction rule to a given state, taking into account the mapping of the UIs to the state's vertices and the mapping of the UIs to the redex vertices of that rule;
* \(Update:Agt\times M_{x}\times\mathcal{R}\times M_{x}\times X\to Agt \times M_{x}\times X\)--a function that transforms the current state.  
The flowchart of the Phase 4 algorithm is shown in Scheme 1. The input arguments of this algorithm and its results are described in Tables 5 and 6 respectively.