package mlsolver

  1. Overview
  2. Docs
On This Page
  1. v1.4
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

  1. O
    Oliver Friedmann
  2. M
    Martin Lange

Maintainers

  1. O
    Oliver Friedmann
  2. M
    Martin Lange

Sources

mlsolver-1.5.tbz
sha256=d6500ed80096e38c5c6cfce90d924dd0c426246bc122ae3dbe289392bddae043
sha512=fe7d5c91a4ee00c103ee848b5d6b1220fcd2e202a28ed4d2340cca6b9022c97b62a2f58cc4f31bc50f8030211e6d4230ba83d236f81d3b9bc512bf0014d1e5b4

doc/CHANGES.html

v1.5

  • Change from OASIS to DUNE
  • Change from OCAML 4 to OCAML 5

v1.4

Feb 24 2012 Oliver Friedmann

  • Added CTL+ procedure
  • Various minor improvements
  • Various minor fixes

Jun 14 2010 Oliver Friedmann

  • Removed automatic sorting of formula (see branching-width optimization)
  • Added parameters: -opt prefersmall and -opt preferlarge for sorting formulas

Apr 12 2010 Oliver Friedmann

  • Branching-width of CTL* and CTL games now linearly bounded in the size of the formula

Jan 17 2010 Oliver Friedmann

  • Added Model Checker for CTL
  • Added Validity Checker for CTL
  • Added Dining Philosophers Benchmark
  • Several Bugs Fixed
  • Enabled Local Solving Capabilities