This code is an example in SMV model checking using Jspin

Could you explain the this code for me and why they use 1 and 0 here ?

next (request [0]) := case next (cabin) = 0 : 0; -disappears request [O] : 1,-- -. -- remains? -may appea esac next (request [1]) case := next (cabin) 1 : 0; -- disappears