← index | JSON descriptor | ▶ simulate
Machine: traffic-light (initial: red) green red (initial) yellow