.model elevator[0]
.inputs init<0> init<1> stop_next continue 
.outputs dec inc 
.table init<0> ->init<0>0 
0 0 
1 1 
.table init<1> ->init<1>0 
0 0 
1 1 
.table stop_next ->stop_next0 
0 0 
1 1 
.table continue ->continue0 
0 0 
1 1 
.table dec0 ->dec 
0 0 
1 1 
.table inc0 ->inc 
0 0 
1 1 
.mv _n245 2 STOPPED MOVING 
.mv movement 2 STOPPED MOVING 
.table _n2450 ->_n245 
0 STOPPED 
1 MOVING 
.table movement ->movement0 
STOPPED 0 
MOVING 1 
.mv movement$raw_n1a 2 STOPPED MOVING 
.table movement$raw_n1a0 ->movement$raw_n1a 
0 STOPPED 
1 MOVING 
.mv _n25c<*2*> 2 ON OFF 
.mv buttons<*2*> 2 ON OFF 
.table _n25c<*2*>0 ->_n25c<*2*> 
0 ON 
1 OFF 
.table buttons<*2*> ->buttons<*2*>0 
ON 0 
OFF 1 
.mv buttons$raw_n1b<*2*> 2 ON OFF 
.table buttons$raw_n1b<*2*>0 ->buttons$raw_n1b<*2*> 
0 ON 
1 OFF 
.mv buttons$raw_n2d<*2*> 2 ON OFF 
.table buttons$raw_n2d<*2*>0 ->buttons$raw_n2d<*2*> 
0 ON 
1 OFF 
.mv buttons$raw_n3f<*2*> 2 ON OFF 
.table buttons$raw_n3f<*2*>0 ->buttons$raw_n3f<*2*> 
0 ON 
1 OFF 
.mv _n25c<*0*> 2 ON OFF 
.mv buttons<*0*> 2 ON OFF 
.table _n25c<*0*>0 ->_n25c<*0*> 
0 ON 
1 OFF 
.table buttons<*0*> ->buttons<*0*>0 
ON 0 
OFF 1 
.mv buttons$raw_n1b<*0*> 2 ON OFF 
.table buttons$raw_n1b<*0*>0 ->buttons$raw_n1b<*0*> 
0 ON 
1 OFF 
.mv buttons$raw_n2d<*0*> 2 ON OFF 
.table buttons$raw_n2d<*0*>0 ->buttons$raw_n2d<*0*> 
0 ON 
1 OFF 
.mv buttons$raw_n3f<*0*> 2 ON OFF 
.table buttons$raw_n3f<*0*>0 ->buttons$raw_n3f<*0*> 
0 ON 
1 OFF 
.mv _n29d 4 OPEN OPENING CLOSED CLOSING 
.mv door 4 OPEN OPENING CLOSED CLOSING 
.table _n29d0 _n29d1 ->_n29d 
0 0 OPEN 
1 0 OPENING 
0 1 CLOSED 
1 1 CLOSING 
.table door ->door0 door1 
OPEN 0 0 
OPENING 1 0 
CLOSED 0 1 
CLOSING 1 1 
.mv door$raw_n19 4 OPEN OPENING CLOSED CLOSING 
.table door$raw_n190 door$raw_n191 ->door$raw_n19 
0 0 OPEN 
1 0 OPENING 
0 1 CLOSED 
1 1 CLOSING 
.table _n2b4<0>0 ->_n2b4<0> 
0 0 
1 1 
.table location<0> ->location<0>0 
0 0 
1 1 
.table location$raw_n17<0>0 ->location$raw_n17<0> 
0 0 
1 1 
.mv _n25c<*1*> 2 ON OFF 
.mv buttons<*1*> 2 ON OFF 
.table _n25c<*1*>0 ->_n25c<*1*> 
0 ON 
1 OFF 
.table buttons<*1*> ->buttons<*1*>0 
ON 0 
OFF 1 
.mv buttons$raw_n1b<*1*> 2 ON OFF 
.table buttons$raw_n1b<*1*>0 ->buttons$raw_n1b<*1*> 
0 ON 
1 OFF 
.mv buttons$raw_n2d<*1*> 2 ON OFF 
.table buttons$raw_n2d<*1*>0 ->buttons$raw_n2d<*1*> 
0 ON 
1 OFF 
.mv buttons$raw_n3f<*1*> 2 ON OFF 
.table buttons$raw_n3f<*1*>0 ->buttons$raw_n3f<*1*> 
0 ON 
1 OFF 
.mv _n2b6 2 UP DOWN 
.mv direction 2 UP DOWN 
.table _n2b60 ->_n2b6 
0 UP 
1 DOWN 
.table direction ->direction0 
UP 0 
DOWN 1 
.mv direction$raw_n18 2 UP DOWN 
.table direction$raw_n180 ->direction$raw_n18 
0 UP 
1 DOWN 
.table _n2cd0 ->_n2cd 
0 0 
1 1 
.table open_next ->open_next0 
0 0 
1 1 
.table open_next$raw_n160 ->open_next$raw_n16 
0 0 
1 1 
.table _n2b4<1>0 ->_n2b4<1> 
0 0 
1 1 
.table location<1> ->location<1>0 
0 0 
1 1 
.table location$raw_n17<1>0 ->location$raw_n17<1> 
0 0 
1 1 
.latch _n245 movement 
.reset movement$raw_n1a ->movement 
-   =movement$raw_n1a  
.latch _n25c<*2*> buttons<*2*> 
.reset buttons$raw_n1b<*2*> buttons$raw_n2d<*2*> buttons$raw_n3f<*2*> ->buttons<*2*> 
.default ON 
OFF -  -   =buttons$raw_n1b<*2*>  
ON OFF -   =buttons$raw_n2d<*2*>  
ON ON OFF  =buttons$raw_n3f<*2*>  
.latch _n25c<*0*> buttons<*0*> 
.reset buttons$raw_n1b<*0*> buttons$raw_n2d<*0*> buttons$raw_n3f<*0*> ->buttons<*0*> 
.default ON 
OFF -  -   =buttons$raw_n1b<*0*>  
ON OFF -   =buttons$raw_n2d<*0*>  
ON ON OFF  =buttons$raw_n3f<*0*>  
.latch _n29d door 
.reset door$raw_n19 ->door 
-   =door$raw_n19  
.latch _n2b4<0> location<0> 
.reset location$raw_n17<0> ->location<0> 
.default 0 
1 1 
.latch _n25c<*1*> buttons<*1*> 
.reset buttons$raw_n1b<*1*> buttons$raw_n2d<*1*> buttons$raw_n3f<*1*> ->buttons<*1*> 
.default ON 
OFF -  -   =buttons$raw_n1b<*1*>  
ON OFF -   =buttons$raw_n2d<*1*>  
ON ON OFF  =buttons$raw_n3f<*1*>  
.latch _n2b6 direction 
.reset direction$raw_n18 ->direction 
-   =direction$raw_n18  
.latch _n2cd open_next 
.reset open_next$raw_n16 ->open_next 
0 0 
1 1 
.latch _n2b4<1> location<1> 
.reset location$raw_n17<1> ->location<1> 
.default 0 
1 1 
.table ->random_push<0> 
-  
.table random_push<0> ->[0]0
.default 0
0 0
1 1
.table ->random_push<1> 
-  
.table random_push<1> ->[1]0
.default 0
0 0
1 1
.table ->random_push<2> 
-  
.table random_push<2> ->[2]0
.default 0
0 0
1 1
.table ->random 
0 
1 
.table random ->[3]0
.default 0
0 0
1 1
.table ->r_stop 
0 
1 
.table r_stop ->[4]0
.default 0
0 0
1 1