=================
                        CFGAnalyzer 
                       =============

          https://github.com/muldvarp/CFGAnalyzer


0) INTRODUCTION
---------------
CFGAnalyzer is a tool that implements semi-decision procedures
for undecidable problems about context-free languages (CFL) and
grammars (CFG).


1) AUTHORSHIP
-------------
CFGAnalyzer was written by Martin Lange, University of Kassel, 
Germany, 2007-2021. 


2) LICENSE
----------
The source code is distributed under the BSD license, see
http://www.opensource.org/licenses/bsd-license.php .


3) REQUIREMENTS
---------------
You will need the following to build a working copy
of cfganalyzer.

- The OCaml compiler. The original code was written for version 3.09.2.
  We recommend using a more recent version, at least 4.07.

- The OCaml packages ocaml-find, ocaml-build and ocaml-sat-solvers.

Both are best installed via the OCaml package manager opam:
https://opam.ocaml.org/


4) INSTALLATION
---------------
1. Download and install opam in the way that is recommended / available
for your operating system. Follow the installation instructions 
including the installation of an OCaml compiler via

> opam switch create 4.07.0

for instance.

2. Install the required packages.

> opam install ocaml-find ocaml-build ocaml-sat-solvers

3. Download CFGAnalyzer-master.zip via the "Code" button on 
https://github.com/muldvarp/CFGAnalyzer, unpack it and change
into the created directory.

> unzip CFGAnalyzer-master.zip
> mv CFGAnalyzer-master CFGAnalyzer
> cd CFGAnalyzer

4. Edit the file Makefile and check that the variables in the top
section point to the right commands on your system.

5. Compile CFGAnalyzer.

> make

This creates a native code executable of CFGAnalyzer called
cfganalyzer in the current directory. If you prefer an OCaml byte 
code executable (which will require the OCaml runtime environment 
to run) use

> make byte 

instead.

5. (optional) To clean up files produced during compilation run

> make clean


5) USAGE GUIDE
--------------
Type `cfganalyzer --help' to see a list of command line switches
and arguments understood by the program. In general it assumes the 
input context-free grammars (CFG) to be given in files listed on the 
command line. In each run, cfganalyzer can analyse the given CFGs
w.r.t. one particular problem. This is specified by an argument again.
For example,

  cfganalyzer -i <file1> <file2> -v 2 -c

will result in cfganalyzer to check whether the language of the CFG
given in <file1> is included ("-i") in the language of the CFG given
in <file2>. It will be quite verbose printing status information 
("-v 2") and it will run continuously ("-c"), i.e. not stop after
finding a counterexample.


6) INPUT FORMAT
---------------
Context-free grammars are specified as follows. A nonterminal can be 
(almost) any string. All productions for a nonterminal must be given 
at once, i.e. not interrupted by productions for another nonterminal. 
It is assumed that the first nonterminal given in the definition is
the starting symbol for the grammar.

Each production is started with a colon and finished with a semi-colon.
Sentential forms are denoted using concatentation with white spaces
in between the symbols. Terminal symbols are strings enclosed in
hyphenation. Currently, it is not possible to include a hyphen in
a terminal symbol. The empty string is denoted by the empty sequence,
i.e.\ a semi-colon following a colon. 

A CFG definition can include comments in Java style, i.e. "/* ... */".
Futhermore, each rule can be given a symbolic name in square brackets
before the colon. Currently, these names are just ignored.

Example:

S : A B C ;
A : "f" "p" "b" A ;
  : ;
B : "h" "f" "h" B ;
  : ;
C : "r" "g" ;


7) OUTPUT
---------
Output depends on the exact problem chosen to be analyzed, e.g.
universality, inclusion, etc.

In general, cfganalyzer searches ranges of Sigma* with Sigma being
the least alphabet for all underlying input grammars for witnesses
or counterexamples. Suppose you want to analyze two grammars w.r.t.
inclusion of their languages. Then cfganalyzer will give you reports
of the form 

L(G1) contains every word of length k with 1 <= k <= 1.
L(G1) contains every word of length k with 2 <= k <= 2.
L(G1) contains every word of length k with 3 <= k <= 3.
L(G1) contains every word of length k with 4 <= k <= 4.
A word not in L(G1) is, e.g., "aaaaa" of length 5

where G1 is the grammar given in the first file on the command line etc.

Note that, when analyzing for ambiguity, cfganalyzer does not necessarily
report as a counterexample an ambiguous word in the languages of the 
given CFG. Instead it first reduces the grammar such that all nonterminals
are reachable and productive. It then looks for an ambiguous word derived
by any nonterminal. It is guaranteed that this can be extended to an 
ambiguous word in the language of the CFG. Currently, finding such an
extension is not implemented yet.


8) TROUBLESHOOTING
------------------
- If you get an OCaml compiler error saying that two modules make
  inconsistent assumptions over some interface, then simply type
  `make clean' and run `make' again.