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