Skip to content
An algorithm that decide if a finite deterministic automaton accepts a set definable in FO[<,mod]
OCaml
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.github
_tags
automaton.ebnf
automaton.ml
automaton.mli
count
formula.dat
formula.ml
formula.mli
formula_min.ml
formula_min.mli
hashcons.ml
hashcons.mli
hmap.ml
hmap.mli
hset.ml
hset.mli
input
int.ml
int.mli
intAr.ml
intAr.mli
intMap.ml
intMap.mli
letter.ml
letter.mli
lexer.mll
main.ml
math.ml
math.mli
oop.ml
oop.mli
pair.ml
parser.mly
pretty.ml
readme
relative.ml
relative.mli
satis.ml
simple.ml
simple.mli
subset.ml
subset.mli
subsets.ml
subsets.mli
transition.ml
transition.mli

readme

This program has been written by Arthur Milchior as part of his Computer Science PhD at University Paris Diderot.

It can be compiled with 
ocamlbuild main.native

The program can run in two modes
In the mode input (default), the program reads a file (by default the file is  ./input, it can otherwise be changed with the command line argument «-input Input_File»), containing automata. The   EBNF of this file is given in automaton.ebnf
the program print "Name of the automaton:OK: a formula defining the set accepted by the state" if the automaton accepts a state definable in the logic, or
"name of the automaton: its description: the property it does not satisfy" otherwise

Note that only the program currently considers only automata reading
set of non-negative integers. The options -none, -quantifier-free and -existential selects whether our algorithm generate no formula, quantifier-free formulas(takes exponential-time), or existential formulas(takes polynomial-time).

In the mode random, selected by the option -random, 1 (or the argument given after the option -number) formulas F of length 10 (or the argument given after the option -size) in dimension 2 (or the argument given after the option -dimension) and base 4 (or the argument given after the option -base). The minimal automaton A accepting the set defined by F is then computed using Büchi-Bruyère algorithm. Our algorithm is then applied to A. The computation time of our algorithm is then appended to formula.dat (this file must already exists)

Arthur@milchior.fr
You can’t perform that action at this time.