% This is a process with states 1,...,N, where
% each state i has transitions to all states 1,...,i+1.
% This means its transitions go maximally back to
% already detected states, and only one transition
% goes to a new state (i.e. i+1) when doing a breadth
% first search.

% Jan Friso Groote, September 3, 2006.


act a;
map N:Pos;
eqn N=1000;

proc X(i:Pos)=sum j:Pos.(j<=i+1 && j<=N)->a.X(j)<>delta;

init X(1);
