# vl2mv dcnew.v # version: 0.2 # date: 11:13:36 12/11/95 (PST) .model dchek # I/O ports .mv interpretation 2 go stop .mv charger 2 discharged charged .mv ts_power 2 on off .mv track3 2 conduct open .mv train 3 present1 present2 absent .mv contact 3 B middle C .mv lamp 2 lit unlit .mv relay 2 pulling neutral .mv track2 2 conduct open .mv track1 2 conduct open .subckt track_mod trk1 track=track1 .subckt track_mod trk2 track=track2 .subckt track_mod trk3 track=track3 .subckt charger_mod chg ts_power=ts_power lamp=lamp out=charger .subckt relay_mod rly charger=charger relay=relay .subckt lamp_mod lmp contact=contact wire3=track3 ts_power=ts_power charger=charger lamp=lamp .subckt contact_mod cnt relay=relay contact=contact .subckt train_mod trn out=train .subckt track_system_mod tsm wire1=track1 wire2=track2 train=train contact=contact ts_power=ts_power .subckt interpretation_mod int lamp=lamp out=interpretation .subckt property_mod prop train=train interpretation=interpretation # conflict arbitrators # non-blocking assignments # latches # quasi-continuous assignment .end .model track_mod # I/O ports .outputs track .mv r_state 3 good faulty1 faulty2 .mv state 3 good faulty1 faulty2 .mv track 2 conduct open # state = 0 .mv state$raw_n0 3 good faulty1 faulty2 .names state$raw_n0 good # non-blocking assignments for initial # assign r_state = $NDset ( 0,1 ) .names r_state good faulty1 # assign track = (state == good ) ? 0 : 1 .mv track$raw_n3 2 conduct open .mv _n5 3 good faulty1 faulty2 .names _n5 good # state == 0 .names state _n5 _n4 .def 0 - =state 1 .mv _n6 2 conduct open .names _n6 conduct .mv _n7 2 conduct open .names _n7 open # (state == 0) ? 0 : 1 .mv _n8 2 conduct open .names _n6 _n7 _n4 _n8 - - 0 =_n7 - - 1 =_n6 .names _n8 track$raw_n3 - =_n8 .mv _na 3 good faulty1 faulty2 .names _na faulty1 # state == 1 .names state _na _n9 .def 0 - =state 1 .names _n9 _nb - =_n9 # state = 1 .mv state$_n9_nc$true 3 good faulty1 faulty2 .names state$_n9_nc$true faulty1 # if/else (state == 1) .mv state$_n9$raw_nf 3 good faulty1 faulty2 .names state$_n9_nc$true state _n9 state$_n9$raw_nf - - 0 =state - - 1 =state$_n9_nc$true .mv _n11 3 good faulty1 faulty2 .names _n11 good # state == 0 .names state$_n9$raw_nf _n11 _n10 .def 0 - =state$_n9$raw_nf 1 .names _n10 _n12 - =_n10 # state = r_state .mv state$_n10_n13$true 3 good faulty1 faulty2 .names r_state state$_n10_n13$true - =r_state # if/else (state == 0) .mv state$_n10$raw_n14 3 good faulty1 faulty2 .names state$_n10_n13$true state$_n9$raw_nf _n10 state$_n10$raw_n14 - - 0 =state$_n9$raw_nf - - 1 =state$_n10_n13$true # conflict arbitrators .names _nb _n12 _n18 .def 0 1 - 1 - 1 1 .mv _n19 3 good faulty1 faulty2 .names _n18 state$_n10$raw_n14 state _n19 1 - - =state$_n10$raw_n14 0 - - =state .names track$raw_n3 track - =track$raw_n3 # non-blocking assignments # latches .r state$raw_n0 state - =state$raw_n0 .latch _n19 state # quasi-continuous assignment .end .model charger_mod # I/O ports .outputs out .inputs ts_power .inputs lamp .mv out 2 discharged charged .mv charger 2 discharged charged .mv r_state 3 good faulty1 faulty2 .mv state 3 good faulty1 faulty2 .mv ts_power 2 on off .mv lamp 2 lit unlit # state = 0 .mv state$raw_n1e 3 good faulty1 faulty2 .names state$raw_n1e good # non-blocking assignments for initial # charger = 0 .mv charger$raw_n1f 2 discharged charged .names charger$raw_n1f discharged # non-blocking assignments for initial # assign r_state = $NDset ( 0,1,2 ) .names r_state good faulty1 faulty2 # assign out = state == faulty1 ? 0 : state == faulty2 ? 1 : charger .mv out$raw_n22 2 discharged charged .mv _n24 3 good faulty1 faulty2 .names _n24 faulty1 # state == 1 .names state _n24 _n23 .def 0 - =state 1 .mv _n26 3 good faulty1 faulty2 .names _n26 faulty2 # state == 2 .names state _n26 _n25 .def 0 - =state 1 .mv _n27 2 discharged charged .names _n27 charged # state == 2 ? 1 : charger .mv _n28 2 discharged charged .names _n27 charger _n25 _n28 - - 0 =charger - - 1 =_n27 .mv _n29 2 discharged charged .names _n29 discharged # state == 1 ? 0 : state == 2 ? 1 : charger .mv _n2a 2 discharged charged .names _n29 _n28 _n23 _n2a - - 0 =_n28 - - 1 =_n29 .names _n2a out$raw_n22 - =_n2a .mv _n2c 3 good faulty1 faulty2 .names _n2c faulty1 # state == 1 .names state _n2c _n2b .def 0 - =state 1 .names _n2b _n2d - =_n2b # state = 1 .mv state$_n2b_n2e$true 3 good faulty1 faulty2 .names state$_n2b_n2e$true faulty1 # if/else (state == 1) .mv state$_n2b$raw_n31 3 good faulty1 faulty2 .names state$_n2b_n2e$true state _n2b state$_n2b$raw_n31 - - 0 =state - - 1 =state$_n2b_n2e$true .mv _n33 3 good faulty1 faulty2 .names _n33 faulty2 # state == 2 .names state$_n2b$raw_n31 _n33 _n32 .def 0 - =state$_n2b$raw_n31 1 .names _n32 _n34 - =_n32 # state = 2 .mv state$_n32_n35$true 3 good faulty1 faulty2 .names state$_n32_n35$true faulty2 # if/else (state == 2) .mv state$_n32$raw_n36 3 good faulty1 faulty2 .names state$_n32_n35$true state$_n2b$raw_n31 _n32 state$_n32$raw_n36 - - 0 =state$_n2b$raw_n31 - - 1 =state$_n32_n35$true .mv _n3b 3 good faulty1 faulty2 .names _n3b good # state == 0 .names state$_n32$raw_n36 _n3b _n3a .def 0 - =state$_n32$raw_n36 1 .names _n3a _n3c - =_n3a # state = r_state .mv state$_n3a_n3d$true 3 good faulty1 faulty2 .names r_state state$_n3a_n3d$true - =r_state .mv _n3f 2 on off .names _n3f on # ts_power == 0 .names ts_power _n3f _n3e .def 0 - =ts_power 1 .names _n3e _n40 - =_n3e # charger = 1 .mv charger$_n3e_n41$true 2 discharged charged .names charger$_n3e_n41$true charged .mv _n43 2 lit unlit .names _n43 lit # lamp == 0 .names lamp _n43 _n42 .def 0 - =lamp 1 .names _n42 _n44 - =_n42 # charger = 0 .mv charger$_n42_n45$true 2 discharged charged .names charger$_n42_n45$true discharged # charger = charger .mv charger$_n42_n46$false 2 discharged charged .names charger charger$_n42_n46$false - =charger # if/else (lamp == 0) .mv charger$_n42$raw_n49 2 discharged charged .names charger$_n42_n45$true charger$_n42_n46$false _n42 charger$_n42$raw_n49 - - 0 =charger$_n42_n46$false - - 1 =charger$_n42_n45$true # if/else (ts_power == 0) .mv charger$_n3e$raw_n51 2 discharged charged .names charger$_n3e_n41$true charger$_n42$raw_n49 _n3e charger$_n3e$raw_n51 - - 0 =charger$_n42$raw_n49 - - 1 =charger$_n3e_n41$true # if/else (state == 0) .mv state$_n3a$raw_n58 3 good faulty1 faulty2 .names state$_n3a_n3d$true state$_n32$raw_n36 _n3a state$_n3a$raw_n58 - - 0 =state$_n32$raw_n36 - - 1 =state$_n3a_n3d$true .mv charger$_n3a$raw_n5b 2 discharged charged .names charger$_n3e$raw_n51 charger _n3a charger$_n3a$raw_n5b - - 0 =charger - - 1 =charger$_n3e$raw_n51 # conflict arbitrators .names out$raw_n22 out - =out$raw_n22 .names _n3c _n40 _n44 _n5e .def 0 1 1 - 1 1 0 1 1 1 0 0 1 .mv _n5f 2 discharged charged .names _n5e charger$_n3a$raw_n5b charger _n5f 1 - - =charger$_n3a$raw_n5b 0 - - =charger .names _n2d _n34 _n3c _n66 .def 0 1 - - 1 - 1 - 1 - - 1 1 .mv _n67 3 good faulty1 faulty2 .names _n66 state$_n3a$raw_n58 state _n67 1 - - =state$_n3a$raw_n58 0 - - =state # non-blocking assignments # latches .r charger$raw_n1f charger - =charger$raw_n1f .latch _n5f charger .r state$raw_n1e state - =state$raw_n1e .latch _n67 state # quasi-continuous assignment .end .model relay_mod # I/O ports .inputs charger .outputs relay .mv charger 2 discharged charged .mv r_state 3 good faulty1 faulty2 .mv state 3 good faulty1 faulty2 .mv relay 2 pulling neutral # state = 0 .mv state$raw_n6e 3 good faulty1 faulty2 .names state$raw_n6e good # non-blocking assignments for initial # assign r_state = $NDset ( 0,1,2 ) .names r_state good faulty1 faulty2 # assign relay = state == faulty1 ? 1 : state == faulty2 ? 0 : state == good && charger == charged ? 0 : 1 .mv relay$raw_n71 2 pulling neutral .mv _n73 3 good faulty1 faulty2 .names _n73 faulty1 # state == 1 .names state _n73 _n72 .def 0 - =state 1 .mv _n75 3 good faulty1 faulty2 .names _n75 faulty2 # state == 2 .names state _n75 _n74 .def 0 - =state 1 .mv _n77 3 good faulty1 faulty2 .names _n77 good # state == 0 .names state _n77 _n76 .def 0 - =state 1 .mv _n79 2 discharged charged .names _n79 charged # charger == 1 .names charger _n79 _n78 .def 0 - =charger 1 # state == 0 && charger == 1 .names _n76 _n78 _n7a .def 0 1 1 1 .mv _n7b 2 pulling neutral .names _n7b pulling .mv _n7c 2 pulling neutral .names _n7c neutral # state == 0 && charger == 1 ? 0 : 1 .mv _n7d 2 pulling neutral .names _n7b _n7c _n7a _n7d - - 0 =_n7c - - 1 =_n7b .mv _n7e 2 pulling neutral .names _n7e pulling # state == 2 ? 0 : state == 0 && charger == 1 ? 0 : 1 .mv _n7f 2 pulling neutral .names _n7e _n7d _n74 _n7f - - 0 =_n7d - - 1 =_n7e .mv _n80 2 pulling neutral .names _n80 neutral # state == 1 ? 1 : state == 2 ? 0 : state == 0 && charger == 1 ? 0 : 1 .mv _n81 2 pulling neutral .names _n80 _n7f _n72 _n81 - - 0 =_n7f - - 1 =_n80 .names _n81 relay$raw_n71 - =_n81 .mv _n83 3 good faulty1 faulty2 .names _n83 faulty1 # state == 1 .names state _n83 _n82 .def 0 - =state 1 .names _n82 _n84 - =_n82 # state = 1 .mv state$_n82_n85$true 3 good faulty1 faulty2 .names state$_n82_n85$true faulty1 # if/else (state == 1) .mv state$_n82$raw_n88 3 good faulty1 faulty2 .names state$_n82_n85$true state _n82 state$_n82$raw_n88 - - 0 =state - - 1 =state$_n82_n85$true .mv _n8a 3 good faulty1 faulty2 .names _n8a faulty2 # state == 2 .names state$_n82$raw_n88 _n8a _n89 .def 0 - =state$_n82$raw_n88 1 .names _n89 _n8b - =_n89 # state = 2 .mv state$_n89_n8c$true 3 good faulty1 faulty2 .names state$_n89_n8c$true faulty2 # if/else (state == 2) .mv state$_n89$raw_n8d 3 good faulty1 faulty2 .names state$_n89_n8c$true state$_n82$raw_n88 _n89 state$_n89$raw_n8d - - 0 =state$_n82$raw_n88 - - 1 =state$_n89_n8c$true .mv _n92 3 good faulty1 faulty2 .names _n92 good # state == 0 .names state$_n89$raw_n8d _n92 _n91 .def 0 - =state$_n89$raw_n8d 1 .names _n91 _n93 - =_n91 # state = r_state .mv state$_n91_n94$true 3 good faulty1 faulty2 .names r_state state$_n91_n94$true - =r_state # if/else (state == 0) .mv state$_n91$raw_n95 3 good faulty1 faulty2 .names state$_n91_n94$true state$_n89$raw_n8d _n91 state$_n91$raw_n95 - - 0 =state$_n89$raw_n8d - - 1 =state$_n91_n94$true # conflict arbitrators .names _n84 _n8b _n93 _n99 .def 0 1 - - 1 - 1 - 1 - - 1 1 .mv _n9a 3 good faulty1 faulty2 .names _n99 state$_n91$raw_n95 state _n9a 1 - - =state$_n91$raw_n95 0 - - =state .names relay$raw_n71 relay - =relay$raw_n71 # non-blocking assignments # latches .r state$raw_n6e state - =state$raw_n6e .latch _n9a state # quasi-continuous assignment .end .model lamp_mod # I/O ports .inputs charger .inputs wire3 .inputs ts_power .outputs lamp .inputs contact .mv charger 2 discharged charged .mv wire3 2 conduct open .mv r_state 3 good faulty1 faulty2 .mv state 3 good faulty1 faulty2 .mv ts_power 2 on off .mv lamp 2 lit unlit .mv contact 3 B middle C # state = 0 .mv state$raw_na0 3 good faulty1 faulty2 .names state$raw_na0 good # non-blocking assignments for initial # assign r_state = $NDset ( 0,1,2 ) .names r_state good faulty1 faulty2 # assign lamp = state == faulty1 ? 1 : state == faulty2 ? 0 : state == good && ((contact == C ) && (wire3 == conduct ) && ((ts_power == on ) | (charger == charged ))) ? 0 : 1 .mv lamp$raw_na3 2 lit unlit .mv _na5 3 good faulty1 faulty2 .names _na5 faulty1 # state == 1 .names state _na5 _na4 .def 0 - =state 1 .mv _na7 3 good faulty1 faulty2 .names _na7 faulty2 # state == 2 .names state _na7 _na6 .def 0 - =state 1 .mv _na9 3 good faulty1 faulty2 .names _na9 good # state == 0 .names state _na9 _na8 .def 0 - =state 1 .mv _nab 3 B middle C .names _nab C # contact == 2 .names contact _nab _naa .def 0 - =contact 1 .mv _nad 2 conduct open .names _nad conduct # wire3 == 0 .names wire3 _nad _nac .def 0 - =wire3 1 # (contact == 2) && (wire3 == 0) .names _naa _nac _nae .def 0 1 1 1 .mv _nb0 2 on off .names _nb0 on # ts_power == 0 .names ts_power _nb0 _naf .def 0 - =ts_power 1 .mv _nb2 2 discharged charged .names _nb2 charged # charger == 1 .names charger _nb2 _nb1 .def 0 - =charger 1 # (ts_power == 0) | (charger == 1) .names _naf _nb1 _nb3 .def 1 0 0 0 # (contact == 2) && (wire3 == 0) && ((ts_power == 0) | (charger == 1)) .names _nae _nb3 _nb4 .def 0 1 1 1 # state == 0 && ((contact == 2) && (wire3 == 0) && ((ts_power == 0) | (charger == 1))) .names _na8 _nb4 _nb5 .def 0 1 1 1 .mv _nb6 2 lit unlit .names _nb6 lit .mv _nb7 2 lit unlit .names _nb7 unlit # state == 0 && ((contact == 2) && (wire3 == 0) && ((ts_power == 0) | (charger == 1))) ? 0 : 1 .mv _nb8 2 lit unlit .names _nb6 _nb7 _nb5 _nb8 - - 0 =_nb7 - - 1 =_nb6 .mv _nb9 2 lit unlit .names _nb9 lit # state == 2 ? 0 : state == 0 && ((contact == 2) && (wire3 == 0) && ((ts_power == 0) | (charger == 1))) ? 0 : 1 .mv _nba 2 lit unlit .names _nb9 _nb8 _na6 _nba - - 0 =_nb8 - - 1 =_nb9 .mv _nbb 2 lit unlit .names _nbb unlit # state == 1 ? 1 : state == 2 ? 0 : state == 0 && ((contact == 2) && (wire3 == 0) && ((ts_power == 0) | (charger == 1))) ? 0 : 1 .mv _nbc 2 lit unlit .names _nbb _nba _na4 _nbc - - 0 =_nba - - 1 =_nbb .names _nbc lamp$raw_na3 - =_nbc .mv _nbe 3 good faulty1 faulty2 .names _nbe faulty1 # state == 1 .names state _nbe _nbd .def 0 - =state 1 .names _nbd _nbf - =_nbd # state = 1 .mv state$_nbd_nc0$true 3 good faulty1 faulty2 .names state$_nbd_nc0$true faulty1 # if/else (state == 1) .mv state$_nbd$raw_nc3 3 good faulty1 faulty2 .names state$_nbd_nc0$true state _nbd state$_nbd$raw_nc3 - - 0 =state - - 1 =state$_nbd_nc0$true .mv _nc5 3 good faulty1 faulty2 .names _nc5 faulty2 # state == 2 .names state$_nbd$raw_nc3 _nc5 _nc4 .def 0 - =state$_nbd$raw_nc3 1 .names _nc4 _nc6 - =_nc4 # state = 2 .mv state$_nc4_nc7$true 3 good faulty1 faulty2 .names state$_nc4_nc7$true faulty2 # if/else (state == 2) .mv state$_nc4$raw_nc8 3 good faulty1 faulty2 .names state$_nc4_nc7$true state$_nbd$raw_nc3 _nc4 state$_nc4$raw_nc8 - - 0 =state$_nbd$raw_nc3 - - 1 =state$_nc4_nc7$true .mv _ncd 3 good faulty1 faulty2 .names _ncd good # state == 0 .names state$_nc4$raw_nc8 _ncd _ncc .def 0 - =state$_nc4$raw_nc8 1 .names _ncc _nce - =_ncc # state = r_state .mv state$_ncc_ncf$true 3 good faulty1 faulty2 .names r_state state$_ncc_ncf$true - =r_state # if/else (state == 0) .mv state$_ncc$raw_nd0 3 good faulty1 faulty2 .names state$_ncc_ncf$true state$_nc4$raw_nc8 _ncc state$_ncc$raw_nd0 - - 0 =state$_nc4$raw_nc8 - - 1 =state$_ncc_ncf$true # conflict arbitrators .names _nbf _nc6 _nce _nd4 .def 0 1 - - 1 - 1 - 1 - - 1 1 .mv _nd5 3 good faulty1 faulty2 .names _nd4 state$_ncc$raw_nd0 state _nd5 1 - - =state$_ncc$raw_nd0 0 - - =state .names lamp$raw_na3 lamp - =lamp$raw_na3 # non-blocking assignments # latches .r state$raw_na0 state - =state$raw_na0 .latch _nd5 state # quasi-continuous assignment .end .model contact_mod # I/O ports .outputs contact .inputs relay .mv r_state 3 good faulty1 faulty2 .mv state 3 good faulty1 faulty2 .mv contact 3 B middle C .mv relay 2 pulling neutral # state = 0 .mv state$raw_nde 3 good faulty1 faulty2 .names state$raw_nde good # non-blocking assignments for initial # assign r_state = $NDset ( 0,1,2 ) .names r_state good faulty1 faulty2 # assign contact = state == faulty1 ? 0 : state == faulty2 ? 2 : state == good && relay == pulling ? 2 : 0 .mv contact$raw_ne1 3 B middle C .mv _ne3 3 good faulty1 faulty2 .names _ne3 faulty1 # state == 1 .names state _ne3 _ne2 .def 0 - =state 1 .mv _ne5 3 good faulty1 faulty2 .names _ne5 faulty2 # state == 2 .names state _ne5 _ne4 .def 0 - =state 1 .mv _ne7 3 good faulty1 faulty2 .names _ne7 good # state == 0 .names state _ne7 _ne6 .def 0 - =state 1 .mv _ne9 2 pulling neutral .names _ne9 pulling # relay == 0 .names relay _ne9 _ne8 .def 0 - =relay 1 # state == 0 && relay == 0 .names _ne6 _ne8 _nea .def 0 1 1 1 .mv _neb 3 B middle C .names _neb C .mv _nec 3 B middle C .names _nec B # state == 0 && relay == 0 ? 2 : 0 .mv _ned 3 B middle C .names _neb _nec _nea _ned - - 0 =_nec - - 1 =_neb .mv _nee 3 B middle C .names _nee C # state == 2 ? 2 : state == 0 && relay == 0 ? 2 : 0 .mv _nef 3 B middle C .names _nee _ned _ne4 _nef - - 0 =_ned - - 1 =_nee .mv _nf0 3 B middle C .names _nf0 B # state == 1 ? 0 : state == 2 ? 2 : state == 0 && relay == 0 ? 2 : 0 .mv _nf1 3 B middle C .names _nf0 _nef _ne2 _nf1 - - 0 =_nef - - 1 =_nf0 .names _nf1 contact$raw_ne1 - =_nf1 .mv _nf3 3 good faulty1 faulty2 .names _nf3 faulty1 # state == 1 .names state _nf3 _nf2 .def 0 - =state 1 .names _nf2 _nf4 - =_nf2 # state = 1 .mv state$_nf2_nf5$true 3 good faulty1 faulty2 .names state$_nf2_nf5$true faulty1 # if/else (state == 1) .mv state$_nf2$raw_nf8 3 good faulty1 faulty2 .names state$_nf2_nf5$true state _nf2 state$_nf2$raw_nf8 - - 0 =state - - 1 =state$_nf2_nf5$true .mv _nfa 3 good faulty1 faulty2 .names _nfa faulty2 # state == 2 .names state$_nf2$raw_nf8 _nfa _nf9 .def 0 - =state$_nf2$raw_nf8 1 .names _nf9 _nfb - =_nf9 # state = 2 .mv state$_nf9_nfc$true 3 good faulty1 faulty2 .names state$_nf9_nfc$true faulty2 # if/else (state == 2) .mv state$_nf9$raw_nfd 3 good faulty1 faulty2 .names state$_nf9_nfc$true state$_nf2$raw_nf8 _nf9 state$_nf9$raw_nfd - - 0 =state$_nf2$raw_nf8 - - 1 =state$_nf9_nfc$true .mv _n102 3 good faulty1 faulty2 .names _n102 good # state == 0 .names state$_nf9$raw_nfd _n102 _n101 .def 0 - =state$_nf9$raw_nfd 1 .names _n101 _n103 - =_n101 # state = r_state .mv state$_n101_n104$true 3 good faulty1 faulty2 .names r_state state$_n101_n104$true - =r_state # if/else (state == 0) .mv state$_n101$raw_n105 3 good faulty1 faulty2 .names state$_n101_n104$true state$_nf9$raw_nfd _n101 state$_n101$raw_n105 - - 0 =state$_nf9$raw_nfd - - 1 =state$_n101_n104$true # conflict arbitrators .names _nf4 _nfb _n103 _n109 .def 0 1 - - 1 - 1 - 1 - - 1 1 .mv _n10a 3 good faulty1 faulty2 .names _n109 state$_n101$raw_n105 state _n10a 1 - - =state$_n101$raw_n105 0 - - =state .names contact$raw_ne1 contact - =contact$raw_ne1 # non-blocking assignments # latches .r state$raw_nde state - =state$raw_nde .latch _n10a state # quasi-continuous assignment .end .model train_mod # I/O ports .outputs out .mv r9_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r8_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r6_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r5_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv out 3 present1 present2 absent .mv r10_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r3_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r2_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r4_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r1_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .mv r7_train 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 # train = 0 .mv train$raw_n110 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$raw_n110 t1 # non-blocking assignments for initial # assign r1_train = $NDset ( 0,1 ) .names r1_train t1 t2 # assign r2_train = $NDset ( 1,2 ) .names r2_train t2 t3 # assign r3_train = $NDset ( 2,3 ) .names r3_train t3 t4 # assign r4_train = $NDset ( 3,4 ) .names r4_train t4 t5 # assign r5_train = $NDset ( 4,5 ) .names r5_train t5 t6 # assign r6_train = $NDset ( 5,6 ) .names r6_train t6 t7 # assign r7_train = $NDset ( 6,7 ) .names r7_train t7 t8 # assign r8_train = $NDset ( 7,8 ) .names r8_train t8 t9 # assign r9_train = $NDset ( 8,9 ) .names r9_train t9 t10 # assign r10_train = $NDset ( 9,0 ) .names r10_train t10 t1 # assign out = (train == t1 ) ? 2 : 0 .mv out$raw_n125 3 present1 present2 absent .mv _n127 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n127 t1 # train == 0 .names train _n127 _n126 .def 0 - =train 1 .mv _n128 3 present1 present2 absent .names _n128 absent .mv _n129 3 present1 present2 absent .names _n129 present1 # (train == 0) ? 2 : 0 .mv _n12a 3 present1 present2 absent .names _n128 _n129 _n126 _n12a - - 0 =_n129 - - 1 =_n128 .names _n12a out$raw_n125 - =_n12a .mv _n12d 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n12d t1 .names train _n12d _n12c .def 0 - =train 1 .names _n12c _n12b 1 1 0 0 # train = r1_train .mv train$_n12b_n12e$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r1_train train$_n12b_n12e$true - =r1_train .mv _n131 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n131 t2 .names train _n131 _n130 .def 0 - =train 1 .names _n130 _n12f 1 1 0 0 # train = r2_train .mv train$_n12f_n132$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r2_train train$_n12f_n132$true - =r2_train .mv _n135 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n135 t3 .names train _n135 _n134 .def 0 - =train 1 .names _n134 _n133 1 1 0 0 # train = r3_train .mv train$_n133_n136$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r3_train train$_n133_n136$true - =r3_train .mv _n139 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n139 t4 .names train _n139 _n138 .def 0 - =train 1 .names _n138 _n137 1 1 0 0 # train = r4_train .mv train$_n137_n13a$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r4_train train$_n137_n13a$true - =r4_train .mv _n13d 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n13d t5 .names train _n13d _n13c .def 0 - =train 1 .names _n13c _n13b 1 1 0 0 # train = r5_train .mv train$_n13b_n13e$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r5_train train$_n13b_n13e$true - =r5_train .mv _n141 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n141 t6 .names train _n141 _n140 .def 0 - =train 1 .names _n140 _n13f 1 1 0 0 # train = r6_train .mv train$_n13f_n142$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r6_train train$_n13f_n142$true - =r6_train .mv _n145 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n145 t7 .names train _n145 _n144 .def 0 - =train 1 .names _n144 _n143 1 1 0 0 # train = r7_train .mv train$_n143_n146$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r7_train train$_n143_n146$true - =r7_train .mv _n149 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n149 t8 .names train _n149 _n148 .def 0 - =train 1 .names _n148 _n147 1 1 0 0 # train = r8_train .mv train$_n147_n14a$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r8_train train$_n147_n14a$true - =r8_train .mv _n14d 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n14d t9 .names train _n14d _n14c .def 0 - =train 1 .names _n14c _n14b 1 1 0 0 # train = r9_train .mv train$_n14b_n14e$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r9_train train$_n14b_n14e$true - =r9_train .mv _n151 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n151 t10 .names train _n151 _n150 .def 0 - =train 1 .names _n150 _n14f 1 1 0 0 # train = r10_train .mv train$_n14f_n152$true 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names r10_train train$_n14f_n152$true - =r10_train # case (train ) .mv train$_n14f$raw_n155 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n14f_n152$true train _n14f train$_n14f$raw_n155 - - 0 =train - - 1 =train$_n14f_n152$true .mv train$_n14b$raw_n156 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n14b_n14e$true train$_n14f$raw_n155 _n14b train$_n14b$raw_n156 - - 0 =train$_n14f$raw_n155 - - 1 =train$_n14b_n14e$true .mv train$_n147$raw_n15a 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n147_n14a$true train$_n14b$raw_n156 _n147 train$_n147$raw_n15a - - 0 =train$_n14b$raw_n156 - - 1 =train$_n147_n14a$true .mv train$_n143$raw_n15e 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n143_n146$true train$_n147$raw_n15a _n143 train$_n143$raw_n15e - - 0 =train$_n147$raw_n15a - - 1 =train$_n143_n146$true .mv train$_n13f$raw_n162 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n13f_n142$true train$_n143$raw_n15e _n13f train$_n13f$raw_n162 - - 0 =train$_n143$raw_n15e - - 1 =train$_n13f_n142$true .mv train$_n13b$raw_n166 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n13b_n13e$true train$_n13f$raw_n162 _n13b train$_n13b$raw_n166 - - 0 =train$_n13f$raw_n162 - - 1 =train$_n13b_n13e$true .mv train$_n137$raw_n16a 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n137_n13a$true train$_n13b$raw_n166 _n137 train$_n137$raw_n16a - - 0 =train$_n13b$raw_n166 - - 1 =train$_n137_n13a$true .mv train$_n133$raw_n16e 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n133_n136$true train$_n137$raw_n16a _n133 train$_n133$raw_n16e - - 0 =train$_n137$raw_n16a - - 1 =train$_n133_n136$true .mv train$_n12f$raw_n172 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n12f_n132$true train$_n133$raw_n16e _n12f train$_n12f$raw_n172 - - 0 =train$_n133$raw_n16e - - 1 =train$_n12f_n132$true .mv train$_n12b$raw_n176 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names train$_n12b_n12e$true train$_n12f$raw_n172 _n12b train$_n12b$raw_n176 - - 0 =train$_n12f$raw_n172 - - 1 =train$_n12b_n12e$true # conflict arbitrators .names out$raw_n125 out - =out$raw_n125 .names _n12b _n12f _n133 _n137 _n13b _n13f _n143 _n147 _n14b _n14f _n17a .def 0 1 - - - - - - - - - 1 0 1 - - - - - - - - 1 0 0 1 - - - - - - - 1 0 0 0 1 - - - - - - 1 0 0 0 0 1 - - - - - 1 0 0 0 0 0 1 - - - - 1 0 0 0 0 0 0 1 - - - 1 0 0 0 0 0 0 0 1 - - 1 0 0 0 0 0 0 0 0 1 - 1 0 0 0 0 0 0 0 0 0 1 1 .mv _n17b 10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 .names _n17a train$_n12b$raw_n176 train _n17b 1 - - =train$_n12b$raw_n176 0 - - =train # non-blocking assignments # latches .r train$raw_n110 train - =train$raw_n110 .latch _n17b train # quasi-continuous assignment .end .model track_system_mod # I/O ports .inputs wire1 .inputs wire2 .outputs ts_power .inputs train .inputs contact .mv wire1 2 conduct open .mv wire2 2 conduct open .mv r_state 3 good faulty1 faulty2 .mv state 3 good faulty1 faulty2 .mv ts_power 2 on off .mv train 3 present1 present2 absent .mv contact 3 B middle C # state = 0 .mv state$raw_n192 3 good faulty1 faulty2 .names state$raw_n192 good # non-blocking assignments for initial # assign r_state = $NDset ( 0,1,2 ) .names r_state good faulty1 faulty2 # assign ts_power = state == faulty1 ? 0 : state == faulty2 ? 1 : state == good && ((wire1 == conduct ) && (wire2 == conduct ) && ((train != absent ) | (contact == B ))) ? 0 : 1 .mv ts_power$raw_n195 2 on off .mv _n197 3 good faulty1 faulty2 .names _n197 faulty1 # state == 1 .names state _n197 _n196 .def 0 - =state 1 .mv _n199 3 good faulty1 faulty2 .names _n199 faulty2 # state == 2 .names state _n199 _n198 .def 0 - =state 1 .mv _n19b 3 good faulty1 faulty2 .names _n19b good # state == 0 .names state _n19b _n19a .def 0 - =state 1 .mv _n19d 2 conduct open .names _n19d conduct # wire1 == 0 .names wire1 _n19d _n19c .def 0 - =wire1 1 .mv _n19f 2 conduct open .names _n19f conduct # wire2 == 0 .names wire2 _n19f _n19e .def 0 - =wire2 1 # (wire1 == 0) && (wire2 == 0) .names _n19c _n19e _n1a0 .def 0 1 1 1 .mv _n1a2 3 present1 present2 absent .names _n1a2 absent # train != 2 .names train _n1a2 _n1a1 .def 1 - =train 0 .mv _n1a4 3 B middle C .names _n1a4 B # contact == 0 .names contact _n1a4 _n1a3 .def 0 - =contact 1 # (train != 2) | (contact == 0) .names _n1a1 _n1a3 _n1a5 .def 1 0 0 0 # (wire1 == 0) && (wire2 == 0) && ((train != 2) | (contact == 0)) .names _n1a0 _n1a5 _n1a6 .def 0 1 1 1 # state == 0 && ((wire1 == 0) && (wire2 == 0) && ((train != 2) | (contact == 0))) .names _n19a _n1a6 _n1a7 .def 0 1 1 1 .mv _n1a8 2 on off .names _n1a8 on .mv _n1a9 2 on off .names _n1a9 off # state == 0 && ((wire1 == 0) && (wire2 == 0) && ((train != 2) | (contact == 0))) ? 0 : 1 .mv _n1aa 2 on off .names _n1a8 _n1a9 _n1a7 _n1aa - - 0 =_n1a9 - - 1 =_n1a8 .mv _n1ab 2 on off .names _n1ab off # state == 2 ? 1 : state == 0 && ((wire1 == 0) && (wire2 == 0) && ((train != 2) | (contact == 0))) ? 0 : 1 .mv _n1ac 2 on off .names _n1ab _n1aa _n198 _n1ac - - 0 =_n1aa - - 1 =_n1ab .mv _n1ad 2 on off .names _n1ad on # state == 1 ? 0 : state == 2 ? 1 : state == 0 && ((wire1 == 0) && (wire2 == 0) && ((train != 2) | (contact == 0))) ? 0 : 1 .mv _n1ae 2 on off .names _n1ad _n1ac _n196 _n1ae - - 0 =_n1ac - - 1 =_n1ad .names _n1ae ts_power$raw_n195 - =_n1ae .mv _n1b0 3 good faulty1 faulty2 .names _n1b0 faulty1 # state == 1 .names state _n1b0 _n1af .def 0 - =state 1 .names _n1af _n1b1 - =_n1af # state = 1 .mv state$_n1af_n1b2$true 3 good faulty1 faulty2 .names state$_n1af_n1b2$true faulty1 # if/else (state == 1) .mv state$_n1af$raw_n1b5 3 good faulty1 faulty2 .names state$_n1af_n1b2$true state _n1af state$_n1af$raw_n1b5 - - 0 =state - - 1 =state$_n1af_n1b2$true .mv _n1b7 3 good faulty1 faulty2 .names _n1b7 faulty2 # state == 2 .names state$_n1af$raw_n1b5 _n1b7 _n1b6 .def 0 - =state$_n1af$raw_n1b5 1 .names _n1b6 _n1b8 - =_n1b6 # state = 2 .mv state$_n1b6_n1b9$true 3 good faulty1 faulty2 .names state$_n1b6_n1b9$true faulty2 # if/else (state == 2) .mv state$_n1b6$raw_n1ba 3 good faulty1 faulty2 .names state$_n1b6_n1b9$true state$_n1af$raw_n1b5 _n1b6 state$_n1b6$raw_n1ba - - 0 =state$_n1af$raw_n1b5 - - 1 =state$_n1b6_n1b9$true .mv _n1bf 3 good faulty1 faulty2 .names _n1bf good # state == 0 .names state$_n1b6$raw_n1ba _n1bf _n1be .def 0 - =state$_n1b6$raw_n1ba 1 .names _n1be _n1c0 - =_n1be # state = r_state .mv state$_n1be_n1c1$true 3 good faulty1 faulty2 .names r_state state$_n1be_n1c1$true - =r_state # if/else (state == 0) .mv state$_n1be$raw_n1c2 3 good faulty1 faulty2 .names state$_n1be_n1c1$true state$_n1b6$raw_n1ba _n1be state$_n1be$raw_n1c2 - - 0 =state$_n1b6$raw_n1ba - - 1 =state$_n1be_n1c1$true # conflict arbitrators .names _n1b1 _n1b8 _n1c0 _n1c6 .def 0 1 - - 1 - 1 - 1 - - 1 1 .mv _n1c7 3 good faulty1 faulty2 .names _n1c6 state$_n1be$raw_n1c2 state _n1c7 1 - - =state$_n1be$raw_n1c2 0 - - =state .names ts_power$raw_n195 ts_power - =ts_power$raw_n195 # non-blocking assignments # latches .r state$raw_n192 state - =state$raw_n192 .latch _n1c7 state # quasi-continuous assignment .end .model interpretation_mod # I/O ports .outputs out .inputs lamp .mv out 2 go stop .mv state 6 stop1 stop2 go1 go2 go3 go4 .mv lamp 2 lit unlit # state = 0 .mv state$raw_n1cf 6 stop1 stop2 go1 go2 go3 go4 .names state$raw_n1cf stop1 # non-blocking assignments for initial # assign out = state == go3 | state == go4 ? 0 : 1 .mv out$raw_n1d0 2 go stop .mv _n1d2 6 stop1 stop2 go1 go2 go3 go4 .names _n1d2 go3 # state == 4 .names state _n1d2 _n1d1 .def 0 - =state 1 .mv _n1d4 6 stop1 stop2 go1 go2 go3 go4 .names _n1d4 go4 # state == 5 .names state _n1d4 _n1d3 .def 0 - =state 1 # state == 4 | state == 5 .names _n1d1 _n1d3 _n1d5 .def 1 0 0 0 .mv _n1d6 2 go stop .names _n1d6 go .mv _n1d7 2 go stop .names _n1d7 stop # state == 4 | state == 5 ? 0 : 1 .mv _n1d8 2 go stop .names _n1d6 _n1d7 _n1d5 _n1d8 - - 0 =_n1d7 - - 1 =_n1d6 .names _n1d8 out$raw_n1d0 - =_n1d8 .mv _n1db 6 stop1 stop2 go1 go2 go3 go4 .names _n1db stop1 .names state _n1db _n1da .def 0 - =state 1 .names _n1da _n1d9 1 1 0 0 .mv _n1dd 2 lit unlit .names _n1dd lit # lamp == 0 .names lamp _n1dd _n1dc .def 0 - =lamp 1 .names _n1dc _n1de - =_n1dc # state = 1 .mv state$_n1dc_n1df$true 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1dc_n1df$true stop2 # state = 0 .mv state$_n1dc_n1e0$false 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1dc_n1e0$false stop1 # if/else (lamp == 0) .mv state$_n1dc$raw_n1e2 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1dc_n1df$true state$_n1dc_n1e0$false _n1dc state$_n1dc$raw_n1e2 - - 0 =state$_n1dc_n1e0$false - - 1 =state$_n1dc_n1df$true .mv _n1e7 6 stop1 stop2 go1 go2 go3 go4 .names _n1e7 stop2 .names state _n1e7 _n1e6 .def 0 - =state 1 .names _n1e6 _n1e5 1 1 0 0 .mv _n1e9 2 lit unlit .names _n1e9 unlit # lamp == 1 .names lamp _n1e9 _n1e8 .def 0 - =lamp 1 .names _n1e8 _n1ea - =_n1e8 # state = 2 .mv state$_n1e8_n1eb$true 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1e8_n1eb$true go1 # state = 0 .mv state$_n1e8_n1ec$false 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1e8_n1ec$false stop1 # if/else (lamp == 1) .mv state$_n1e8$raw_n1ee 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1e8_n1eb$true state$_n1e8_n1ec$false _n1e8 state$_n1e8$raw_n1ee - - 0 =state$_n1e8_n1ec$false - - 1 =state$_n1e8_n1eb$true .mv _n1f3 6 stop1 stop2 go1 go2 go3 go4 .names _n1f3 go1 .names state _n1f3 _n1f2 .def 0 - =state 1 .names _n1f2 _n1f1 1 1 0 0 .mv _n1f5 2 lit unlit .names _n1f5 lit # lamp == 0 .names lamp _n1f5 _n1f4 .def 0 - =lamp 1 .names _n1f4 _n1f6 - =_n1f4 # state = 3 .mv state$_n1f4_n1f7$true 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1f4_n1f7$true go2 # state = 0 .mv state$_n1f4_n1f8$false 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1f4_n1f8$false stop1 # if/else (lamp == 0) .mv state$_n1f4$raw_n1fa 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1f4_n1f7$true state$_n1f4_n1f8$false _n1f4 state$_n1f4$raw_n1fa - - 0 =state$_n1f4_n1f8$false - - 1 =state$_n1f4_n1f7$true .mv _n1ff 6 stop1 stop2 go1 go2 go3 go4 .names _n1ff go2 .names state _n1ff _n1fe .def 0 - =state 1 .names _n1fe _n1fd 1 1 0 0 .mv _n201 2 lit unlit .names _n201 unlit # lamp == 1 .names lamp _n201 _n200 .def 0 - =lamp 1 .names _n200 _n202 - =_n200 # state = 4 .mv state$_n200_n203$true 6 stop1 stop2 go1 go2 go3 go4 .names state$_n200_n203$true go3 # state = 0 .mv state$_n200_n204$false 6 stop1 stop2 go1 go2 go3 go4 .names state$_n200_n204$false stop1 # if/else (lamp == 1) .mv state$_n200$raw_n206 6 stop1 stop2 go1 go2 go3 go4 .names state$_n200_n203$true state$_n200_n204$false _n200 state$_n200$raw_n206 - - 0 =state$_n200_n204$false - - 1 =state$_n200_n203$true .mv _n20b 6 stop1 stop2 go1 go2 go3 go4 .names _n20b go3 .names state _n20b _n20a .def 0 - =state 1 .names _n20a _n209 1 1 0 0 .mv _n20d 2 lit unlit .names _n20d lit # lamp == 0 .names lamp _n20d _n20c .def 0 - =lamp 1 .names _n20c _n20e - =_n20c # state = 5 .mv state$_n20c_n20f$true 6 stop1 stop2 go1 go2 go3 go4 .names state$_n20c_n20f$true go4 # state = 0 .mv state$_n20c_n210$false 6 stop1 stop2 go1 go2 go3 go4 .names state$_n20c_n210$false stop1 # if/else (lamp == 0) .mv state$_n20c$raw_n212 6 stop1 stop2 go1 go2 go3 go4 .names state$_n20c_n20f$true state$_n20c_n210$false _n20c state$_n20c$raw_n212 - - 0 =state$_n20c_n210$false - - 1 =state$_n20c_n20f$true .mv _n217 6 stop1 stop2 go1 go2 go3 go4 .names _n217 go4 .names state _n217 _n216 .def 0 - =state 1 .names _n216 _n215 1 1 0 0 .mv _n219 2 lit unlit .names _n219 unlit # lamp == 1 .names lamp _n219 _n218 .def 0 - =lamp 1 .names _n218 _n21a - =_n218 # state = 4 .mv state$_n218_n21b$true 6 stop1 stop2 go1 go2 go3 go4 .names state$_n218_n21b$true go3 # state = 0 .mv state$_n218_n21c$false 6 stop1 stop2 go1 go2 go3 go4 .names state$_n218_n21c$false stop1 # if/else (lamp == 1) .mv state$_n218$raw_n21e 6 stop1 stop2 go1 go2 go3 go4 .names state$_n218_n21b$true state$_n218_n21c$false _n218 state$_n218$raw_n21e - - 0 =state$_n218_n21c$false - - 1 =state$_n218_n21b$true # case (state ) .mv state$_n215$raw_n223 6 stop1 stop2 go1 go2 go3 go4 .names state$_n218$raw_n21e state _n215 state$_n215$raw_n223 - - 0 =state - - 1 =state$_n218$raw_n21e .mv state$_n209$raw_n224 6 stop1 stop2 go1 go2 go3 go4 .names state$_n20c$raw_n212 state$_n215$raw_n223 _n209 state$_n209$raw_n224 - - 0 =state$_n215$raw_n223 - - 1 =state$_n20c$raw_n212 .mv state$_n1fd$raw_n228 6 stop1 stop2 go1 go2 go3 go4 .names state$_n200$raw_n206 state$_n209$raw_n224 _n1fd state$_n1fd$raw_n228 - - 0 =state$_n209$raw_n224 - - 1 =state$_n200$raw_n206 .mv state$_n1f1$raw_n22c 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1f4$raw_n1fa state$_n1fd$raw_n228 _n1f1 state$_n1f1$raw_n22c - - 0 =state$_n1fd$raw_n228 - - 1 =state$_n1f4$raw_n1fa .mv state$_n1e5$raw_n230 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1e8$raw_n1ee state$_n1f1$raw_n22c _n1e5 state$_n1e5$raw_n230 - - 0 =state$_n1f1$raw_n22c - - 1 =state$_n1e8$raw_n1ee .mv state$_n1d9$raw_n234 6 stop1 stop2 go1 go2 go3 go4 .names state$_n1dc$raw_n1e2 state$_n1e5$raw_n230 _n1d9 state$_n1d9$raw_n234 - - 0 =state$_n1e5$raw_n230 - - 1 =state$_n1dc$raw_n1e2 # conflict arbitrators .names out$raw_n1d0 out - =out$raw_n1d0 .names _n1d9 _n1de _n1e5 _n1ea _n1f1 _n1f6 _n1fd _n202 _n209 _n20e _n215 _n21a _n238 .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 0 - 0 - 0 - 0 - 1 1 - - 1 0 - 0 - 0 - 0 - 1 0 - - 1 0 - 0 - 0 - 0 - 0 - 1 1 1 0 - 0 - 0 - 0 - 0 - 1 0 1 .mv _n239 6 stop1 stop2 go1 go2 go3 go4 .names _n238 state$_n1d9$raw_n234 state _n239 1 - - =state$_n1d9$raw_n234 0 - - =state # non-blocking assignments # latches .r state$raw_n1cf state - =state$raw_n1cf .latch _n239 state # quasi-continuous assignment .end .model property_mod # I/O ports .inputs interpretation .inputs train .mv interpretation 2 go stop .mv state 2 good bad .mv train 3 present1 present2 absent # state = 0 .mv state$raw_n23d 2 good bad .names state$raw_n23d good # non-blocking assignments for initial .mv _n23f 3 present1 present2 absent .names _n23f present2 # train == 1 .names train _n23f _n23e .def 0 - =train 1 .mv _n241 2 go stop .names _n241 go # interpretation == 0 .names interpretation _n241 _n240 .def 0 - =interpretation 1 # (train == 1) && (interpretation == 0) .names _n23e _n240 _n242 .def 0 1 1 1 .mv _n244 2 good bad .names _n244 bad # state == 1 .names state _n244 _n243 .def 0 - =state 1 # ((train == 1) && (interpretation == 0)) | (state == 1) .names _n242 _n243 _n245 .def 1 0 0 0 .names _n245 _n246 - =_n245 # state = 1 .mv state$_n245_n247$true 2 good bad .names state$_n245_n247$true bad # state = 0 .mv state$_n245_n248$false 2 good bad .names state$_n245_n248$false good # if/else (((train == 1) && (interpretation == 0)) | (state == 1)) .mv state$_n245$raw_n24a 2 good bad .names state$_n245_n247$true state$_n245_n248$false _n245 state$_n245$raw_n24a - - 0 =state$_n245_n248$false - - 1 =state$_n245_n247$true # conflict arbitrators .names _n246 _n24d .def 0 1 1 0 1 .mv _n24e 2 good bad .names _n24d state$_n245$raw_n24a state _n24e 1 - - =state$_n245$raw_n24a 0 - - =state # non-blocking assignments # latches .r state$raw_n23d state - =state$raw_n23d .latch _n24e state # quasi-continuous assignment .end