#ifndef MODEL2C_H
#define MODEL2C_H
#include <string>
#include <vector>
#include <iosfwd>
#include <stdexcept>
#ifdef WITH_PARAM
// TODO use forward declaration of unordered_map
// TODO templatize for value types double/parametric
// TODO remove stuff from teaching not needed anymore
// TODO functions which do not need to be fast need not be inlined
#include <tr1/unordered_map>
#endif

namespace lang {
  class Model;
  class Commands;
  class Alternative;
  class Properties;
  class Property;
}

namespace CVC3 {
  class Expr;
  template<class T>
    class ExprHashMap;
}

#ifdef WITH_PARAM
namespace Rational {
  class RationalFunction;
  class CVC3Converter;
}
#endif

namespace infamation {
  // TODO add possibility not to safe states (needed eg. for simulation)
  // TODO for some models, Flatten() is too expensive, do other way
  /**
   * This code is belong to Ernst Moritz Hahn (emh@cs.uni-sb.de)
   */
  class Model2C {
  public:
    typedef enum {hash_map, map} StateMapType;
    typedef enum {doubleVal, paramVal} ValueType;

    Model2C(lang::Model &);
    Model2C(const std::string &);
    Model2C(const std::string &, const std::string &);
    ~Model2C();
    /**
     * Return number of states obtained so far.
     *
     * @return number of model states
     */
    inline unsigned getNumStates() {
      return externGetNumStates();
    }
    /**
     * Return successors of a state @a state.
     * Successors will be written to successor list to be read later.
     *
     * @param state state to get successors of
     */
    inline void getStateSuccessors(unsigned state) {
      externGetStateSuccessors(state);
#ifdef WITH_PARAM
      if (paramVal == valueType) {
        computeTransRationals();
      }
#endif
    }
    /**
     * Return number of successors from last call of "getStateSuccessors".
     *
     * @return number of successor states
     */
    inline unsigned getNumSuccStates() {
      return *numSuccStates;
    }
    /**
     * Get array of successor states.
     * This value won't change for calls of "getStateSuccessors".
     *
     * @return array of successor states
     */
    inline unsigned *getSuccStatesList() {
      return succStatesList;
    }
    /**
     * Get array of rates to successor states.
     * This value won't change for calls of "getStateSuccessors".
     *
     * @return array of rates to successor states
     */
    inline double *getSuccRatesList() {
      return succRatesList;
    }
#ifdef WITH_PARAM
    /**
     * Get array of rates to successor states.
     * This value won't change for calls of "getStateSuccessors".
     *
     * @return array of rates to successor states
     */
    inline Rational::RationalFunction *getSuccRatesListRational() {
      return succRatesListRational;
    }
#endif
    /**
     * Get array of rewards to successor states.
     * This value won't change for calls of "getStateSuccessors".
     *
     * @return array of rates to successor states
     */
    inline double *getSuccRewardsList() {
      return succRewardsList;
    }
#ifdef WITH_PARAM
    /**
     * Get array of rewards to successor states.
     * This value won't change for calls of "getStateSuccessors".
     *
     * @return array of rates to successor states
     */
    inline Rational::RationalFunction *getSuccRewardsListRational() {
      return succRewardsListRational;
    }
#endif
    /**
     * Get non-determinism bounds.
     */
    inline unsigned *getNonDetBounds() {
      return nonDetBounds;
    }
    /**
     * Return reward of state @a state.
     *
     * @param state state to obtain reward of
     * @return reward of @a state
     */
    inline double getReward(unsigned state) const {
      return externGetReward(state);
    }
    /**
     * Set whether states shall be saved in compressed form.
     *
     * @param __compress true to safe states in compressed form
     */
    inline void setCompress(bool __compress) {
      compress = __compress;
    }
    /**
     * Set whether a reward analysis shall be done.
     *
     * @param __rewards true for reward analysis
     */
    inline void setRewards(bool __rewards) {
      rewards = __rewards;
    }
    /**
     * Check whether state is in given state set.
     *
     * @param setNr number of set to check whether state is in
     * @param state state to check whether it is in set
     * @return true iff given state is in given set
     */
    inline bool inStateSet(unsigned setNr, unsigned state) const {
      return externInStateSet(setNr, state);
    }
    /**
     * Get vector of initial states.
     *
     * @return vector of initial states
     */
    inline const std::vector<unsigned> &getInitialStates() const {
      return *externGetInitialStates();
    }
    bool exprValid(const CVC3::Expr &, unsigned) const;
    /**
     * Set optimization level to compile model with.
     * Notice that for some models, using high optimization levels,
     * the compilation of the model may take more time than the model
     * exploration, given it is very complex. 0 stands for no
     * optimizations, 3 for most.
     *
     * @param gccOptimizationLevel__ optimization level, from 0 to 3
     */
    inline void setGCCOptimizationLevel(unsigned gccOptimizationLevel__) {
      gccOptimizationLevel = gccOptimizationLevel__;
    }
    /**
     * Set data structure to map state to state number
     *
     * @param data structure to use to map state to state number
     */
    inline void setStateMapType(StateMapType stateMapType__) {
      stateMapType = stateMapType__;
    }
    /**
     * Set C++ compiler to use to compile model.
     * The parameter @a cppCompiler__ should specify the string to be
     * used call the compiler. Depending on PATH settings, it may be
     * absolute or relative.
     *
     * @param cppCompiler__ C++ compiler to use
     */
    inline void setCPPCompiler(const std::string &cppCompiler__) {
      cppCompiler = cppCompiler__;
    }
    /**
     * Obtain the value @a variable has at given @a state.
     * For boolean values, you will get "0" for false and "1" for true.
     *
     * @param state state to get value from
     * @param variable to get value of
     */
    inline int getValue(unsigned state, const std::string &variable) const {
      return externGetValue(state, variable);
    }
    void setValueType(ValueType);
    inline const std::string valueTypeString() {
      if (doubleVal == valueType) {
        return "double";
      } else if (paramVal == valueType) {
        return "unsigned";
      } else {
	throw std::runtime_error("Unsupported value type in Model2C.");
      }
    }
    void build();
    void addStateSet(const CVC3::Expr &);
    void exploreAllStates();
    const lang::Properties &getProperties();
    bool isContinuousTimeModel() const;
    inline unsigned getNumActiveCommands() const {
      return *externGetNumActiveCommands();
    }
    std::string getStateString(unsigned);
    bool isNonDet() const;
#ifdef WITH_PARAM
    Rational::RationalFunction getReward(unsigned);
#endif

  private:
#ifdef WITH_PARAM
    typedef std::tr1::unordered_map<Rational::RationalFunction, unsigned>
      RationalToNumber;
    typedef std::vector<Rational::RationalFunction> NumberToRational;
#endif
    bool fileExists(const std::string &) const;
    void prepareStateFormulasFromPropertyStructure();
    void prepareStateFormulasFromPropertyStructure
      (const lang::Property &);
    void init();
    template<typename T>
      void fetchExtFunction(const std::string &, T *);
    lang::Model *model;
    const lang::Commands *guardedTransitions;
    bool compress;
    std::ostream *streamP;
    std::ostream &stream;
    std::vector<CVC3::Expr> variables;
    std::vector<CVC3::Expr> variablesInC;
    std::ofstream *file;
    typedef void (*addInitialStates_t)();
    typedef unsigned* (*getNonDetBounds_t)();
    typedef void (*getStateSuccessors_t)(unsigned);
    typedef unsigned* (*getNumSuccStates_t)();
    typedef unsigned* (*getNumActiveCommands_t)();
    typedef unsigned* (*getSuccStatesList_t)();
    typedef double* (*getSuccRatesList_t)();
#ifdef WITH_PARAM
    typedef unsigned* (*getSuccRatesListUnsigned_t)();
#endif
    typedef double* (*getSuccRewardsList_t)();
#ifdef WITH_PARAM
    typedef unsigned* (*getSuccRewardsListUnsigned_t)();
#endif
    typedef unsigned (*getNumStates_t)();
    typedef void (*cleanup_t)();
    typedef double (*getReward_t)(unsigned);
    typedef unsigned (*getRationalReward_t)(unsigned);
    typedef bool (*inStateSet_t)(unsigned, unsigned);
    typedef std::vector<unsigned> *(*getInitialStates_t)();
    typedef int (*getValue_t)(unsigned, const std::string &);
    typedef std::vector<void *> *(*getStateList_t)();
    addInitialStates_t externAddInitialStates;
    getStateSuccessors_t externGetStateSuccessors;
    getNumSuccStates_t externGetNumSuccStates;
    getNumActiveCommands_t externGetNumActiveCommands;
    getSuccStatesList_t externGetSuccStatesList;
    getSuccRatesList_t externGetSuccRatesList;
    getStateList_t externGetStateList;
#ifdef WITH_PARAM
    getSuccRatesListUnsigned_t externGetSuccRatesListUnsigned;
#endif
    getSuccRewardsList_t externGetSuccRewardsList;
#ifdef WITH_PARAM
    getSuccRewardsListUnsigned_t externGetSuccRewardsListUnsigned;
#endif
    getNumStates_t externGetNumStates;
    void restrictExprToValidVariablesRange(CVC3::Expr &);
    getInitialStates_t externGetInitialStates;
    getNonDetBounds_t externGetNonDetBounds;
    cleanup_t externCleanup;
    getReward_t externGetReward;
    getRationalReward_t externGetRationalReward;
    inStateSet_t externInStateSet;
    getValue_t externGetValue;
    unsigned *numSuccStates;
    unsigned *numActiveCommands;
    unsigned *succStatesList;
    double *succRatesList;
    unsigned *succRatesListUnsigned;
#ifdef WITH_PARAM
    Rational::RationalFunction *succRatesListRational;
#endif
    double *succRewardsList;
    unsigned *succRewardsListUnsigned;
#ifdef WITH_PARAM
    Rational::RationalFunction *succRewardsListRational;
#endif
    unsigned *nonDetBounds;
    void* libHandle;
    void printGetters();
    void enumerateVariables();
    void printExprC(const CVC3::Expr &);
    void printGetStateSuccessors();
    void printDecodeState();
    void printSuccStateAssignments(lang::Alternative &);
    void printSuccVarDefinition();
    void printSuccToSuccProp();
    void printSafeSuccState();
    bool isInfVariable(unsigned);
    unsigned numVariableBits(unsigned);
    void printStateMapDef();
    void printStatePropType();
    void printFileHeader();
    void printAddInitialStates();
    void printGetStateList();
    void printStateBuffer();
    void printCleanup();
    void printNewStateProp();
    void setOutput(std::ostream &);
    void setOutput(const std::string &);
    void print();
    std::string computeCallString();
    void compileAndLoad();
    void printGetReward();
    void printGetRationalReward();
    void printInStateSet();
    void printAdjustNextStateProbabilities();
    void printGetValue();
#ifdef WITH_PARAM
    void preparePARAMSpecific();
    void computeTransRationals();
#endif
    std::string getVarName(unsigned);

    unsigned maxSuccStates;
    std::vector<int> lowerBounds;
    std::vector<int> upperBounds;
    bool rewards;
    std::vector<CVC3::Expr> stateSets;
    std::vector<unsigned> *initialStates;
    unsigned gccOptimizationLevel;
    StateMapType stateMapType;
    std::string cppCompiler;
    bool internalModel;
    CVC3::ExprHashMap<unsigned> *exprNumbers;
    ValueType valueType;
#ifdef WITH_PARAM
    RationalToNumber  *rateToNumber;
    NumberToRational *numberToRate;
    NumberToRational *numberToTransReward;
    NumberToRational *numberToStateReward;
    Rational::CVC3Converter *cvc3converter;
#endif
  };
}

#endif
