error: livelock in model livelock_unfold
model: livelock_unfold
h.hello
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
<loop>
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
w.hello
w.world
w.return
<livelock>
