ACME is a tool implementing algebraic techniques to solve decision problems from automata theory. The core generic algorithm takes as input an automaton and computes its stabilization monoid, which is a generalization of its transition monoid.
ACME has been written in OCaml, by Nathanaël Fijalkow and Denis Kuperberg.
ACME uses graphviz to visualize the automata and monoids produced.
See the ATVA'2014 tool paper
- Linux: Type "make linux" to compile, it produces the executable acme.
- Windows: You need the "make" utility package, which you can get here. Use "make win" to compile, it produces acme.exe.
We describe it line by line:
- the first line is the size of the automaton
- the second line is the type of the automaton:
c: classical p: probabilistic n (int): a B-automaton with n counters
- the third line is the alphabet. Each character is a letter, they should not be separated
- the fourth line is the initial states. Each state should be separated by spaces
- the fifth line is the final states. Each state should be separated by spaces
- the next lines are the transition matrices, one for each letter in the input order. A transition matrix is given by actions (like IE,RI, OO, __) separated by spaces. Each matrix is preceded by a single character line, the letter (for readability and checking purposes).
For classical automata (without counters), the transition matrix contains only 1 and _.
The blank lines and lines starting with "%" are ignored.
- Computing the Stabilization Monoid of a
$B$ -Automaton
-sm: Computes the stabilization monoid of a B-automaton and minimizes it
in text verbose mode:
acme -sm Examples/test_sm.txt -textto visualize it using Graphviz:
acme -sm Examples/test_sm.txt -dotty- Checking the Equivalence of two
$B$ -Automata
-equ: Checks whether two B-automata are equivalent
in text verbose mode:
acme -equ Examples/test_equ.txt -textto visualize them using Graphviz:
acme -equ Examples/test_equ.txt -dotty- Running the Markov Monoid Algorithm on a Probabilistic Automaton
-mma: Runs the Markov Monoid algorithm on a probabilistic automaton
in text verbose mode:
acme -mma Examples/test_mma.txt -textto visualize it using Graphviz:
acme -mma Examples/test_mma.txt -dotty- Checking whether a Classical Automaton has the Finite Power Property
-fpp: Checks whether a classical automaton has the finite power property, i.e. whether there exists n such that L^* = L^0 + L^1 + ... + L^n
in text verbose mode:
acme -fpp Examples/test_fpp_true.txt -textTo visualize it using Graphviz:
acme -fpp Examples/test_fpp_true.txt -dotty- Drawing an automaton using Graphviz
-dotty: Produces a file output.gv (DOT format) and output.ps, which can be visualized using graphviz
acme -dotty Examples/test_sm.txt -text