Ctlstartracenba (p.mlsolver.1.5.doc.mlsolver.Ctlstartracenba)

type rules =

| Branch of Tcsctlstarformula.block * int * bool
| Follow of Tcsctlstarformula.block * int
| Next0
| Next1 of Tcsctlstarformula.block
| Delete of Tcsctlstarformula.block * int
| DeleteBlock of Tcsctlstarformula.block

val ctlstar_trace_nba_format_rule : 
  Tcsctlstarformula.decomposed_ctlstar_formula ->
  rules ->
  string

type ('a, 'b) ctlstar_trace_nba_state =

| Failed
| Waiting
| TrackingE of Tcsctlstarformula.block * 'a
| TrackingA of Tcsctlstarformula.block * 'b

val ctlstar_trace_nba : 
  Tcsctlstarformula.decomposed_ctlstar_formula ->
  ('a, Ctlstarthreadnba.rules) Tcsautomata.DBA.t ->
  ('b, Ctlstarthreadnba.rules) Tcsautomata.NBA.t ->
  (('a, 'b) ctlstar_trace_nba_state, rules) Tcsautomata.NBA.t

val ctlstar_trace_nba_state_size : 
  Tcsctlstarformula.decomposed_ctlstar_formula ->
  Tcsautomata.NMAFunctions.state_size ->
  Tcsautomata.NMAFunctions.state_size ->
  Tcsautomata.NMAFunctions.state_size