\section{Study Case: K-State Token Ring Program}\label{sec:kstate}
In this section, we study Dijkstra's K-state token ring program \cite{Dijkstra} for illustration purpose. The token ring program is as follows: The program consists of $N+1$ processes, numbered from $0$ to $N$. Each process $p.i$, $0\leq i\leq N$, has one variable $x.i$. The domain of $x.i$ is $\{0,1, \ \dots,\ K-1\}$. These processes are organized in a unidirectional ring.
The program consists of two types of actions. The first type is for process $0$. This action is enabled when $x.0$ equals $x.N$. When $p.0$ executes its action, it increments $x.0$ by $1$ in modulo K arithmetic. The second type of action is for process $p.i$, $i\neq 0$. This action is enabled when $x.i$ is not equal to $x.(i-1)$. When $p.i$ executes its action, it copies $x.(i-1)$. Thus, the actions are as follows:
\begin{tabbing}
\hspace*{5mm} \= ${K_0}$:: \hspace*{5mm}\= $x.0$\= = \= $x.N\ \hspace*{1cm}
$\= $\longrightarrow$ \hspace*{4mm} \= $x.0$ = $(x.0+1)\ mod\ K$; \\
\> ${K_i}$::\> $x.i$\> $\neq$ \> $x.(i-1)$\> $\longrightarrow$ \> $x.i$ = $x.(i-1)$;\\
\end{tabbing}
\textit{Performance evaluation. } \
We evaluate the performance of the token ring program in Table \ref{tab:bound}. In particular, Table \ref{tab:bound} illustrates the time for verifying the closure and the convergence property.
\begin{table*}
\caption{Verification Time for $\convformula$ for Token Ring}
\centering
\begin{tabular}{|c|c|c|c|c|}
\hline
Number of nodes & state space & \shortstack{Number of steps \\for convergence} & \shortstack{Execution time(s)\\ for convergence} & \shortstack{Execution time(s)\\ for closure}\\
\hline
3&$10^1$&4&0.008944&0.005617\\
4&$10^2$&14&0.494496 &0.005979\\
5&$10^3$&25&214.0957 &0.013349\\
\hline
\end{tabular}
\label{tab:bound}
\end{table*}