// 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 Mkel (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 */
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
   */
  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
   * @param flat	flag: generate a flattened state space
   */
  void linkReporter (ssync_t syncstate, bool arcs, bool flat) const {
    *mySyncState = syncstate;
    *myAddArcs = arcs;
    *myFlat = flat;
  }

  /** Get a pointer to the flag for reporting fatal errors */
  bool*& getFatal () const { return *myFatal; }
  /** Get a reference to the flag for indicating flattened analysis */
  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 */
  void clearProp () { *myPropBits = 0; }

  /** Clean up (deallocate) the multi-sets */
  void msetClean () const {
    (*myMsetClean) ();
  }
  /** Clean up (deallocate) the event encoding buffer */
  void eventClean () const {
    (*myEventClean) ();
  }
  /** Clear (empty) the event encoding buffer */
  void eventClear () const {
    (*myEventClear) ();
  }
  /** Initialize the event decoding buffer
   * @param buf		the decoding buffer
   * @param size	length of the decoding buffer
   */
  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
   */
  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
   */
  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
   */
  enum Error eventDecode (bool strong) const {
    return (*myEventDecoder) (strong);
  }
  /** Get the active weak fairness sets after a call to eventDecode () */
  unsigned* getWeaklyFair () const { return myWeaklyFair; }
  /** Get the active strong fairness sets after a call to eventDecode () */
  unsigned* getStronglyFair () const { return myStronglyFair; }

  /** Clean up (deallocate) the state encoding buffer */
  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
   */
  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)
   */
  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
   */
  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
   */
  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
   */
  enum Error propEval (unsigned s) const { return (*myPropEval[s]) (); }
  /** Get the enabled successors after a call to propEval () */
  const unsigned* getPropSucc () const { return *myPropSucc; }

private:
  /** The net to be compiled */
  const class Net& myNet;
  /** The directory name */
  const char* myDirectory;
  /** Prefix for external program names */
  const char* myPrefix;
  /** Handle to a dynamic library */
  void* myHandle;
  /** Multi-set clean-up function */
  vf_t myMsetClean;
  /** Event clean-up function */
  vf_t myEventClean;
  /** Event clearing function */
  vf_t myEventClear;
  /** Event analyzer functions */
  uf_t* myEventAnalyzers;
  /** Event inflater function */
  inf_t myEventInflater;
  /** Event deflater function */
  def_t myEventDeflater;
  /** Event decoder function */
  fair_t myEventDecoder;
  /** State clean-up function */
  vf_t myStateClean;
  /** State projection function */
  sproj_t myStateProject;
  /** State decoder function */
  sdec_t myStateDecoder;
  /** Fatalness flag */
  bool** myFatal;
  /** Flattenedness flag */
  bool* myFlattened;
  /** Add encoded state (callback) */
  sadd_t* myAddState;
  /** Report synchronisation (callback) */
  ssync_t* mySyncState;
  /** Flag: generate arcs */
  char* myAddArcs;
  /** Flag: generate flattened state space */
  char* myFlat;
  /** State deadlock property evaluator function */
  deval_t myStateDeadlock;
  /** Active weak fairness sets */
  unsigned* myWeaklyFair;
  /** Active strong fairness sets */
  unsigned* myStronglyFair;
  /** Bits per finite-word property automaton state */
  unsigned* myPropBits;
  /** Enabled successors in the property automaton */
  const unsigned** myPropSucc;
  /** Handle to a property automaton library */
  void* myPropHandle;
  /** Property gate evaluators */
  eval_t* myPropEval;
  /** State property evaluator */
  prop_t myStateProps;
};

#endif // COMPILATION_H_