Ctlplustracenbatype rules = Ctlstartracenba.rulestype ctlplus_trace_nba_state = | Failed| Waiting| TrackingE of Tcsctlstarformula.block| TrackingA of Tcsctlstarformula.block * intval ctlplus_trace_nba :
Tcsctlstarformula.decomposed_ctlstar_formula ->
(ctlplus_trace_nba_state, rules) Tcsautomata.NBA.tval ctlplus_trace_nba_state_size :
Tcsctlstarformula.decomposed_ctlstar_formula ->
Tcsautomata.NMAFunctions.state_size