## 4 Case Study
### T-Intvariant Analysis of the Petri Net Model
\begin{table}
\begin{tabular}{c c c c c c} \hline
**Output** & **Place** & **Action** & **Input** & **Transition** & **Logical Condition** \\
**Signal** & & & & **Signal** & **Transition** & **Logical Condition** \\ \hline \(y_{1}\) & \(p_{1}\) & Standby & \(x_{4}\) & \(t_{4}\) & \(AOFF\) \\ \(y_{2}\) & \(p_{2}\) & L4, L5 & & \(x_{5}\) & \(t_{5}\) \(t_{8}\) & \(U1\wedge M5\wedge night\) \\ \(y_{3}\) & \(p_{3}\) & Bedroom light off & \(x_{6}\) & \(t_{6}\) \(t_{9}\) & \(\
eg M5\) \\ \(y_{4}\) & \(p_{4}\) & Table lamps on R6, R7 & \(x_{7}\) & \(t_{7}\) \(t_{10}\) & \(U1\wedge M5\wedge(day\lor guard)\) \\ \(y_{5}\) & \(p_{5}\) & Bedroom light on L5 & \(x_{8}\) & \(t_{11}\) \(t_{15}\) & \(\
eg M4\) \\ \(y_{6}\) & \(p_{6}\) & Living room light off & \(x_{9}\) & \(t_{12}\) \(t_{14}\) & \(U1\wedge M4\wedge night\) \\ \(y_{7}\) & \(p_{7}\) & Desk lamp on R5 & \(x_{10}\) & \(t_{13}\) \(t_{16}\) & \(U1\wedge M4\wedge(day\lor guard)\) \\ \(y_{8}\) & \(p_{8}\) & Living room light on L4 & \(x_{11}\) & \(t_{17}\) & \(\
eg M3\) \\ \(y_{9}\) & \(p_{9}\) & Kitchen light off & \(x_{12}\) & \(t_{18}\) & \(U1\wedge M3\) \\ \(y_{10}\) & \(p_{10}\) & Kitchen light on L3 & \(x_{13}\) & \(t_{19}\) & \(\
eg M2\) \\ \(y_{11}\) & \(p_{11}\) & Bathroom light off & \(x_{14}\) & \(t_{20}\) & \(M2\) \\ \(y_{12}\) & \(p_{12}\) & Bathroom light on L2 & \(x_{15}\) & \(t_{21}\) & \(\
eg DSR\) \\  & & & Low price of energy on R1, & \(x_{16}\) & \(t_{22}\) & \(DSR\) \\ \(y_{13}\) & \(p_{13}\) & R2, R3, R4, R8 & \(x_{16}\) & \(t_{22}\) & \(DSR\) \\ \(y_{14}\) & \(p_{14}\) & High price of energy & \(x_{17}\) & \(t_{23}\) & \(\
eg M1\) \\ \(y_{15}\) & \(p_{15}\) & Hall light off & \(x_{18}\) & \(t_{24}\) & \(U1\wedge M1\) \\ \(y_{16}\) & \(p_{16}\) & Hall light on L1 & & \(t_{25}\) \(t_{26}\) & \\ \(y_{17}\) & \(p_{24}\) & System on & & \(t_{27}\) \(t_{28}\) & \([((guard\wedge(M1\lor M2\lor M3\lor M4\lor M5\) \\  & & & & \(t_{29}\) \(t_{30}\) & \(\lor D1\lor V\lor D2\lor W1\lor W2\lor W3)\lor F1\) \\  & & & & \(t_{31}\) \(t_{32}\) & \(\lor F2\lor S1)\wedge\
eg AOFF\lor ALARM\)\(\lor OFF\) \\ \(x_{1}\) & \(t_{1}\) & \(OFF\) & \(t_{35}\) \(t_{36}\) & \\ \(x_{2}\) & \(t_{2}\) & \(day\lor night\lor guard\) & \(t_{37}\) \(t_{38}\) & \\  & & & \(((guard\wedge(M1\lor M2\lor M3\) \\ \(x_{3}\) & \(t_{3}\) & \(\lor M4\lor M5\lor D1\lor D2\lor W1\) & \\  & & & \(\lor W2\lor W3\)\()\lor F1\lor F2\) & \\  & & & \(\lor S1)\wedge\
eg AOFF\lor ALARM\) & \\ \hline \end{tabular}
\end{table} 
Table 2: Assignment of signals to places and transitions. (activation or deactivation of a DSR). It shows that malfunctioning of the system can expose users to excessive costs. Although the Petri net model is in line with the assumptions and it is safe and has no deadlocks, the prepared specification clearly does not meet the designer's expectations. However, verification of the transition invariants allows us to identify potential design errors. Unfortunately, the available method in the PIPE tool, does not allow for efficient verification of this model. PIPE could not accomplish the task in the assumed one hour. This outcome was due to the exponential growth of iterations in the algorithm implemented within PIPE. This exponential complexity made it impossible for the tool to compute all t-invariants within the one-hour time limit. This contrasts with the proposed algorithm, which gave a response in 4.06 ms. The introduced algorithm works in polynomial time, so even for larger Petri nets, the time of operation to obtain a result will be satisfactory. The corrected Petri net model of the HAN system is presented in Figure 4. It can be observed that place \(p_{25}\), which was connected to transition \(t_{22}\), has been removed (marked by green square). Previously, for transition \(t_{22}\) to fire, a token was required in both places, \(p_{25}\) and \(p_{13}\), simultaneously.