source: vis_dev/vis-2.3/models/transition/simple.mv @ 31

# vl2mv simple.v 
# version: 2.1
# date:    16:16:51 12/06/2011 (CET)
.model concret 
# I/O ports
.inputs i
# p  = 0
.names p$raw_n0
0
# q  = 0
.names q$raw_n1
0
# state [1 : 0] = 0
.names state$raw_n2<0>
0
.names state$raw_n2<1>
0
# non-blocking assignments for initial
.names _n5<0>
0
.names _n5<1>
0
.names state<0> _n5<0> _n6<0>
.def 0
0 1 1
1 0 1
.names state<1> _n5<1> _n6<1>
.def 0
0 1 1
1 0 1
.names _n6<0> _n6<1> _n7
.def 1
0 0 0
.names _n7 _n4
0 1  
1 0  
.names _n4  _n3
.def 1
0 0
.names _n9
1
# i  == 1
.names i _n9 _na
.def 0
0 1 1
1 0 1
.names _na _n8
0 1  
1 0  
.names _n8 _nc
- =_n8
# state [1 : 0] = 1
.names state$_n8_nd$true<0>
1
.names state$_n8_nd$true<1>
0
# p  = 0
.names p$_n8_ne$true
0
# q  = 1
.names q$_n8_nf$true
1
# state [1 : 0] = 2
.names state$_n8_n10$false<0>
0
.names state$_n8_n10$false<1>
1
# p  = 1
.names p$_n8_n11$false
1
# q  = 0
.names q$_n8_n12$false
0
# if/else (i  == 1)
.names _n8 p$_n8_ne$true p$_n8_n11$false p$_n8$raw_n16
.def 0
1 1 - 1
0 - 1 1
.names _n8 q$_n8_nf$true q$_n8_n12$false q$_n8$raw_n18
.def 0
1 1 - 1
0 - 1 1
.names _n8 state$_n8_nd$true<0> state$_n8_n10$false<0> state$_n8$raw_n1a<0>
.def 0
1 1 - 1
0 - 1 1
.names _n8 state$_n8_nd$true<1> state$_n8_n10$false<1> state$_n8$raw_n1a<1>
.def 0
1 1 - 1
0 - 1 1
.names _n25<0>
1
.names _n25<1>
0
.names state<0> _n25<0> _n26<0>
.def 0
0 1 1
1 0 1
.names state<1> _n25<1> _n26<1>
.def 0
0 1 1
1 0 1
.names _n26<0> _n26<1> _n27
.def 1
0 0 0
.names _n27 _n24
0 1  
1 0  
.names _n24  _n23
.def 1
0 0
.names _n29
1
# i  == 1
.names i _n29 _n2a
.def 0
0 1 1
1 0 1
.names _n2a _n28
0 1  
1 0  
.names _n28 _n2c
- =_n28
# state [1 : 0] = 1
.names state$_n28_n2d$true<0>
1
.names state$_n28_n2d$true<1>
0
# p  = 0
.names p$_n28_n2e$true
0
# q  = 1
.names q$_n28_n2f$true
1
# state [1 : 0] = 3
.names state$_n28_n30$false<0>
1
.names state$_n28_n30$false<1>
1
# p  = 1
.names p$_n28_n31$false
1
# q  = 1
.names q$_n28_n32$false
1
# if/else (i  == 1)
.names _n28 p$_n28_n2e$true p$_n28_n31$false p$_n28$raw_n36
.def 0
1 1 - 1
0 - 1 1
.names _n28 q$_n28_n2f$true q$_n28_n32$false q$_n28$raw_n38
.def 0
1 1 - 1
0 - 1 1
.names _n28 state$_n28_n2d$true<0> state$_n28_n30$false<0> state$_n28$raw_n3a<0>
.def 0
1 1 - 1
0 - 1 1
.names _n28 state$_n28_n2d$true<1> state$_n28_n30$false<1> state$_n28$raw_n3a<1>
.def 0
1 1 - 1
0 - 1 1
.names _n45<0>
0
.names _n45<1>
1
.names state<0> _n45<0> _n46<0>
.def 0
0 1 1
1 0 1
.names state<1> _n45<1> _n46<1>
.def 0
0 1 1
1 0 1
.names _n46<0> _n46<1> _n47
.def 1
0 0 0
.names _n47 _n44
0 1  
1 0  
.names _n44  _n43
.def 1
0 0
.names _n49
1
# i  == 1
.names i _n49 _n4a
.def 0
0 1 1
1 0 1
.names _n4a _n48
0 1  
1 0  
.names _n48 _n4c
- =_n48
# state [1 : 0] = 2
.names state$_n48_n4d$true<0>
0
.names state$_n48_n4d$true<1>
1
# p  = 1
.names p$_n48_n4e$true
1
# q  = 0
.names q$_n48_n4f$true
0
# state [1 : 0] = 3
.names state$_n48_n50$false<0>
1
.names state$_n48_n50$false<1>
1
# p  = 1
.names p$_n48_n51$false
1
# q  = 1
.names q$_n48_n52$false
1
# if/else (i  == 1)
.names _n48 p$_n48_n4e$true p$_n48_n51$false p$_n48$raw_n56
.def 0
1 1 - 1
0 - 1 1
.names _n48 q$_n48_n4f$true q$_n48_n52$false q$_n48$raw_n58
.def 0
1 1 - 1
0 - 1 1
.names _n48 state$_n48_n4d$true<0> state$_n48_n50$false<0> state$_n48$raw_n5a<0>
.def 0
1 1 - 1
0 - 1 1
.names _n48 state$_n48_n4d$true<1> state$_n48_n50$false<1> state$_n48$raw_n5a<1>
.def 0
1 1 - 1
0 - 1 1
.names _n65<0>
1
.names _n65<1>
1
.names state<0> _n65<0> _n66<0>
.def 0
0 1 1
1 0 1
.names state<1> _n65<1> _n66<1>
.def 0
0 1 1
1 0 1
.names _n66<0> _n66<1> _n67
.def 1
0 0 0
.names _n67 _n64
0 1  
1 0  
.names _n64  _n63
.def 1
0 0
.names _n69
1
# i  == 1
.names i _n69 _n6a
.def 0
0 1 1
1 0 1
.names _n6a _n68
0 1  
1 0  
.names _n68 _n6c
- =_n68
# state [1 : 0] = 2
.names state$_n68_n6d$true<0>
0
.names state$_n68_n6d$true<1>
1
# p  = 1
.names p$_n68_n6e$true
1
# q  = 0
.names q$_n68_n6f$true
0
# state [1 : 0] = 3
.names state$_n68_n70$false<0>
1
.names state$_n68_n70$false<1>
1
# p  = 1
.names p$_n68_n71$false
1
# q  = 1
.names q$_n68_n72$false
1
# if/else (i  == 1)
.names _n68 p$_n68_n6e$true p$_n68_n71$false p$_n68$raw_n76
.def 0
1 1 - 1
0 - 1 1
.names _n68 q$_n68_n6f$true q$_n68_n72$false q$_n68$raw_n78
.def 0
1 1 - 1
0 - 1 1
.names _n68 state$_n68_n6d$true<0> state$_n68_n70$false<0> state$_n68$raw_n7a<0>
.def 0
1 1 - 1
0 - 1 1
.names _n68 state$_n68_n6d$true<1> state$_n68_n70$false<1> state$_n68$raw_n7a<1>
.def 0
1 1 - 1
0 - 1 1
# case (state )
.names _n63 p$_n68$raw_n76 p p$_n63$raw_n89
.def 0
1 1 - 1
0 - 1 1
.names _n63 q$_n68$raw_n78 q q$_n63$raw_n8b
.def 0
1 1 - 1
0 - 1 1
.names _n63 state$_n68$raw_n7a<0> state<0> state$_n63$raw_n8d<0>
.def 0
1 1 - 1
0 - 1 1
.names _n63 state$_n68$raw_n7a<1> state<1> state$_n63$raw_n8d<1>
.def 0
1 1 - 1
0 - 1 1
.names _n43 p$_n48$raw_n56 p$_n63$raw_n89 p$_n43$raw_n90
.def 0
1 1 - 1
0 - 1 1
.names _n43 q$_n48$raw_n58 q$_n63$raw_n8b q$_n43$raw_n92
.def 0
1 1 - 1
0 - 1 1
.names _n43 state$_n48$raw_n5a<0> state$_n63$raw_n8d<0> state$_n43$raw_n94<0>
.def 0
1 1 - 1
0 - 1 1
.names _n43 state$_n48$raw_n5a<1> state$_n63$raw_n8d<1> state$_n43$raw_n94<1>
.def 0
1 1 - 1
0 - 1 1
.names _n23 p$_n28$raw_n36 p$_n43$raw_n90 p$_n23$raw_na0
.def 0
1 1 - 1
0 - 1 1
.names _n23 q$_n28$raw_n38 q$_n43$raw_n92 q$_n23$raw_na2
.def 0
1 1 - 1
0 - 1 1
.names _n23 state$_n28$raw_n3a<0> state$_n43$raw_n94<0> state$_n23$raw_na4<0>
.def 0
1 1 - 1
0 - 1 1
.names _n23 state$_n28$raw_n3a<1> state$_n43$raw_n94<1> state$_n23$raw_na4<1>
.def 0
1 1 - 1
0 - 1 1
.names _n3 p$_n8$raw_n16 p$_n23$raw_na0 p$_n3$raw_nb0
.def 0
1 1 - 1
0 - 1 1
.names _n3 q$_n8$raw_n18 q$_n23$raw_na2 q$_n3$raw_nb2
.def 0
1 1 - 1
0 - 1 1
.names _n3 state$_n8$raw_n1a<0> state$_n23$raw_na4<0> state$_n3$raw_nb4<0>
.def 0
1 1 - 1
0 - 1 1
.names _n3 state$_n8$raw_n1a<1> state$_n23$raw_na4<1> state$_n3$raw_nb4<1>
.def 0
1 1 - 1
0 - 1 1
# conflict arbitrators
.names _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c _nc0
.def 0
 1 1 - - - - - - 1
 1 0 - - - - - - 1
 0 - 1 1 - - - - 1
 0 - 1 0 - - - - 1
 0 - 0 - 1 1 - - 1
 0 - 0 - 1 0 - - 1
 0 - 0 - 0 - 1 1 1
 0 - 0 - 0 - 1 0 1
.names _nc0 p$_n3$raw_nb0 p _nc1 
1 0 - 0
1 1 - 1
0 - 0 0
0 - 1 1
.names _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c _nc2
.def 0
 1 1 - - - - - - 1
 1 0 - - - - - - 1
 0 - 1 1 - - - - 1
 0 - 1 0 - - - - 1
 0 - 0 - 1 1 - - 1
 0 - 0 - 1 0 - - 1
 0 - 0 - 0 - 1 1 1
 0 - 0 - 0 - 1 0 1
.names _nc2 q$_n3$raw_nb2 q _nc3 
1 0 - 0
1 1 - 1
0 - 0 0
0 - 1 1
.names _n3 _nc _n23 _n2c _n43 _n4c _n63 _n6c _nc4
.def 0
 1 1 - - - - - - 1
 1 0 - - - - - - 1
 0 - 1 1 - - - - 1
 0 - 1 0 - - - - 1
 0 - 0 - 1 1 - - 1
 0 - 0 - 1 0 - - 1
 0 - 0 - 0 - 1 1 1
 0 - 0 - 0 - 1 0 1
.names _nc4 state$_n3$raw_nb4<0> state$_n3$raw_nb4<1> state<0> state<1> -> _nc5<0> _nc5<1> 
1 - - - - =state$_n3$raw_nb4<0> =state$_n3$raw_nb4<1> 
0 - - - - =state<0> =state<1> 
# non-blocking assignments 
# latches
.r p$raw_n0 p
0 0
1 1
.latch _nc1 p
.r q$raw_n1 q
0 0
1 1
.latch _nc3 q
.r state$raw_n2<0> state<0>
.def 0
1 1
.r state$raw_n2<1> state<1>
.def 0
1 1
.latch _nc5<0> state<0>
.latch _nc5<1> state<1>
# quasi-continuous assignment
.end