/***
 *** See the file "mba/disclaimers-and-notices-L2.txt" for
 *** information on usage and redistribution of this file,
 *** and for a DISCLAIMER OF ALL WARRANTIES.
 ***/

/* $Id: to_t_system.cpp,v 1.1.1.1 2006/10/09 06:58:18 shao Exp $ */

#include <readers/L2_file.h>
#include <readers/to_t_system.h>
#include <readers/transition.h>
#include <transition/transitioned.h>

// verbose output
// The do-while(0) is the only portable way to block
#ifdef ENABLE_L2_VERBOSE
#  define verbose(expr) do { if (isVerbose()) { expr; } } while(0)
#else
#  define verbose(expr)
#endif

// record via the listener
// The do-while(0) is the only portable way to block
#ifndef DISABLE_TO_T_SYSTEM_LISTEN
#  include <readers/to_t_system_listener.h>
#  define record(call_with_args) \
   do { \
    Slist<to_t_system_listener*>::iterator listen_it##__LINE__ \
        = listeners_.begin(); \
    while(listen_it##__LINE__ != listeners_.end()) { \
        (*listen_it##__LINE__)->call_with_args;  \
        ++listen_it##__LINE__; \
    } \
   } while(0)
#else
#  define record(call_with_args)
#endif


// Needed to implement created_clause: a listener into the TMS that catches the
// created_clause event and translates it to the user's to_t_system_listener
// call.  We also need to pass call on to the other listener.

#ifndef DISABLE_TO_T_SYSTEM_LISTEN
#include <tms/ptheory_listener.h>
class to_t_system::tms_listener : public Pooled,
		   public virtual Ptheory_listener
{
private:
  // can't be null
  Slist<to_t_system_listener*>& listeners_;
  Ptheory& theory;
  friend class to_t_system;

public:
  tms_listener(Slist<to_t_system_listener*>& l, Ptheory& p)
    : listeners_(l), theory(p) {
    theory.add_listener(this);
  }

  virtual ~tms_listener() {
    theory.remove_listener(this);
  }

  // translate into a call on the user's to_t_system_listener
  virtual void created_clause(Clause& newclause) {
    if (creating_from_variable)
      record(created_clause(var, newclause));
    else
      record(created_clause(cls, newclause));
  }

  // we ignore all these
  virtual void created_proposition(Proposition&) { }
  virtual void destroying_proposition(Proposition&) { }
  virtual void destroying_clause(Clause&) { }
  virtual void destroying_container(Ptheory&) {
    L2_throw(L2_fatal_error,
	     ("Expected theory to outlast the reader!"));
  }

private:
  // We could use a union, but we'd only save all of 4 bytes,
  // and unions are ugly.
  const L2rVariable *var;
  const L2rClause   *cls;
  bool creating_from_variable; // if false, creating from clause
};
#endif


/***************************************************************************
        Constructor
 ***************************************************************************/

to_t_system::to_t_system(const L2_file *f, T_system *tsys)
    : L2_file_writer (f), t_system(tsys) {
}

to_t_system::~to_t_system() {
  record(destroying_container(*this));
}

/***************************************************************************
        The main function
 ***************************************************************************/

// Take info from the l2_file and put it into the T_system

bool to_t_system::write() {
#ifndef DISABLE_TO_T_SYSTEM_LISTEN
  // Set a listener which will allow us to keep track of where clauses come
  // from.  The internal_listen just translates TMS listener calls into
  // to_t_system_listener calls.
  if (!listeners_.empty()) {
    internal_tms_listen =
      new tms_listener(listeners_, *t_system->get_solver());
  } else {
    internal_tms_listen = 0;
  }
#endif

  // The model from the reader
  const L2_file *source = get_source();

  // Some checks that the model has needed elements
  L2_assert(source->nenums() != 0,
	    L2_empty_model_error,
            ("model has no enumerations"));
  L2_assert(source->nvars() != 0,
	    L2_empty_model_error,
            ("model has no variables"));
  L2_assert(source->nclauses() != 0,
	    L2_empty_model_error,
            ("model has no clauses"));

  // Create the 3 tyeps of elements (variables, clauses, transitions)
  {
    for (unsigned i = 0; i < source->nvars(); i++)
      createVariable(source->getVar(i));
  }
  {
    for (unsigned i = 0; i < source->nclauses(); i++)
      createBackground(source->getClause(i));
  }
  {
    for (unsigned i = 0; i < source->nvars(); ++i) {
      const L2rVariable* pL2rVariable = source->getVar(i);
      if (pL2rVariable->kind() == vk_mode) {
	// It is a mode
	createTransitions(source->getVar(i)); // ignored if not a mode
      }
    }
  }

#ifndef DISABLE_TO_T_SYSTEM_LISTEN
  // Undo the work we did at the top of the file.
  if (!listeners_.empty()) {
    delete internal_tms_listen;
  }
#endif

  return true;
}


// Turn an L2rVariable (from the l2_file) into a Variable (in the T_system)

void to_t_system::createVariable(const L2rVariable *pL2rVariable) {
#ifndef DISABLE_TO_T_SYSTEM_LISTEN
  if (internal_tms_listen) {
    internal_tms_listen->creating_from_variable = true;
    internal_tms_listen->var = pL2rVariable;
  }
#endif
  unsigned domainCardinality = pL2rVariable->type()->nmembers();
  unsigned variableID = pL2rVariable->id();
  Variable *pVariable = NULL;
  switch(pL2rVariable->kind()) {
  case vk_commanded:
    {
      Command* pCommand =
	t_system->create_command(domainCardinality, T_system::NOW, variableID);
      // It's OK to assign the present state Command because the present state
      // Command doesn't constrain anything. The previous Command constrains
      // the current state Variables, but the current Commands don't constrain
      // anything and are always noCommand (index 0) -- nothing will ever set
      // them to anything else!
      pCommand->assign(0u);
      pVariable = pCommand;
    }
    break;
  case vk_observed:
    pVariable =
      t_system->create_observable(domainCardinality, T_system::NOW, variableID);
    break;
  case vk_mode:
    pVariable =
      new Transitioned(*t_system, domainCardinality, variableID,
		       pL2rVariable->mode()->domain_size(), T_system::NOW);
    break;
  default:
    pVariable =
      t_system->create_dependent(domainCardinality, T_system::NOW, variableID);
    break;
  }
  t_system->register_new_variable(pVariable);
  verbose(_STD_ cout << "Created variable " << pVariable->get_id() << " `"
	  << pL2rVariable << "'\n");
  record(created_variable(pL2rVariable, *pVariable));
}


// Create the Transition objects that go from one mode to another

void to_t_system::createTransitions(const L2rVariable *pL2rVariable) {
  const L2rMode *pL2rMode = pL2rVariable->mode();
  // Map from L2rVariable (l2_file) to Variable (T_system) and cast to
  // Transitioned*
  Transitioned *pTransitioned =
    static_cast<Transitioned*>(findVar(pL2rVariable));

  // Create the nominal Transition. The index of the nominal value is zero.
  // Note there must be exactly one of them.
  {
    for (L2rMode::iterator it = pL2rMode->begin_nominal();
	 it != pL2rMode->end_nominal(); ++it) {
      const L2rTransition *pL2rTransition = *it;
      createTransition(pTransitioned, pL2rTransition, 0); // 0 is nominal index
    }
  }

  // Create the failure Transitions. Each failure has its own index.
  // The first failure has index 1, not 0 (0 is nominal)
  
  // When doing recovery instead of diagnosis, failures are irrelevant.
  if (!t_system->isPlanning()) {
    unsigned i = 1;
    for (L2rMode::iterator it = pL2rMode->begin_failure();
	 it != pL2rMode->end_failure() ; ++it) {
      const L2rTransition *pL2rTransition = *it;
      createTransition(pTransitioned, pL2rTransition, i++);
    }
    L2_assert(i == pTransitioned->get_ntransitions(),
	      L2_writer_error,
	      ("Mode v" + MBA_string(pTransitioned->get_id()) +
	       " has the wrong number of transitions"));
  }
}