## 4 Example  
A flexible manufacturing system composed of three stations in UFR-MIM FRANCE and its PN model are presented in Figure 5a,b, respectively. In the first station \((P_{1})\), glass pieces are laser-engraved and stored in appropriate locations. Stations 2 and 3 modeled by \(P_{2}\)&\(P_{3}\) pack the engraved pieces, respectively, in black and red boxes. The capacity of each station is modeled by \(P_{4}\) and \(P_{5}\) and is equal to three tokens. Transitions \((t_{1},t_{2})\) and \((t_{4},t_{5})\) represent, respectively, the events of entry and exit of the pallets through their annex conveyors. Otherwise, the pallets can continue their way to the main conveyor by crossing \(t_{3}\). Note that only the transitions \(t_{1}\) and \(t_{2}\) are controllable. Since the used black boxes are cheaper than red ones, the constraint to respect is keeping the marking of \(P_{2}\) plus the doubled marking of \(P_{3}\) less than three tokens. This control specification can be formulated by the following GMEC:  
\[M(P_{2})+2M(P_{3})\leq 3\]  
The \(t\)-invariants can be determined by resolving the following system: \(C.[x_{t1}x_{t2}x_{t3}x_{t4}x_{t5}]^{t}~{}=~{}0\). \[\left[ \begin{array}{cccc}-1&-1&0&1&1\\ 1&0&0&-1&0\\ 0&1&0&0&-1\\ -1&0&0&1&0\\ 0&-1&0&0&1\end{array} \right]\left[ \begin{array}{c}x_{t1}\\ x_{t2}\\ x_{t3}\\ x_{t4}\\ x_{t5}\end{array} \right]~{}=~{}\left[ \begin{array}{c}0\\ 0\\ 0\\ 0\\ 0\end{array} \right]\]  
\(\left(X_{t}^{1}\right)^{t}~{}=~{}[10010]\); \(\left(X_{t}^{2}\right)^{t}~{}=~{}[01001]\); therefore, the sequences corresponding to the cycle equations are: \(\sigma_{1}~{}=~{}(t_{1}t_{4})\) and \(\sigma_{2}~{}=~{}(t_{2}t_{5})\). The basic cycle equations can be detailed as follows:  
\[C(P_{ci},t_{3})~{}=~{}0,\]  
\[C(P_{ci},t_{1})+~{}C(P_{ci},t_{4})~{}=~{}0,\]  
\[C(P_{ci},t_{2})+~{}C(P_{ci},t_{5})~{}=~{}0.\]  
Figure 5: UFR-MIM flexible manufacturing system. (**a**) PN model, (**b**) experimental environment. According to our PN model \(M_{p}\ =\ \left(p_{1}^{\prime}\,p_{2}^{\prime}\,p_{3}^{\prime}\,p_{4}^{\prime}\,p_{5}^{ \prime}\right)\). Thus, one can define the LSP in order to identify the set of paths \(P_{s}\ =\ \sum_{i}\sigma_{i}\):  
\[C.\sigma\ =\ M_{p}-M_{0}\ =\ \left( \begin{array}{c}p_{1}^{\prime}-4\\ p_{2}^{\prime}-0\\ p_{3}^{\prime}-0\\ p_{4}^{\prime}-3\\ p_{5}^{\prime}-3\end{array} \right)\geq\left( \begin{array}{c}-4\\ 0\\ 0\\ 0\\ -3\\ \end{array} \right).\]  
The detailed information of the calculated paths \(P_{s}\ =\ \sum_{i}\sigma_{i}\) is listed in Table 1. Once all paths are determined, one can obtain the set of reachable markings \(M_{x}\). The detailed information of \(M_{x}\) is listed in Table 2.  
It is noticed that there are no dangerous markings \(MD\). On the other hand, we should subtract the uncontrollable transition(s) from the corresponding path. Hence, the reachability conditions can be obtained as follows. \[M_{0}(P_{ci})\geq 0,\]  
\[M_{0}(P_{c})+C(P_{ci},\ t_{1})\geq 0,\]  
\[M_{0}(P_{c})+C(P_{ci},\ t_{1})+C(P_{ci},\ t_{2})\geq 0,\]  
\[M_{0}(P_{c})+2C(P_{ci},\ t_{1})\geq 0,\]  
\[M_{0}(P_{c})+3C(P_{ci},\ t_{1})\geq 0.\] \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Sequence of Transitions** & \
\begin{tabular}{c} **Information of Sequence** \\ **(\(t_{1}t_{2}t_{3}t_{4}t_{5}\))** \\ \end{tabular} & **Sequence of Transitions** &
\begin{tabular}{c} **Information of Sequence** \\ **(\(t_{1}t_{2}t_{3}t_{4}t_{5}\))** \\ \end{tabular} \\ \hline \(\sigma_{1}\) & \((1\,0\,0\,0\,0)\) & \(\sigma_{7}\) & \((1\,2\,0\,0\,0)\) \\ \(\sigma_{2}\) & \((0\,1\,0\,0\,0)\) & \(\sigma_{8}\) & \((2\,1\,0\,0\,0)\) \\ \(\sigma_{3}\) & \((0\,2\,0\,0\,0)\) & \(\sigma_{9}\) & \((3\,0\,0\,0\,0)\) \\ \(\sigma_{4}\) & \((1\,1\,0\,0\,0)\) & \(\sigma_{10}\) & \((1\,3\,0\,0\,0)\) \\ \(\sigma_{5}\) & \((2\,0\,0\,0\,0)\) & \(\sigma_{11}\) & \((2\,2\,0\,0\,0)\) \\ \(\sigma_{6}\) & \((0\,3\,0\,0\,0)\) & \(\sigma_{12}\) & \((3\,1\,0\,0\,0)\) \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Information of paths. \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Marking No.