/*
 * SymbolicModel.hh
 *
 *  created on: 09.10.2015
 *      author: rungger
 */

#ifndef SYMBOLICMODEL_HH_
#define SYMBOLICMODEL_HH_

#include <iostream>

#include "cuddObj.hh"
#include "dddmp.h"

#include "SymbolicSet.hh"


namespace scots {
/*
 * class: SymbolicModel
 *
 * base class for <SymbolicModelGrowthBound>
 * 
 * it stores the bdd of the transition relation and its bdd variable information
 * it provides an iterator to loop over all elements in the stateSpace and inputSpace
 *
 * the actual computation of the transition relation is computs in the derived
 * classes
 */
class SymbolicModel {
protected:
  /* var: ddmgr_ */
  Cudd *ddmgr_;
  /* var: stateSpace_ */
  SymbolicSet *stateSpace_;
  /* var: inputSpace_ */
  SymbolicSet *inputSpace_;
  /* var: nssVars_ 
   * number of state space bdd variables (= number of pre/post variables)  */
  size_t nssVars_;
  /* var: preVars_ 
   * array of indices of the state space pre bdd variables  */
  size_t* preVars_;
  /* var: postVars_ 
   * array of indices of the state space post bdd variables  */
  size_t* postVars_;
  /* var: nisVars_ 
   * number of input space bdd variables */
  size_t nisVars_;
  /* var: inpVars_ 
   * array of indices of the input space bdd variables  */
  size_t* inpVars_;
  /* var: iterator_ 
   * CuddMintermIterator to iterate over all elements in stateSpace_ and
   * inputSpace_ */
  CuddMintermIterator *iterator_;
  BDD it;
  /* var: transitionRelation_ 
   * the bdd representation of the transition relation  X x U x X
   * the bdd variables of the transition relation are 
   * given by preVars_ x inpVars_ x postVars_ */
  BDD transitionRelation_;
  friend class FixedPoint;
public:
  SymbolicModel(SymbolicSet *stateSpace, SymbolicSet *inputSpace): stateSpace_(stateSpace), inputSpace_(inputSpace) {
    if(stateSpace_->ddmgr_!=inputSpace_->ddmgr_) {
      std::ostringstream os;
      os << "Error: scots::SymbolicModel: stateSpace and inputSpace need to have the same dd manager.";
      throw std::invalid_argument(os.str().c_str());
    }
    ddmgr_=stateSpace_->ddmgr_;
    nssVars_=0;
    for(size_t i=0; i<stateSpace_->dim_; i++) 
      for(size_t j=0; j<stateSpace_->nofBddVars_[i]; j++) 
       nssVars_++; 
    nisVars_=0;
    for(size_t i=0; i<inputSpace_->dim_; i++) 
      for(size_t j=0; j<inputSpace_->nofBddVars_[i]; j++) 
       nisVars_++; 

    /* set the preVars_ to the variable indices of stateSpace_ 
     * and get new indices for the postVars_ */
    preVars_ = new size_t[nssVars_];
    postVars_ = new size_t[nssVars_];
    for(size_t k=0, i=0; i<stateSpace_->dim_; i++) {
      for(size_t j=0; j<stateSpace_->nofBddVars_[i]; k++, j++) {
       preVars_[k]=stateSpace_->indBddVars_[i][j];
       BDD t=stateSpace_->ddmgr_->bddVar();
       postVars_[k]=t.NodeReadIndex();
      }
    }
    inpVars_ = new size_t[nisVars_];
    for(size_t k=0, i=0; i<inputSpace_->dim_; i++) {
      for(size_t j=0; j<inputSpace_->nofBddVars_[i]; k++, j++) {
       inpVars_[k]=inputSpace_->indBddVars_[i][j];
      }
    }
    /* initialize the transition relation */
    transitionRelation_=stateSpace_->symbolicSet_*inputSpace_->symbolicSet_;
    it=transitionRelation_;
  };

  ~SymbolicModel(void) {
    delete[] preVars_;
    delete[] postVars_;
    delete[] inpVars_;
  };
  /* function:  getSize 
   * get the number of elements in the transition relation */
  inline double getSize(void) {
    return transitionRelation_.CountMinterm(2*nssVars_+nisVars_);
  };
  /* function:  getTransitionRelation 
   * get the BDD which represents the transition relation */
  inline BDD getTransitionRelation(void) {
    return transitionRelation_;
  }; 
  /* iterator methods */
  /* function: begin
   * initilize the iterator and compute the first element */
  inline void begin(void) {
    size_t nvars_=nssVars_+nisVars_;
    std::vector<size_t> ivars_;
    ivars_.reserve(nvars_);
    for(size_t i=0; i<nssVars_; i++) 
      ivars_.push_back(preVars_[i]);
    for(size_t i=0; i<nisVars_; i++) 
      ivars_.push_back(inpVars_[i]);
    /* set up iterator */
    iterator_ = new CuddMintermIterator(it,ivars_,nvars_);
  }
  /* function: next
   * compute the next minterm */
  inline void next(void) {
    ++(*iterator_);
  }
  /* function: progress
   * print progess of iteratin in percent */
  inline void progress(void) const {
    iterator_->printProgress();
  }  /* function: done
   * changes to one if iterator reached the last element */
  inline int done(void) {
    if(iterator_->done()) {
      delete iterator_;
      iterator_=NULL;
      return 1;
    } else 
    return 0;
  }
  /* function: currentMinterm
   * returns the pointer to the current minterm in the iteration */
  inline const int* currentMinterm(void) const {
    if (iterator_)
      return iterator_->currentMinterm();
    else
      return NULL;
  }
  /* function:  writeToFile
   * stores the bdd of transition function as a <SymbolicSet> with all information to file*/
  void writeToFile(const char *filename) {
    /* produce string with parameters to be written into file */
    std::stringstream dim;
    std::stringstream z;
    std::stringstream eta;
    std::stringstream first;
    std::stringstream last;
    std::stringstream nofGridPoints;
    std::stringstream indBddVars;

    size_t dim_ = 2*stateSpace_->dim_+inputSpace_->dim_;

    dim <<"#scots dimension: " << dim_ << std::endl;
    z << "#scots measurement error bound: ";
    eta << "#scots grid parameter eta: ";
    first << "#scots coordinate of first grid point: ";
    last << "#scots coordinate of last grid point: ";
    nofGridPoints << "#scots number of grid points (per dim): ";
    indBddVars << "#scots index of bdd variables: ";

    /* write information of the pre state space */
    for(size_t i=0; i<stateSpace_->dim_; i++) {
      z << stateSpace_->z_[i] << " ";
      eta << stateSpace_->eta_[i] << " ";
      first << stateSpace_->firstGridPoint_[i] << " ";
      last << stateSpace_->lastGridPoint_[i] << " ";
      nofGridPoints << stateSpace_->nofGridPoints_[i] << " ";
    }
    for(size_t j=0; j<nssVars_; j++) 
      indBddVars << preVars_[j] << " ";

    /* write information of the input space */
    for(size_t i=0; i<inputSpace_->dim_; i++) {
      z << inputSpace_->z_[i] << " ";
      eta << inputSpace_->eta_[i] << " ";
      first << inputSpace_->firstGridPoint_[i] << " ";
      last << inputSpace_->lastGridPoint_[i] << " ";
      nofGridPoints << inputSpace_->nofGridPoints_[i] << " ";
    }
    for(size_t j=0; j<nisVars_; j++) 
      indBddVars << inpVars_[j] << " ";

    /* write information of the post state space */
    for(size_t i=0; i<stateSpace_->dim_; i++) {
      z << stateSpace_->z_[i] << " ";
      eta << stateSpace_->eta_[i] << " ";
      first << stateSpace_->firstGridPoint_[i] << " ";
      last << stateSpace_->lastGridPoint_[i] << " ";
      nofGridPoints << stateSpace_->nofGridPoints_[i] << " ";
    }
    for(size_t j=0; j<nssVars_; j++) 
      indBddVars << postVars_[j] << " ";

    z << std::endl;
    eta << std::endl;
    first << std::endl;
    last << std::endl;
    nofGridPoints << std::endl;
    indBddVars << std::endl;

    std::stringstream paramss;
    paramss << "################################################################################" << std::endl
            << "########### symbolic controller synthesis toolbox information added ############" << std::endl
            << "################################################################################" << std::endl
            << dim.str() \
            << eta.str() \
            << z.str() \
            << first.str() \
            << last.str() \
            << nofGridPoints.str() \
            << indBddVars.str();
    std::string param=paramss.str();


    FILE *file = fopen (filename,"w");
    if (file == NULL){
        std::ostringstream os;
        os << "Error: Unable to open file for writing." << filename << "'.";
        throw std::runtime_error(os.str().c_str());
    }
    if (param.size() != fwrite(param.c_str(),1,param.size(),file)) {
        throw "Error: Unable to write set information to file.";
    }

    int storeReturnValue = Dddmp_cuddBddStore(
      ddmgr_->getManager(),
      NULL,
      transitionRelation_.getNode(),
      //(char**)varnameschar, // char ** varnames, IN: array of variable names (or NULL)
      NULL, // char ** varnames, IN: array of variable names (or NULL)
      NULL,
      DDDMP_MODE_BINARY,
      // DDDMP_VARNAMES,
      DDDMP_VARIDS,
      NULL,
      file
    );

    fclose(file);
    if (storeReturnValue!=DDDMP_SUCCESS) 
      throw "Error: Unable to write BDD to file.";
    else
      std::cout << "Symbolic set saved to file: "<< filename << std::endl;
  } 
}; /* close class def */
} /* close namespace */

#endif /* SYMBOLICMODEL_HH_ */