LMU

Tool Documentation for mchfl and mcflc


License:

Copyright © 2008 Roland Axelsson

The source code in the provided package may be used under the terms of the BSD license. Please read the file 'COPYING' for details.

Overview:

The programs mchfl and mcflc are model checkers for the first-order fragment of Higher-Order Fixpoint Logic (HFL) and Fixpoint Logic with Chop (FLC) respectively. Behind the scene, there is only one model checking procedure for both logics. mcflc merely translates an FLC formula into HFL and then runs mchfl on it.
We also provide a model specification language (MSL) and offer to create a symbolic representation using a very simple BDD package.

Download:

This distribution comes with no warranty whatsoever and is distributed under the BSD license (see above).
The programs are meant to be the first in a series of non-regular model checkers. A model checker for PDL[CFG] will soon be available.

Feel free to provide your personal details.

Name:
Email:
Affiliation:

Installation:

The following tools and libraries have to be installed on your system:

Download the above file mc_light.tgz. Unpack the files. Switch to the top-level directory of the distribution and edit the marked passages in the Makefile. Execute the following commands in the top-level directory:

touch .depend
make

This should result in the two executables mchfl and mcflc in the ./bin directory.

Usage:

mchfl and mcflc take as input a text file with a string content as specified in the MSL documentation page. In its SPEC section a formula in either HFL or FLC should be provided over which the model is checked. For a FLC formula call mcflc <filename> and for a HFL formula mchfl <filename>.
There are several options which can be displayed with mchfl -help:

  • -v <level>
    defines the verbosity level of the execution. <level> may take values between 0 and 3, where 0 is quiet and 3 is extremely verbose.
  • --quiet
    no output other than errors, same as -v 0
  • --msg
    a few basic messages about the program status, same as -v 1
  • --verbose
    detailled information about the model checking progress, same as -v 2
  • --debug
    almost unreadable very low level debug information, same as -v 3
  • -t <secs>
    timeout for the model checking procedure in seconds, causes the program to terminate at the first possible occasion (after finishing the current subformula which in most cases should be almost immediately)
  • --timeout <secs>
    same as -t <secs>
  • -s
    transforms the gathered model information into a symbolic representation which uses a primitive BDD library; output is textual, see section "Output" below
  • --symbolic
    same as -s
  • -d <filename>
    results in a symbolic execution as caused by -s but produces an output file which contains the result BDD readable by the program dot
  • --dotfile <filename>
    same as -d <filename>
  • -l <filename>
    produces latex conform debug information about the fixpoint iteration
  • --latex <filename>
    produces latex conform debug information about the fixpoint iteration, same as -l <filename>
  • -help
    displays a list of options similar to this
  • --help
    same as -help

Output:

Depending on the verbosity level in which the tools are executed, there is textual output. Unless sojourning in the highest of these levels, its meaning should be more or less clear, at least if the user has read the papers on which the tools rely.
However, when the tool is run with the -s flag, there are lots of BDD dumps which need some explanation. A textual representation of a BDD is given as follows:

BDD ::= F | T | (v1, BDD, BDD, id)

v1 is the least variable (of type integer) in the current BDD according to the variable ordering. The first BDD is the high-branch and the second the low-branch. 'False' and 'True' BDDs are written as F and T. id is a unique integer identifier for this BDD and can be ignored. It is now with a little effort possible to read sets of states from a BDD textual representation, because the translation from the explicit model encodes the integer states as their binary counterpart with variables ordered as the binary digits from left to right. Example:

(1,F,(2,F,T,3),5)

is the following BDD (generated with the -d option):

bdd

and represents the set {0} as the only path to the T-node requires variables 1 and 2 (representing two binary digits) to be set to false.

Bug Reports:

I am grateful for every report on existing bugs in the software. Please send to:

to make mail visible: move mouse over

Last modified: Tue Jan 15 18:43:32 2008