package mlsolver

You can search for identifiers within the package.

in-package search v0.2.0

A tool for solving the satisfiability and validity problems for modal fixpoint logics

Install

dune-project

Dependency

github.com Readme Changelog BSD-3-clause License Edit opam file Versions (1)

Authors

Maintainers

Sources

mlsolver-1.5.tbz

sha256=d6500ed80096e38c5c6cfce90d924dd0c426246bc122ae3dbe289392bddae043

sha512=fe7d5c91a4ee00c103ee848b5d6b1220fcd2e202a28ed4d2340cca6b9022c97b62a2f58cc4f31bc50f8030211e6d4230ba83d236f81d3b9bc512bf0014d1e5b4

doc/mlsolver/Modelcheckinggamesregistry/index.html

Module `Modelcheckinggamesregistry`

type modelchecking_answer =

| ModelSatisfiesFormula
| ModelFalsifiesFormula

type modelchecking_procedure =
  Tcsmetaformula.formula_expr ->
  in_channel ->
  string array ->
  (Tcsmessage.MessageChannel.message_channel
   * Tcsmessage.MessageChannel.message_channel
   * Tcsmessage.MessageChannel.message_channel) ->
  int Tcsgames.initpg
  * (unit ->
  unit)
  * (int Tcsgames.initpg_solution ->
  modelchecking_answer)

val register_modelchecking_procedure : 
  modelchecking_procedure ->
  string ->
  string ->
  unit

val mem_modelchecking_procedure : string -> bool

val find_modelchecking_procedure : string -> modelchecking_procedure * string

val enum_modelchecking_procedures : 
  (modelchecking_procedure -> string -> string -> unit) ->
  unit

val fold_modelchecking_procedures : 
  (modelchecking_procedure -> string -> string -> 'a -> 'a) ->
  'a ->
  'a