Tool Documentation for mcpdl

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 program mcpdl is a model checker for Propositional Dynamic Logic with Indexed Grammars (PDL[IG])). The model and specification has to be provided explicitly via an input file as described in the model specification language (MSL). Note that the implementation has not yet been tested thoroughly yet.

Download:

This distribution comes with no warranty whatsoever and is distributed under the BSD license (see above).

Feel free to provide your personal details.

Installation:

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

• The OCaml compiler. Works with version 3.09.3 but probably also with lower ones.
  http://www.ocaml.org
• The Ocaml extlib library.
  http://caml.inria.fr//cgi-bin/hump.en.cgi

touch .depend
make

This should result in an executables mcpdl in the ./bin directory.

Usage:

mcpdl takes as input a text file with a string content as specified in the MSL documentation page. In its SPEC section a formula in PDL[IG] should be provided over which the model is checked.
There are several options which can be displayed with mcpdl -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>
• -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 tool relies. At the end, there is output of a result set containing those states which satisfy the specification formula.

Bug Reports:

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

to make mail visible: move mouse over