Pushed to
dpous/monaco

bc61c45
gaston benchmarks

Atlassian Sourcetree is a free Git and Mercurial client for Windows.

Atlassian Sourcetree is a free Git and Mercurial client for Mac.

MonaCo: Symbolic Coalgebraic Algorithms for Weak Monadic Second-Order Logic of One Successor (WS1S) Damien Pous CNRS - LIP, ENS Lyon (UMR 5668), France Dmitriy Traytel Department of Computer Science, ETH Zurich, Switzerland This library is distributed under the terms of the GNU Lesser General Public License version 3. See files LICENSE and COPYING. Webpage of the project: http://perso.ens-lyon.fr/damien.pous/monaco This OCaml library contains constructions for M2L/WS1S formulas, that produce symbolic automata out of formulas, which can then be checked for equivalence using the symbolic algorithms provided in the SAFA library. The automata construction uses a variant of Brzozowski derivatives which is due to Dmitriy Traytel. These derivatives are computed symbolically using BDDs, so that one can use the algorithms recently proposed by Damien Pous. Dependencies: ocamlfind, safa (all available through opam) You can compile a standalone program by typing [make]. Run [./monaco.native -help] to get a list of options and the syntax for expressions. Typically [./monaco.native '\A x, \E Y, x\in Y' 'T'] will check whether the two given expressions are equivalent. Alternatively, you can build an OCaml library by typing [make lib], or look at the makefile for other targets. Here is a succinct description of each module: ast : simple datatype for M2L/WS1S formulas formula : normalised M2L/WS1S formulas, symbolic Brzozowski derivatives parse : parser for formulas m2l : M2L automaton ws1s : WS1S automaton monaco : high-level interface of the library, main entry point for standalone program tests : a few sanity tests (not so much for now) bench : a few benchmarks