%
% M. Talebi
% The number of nodes in the network is 3. Every time a node becomes a cluster slave or a cluster head, an increase action is performed.
% Initially there is 1 cluster head in the network.
%
% "For every possible computation at some finite point in the future the action increase has occurred 2 (=3-1) times"
%
mu X(n:Nat=1).([increase]X(n+1) && [!increase]X(n) && true) || (val(n==3))