% There is a path of length 7 leading to the situation where all
% girls know all gossips (true)
% This formula has bogus fixed points to make sure lps2pbes does
% not have to look ahead through the conditions of the entire
% state space.
mu X1 .
mu X2 .
mu X3 .
mu X4 . true