source: vis_dev/vis-2.1/examples/ctlp3/ctlp3.mv @ 15

# vl2mv ctlp3.v 
# version: 0.2
# date:    11:13:08 12/11/95 (PST)
.model diners 
# I/O ports

.mv s0 4 THINKING HUNGRY EATING READING 
.mv s1 4 THINKING HUNGRY EATING READING 
.mv s2 4 THINKING HUNGRY EATING READING 
.mv _n0 4 THINKING HUNGRY EATING READING 
.names _n0
EATING
.subckt philosopher ph0 out=s0  left=s1  right=s2  init=_n0 
.mv _n1 4 THINKING HUNGRY EATING READING 
.names _n1
READING
.subckt philosopher ph1 out=s1  left=s2  right=s0  init=_n1 
.mv _n2 4 THINKING HUNGRY EATING READING 
.names _n2
HUNGRY
.subckt philosopher ph2 out=s2  left=s0  right=s1  init=_n2 
.subckt starvation str starv=s0  
# conflict arbitrators
# non-blocking assignments 
# latches
# quasi-continuous assignment
.end


.model philosopher 
# I/O ports
.inputs left
.outputs out
.inputs init
.inputs right

.mv left 4 THINKING HUNGRY EATING READING 
.mv out 4 THINKING HUNGRY EATING READING 
.mv r0_state 4 THINKING HUNGRY EATING READING 
.mv r1_state 4 THINKING HUNGRY EATING READING 
.mv state 4 THINKING HUNGRY EATING READING 
.mv init 4 THINKING HUNGRY EATING READING 
.mv right 4 THINKING HUNGRY EATING READING 
# state  = init 
.mv state$raw_n3 4 THINKING HUNGRY EATING READING 
.names init state$raw_n3
- =init
# non-blocking assignments for initial
# assign r0_state  = $NDset ( 0,1 ) 
.names r0_state
THINKING 
HUNGRY 
# assign r1_state  = $NDset ( 0,2 ) 
.names r1_state
THINKING 
EATING 
# assign out  = state 
.mv out$raw_n8 4 THINKING HUNGRY EATING READING 
.names state out$raw_n8
- =state
.mv _nb 4 THINKING HUNGRY EATING READING 
.names _nb
READING
.names state _nb _na
.def 0
- =state 1
.names _na  _n9
1 1
0 0
.mv _nd 4 THINKING HUNGRY EATING READING 
.names _nd
THINKING
# left  == 0
.names left _nd _nc
.def 0
- =left 1
.names _nc _ne
- =_nc
# state  = 0
.mv state$_nc_nf$true 4 THINKING HUNGRY EATING READING 
.names state$_nc_nf$true
THINKING
# if/else (left  == 0)
.mv state$_nc$raw_n12 4 THINKING HUNGRY EATING READING 
.names state$_nc_nf$true state _nc state$_nc$raw_n12
- - 0 =state
- - 1 =state$_nc_nf$true
.mv _n15 4 THINKING HUNGRY EATING READING 
.names _n15
THINKING
.names state _n15 _n14
.def 0
- =state 1
.names _n14  _n13
1 1
0 0
.mv _n17 4 THINKING HUNGRY EATING READING 
.names _n17
READING
# right  == 3
.names right _n17 _n16
.def 0
- =right 1
.names _n16 _n18
- =_n16
# state  = 3
.mv state$_n16_n19$true 4 THINKING HUNGRY EATING READING 
.names state$_n16_n19$true
READING
# state  = r0_state 
.mv state$_n16_n1a$false 4 THINKING HUNGRY EATING READING 
.names r0_state state$_n16_n1a$false
- =r0_state
# if/else (right  == 3)
.mv state$_n16$raw_n1c 4 THINKING HUNGRY EATING READING 
.names state$_n16_n19$true state$_n16_n1a$false _n16 state$_n16$raw_n1c
- - 0 =state$_n16_n1a$false
- - 1 =state$_n16_n19$true
.mv _n21 4 THINKING HUNGRY EATING READING 
.names _n21
EATING
.names state _n21 _n20
.def 0
- =state 1
.names _n20  _n1f
1 1
0 0
# state  = r1_state 
.mv state$_n1f_n22$true 4 THINKING HUNGRY EATING READING 
.names r1_state state$_n1f_n22$true
- =r1_state
.mv _n25 4 THINKING HUNGRY EATING READING 
.names _n25
HUNGRY
.names state _n25 _n24
.def 0
- =state 1
.names _n24  _n23
1 1
0 0
.mv _n27 4 THINKING HUNGRY EATING READING 
.names _n27
EATING
# left  != 2
.names left _n27 _n26
.def 1
- =left 0
.mv _n29 4 THINKING HUNGRY EATING READING 
.names _n29
HUNGRY
# right  != 1
.names right _n29 _n28
.def 1
- =right 0
# left  != 2 && right  != 1
.names _n26 _n28 _n2a
.def 0
1 1 1
.mv _n2c 4 THINKING HUNGRY EATING READING 
.names _n2c
EATING
# right  != 2
.names right _n2c _n2b
.def 1
- =right 0
# left  != 2 && right  != 1 && right  != 2
.names _n2a _n2b _n2d
.def 0
1 1 1
.names _n2d _n2e
- =_n2d
# state  = 2
.mv state$_n2d_n2f$true 4 THINKING HUNGRY EATING READING 
.names state$_n2d_n2f$true
EATING
# if/else (left  != 2 && right  != 1 && right  != 2)
.mv state$_n2d$raw_n32 4 THINKING HUNGRY EATING READING 
.names state$_n2d_n2f$true state _n2d state$_n2d$raw_n32
- - 0 =state
- - 1 =state$_n2d_n2f$true
# case (state )
.mv state$_n23$raw_n35 4 THINKING HUNGRY EATING READING 
.names state$_n2d$raw_n32 state _n23 state$_n23$raw_n35
- - 0 =state
- - 1 =state$_n2d$raw_n32
.mv state$_n1f$raw_n36 4 THINKING HUNGRY EATING READING 
.names state$_n1f_n22$true state$_n23$raw_n35 _n1f state$_n1f$raw_n36
- - 0 =state$_n23$raw_n35
- - 1 =state$_n1f_n22$true
.mv state$_n13$raw_n3a 4 THINKING HUNGRY EATING READING 
.names state$_n16$raw_n1c state$_n1f$raw_n36 _n13 state$_n13$raw_n3a
- - 0 =state$_n1f$raw_n36
- - 1 =state$_n16$raw_n1c
.mv state$_n9$raw_n3e 4 THINKING HUNGRY EATING READING 
.names state$_nc$raw_n12 state$_n13$raw_n3a _n9 state$_n9$raw_n3e
- - 0 =state$_n13$raw_n3a
- - 1 =state$_nc$raw_n12
# conflict arbitrators
.names out$raw_n8  out
- =out$raw_n8
.names _n9 _ne _n13 _n18 _n1f _n23 _n2e _n42
.def 0
 1 1 - - - - - 1
 0 - 1 1 - - - 1
 0 - 1 0 - - - 1
 0 - 0 - 1 - - 1
 0 - 0 - 0 1 1 1
.mv _n43 4 THINKING HUNGRY EATING READING 
.names _n42 state$_n9$raw_n3e state _n43 
1 - - =state$_n9$raw_n3e
0 - - =state
# non-blocking assignments 
# latches
.r state$raw_n3 state
- =state$raw_n3
.latch _n43 state
# quasi-continuous assignment
.end


.model starvation 
# I/O ports
.inputs starv

.mv starv 4 THINKING HUNGRY EATING READING 
# state  = 0
.names state$raw_n49
0
# non-blocking assignments for initial
.names _n4c
0
.names state _n4c _n4d
.def 0
0 1 1
1 0 1
.names _n4d _n4b
0 1  
1 0  
.names _n4b  _n4a
1 1
0 0
.mv _n50 4 THINKING HUNGRY EATING READING 
.names _n50
HUNGRY
# starv  == 1
.names starv _n50 _n4f
.def 0
- =starv 1
.names _n4f _n51
- =_n4f
# state  = 1
.names state$_n4f_n52$true
1
# if/else (starv  == 1)
.names state$_n4f_n52$true state _n4f state$_n4f$raw_n55
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names _n59
1
.names state _n59 _n5a
.def 0
0 1 1
1 0 1
.names _n5a _n58
0 1  
1 0  
.names _n58  _n57
1 1
0 0
.mv _n5d 4 THINKING HUNGRY EATING READING 
.names _n5d
THINKING
# starv  == 0
.names starv _n5d _n5c
.def 0
- =starv 1
.names _n5c _n5e
- =_n5c
# state  = 0
.names state$_n5c_n5f$true
0
# if/else (starv  == 0)
.names state$_n5c_n5f$true state _n5c state$_n5c$raw_n62
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
# case (state )
.names state$_n5c$raw_n62 state _n57 state$_n57$raw_n66
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names state$_n4f$raw_n55 state$_n57$raw_n66 _n4a state$_n4a$raw_n68
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
# conflict arbitrators
.names _n4a _n51 _n57 _n5e _n6d
.def 0
 1 1 - - 1
 0 - 1 1 1
.names _n6d state$_n4a$raw_n68 state _n6e 
1 0 - 0
1 1 - 1
0 - 0 0
0 - 1 1
# non-blocking assignments 
# latches
.r state$raw_n49 state
0 0
1 1
.latch _n6e state
# quasi-continuous assignment
.end