import divine-2.4

AUTHORS

@@ -17,5 +17,7 @@ Michael Weber
 HOARD (1998-2007) by Emery Berger <emery@cs.umass.edu>.
 LPSOLVE by Michel Berkelaar, Kjell Eikland, Peter Notebaert.
 dlfcn-win32 by Ramiro Polla
+Murphi (1990-1999) by David Dill, Andreas Drexler, Alan Hu, Han Yang,
+       Norris Ip, Ralph Melton, Seungjoon Park, Ulrich Stern
 
 See COPYING for authoritative copyright and licence information.

CMakeLists.txt

 cmake_minimum_required(VERSION 2.4.7)
 project( divine )
 
+set( CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_CURRENT_SOURCE_DIR}/cmake" )
+
 if(COMMAND cmake_policy)
   cmake_policy(SET CMP0002 OLD) # FIXME
   cmake_policy(SET CMP0003 NEW)
 endif(COMMAND cmake_policy)
 
-if( NOT CMAKE_BUILD_TYPE )
-  set( CMAKE_BUILD_TYPE "Release" )
-endif( NOT CMAKE_BUILD_TYPE )
+if(NOT CMAKE_BUILD_TYPE)
+ set(CMAKE_BUILD_TYPE "Release" CACHE STRING
+     "Choose the type of build, options are: Debug Release RelWithDebInfo MinSizeRel."
+     FORCE)
+endif(NOT CMAKE_BUILD_TYPE)
 
 macro(appendFlag flags value)
   foreach( F ${flags} )
-    set( CMAKE_${F}_FLAGS_${CMAKE_BUILD_TYPE}
-      "${CMAKE_${F}_FLAGS_${CMAKE_BUILD_TYPE}} ${value}" )
+    set( CMAKE_${F}_FLAGS "${CMAKE_${F}_FLAGS} ${value}" )
   endforeach( F )
 endmacro(appendFlag)
 
@@ -24,11 +27,17 @@ option( USE64 "pass -m64 to gcc to force 64b on multiarch" OFF )
 option( USE32 "pass -m32 to gcc to force 32b on multiarch" OFF )
 option( MPI "compile DiVinE with MPI for clustering support" ON )
 option( GUI "compile the Qt GUI" ON )
+option( MURPHI "enable Murphi model compiler" ON )
+option( PERFORMANCE "compile for maximum performance (LONG compilation)" ON )
 
 if( NOT WIN32 )
   add_definitions( -DPOSIX )
 endif( NOT WIN32 )
 
+if( PERFORMANCE )
+  add_definitions( -DPERFORMANCE )
+endif( PERFORMANCE )
+
 if( PROFILE )
   appendFlag( "CXX;C" "-fprofile-arcs -ftest-coverage" )
   link_libraries( "gcov" )
@@ -36,10 +45,12 @@ endif( PROFILE )
 
 if( USE64 )
   appendFlag( "CXX;C;EXE_LINKER;SHARED_LINKER" "-m64" )
+  add_definitions( -DUSE_GCC_M64 )
 endif( USE64 )
 
 if( USE32 )
   appendFlag( "CXX;C;EXE_LINKER;SHARED_LINKER" "-m32" )
+  add_definitions( -DUSE_GCC_M32 )
 endif( USE32 )
 
 if( NOT POOLS )
@@ -50,6 +61,14 @@ if( GUI )
   find_package( Qt4 4.5.0 )
 endif( GUI )
 
+if( NOT USE32 AND NOT USE64 )
+  # the curses package we'd find probably wouldn't work anyway
+  find_package( Curses )
+  if( CURSES_FOUND )
+    add_definitions( -DHAVE_CURSES )
+  endif()
+endif()
+
 # on some mingw32, regex.h is not on the default include path
 find_path( RX_PATH regex.h )
 include_directories( ${RX_PATH} )
@@ -78,20 +97,6 @@ set( DIVINE_INCLUDES
   ${MPI_INCLUDE_PATH}
   ${divine_SOURCE_DIR}/divine/legacy )
 
-include( CheckCXXSourceCompiles )
-check_cxx_source_compiles(
- "template< typename T > struct A {
-	static const int x = sizeof( T );
-  };
-  struct B {
-        A< B > a;
-  };
-  int main() { return 0; }" TMPL_SIZEOF_WORKS )
-
-if( NOT TMPL_SIZEOF_WORKS )
-  message( FATAL_ERROR "Your C++ compiler apparently does not support language features required by DiVinE. It is recommended that you compile with G++ 4.1 or 4.2." )
-endif( NOT TMPL_SIZEOF_WORKS )
-
 find_program( SHA1SUM sha1sum )
 
 if( NOT SHA1SUM )
@@ -145,6 +150,18 @@ if( HOARD )
   add_subdirectory( hoard )
 endif( HOARD )
 add_subdirectory( lpsolve )
+
+find_program( BYACC "byacc" )
+find_package( FLEX )
+find_package( BYACC )
+
+if( MURPHI AND FLEX_FOUND AND BYACC_FOUND AND BYACC )
+add_subdirectory( murphi )
+add_definitions( -DHAVE_MURPHI )
+else()
+set( MURPHI OFF )
+endif()
+
 add_subdirectory( divine )
 add_subdirectory( tools )
 add_subdirectory( examples )

COPYING

@@ -834,4 +834,114 @@ necessary.  Here is a sample; alter the names:
 
 That's all there is to it!
 
+--
+
+The files under murphi/ are copyright (C) 1992 - 1999 by the Board of Trustees
+of Leland Stanford Junior University.
+
+License to use, copy, modify, sell and/or distribute this software and its
+documentation any purpose is hereby granted without royalty, subject to the
+following terms and conditions:
+
+1.  The above copyright notice and this permission notice must appear in all
+copies of the software and related documentation.
+
+2.  The name of Stanford University may not be used in advertising or publicity
+pertaining to distribution of the software without the specific, prior written
+permission of Stanford.
+
+3.  This software may not be called "Murphi" if it has been modified in any
+way, without the specific prior written permission of David L.  Dill.
+
+4.  THE SOFTWARE IS PROVIDED "AS-IS" AND STANFORD MAKES NO REPRESENTATIONS OR
+WARRANTIES, EXPRESS OR IMPLIED, BY WAY OF EXAMPLE, BUT NOT LIMITATION.
+STANFORD MAKES NO REPRESENTATIONS OR WARRANTIES OF MERCHANTABILITY OR FITNESS
+FOR ANY PARTICULAR PURPOSE OR THAT THE USE OF THE SOFTWARE WILL NOT INFRINGE
+ANY PATENTS, COPYRIGHTS TRADEMARKS OR OTHER RIGHTS. STANFORD SHALL NOT BE
+LIABLE FOR ANY LIABILITY OR DAMAGES WITH RESPECT TO ANY CLAIM BY LICENSEE OR
+ANY THIRD PARTY ON ACCOUNT OF, OR ARISING FROM THE LICENSE, OR ANY SUBLICENSE
+OR USE OF THE SOFTWARE OR ANY SERVICE OR SUPPORT.
+
+LICENSEE shall indemnify, hold harmless and defend STANFORD and its trustees,
+officers, employees, students and agents against any and all claims arising out
+of the exercise of any rights under this Agreement, including, without limiting
+the generality of the foregoing, against any damages, losses or liabilities
+whatsoever with respect to death or injury to person or damage to property
+arising from or out of the possession, use, or operation of Software or
+Licensed Program(s) by LICENSEE or its customers.
+
+Notes:
+
+A.  Responsible use:
+
+Murphi is to be used as a DEBUGGING AID, not as a means of guaranteeing the
+correctness of a design.  We do not guarantee that all errors can be caught
+with Murphi.  There are many reasons for this:
+
+1. Specifications and verification conditions do not necessarily capture the
+conditions necessary for correct operation in practice.
+
+2. Many properties cannot be stated Murphi, including timing requirements,
+performance requirements, "liveness" properties (such as "x will eventually
+occur") and many others.
+
+3. Murphi cannot verify "large" systems.  Almost always, the sizes of various
+objects in the description must be modelled as being much smaller than they are
+in reality, in order to make verification feasible.  There is a high
+probability that design errors will only be manifested when the objects are
+large.
+
+4. The description of a design may not be consistent with what is actually
+implemented.
+
+5.  Murphi may have bugs that cause errors to be overlooked.
+
+In short, Murphi is totally inadequate for guaranteeing that there are no
+errors; however, it is sometimes effective for discovering errors that are
+difficult to detect by other means.
+
+B.  Courtesy
+
+Our motivation in distributing this software freely is to encourage others to
+evaluate its effectiveness on a wider range of applications than we have
+resources to attempt, and to provide a foundation for further development of
+automatic verification techniques.
+
+We would very much appreciate learning about other's experiences with the
+system and suggestions for improvements.  Even more, we would appreciate
+contributions of two kinds: additional verification examples that can be added
+to the distribution, and enhancements to the verification system.  Although we
+do not promise to distribute the examples or enhancements, we may do so if
+feasible.
+
+C.  Historical Notes
+
+The first version of the Murphi language and verification system was originally
+designed in 1990-1991 by David Dill, Andreas Drexler, Alan Hu, and Han Yang of
+the Stanford University Computer Systems Laboratory.  The first version of the
+program was primarily implemented by Andreas Drexler.
+
+The Murphi language was extensively modified and extended by David Dill, Alan
+Hu, Norris Ip, Ralph Melton, Seungjoon Park, and Han Yang in 1992.  The new
+version was almost entirely reimplemented by Ralph Melton during the summer and
+fall of 1992.
+
+The symmetry and multiset reduction was implemented by Norris Ip, Ulrich Stern
+added the hash compaction algorithms.
 
+Financial and other support for the design and implementation of Murphi has
+come from many sources, the Defense Advanced Research Projects Agency (under
+contract number N00039-91-C-0138), the National Science Foundation (grant
+number MIP-8858807), the Powell Foundation, the Stanford Center for Integrated
+Systems, the U.S. Office of Naval Research, and Mitsubishi Electronic
+Laboratories America.  Equipment was provided by Sun Microsystems, the Digital
+Equipment Corporation, and IBM.
+
+These notes are based on information provided to Stanford that has not been
+independently verified or checked.
+
+D.  Support, comments, feedback
+
+If you need help or have comments or suggestions regarding Murphi, please send
+electronic mail to "murphi@verify.stanford.edu".  We do not have the resources
+to provide commercial-quality support, but we may be able to help you.

WHATS_NEW → NEWS

-DiVinE 2.2
-==========
+DiVinE 2.4 (29.9.2010)
+======================
+
+- C3 check for parallel partial order reduction.
+- Partial order reduction for (interpreted) DVE (--por).
+- Real-time hashtable & queue statistics (--statistics).
+- Custom generators are not allowed with pool-less builds.
+- Further optimisations to the exploration engine (hash table, FIFOs, MPI).
+- Better --version output.
+- In addition to G++, DiVinE can be compiled with Clang now.
+- More fixes in MPI.
+- A curses-based interface for observing runtime algorithm behaviour.
+- Dual-threaded nested DFS (Holzmann '07).
+- Counterexamples in (single-threaded) nested DFS.
+- Enable on-the-fly heuristic in distributed (MPI) OWCTY.
+- Make "divine verify" work with non-DVE inputs correctly.
+- Fix BA translation of F((F a) U b) form formulae (J. Strejcek &c.)
+
+DiVinE 2.3 (8.8.2010)
+=====================
+
+- Basic support for Murphi model compilation and parallel verification.
+- Fix a bug in DVE compiler that made some models uncompilable.
+- Improved, distributed (MPI-enabled) MAP algorithm.
+- Track state space statistics in OWCTY (--report).
+- Proper deadlock detection (with traces) for all model types.
+- Improved --report output format consistency.
+- Fix handling of committed states in the DVE compiler.
+- Multiple stability and correctness fixes in distributed memory support (MPI).
+- Limit the override of global allocator to avoid occasional crashes in glibc.
+- Add an option to limit maximum verification runtime (--max-time, POSIX only).
+
+Furthermore, a new binary ABI is available in this release. There are two
+caveats though:
+
+  1) The ABI is NOT STABLE and should not be relied upon. It will be subject of
+  further changes in future releases.
+
+  2) The win32 support is somewhat limited, since some models may expect access
+  to symbols exported by the divine binary itself, which is not supported on
+  win32.
+
+DiVinE 2.2 (17.2.2010)
+======================
 
 - Further optimisations in compiled DVE.
 - Improved overall performance of the verifier.
@@ -17,24 +59,24 @@ KNOWN ISSUES: Error state handling is not consistent between interpreted and
 compiled DVE. The profiled build (-DPROFILE=ON) is currently broken. (Both
 issues exist since version 2.1.)
 
-DiVinE 2.1.1
-============
+DiVinE 2.1.1 (26.1.2010)
+========================
 
 - Fixed a number of issues with compiled DVE models.
 - Bugfixes in the custom model loader.
 - Improved performance of compiled DVE.
 - Fixed Windows build.
 
-DiVinE 2.1
-==========
+DiVinE 2.1 (17.1.2010)
+======================
 
 - A new DVE to C (to native binary) compiler available as `divine compile'.
 - Fixed handling of error states in interpreted DVE.
 - The GUI can now be compiled & used on Windows.
 - A number of GUI improvements and usability fixes.
 
-DiVinE 2.0
-==========
+DiVinE 2.0 (19.11.2009)
+=======================
 
 - This version is a major rewrite of the parallel framework and algorithms.
 - MPI is now partially supported in addition to shared memory parallelism
@@ -46,8 +88,8 @@ DiVinE 2.0
 - More data available in --report (including machine-readable counterexample).
 - The divine.combine binary has been removed, use "divine combine" instead.
 
-DiVinE Multi-Core 1.4
-=====================
+DiVinE Multi-Core 1.4 (23.4.2009)
+=================================
 
 - Unfortunately, an incorrect implementation of Nested DFS has slipped into the
   1.3 release. Version 1.4 fixes this problem.
@@ -55,8 +97,8 @@ DiVinE Multi-Core 1.4
   self-loops are now detected on-the-fly, and early termination is now more
   efficient.
 
-DiVinE Multi-Core 1.3
-=====================
+DiVinE Multi-Core 1.3 (17.11.2008)
+==================================
 
 - Improved and newly included algorithms:
   - MAP: improved progress reports, early termination and counterexamples
@@ -69,16 +111,16 @@ DiVinE Multi-Core 1.3
   This has been fixed.
 - A few other user experience fixes: improved warnings and overall robustness.
 
-DiVinE Multi-Core 1.2.1
-=======================
+DiVinE Multi-Core 1.2.1 (1.11.2008)
+===================================
 
 - Fix compilation with g++ 4.3.
 - Update the bundled version of HOARD to 3.7.1.
 - Include some updates to the bundled version of wibble (no major impact on
   DiVinE itself).
 
-DiVinE Multi-Core 1.2
-=====================
+DiVinE Multi-Core 1.2 (15.5.2008)
+=================================
 
 - A few minor bugfixes.
 - The divine-mc.combine utility can now handle .mdve and .mprobdve files.

README

@@ -57,7 +57,7 @@ above. The most useful invocations are these:
 
  * run reachability on 8 cores:
    `./_build/tools/divine reachability -w 8 input.dve`
- * run model checking on 4 cores:
+ * run LTL model checking on 4 cores:
    `./_build/tools/divine owcty -w 4 input-with-property.dve`
 
 There are several example inputs, mostly coming from [The BEEM Database] [1],
@@ -67,6 +67,24 @@ repository.
 
 [1]: http://anna.fi.muni.cz/models
 
+To run DiVinE in a cluster, you can use the usual MPI tools, `mpirun` or
+`mpiexec`. For detailed info about these, please consult the documentation of
+your MPI implementation. You may also need to use a batch queue system like PBS
+to run DiVinE on your cluster -- please consult your cluster administrator
+about that.
+
+When running DiVinE on a cluster manually (without any queue management
+system), using machines node1 through node3, each of the nodes using 4 CPU
+cores, you could use the following command:
+
+    mpiexec -H node1,node2,node3 ./_build/tools/divine owcty -w 4 model.dve
+
+Please note that this assumes that both the divine binary and the model are
+available on all the mentioned cluster nodes, with the same paths (relative to
+your working directory). Your MPI implementation may support binary and input
+preloading, which would let you run DiVinE without a shared (NFS) filesystem as
+well.
+
 Graphical User Interface
 ------------------------
 
@@ -80,21 +98,6 @@ Please see online help for further information about using the interface. If
 you have chosen to install the tool, you should put it on your PATH, and then
 issue `divine.ide`.
 
-Known Issues
-------------
-
-Scalability on 64-bit platforms is inferior to scalability on 32-bit
-platforms. If you are running on x86_64 or other similar architecture
-which can run 32-bit binaries natively, you can compile DiVinE in
-32-bit mode:
-
-    $ CXXFLAGS=-m32 ./configure
-    $ make
-
-If you have previously run configure, you may need to delete or move
-the _build directory out of way. However, using 32-bit mode limits the
-size of verifiable models to roughly 3GB.
-
 Reporting Problems
 ------------------
 
@@ -106,15 +109,15 @@ already (in the latter case, please add a comment to the existing ticket, that
 you have encountered the issue, and if possible, any further details you may
 know about the problem). Thanks in advance.
 
-[1]: http://divine.fi.muni.cz/trac/newticket?version=2.0
+[1]: http://divine.fi.muni.cz/trac/newticket?version=2.3
 [2]: http://divine.fi.muni.cz/trac/
 
 Obtaining New Versions
 ----------------------
 
-The latest release is always available through [project pages] [1], section
+The latest release is always available through the [project pages] [1], section
 Download. You could also obtain the latest development snapshot through darcs
-(you need version 2.0 or later), which is used for version control:
+(you need darcs version 2.0 or later), which is used for version control:
 
     $ darcs get http://divine.fi.muni.cz/darcs/mainline divine
 

README.html

@@ -55,7 +55,7 @@ above. The most useful invocations are these:</p>
 <ul>
 <li>run reachability on 8 cores:
 <code>./_build/tools/divine reachability -w 8 input.dve</code></li>
-<li>run model checking on 4 cores:
+<li>run LTL model checking on 4 cores:
 <code>./_build/tools/divine owcty -w 4 input-with-property.dve</code></li>
 </ul>
 
@@ -64,6 +64,25 @@ distributed with the tool under the <code>examples/</code> directory. These are
 prefixed <code>beem-</code>. Many more models are available for download in the BEEM
 repository.</p>
 
+<p>To run DiVinE in a cluster, you can use the usual MPI tools, <code>mpirun</code> or
+<code>mpiexec</code>. For detailed info about these, please consult the documentation of
+your MPI implementation. You may also need to use a batch queue system like PBS
+to run DiVinE on your cluster -- please consult your cluster administrator
+about that.</p>
+
+<p>When running DiVinE on a cluster manually (without any queue management
+system), using machines node1 through node3, each of the nodes using 4 CPU
+cores, you could use the following command:</p>
+
+<pre><code>mpiexec -H node1,node2,node3 ./_build/tools/divine owcty -w 4 model.dve
+</code></pre>
+
+<p>Please note that this assumes that both the divine binary and the model are
+available on all the mentioned cluster nodes, with the same paths (relative to
+your working directory). Your MPI implementation may support binary and input
+preloading, which would let you run DiVinE without a shared (NFS) filesystem as
+well.</p>
+
 <h2>Graphical User Interface</h2>
 
 <p>If Qt4 development files are available on your machine, a graphical user
@@ -77,21 +96,6 @@ You can run the interface with:</p>
 you have chosen to install the tool, you should put it on your PATH, and then
 issue <code>divine.ide</code>.</p>
 
-<h2>Known Issues</h2>
-
-<p>Scalability on 64-bit platforms is inferior to scalability on 32-bit
-platforms. If you are running on x86_64 or other similar architecture
-which can run 32-bit binaries natively, you can compile DiVinE in
-32-bit mode:</p>
-
-<pre><code>$ CXXFLAGS=-m32 ./configure
-$ make
-</code></pre>
-
-<p>If you have previously run configure, you may need to delete or move
-the _build directory out of way. However, using 32-bit mode limits the
-size of verifiable models to roughly 3GB.</p>
-
 <h2>Reporting Problems</h2>
 
 <p>The DiVinE project uses Trac for managing problem reports. If you encounter a
@@ -104,9 +108,9 @@ know about the problem). Thanks in advance.</p>
 
 <h2>Obtaining New Versions</h2>
 
-<p>The latest release is always available through <a href="http://divine.fi.muni.cz/">project pages</a>, section
+<p>The latest release is always available through the <a href="http://divine.fi.muni.cz/">project pages</a>, section
 Download. You could also obtain the latest development snapshot through darcs
-(you need version 2.0 or later), which is used for version control:</p>
+(you need darcs version 2.0 or later), which is used for version control:</p>
 
 <pre><code>$ darcs get http://divine.fi.muni.cz/darcs/mainline divine
 </code></pre>

cmake/FindBISON.cmake

+# - Find bison executable and provides macros to generate custom build rules
+# The module defines the following variables:
+#
+#  BISON_EXECUTABLE - path to the bison program
+#  BISON_VERSION - version of bison
+#  BISON_FOUND - true if the program was found
+#
+# If bison is found, the module defines the macros:
+#  BISON_TARGET(<Name> <YaccInput> <CodeOutput> [VERBOSE <file>]
+#              [COMPILE_FLAGS <string>])
+# which will create  a custom rule to generate  a parser. <YaccInput> is
+# the path to  a yacc file. <CodeOutput> is the name  of the source file
+# generated by bison.  A header file is also  be generated, and contains
+# the  token  list.  If  COMPILE_FLAGS  option is  specified,  the  next
+# parameter is  added in the bison  command line.  if  VERBOSE option is
+# specified, <file> is created  and contains verbose descriptions of the
+# grammar and parser. The macro defines a set of variables:
+#  BISON_${Name}_DEFINED - true is the macro ran successfully
+#  BISON_${Name}_INPUT - The input source file, an alias for <YaccInput>
+#  BISON_${Name}_OUTPUT_SOURCE - The source file generated by bison
+#  BISON_${Name}_OUTPUT_HEADER - The header file generated by bison
+#  BISON_${Name}_OUTPUTS - The sources files generated by bison
+#  BISON_${Name}_COMPILE_FLAGS - Options used in the bison command line
+#
+#  ====================================================================
+#  Example:
+#
+#   find_package(BISON)
+#   BISON_TARGET(MyParser parser.y ${CMAKE_CURRENT_BINARY_DIR}/parser.cpp)
+#   add_executable(Foo main.cpp ${BISON_MyParser_OUTPUTS})
+#  ====================================================================
+
+#=============================================================================
+# Copyright 2009 Kitware, Inc.
+# Copyright 2006 Tristan Carel
+#
+# Distributed under the OSI-approved BSD License (the "License");
+# see accompanying file Copyright.txt for details.
+#
+# This software is distributed WITHOUT ANY WARRANTY; without even the
+# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+# See the License for more information.
+#=============================================================================
+# (To distributed this file outside of CMake, substitute the full
+#  License text for the above reference.)
+
+FIND_PROGRAM(BISON_EXECUTABLE bison DOC "path to the bison executable")
+MARK_AS_ADVANCED(BISON_EXECUTABLE)
+
+IF(BISON_EXECUTABLE)
+
+  EXECUTE_PROCESS(COMMAND ${BISON_EXECUTABLE} --version
+    OUTPUT_VARIABLE BISON_version_output
+    ERROR_VARIABLE BISON_version_error
+    RESULT_VARIABLE BISON_version_result
+    OUTPUT_STRIP_TRAILING_WHITESPACE)
+  IF(NOT ${BISON_version_result} EQUAL 0)
+    MESSAGE(SEND_ERROR "Command \"${BISON_EXECUTABLE} --version\" failed with output:\n${BISON_version_error}")
+  ELSE()
+    STRING(REGEX REPLACE "^bison \\(GNU Bison\\) ([^\n]+)\n.*" "\\1"
+      BISON_VERSION "${BISON_version_output}")
+  ENDIF()
+
+  # internal macro
+  MACRO(BISON_TARGET_option_verbose Name BisonOutput filename)
+    LIST(APPEND BISON_TARGET_cmdopt "--verbose")
+    GET_FILENAME_COMPONENT(BISON_TARGET_output_path "${BisonOutput}" PATH)
+    GET_FILENAME_COMPONENT(BISON_TARGET_output_name "${BisonOutput}" NAME_WE)
+    ADD_CUSTOM_COMMAND(OUTPUT ${filename}
+      COMMAND ${CMAKE_COMMAND}
+      ARGS -E copy
+      "${BISON_TARGET_output_path}/${BISON_TARGET_output_name}.output"
+      "${filename}"
+      DEPENDS
+      "${BISON_TARGET_output_path}/${BISON_TARGET_output_name}.output"
+      COMMENT "[BISON][${Name}] Copying bison verbose table to ${filename}"
+      WORKING_DIRECTORY ${CMAKE_SOURCE_DIR})
+    SET(BISON_${Name}_VERBOSE_FILE ${filename})
+    LIST(APPEND BISON_TARGET_extraoutputs
+      "${BISON_TARGET_output_path}/${BISON_TARGET_output_name}.output")
+  ENDMACRO(BISON_TARGET_option_verbose)
+
+  # internal macro
+  MACRO(BISON_TARGET_option_extraopts Options)
+    SET(BISON_TARGET_extraopts "${Options}")
+    SEPARATE_ARGUMENTS(BISON_TARGET_extraopts)
+    LIST(APPEND BISON_TARGET_cmdopt ${BISON_TARGET_extraopts})
+  ENDMACRO(BISON_TARGET_option_extraopts)
+
+  #============================================================
+  # BISON_TARGET (public macro)
+  #============================================================
+  #
+  MACRO(BISON_TARGET Name BisonInput BisonOutput)
+    SET(BISON_TARGET_output_header "")
+    SET(BISON_TARGET_command_opt "")
+    SET(BISON_TARGET_outputs "${BisonOutput}")
+    IF(NOT ${ARGC} EQUAL 3 AND NOT ${ARGC} EQUAL 5 AND NOT ${ARGC} EQUAL 7)
+      MESSAGE(SEND_ERROR "Usage")
+    ELSE()
+      # Parsing parameters
+      IF(${ARGC} GREATER 5 OR ${ARGC} EQUAL 5)
+        IF("${ARGV3}" STREQUAL "VERBOSE")
+          BISON_TARGET_option_verbose(${Name} ${BisonOutput} "${ARGV4}")
+        ENDIF()
+        IF("${ARGV3}" STREQUAL "COMPILE_FLAGS")
+          BISON_TARGET_option_extraopts("${ARGV4}")
+        ENDIF()
+      ENDIF()
+
+      IF(${ARGC} EQUAL 7)
+        IF("${ARGV5}" STREQUAL "VERBOSE")
+          BISON_TARGET_option_verbose(${Name} ${BisonOutput} "${ARGV6}")
+        ENDIF()
+      
+        IF("${ARGV5}" STREQUAL "COMPILE_FLAGS")
+          BISON_TARGET_option_extraopts("${ARGV6}")
+        ENDIF()
+      ENDIF()
+
+      # Header's name generated by bison (see option -d)
+      LIST(APPEND BISON_TARGET_cmdopt "-d")
+      STRING(REGEX REPLACE "^(.*)(\\.[^.]*)$" "\\2" _fileext "${ARGV2}")
+      STRING(REPLACE "c" "h" _fileext ${_fileext})
+      STRING(REGEX REPLACE "^(.*)(\\.[^.]*)$" "\\1${_fileext}" 
+          BISON_${Name}_OUTPUT_HEADER "${ARGV2}")
+      LIST(APPEND BISON_TARGET_outputs "${BISON_${Name}_OUTPUT_HEADER}")
+        
+      ADD_CUSTOM_COMMAND(OUTPUT ${BISON_TARGET_outputs}
+        ${BISON_TARGET_extraoutputs}
+        COMMAND ${BISON_EXECUTABLE}
+        ARGS ${BISON_TARGET_cmdopt} -o ${ARGV2} ${ARGV1}
+        DEPENDS ${ARGV1}
+        COMMENT "[BISON][${Name}] Building parser with bison ${BISON_VERSION}"
+        WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
+    
+      # define target variables
+      SET(BISON_${Name}_DEFINED TRUE)
+      SET(BISON_${Name}_INPUT ${ARGV1})
+      SET(BISON_${Name}_OUTPUTS ${BISON_TARGET_outputs})
+      SET(BISON_${Name}_COMPILE_FLAGS ${BISON_TARGET_cmdopt})
+      SET(BISON_${Name}_OUTPUT_SOURCE "${BisonOutput}")
+
+    ENDIF(NOT ${ARGC} EQUAL 3 AND NOT ${ARGC} EQUAL 5 AND NOT ${ARGC} EQUAL 7)
+  ENDMACRO(BISON_TARGET)
+  #
+  #============================================================
+
+ENDIF(BISON_EXECUTABLE)
+