// Create a clause if it is in the background

void to_t_system::createBackground(const L2rClause *pL2rClause) {
  if (pL2rClause->isInBackground()) {
    // background clauses are 'state' constraints by definition
    expandClause(pL2rClause, true);
  }
}

// Handle a Clause with any number of Variable1 == Variable2 Propositions

void to_t_system::expandClauseEquality(const Slist<const L2rPropVarVar*>&
				       equality,
				       T_system::Proto_assignment_list& pos,
				       T_system::Proto_assignment_list& neg,
				       bool state_constr) {
  Slist<Partition*> stack; // stack of Partition to avoid recursion
  stack.push_front(new Partition(pos, neg, equality)); // the initial Partition
  while (!stack.empty()) {
    // Pop the top element from the stack; note that this takes two operations.
    Partition* pPartition = stack.front(); stack.pop_front();
    // Extract the lists of Propositions
    T_system::Proto_assignment_list& positiveSingles =
      pPartition->getPositiveSingles();
    T_system::Proto_assignment_list& negativeSingles =
      pPartition->getNegativeSingles();
    const Slist<const L2rPropVarVar*>& duals = pPartition->getDuals();
    if (duals.empty()) { // the base step; create the Clause
      t_system->create_constraint(positiveSingles, negativeSingles, false,
				  true, state_constr);
    } else { // a recursive step
      // Non-destructively retrieve the first L2rPropVarVar
      const L2rPropVarVar* pL2rPropVarVar = duals.front();
      // Take the "cdr" of the duals list; note that this takes two operations.
      Slist<const L2rPropVarVar*> tail(duals); tail.pop_front();
      // The two Variables must be of the same type
      L2_assert(pL2rPropVarVar->var()->type() ==
		pL2rPropVarVar->otherVar()->type(),
		L2_reader_error,
		("Type mismatch in equality"));
      // Get the Variables as known in the T_system; and the domain
      Variable* pVariable1 = findVar(pL2rPropVarVar->var());
      Variable* pVariable2 = findVar(pL2rPropVarVar->otherVar());
      const L2rEnumeration* pL2rEnumeration = pL2rPropVarVar->var()->type();
      const unsigned domainCardinality = pL2rEnumeration->nmembers();
      if (pL2rPropVarVar->isPositive()) {
	// positive: create clauses (c is the current list in neg/pos)
	//   foreach i in domain[v],
	//      c  !v1=i v2=i               (v1=i implies v2=i)
	//      c  !v2=i v1=i               (v2=i implies v1=i)
	for (unsigned i = 0 ; i < domainCardinality; i++) {
	  unsigned j = domainCardinality - i - 1; // to pass regression tests
	  {
	    // c !v1=i v2=i; v1 == i ==> v2 == i 
	    Partition* p = new Partition(pos, neg, tail); // delete when popped
	    p->getNegativeSingles().push(
	      T_system::Proto_assignment(pVariable1, j)
	    );
	    p->getPositiveSingles().push(
	      T_system::Proto_assignment(pVariable2, j)
	    );
	    stack.push_front(p);
	  }
	  {
	    // c  !v2=i v1=i; v2 == i ==> v1 == i
	    Partition* p = new Partition(pos, neg, tail); // delete when popped
	    p->getNegativeSingles().push(
	      T_system::Proto_assignment(pVariable2, j)
	    );
	    p->getPositiveSingles().push(
	      T_system::Proto_assignment(pVariable1, j)
	    );
	    stack.push_front(p);
	  }
	}
      } else {
	// negative:
	//   foreach i in domain[v],
	//      c  !v1=i !v2=i              (v1=i implies v2!=i and v-v)
	for (unsigned i = 0; i < domainCardinality; i++) {
	  unsigned j = domainCardinality - i - 1; // to pass regression tests
	  // c  !v1=i !v2=i; v1 == i ==> v2 != i
	  Partition* p = new Partition(pos, neg, tail); // delete when popped 
	  p->getNegativeSingles().push(T_system::Proto_assignment(pVariable1,
								  j));
	  p->getNegativeSingles().push(T_system::Proto_assignment(pVariable2,
								  j));
	  stack.push_front(p);
	} // end for
      } // end else
    } // end else
    delete pPartition; // done with this "stack frame"
  }
}


// Create a Clause from an L2rClause

void to_t_system::expandClause(const L2rClause *pL2rClause,
			       bool state_constr) {
#ifndef DISABLE_TO_T_SYSTEM_LISTEN
  if (internal_tms_listen) {
    internal_tms_listen->creating_from_variable = false;
    internal_tms_listen->cls = pL2rClause;
  }
#endif

  T_system::Proto_assignment_list pos(pL2rClause->nprops());
  T_system::Proto_assignment_list neg(pL2rClause->nprops());

  // A Variable1 == Variable2 L2rProposition in the L2rClause, if there is any
  Slist<const L2rPropVarVar*> equality;

  for (unsigned i = 0; i < pL2rClause->nprops(); i++) {
    const L2rProposition *pL2rProposition = pL2rClause->prop(i);
    if (pL2rProposition->isEquality()) {
      equality.push_front(static_cast<const L2rPropVarVar*>(pL2rProposition));
    } else {
      // Variable == Value
      // Downcast
      const L2rPropVarValue *pL2rPropVarValue =
	static_cast<const L2rPropVarValue*>(pL2rProposition);
      // Find the Proposition's Variable and value index
      Variable *pVariable = findVar(pL2rPropVarValue->var());
      int valueIndex = pL2rPropVarValue->value();
      if (pL2rPropVarValue->isPositive()) {
	pos.push(T_system::Proto_assignment(pVariable, valueIndex));
      } else {
	neg.push(T_system::Proto_assignment(pVariable, valueIndex));
      }
    }
  }

  expandClauseEquality(equality, pos, neg, state_constr);
}


// Create a Transitioned from an L2rTransition

void to_t_system::createTransition(Transitioned *pTransitioned,
				   const L2rTransition *pL2rTransition,
				   unsigned transition_value) {
  unsigned rank = pL2rTransition->rank();
  if (rank != 0) { // Non-default cost/rank
    pTransitioned->add_transition_cost(static_cast<Assignment::weight_t>(rank));
  }

  if (pL2rTransition->nclauses() == 0) {
    if (pL2rTransition->isFailure()) {
      // Add an autonomous transition; no from
      pTransitioned->add_failure_prototype(transition_value,
					   pL2rTransition->to());
    } else {
      // Add an idle transition; from == to
      L2_assert(pL2rTransition->from() == pL2rTransition->to(),
		L2_reader_error,
		("non-idle non-failure uncommanded transition"));
      pTransitioned->add_idle_prototype(pL2rTransition->to());
    }
  } else {
    // Add a nominal transition
    for (unsigned i = 0; i < pL2rTransition->nclauses(); ++i) {
      const L2rClause *pL2rClause = pL2rTransition->clause(i);

      // Collect the positive and negative assignments
      Slist<T_system::Proto_assignment> pos;
      Slist<T_system::Proto_assignment> neg;
      for (unsigned j = 0; j < pL2rClause->nprops(); ++j) {
	const L2rProposition *pL2rProposition = pL2rClause->prop(j);
	// A Transition can not assert Variable1 == Variable2
	L2_assert(!pL2rProposition->isEquality(),
		  L2_reader_error,
		  ("found equality as guard condition"));
	// Cast as L2rPropVarValue (Variable == Value)
	const L2rPropVarValue *pL2rPropVarValue =
	  static_cast<const L2rPropVarValue*>(pL2rProposition);
	Variable *pVariable = findVar(pL2rPropVarValue->var());
	int valueIndex = pL2rPropVarValue->value();
	T_system::Proto_assignment pa(pVariable, valueIndex);
	if (pL2rPropVarValue->isPositive()) {
	  pos.push_front(pa);
	} else {
	  neg.push_front(pa);
	}
      }

      pTransitioned->add_commanded_prototype(transition_value,
					     pL2rTransition->from(),
					     pL2rTransition->to(),
					     pos, neg);
    }
  }
  verbose(_STD_ cout << "Created transition " << pL2rTransition << _STD_ endl);
}


/***************************************************************************
  Creating the initial state.  Quite likely we don't actually want this
  encoded in the model, but in some other file somewhere.  But it's here
  for now.
 ***************************************************************************/

void to_t_system::createInitialState() {
  State_variable* pStateVariable =
    t_system->create_state_var(0,  // horizon time step
			       1); // state count
  for (unsigned i = 0; i < get_source()->nvars(); i++) {
    const L2rVariable *pL2rVariable = get_source()->getVar(i);
    // if not set, ignore
    if (pL2rVariable->initial() != L2rVariable::NO_INITIAL_VALUE) {
      // Only mode or Observable Variables can have initial values
      L2_assert((pL2rVariable->kind() == vk_mode) ||
		(pL2rVariable->kind() == vk_observed),
		L2_reader_error,
		("v" + MBA_string(pL2rVariable->id()) +
		 " is neither mode nor observation yet has an initial value"));
      if (pL2rVariable->kind() == vk_mode) {
	Transitioned *pTransitioned =
	  static_cast<Transitioned*>(findVar(pL2rVariable));
	pTransitioned->set_initial_mode(0,                       // state=s0
					pL2rVariable->initial(),
					T_system::NOW,
					true);                   // inTheory
      } else if (pL2rVariable->kind() == vk_observed) {
	Observable* pObservable =
	  static_cast<Observable*>(findVar(pL2rVariable));
	pObservable->observe(pL2rVariable->initial());
      } else {
	// Shouldn't get here
      }
    }
  }

  pStateVariable->assign(unsigned(0)); // 0 is ambiguous unsigned or pointer

  // no need to progress; this does all we need
  t_system->next_timestep();
  t_system->propagate();
}


/***************************************************************************
  Fast lookup from L2_file data types to T_system types.
  This is likely a duplicate of some information we'd keep anyway,
  but this way, the to_t_system class is independent of who's using
  it (flight, GPU, etc).
 ***************************************************************************/
Variable *to_t_system::findVar(const L2rVariable *var) const {
    return t_system->get_present_variable(var->id());
}