# Neighbor Session Solutions for Integrated Routing Protocols
## 4 Modeling Protocol Integration Solution Classes
### PISC 3--L3 Transport, Multiple Adjacencies
#### 4.1.1 Sending Part
This fact leads us to a deeper examination of sample models in the literature [20,26,44] and the documentation on the official website of the CPN Tools, which we already dealt with during the previous analysis since the scientific articles that we used during the analysis do not describe in detail how to model, verify and simulate colored Petri nets. Additional study of these resources and state space computation and simulation of sample models of colored Petri nets for CPN Tools lead us to a solution to the described problem. ### Identification of the Full State Space Calculation and Automatic Simulation Problem

The problem is caused by a situation where a large number of transitions in the model are active at certain steps of the model execution. As an example, we can describe a situation where even in the first step of implementing the proposed model of the third PISC, any of the following four transitions can be performed:

* Encapsulate L3;
* Encapsulate IPv6;
* Encapsulate L3 B;
* Encapsulate IPv6 B. Therefore, it is obvious that just by combining active transitions, the state space grows by a very large number of nodes and edges. The second problem identified due to the uncontrolled number of activated transitions is, for example, that only transitions responsible for sending the initial IPv4 Adjacency message from Neighbor A to Router B would be performed. Since Router B would never reply to Router A, the adjacency would not start to form, and thus, in the model, deadlock would occur. These described problems caused the calculation of only a partial state space and the \"never-ending\" automatic simulation. Thus, the created model is not deterministic, and it is necessary to limit the number of active transitions and synchronize both neighboring routers. ### Solving the Problem of Full State Space Calculation and Automatic Simulation

Based on the sample models in the literature [26,44] and the official CPN Tools documentation, we create several limiting and synchronization points that limit the active transitions in the model. Figure 12 shows a limiting place called limit encapsulation (highlighted in turquoise), which ensures that only one message can be processed by the Encapsulate L3 and Encapsulate L2 transitions at a time. This means that the Encapsulate L3 transition will only be active if the Encapsulate L2 transition is not active. In a similar way, limits can also be

applied to multiple transitions (not just two). We also apply a limiting place, for example, between the Decapsulate L2 and Process RoutePacket transitions, which means that the Decapsulate L2 transition will be able to be active again only after the Decapsulate L3 and Process RoutePacket transitions have been executed. The synchronization place named SyncA, highlighted in turquoise, is the same as the limiting place shown in Figure 3:7 This place is used to fix the model deadlock problem caused by only one router in the model constantly sending messages but never receiving a response. Synchronization points are created one for each neighborship and for each router in the model. A function similar to synchronization places in the model is performed by timers in the real implementations of routing protocols. After applying the described corrections to all four PISC models, we successfully manage to verify all created models. ## 6 Results

Computation of the state space of each model using CPN Tools results are in a text file format and contain information and statistics. By analyzing these outputs, we can determine whether the model is stuck and obtain statistical information such as the maximum number of tokens present at each place. The most important part of the first PISC state space calculation output is shown in Figure 3:8

Figure 3:9 Limiting place in the model. Figure 5.0 Synchronization point in the model. The state space paragraph contains information about the calculated state space.