1MODULE main
2VAR
3  request : boolean;
4  state : {ready,busy};
5ASSIGN
6  init(state) := ready;
7  next(state) := case
8                   state = ready & request : busy;
9                   1 : {ready,busy};
10                 esac;
11SPEC
12  AG(request -> AF state = busy)
13