Read Me

                BuddyScout  ver.0.3


BuddyScout is an interface between BuDDy (Binary Decision Diagram
library) and GHC (Glasgow Haskell Compiler).  It enables you to use
the BDD library from within Haskell programs.

---- License

MIT style.  See COPYING and each file.

---- How to use

BuddyScout is a source file to the Haskel->C translator (c2hs), which
generates an FFI (Foreign Function Interface) description in Haskell.

To compile and use it, the following tools are required.  You can
consult examples/Makefile for the details of compiler options.

  BuDDy (Binary Decision Diagram library)
  http://sourceforge.net/projects/buddy

  GHC (Glasgow Haskell Compiler)
  http://www.haskell.org/ghc/

  Haskell->C (Haskell Interface Generator)
  http://www.cse.unsw.edu.au/~chak/haskell/c2hs/

The bundled examples are tested with the following environments, and
it is hoped to work on many other unix-like platforms.

  BuDDy 2.4,  GHC 6.8.2, Haskell->C 0.15.1

  Mac OS X 10.5.2 (Leopard, Intel)
  Linux (CentOS 5.1, i386)
  Windows XP SP2 + MinGW 5.1.4 + MSYS 1.0.10

The LANG variable could lead `c2hs' to failure.  If this is the case,
try `unsetenv LANG' or `env LANG=C make'.

* Note for Linux 

Some distributions require you to set LD_LIBRARY_PATH to indicate the
place where the BuDDy library resides (possibly /usr/local/lib).

* Note for Windows

Cygwin does not work with GHC because it is based on MinGW.  Since
path names are inconsistent with Cygwin, GHC cannot find the /usr
directory.  Therefore the BuDDy library must be compiled with MinGW
and MSYS.

---- Documents

BuddyScout requires a detailed knowledge about the BuDDy library and
some about Haskell's FFI (Foreign Function Interface).  For BuDDy,
good documents are included in its package.  For FFI, you can consult
http://www.cse.unsw.edu.au/~chak/haskell/ffi/ .


---- Examples

There are some examples in `examples' directory.

  simple.hs --- Basic usage and a callback handler.
  money.hs  --- Puzzle.
                (Haskell version of money.cxx from the BuDDy package)
  fdd.hs    --- Reachable states with FDD.
                (Haskell version of fdd.cxx from BuDDy)
  model-checking.hs --- CTL formulas and Kripke structures.


---- Interactive session

You can use BuddyScout interactively with GHCi as follows.

  % c2hs -l BuddyScout.chs
  % ghc --make BuddyScout.hs
  % ghci BuddyScout -lbdd

  GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
  Prelude BuddyScout> bdd_init 1000 1000
  Prelude BuddyScout> bdd_setvarnum 10
  0
  Prelude BuddyScout> [a,b,c,d] <- sequence $ map bdd_ithvar [0..3]
  Prelude BuddyScout> (.!)(a .& b) == ((.!)a .| (.!) b)
  True
  Prelude BuddyScout> import System
  Prelude BuddyScout System> bdd_fnprintdot "abc.dot" ((.!)a.&b.|(.!)c)
  Prelude BuddyScout System> system "dot -Tpng abc.dot > abc.png"
  ExitSuccess
  Prelude BuddyScout System> system "gimp abc.png"

The last few lines indicate how to use the `dot' command of Graphviz.


---- Utility functions

* fdd_extdomain :: [Int] -> Int

The original C version has two arguments to pass the array's address
and size, but the Haskell version takes a list of type [Int].

* set_varname_hook ::
       (FunPtr BddFileHandler -> IO (FunPtr BddFileHandler))
       -> (Int->String) -> IO ()

This function make the variable names displayed in the output of
fdd_printset and bdd_printset.  It takes a Haskell function, converts
it to a C language callback, and passes it to BuDDy's hook for
bdd_printset and fdd_printset.

For example, consider the following code.
  [a,b,c,d] <- sequence $ map bdd_ithvar [0..3]
  bdd_printset (a.&b.&c)
You will obtain the output like this by default.
  <0:1, 1:1, 2:1>
However, after you have
  set_varname_hook bdd_file_hook (\n->[['a'..]!!n]) ,
then you will get the following output.
  <a:1, b:1, c:1>

The first argument is bdd_file_hook or fdd_file_hook.  They are the
original functions prepared in BuDDy.  The second argument is the
user-specified function to convert a variable number of type Int into
the corresponding name of type String.


* withBDDPairs :: [Int] -> [Int] -> (Ptr BddPair -> IO a) -> IO a
* withFDDPairs :: [Int] -> [Int] -> (Ptr BddPair -> IO a) -> IO a

These functions manage the storage related to `bddPair'.  A usage
example is as follows.

  b <- withFDDPairs [2,3] [0,1] $ \p -> bdd_replace a p

These functions take two list of variable numbers, and the
user-specified function that calls bdd_replace or something to use
`bddPair'.  They allocate some storage required to call bdd_newpair,
then call bdd_newpair internally, and call also bdd_setpairs or
fdd_setpairs.  After these preparations, they pass the pointer to`
bddPair' to the third argument.  Finally, after the execution of the
third argument finished, they free the `bddPair' area and the storage
allocated before calling bdd_newpair.


* Operators (precedence and fixity)

binary
  infixl 7 .*, ./, .*#, ./#
  infixl 6 .+, .-, .\
  infix 5 .<<, .<<#, .>>, .>>#
  infix 4 .==, .!=, .<, .<=, .>, .>=
  infixl 3 .&
  infixl 2 .|, .^
  infixr 1 .->
  infix 1 .<>
  infixl 1 .<-

unary
  (.!)

meanings
  (.!) a = unsafePerformIO $ bdd_not a
  a .& b = unsafePerformIO $ bdd_apply a b bddop_and
  a .| b = unsafePerformIO $ bdd_apply a b bddop_or
  a .\ b = unsafePerformIO $ bdd_apply a b bddop_diff
  a .^ b = unsafePerformIO $ bdd_apply a b bddop_xor
  a .-> b = unsafePerformIO $ bdd_apply a b bddop_imp
  a .<> b = unsafePerformIO $ bdd_apply a b bddop_biimp
  a .<- b = unsafePerformIO $ bdd_apply a b bddop_invimp
  a .* b = unsafePerformIO $ bvec_mul a b
  a .*# b = unsafePerformIO $ bvec_mulfixed a b
  a ./ b = unsafePerformIO $ bvec_div a b
  a ./# b = unsafePerformIO $ bvec_divfixed a b
  a .+ b = unsafePerformIO $ bvec_add a b
  a .- b = unsafePerformIO $ bvec_sub a b
  a .< b = unsafePerformIO $ bvec_lth a b
  a .<= b = unsafePerformIO $ bvec_lte a b
  a .> b = unsafePerformIO $ bvec_gth a b
  a .>= b = unsafePerformIO $ bvec_gte a b
  a .== b = unsafePerformIO $ bvec_equ a b
  a .!= b = unsafePerformIO $ bvec_neq a b
  a .<< b = unsafePerformIO $ bvec_shl a b bddfalse
  a .<<# b = unsafePerformIO $ bvec_shlfixed a b bddfalse
  a .>> b = unsafePerformIO $ bvec_shr a b bddfalse
  a .>># b = unsafePerformIO $ bvec_shrfixed a b bddfalse

---- Notes

* BDD

Since the `BDD' type is declared as an instance of Eq, we can use the
operator `==' to determine the equivalence of two BDDs.


* BVEC

Every time a `bvec_*' function generates a BVEC, BuddyScout translates
it into a list of BDDs.  Therefore, we can manipulate it as a
Haskell's list, even though some of BVEC functions are not supported
by BuddyScout.


* Flushing the output buffer

It seems necessary to flush the output buffer of the GHC runtime
before using the BuDDy's printing functions (such as bdd_printset).
An easy way to do so is to insert the line of 'hSetBuffering stdout
NoBuffering' into the Haskell program, which disables the output
buffer.


* Garbage collection

To link the BuDDy's garbage collector with the GHC's one, we must take
care of reference counting.  BuddyScout applies `bdd_addref' to
any BDDs generated by bdd_* functions, and further attaches finalizers
to the BDD objects.  Such the finalizers will call bdd_delref when the
GHC runtime attempts to expire the objects.  On the other hand,
BuddyScout does not apply `bdd_addref' to the BDDs contained in
BVECs, because the BuDDy package must have done it when creating them.

Because of the finalizers, BDD type must be a boxed type.  It is
currently defined as `data BDD = BDD CInt'.


----------------
Yoshisato Sakai    (yoshisato(at)users.sourceforge.net)