package mlsolver
A tool for solving the satisfiability and validity problems for modal fixpoint logics
Install
dune-project
Dependency
Authors
Maintainers
Sources
mlsolver-1.5.tbz
sha256=d6500ed80096e38c5c6cfce90d924dd0c426246bc122ae3dbe289392bddae043
sha512=fe7d5c91a4ee00c103ee848b5d6b1220fcd2e202a28ed4d2340cca6b9022c97b62a2f58cc4f31bc50f8030211e6d4230ba83d236f81d3b9bc512bf0014d1e5b4
doc/mlsolver/Ctlplustracenba/index.html
Module Ctlplustracenba
type rules = Ctlstartracenba.rulestype ctlplus_trace_nba_state = | Failed| Waiting| TrackingE of Tcsctlstarformula.block| TrackingA of Tcsctlstarformula.block * int
val 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