Logo Search packages:      
Sourcecode: maria version File versions

Compilation.h

Go to the documentation of this file.
// Compilation of types, variables and expressions -*- c++ -*-

#ifndef COMPILATION_H_
# define COMPILATION_H_
# ifdef __GNUC__
#  pragma interface
# endif // __GNUC__

# include "Error.h"
# include <sys/types.h>

/** @file Compilation.h
 * Interface to compiled code
 */

/* Copyright © 2000-2003 Marko Mäkelä (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA is free software; you can redistribute it and/or modify it
   under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   MARIA is distributed in the hope that it will be useful, but
   WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   General Public License for more details.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

/** Compilation of types, variables and expressions */
00037 class Compilation
{
  /** Parameterless void function */
  typedef void (*vf_t) (void);
  /** Transition instance analysis function */
  typedef unsigned (*uf_t) (void*, char*);
  /** Event buffer inflater */
  typedef unsigned (*inf_t) (void*, size_t);
  /** Event buffer deflater */
  typedef void* (*def_t) (size_t*);
  /** State encoder */
  typedef const void* (*sproj_t) (unsigned,unsigned,unsigned,unsigned*);
  /** State decoder */
  typedef void (*sdec_t) (unsigned,void*,unsigned);
  /** Add encoded state */
  typedef void (*sadd_t) (const void*,size_t,enum Error,
                    unsigned,unsigned,int,void*);
  /** Report that a synchronising transition is enabled */
  typedef void (*ssync_t) (unsigned,void*);
  /** Evaluate deadlock condition for a given net */
  typedef enum Error (*deval_t) (unsigned);
  /** Evaluator function */
  typedef enum Error (*eval_t) (void);
  /** Event decoder and fairness evaluator */
  typedef enum Error (*fair_t) (unsigned);
  /** State property evaluator function */
  typedef int (*prop_t) (bool (*) (unsigned, const void*), const void*);

public:
  /** Constructor
   * @param net         the net to be compiled
   * @param directory   name of the directory for the files
   * @param prefix      prefix for invoking external programs
   */
  explicit Compilation (const class Net& net,
                  const char* directory,
                  const char* prefix);
private:
  /** Copy constructor */
  Compilation (const class Compilation& old);
  /** Assignment operator */
  class Compilation& operator= (const class Compilation& old);
public:
  /** Destructor */
  ~Compilation ();

  /** Compile the type definitions and expressions of a net
   * @return            true if everything succeeded
   */
  bool compile () const;

  /** Link the compiled functions of a net
   * @return            NULL on success; error message on failure
   */
  char* link ();

  /** Link the state storage function
   * @param addstate    function to be called when adding states
   * @param arcs  flag: generate arcs
   */
00097   void linkAddState (sadd_t addstate) const { *myAddState = addstate; }

  /** Link the state space reporting functions
   * @param syncstate   function for reporting potential synchronisations
   * @param arcs  flag: generate arcs
   */
00103   void linkReporter (ssync_t syncstate, bool arcs) const {
    *mySyncState = syncstate;
    *myAddArcs = arcs;
  }

  /** Get a pointer to the flag for reporting fatal errors */
00109   bool*& getFatal () const { return *myFatal; }
  /** Get a reference to the flag for indicating flattened analysis */
00111   bool& getFlattened () const { return *myFlattened; }

  /** Unlink the compiled functions of a net */
  void unlink ();

  /** Compile and link a property automaton
   * @param property    the property automaton
   * @return            true if everything succeeded
   */
  bool compile (const class Property& property);

  /** Clear the finite property automaton */
00123   void clearProp () { *myPropBits = 0; }

  /** Clean up (deallocate) the multi-sets */
00126   void msetClean () const {
    (*myMsetClean) ();
  }
  /** Clean up (deallocate) the event encoding buffer */
00130   void eventClean () const {
    (*myEventClean) ();
  }
  /** Clear (empty) the event encoding buffer */
00134   void eventClear () const {
    (*myEventClear) ();
  }
  /** Initialize the event decoding buffer
   * @param buf         the decoding buffer
   * @param size  length of the decoding buffer
   */
00141   void eventInflate (void*buf, size_t size) const {
    (*myEventInflater) (buf, size);
  }
  /** Get the event encoding buffer
   * @param size  (output): length encoded data in bytes
   * @return            the buffer
   */
00148   const void* eventDeflate (size_t& size) const {
    return (*myEventDeflater) (&size);
  }

  /** Analyze and fire the enabled instances of a transition
   * @param tr          number of the transition
   * @param ctx         the call-back context
   * @param log         log of enabled transition instance sets (optional)
   * @return            number of errors occurred
   */
00158   unsigned eventAnalyze (unsigned tr, void* ctx, char* log) const {
    return (*myEventAnalyzers[tr]) (ctx, log);
  }
  /** Decode a transition instance and compute fairness constraints
   * @param strong      flag: compute also strong fairness constraints?
   * @return            errNone or an error code
   */
00165   enum Error eventDecode (bool strong) const {
    return (*myEventDecoder) (strong);
  }
  /** Get the active weak fairness sets after a call to eventDecode () */
00169   unsigned* getWeaklyFair () const { return myWeaklyFair; }
  /** Get the active strong fairness sets after a call to eventDecode () */
00171   unsigned* getStronglyFair () const { return myStronglyFair; }

  /** Clean up (deallocate) the state encoding buffer */
00174   void stateClean () const {
    (*myStateClean) ();
  }
  /** Project the state on a module
   * @param net         the module
   * @param d           extra data to be appended to the state vector
   * @param dbits width of d in bits
   * @param size  (output) length of the encoded state in bytes
   * @return            the encoded data
   */
00184   const void* stateProject (unsigned net, unsigned d, unsigned dbits,
                      unsigned& size) const {
    return (*myStateProject) (net, d, dbits, &size);
  }
  /** Decode a state
   * @param net         the number of the net (0=root)
   * @param buf         the encoded data (deflated if size is nonzero)
   * @param size  length of the encoded state in bytes (0=inflated data)
   */
00193   void stateDecode (unsigned net, void* buf, unsigned size) const {
    (*myStateDecoder) (net, buf, size);
  }

  /** Evaluate the reject condition
   * @param net         the number of the net (0=root)
   * @return            errNone, errComp (condition holds) or an error code
   */
00201   enum Error stateDeadlock (unsigned net) const {
    return (*myStateDeadlock) (net);
  }
  /** Evaluate state properties
   * @param operation   operation to invoke on properties that hold
   * @param data  context data to pass to the operation
   */
00208   bool checkProps (bool (*operation) (unsigned, const void*),
               const void* data) const {
    return bool ((*myStateProps) (operation, data));
  }

  /** Evaluate the successors of a property automaton
   * @param s           the number of the state where to evaluate the gates
   * @return            errNone, or an error code
   */
00217   enum Error propEval (unsigned s) const { return (*myPropEval[s]) (); }
  /** Get the enabled successors after a call to propEval () */
00219   const unsigned* getPropSucc () const { return *myPropSucc; }

private:
  /** The net to be compiled */
00223   const class Net& myNet;
  /** The directory name */
00225   const char* myDirectory;
  /** Prefix for external program names */
00227   const char* myPrefix;
  /** Handle to a dynamic library */
00229   void* myHandle;
  /** Multi-set clean-up function */
00231   vf_t myMsetClean;
  /** Event clean-up function */
00233   vf_t myEventClean;
  /** Event clearing function */
00235   vf_t myEventClear;
  /** Event analyzer functions */
00237   uf_t* myEventAnalyzers;
  /** Event inflater function */
00239   inf_t myEventInflater;
  /** Event deflater function */
00241   def_t myEventDeflater;
  /** Event decoder function */
00243   fair_t myEventDecoder;
  /** State clean-up function */
00245   vf_t myStateClean;
  /** State projection function */
00247   sproj_t myStateProject;
  /** State decoder function */
00249   sdec_t myStateDecoder;
  /** Fatalness flag */
00251   bool** myFatal;
  /** Flattenedness flag */
00253   bool* myFlattened;
  /** Add encoded state (callback) */
00255   sadd_t* myAddState;
  /** Report synchronisation (callback) */
00257   ssync_t* mySyncState;
  /** Flag: generate arcs */
00259   char* myAddArcs;
  /** State deadlock property evaluator function */
00261   deval_t myStateDeadlock;
  /** Active weak fairness sets */
00263   unsigned* myWeaklyFair;
  /** Active strong fairness sets */
00265   unsigned* myStronglyFair;
  /** Bits per finite-word property automaton state */
00267   unsigned* myPropBits;
  /** Enabled successors in the property automaton */
00269   const unsigned** myPropSucc;
  /** Handle to a property automaton library */
00271   void* myPropHandle;
  /** Property gate evaluators */
00273   eval_t* myPropEval;
  /** State property evaluator */
00275   prop_t myStateProps;
};

#endif // COMPILATION_H_

Generated by  Doxygen 1.6.0   Back to index