#include "MemoryManager.h"
#include "spnbox.h"
#include "matrixmath.h"
#include "../pnheaders/matrix.h"
#include "../pnheaders/pns.h"

/* Return 0 if two leaves are identical.*/
int cmpLeaf(inequality2 *l1, inequality2 *l2);

/* Given a plant and a expression tree with state interpretation,
   CONSTRUCT_SPEC_PROP constructs the new constraints that can be used in 
   LINENF.*/
int construct_spec(pns* plant1, expression2 *root, pns* plant2, matrix *L, \
		   int **b);

/* Given a plant and a expression tree with dynamic interpretation, 
   CONVERT_LEAVES will convert the original tree and plant to the new tree and 
   plant that can be used in CONSTRUCT_SPEC. All the leaves of the original 
   tree will be converted.*/
int convert_leaves(pns* plant1, pns* plant2, expression2 *root);

/* Given a PN and set of constraints in state-based interpretation, 
   CONVERT_PROP will convert the current constraints to new constraints and 
   update the PN accordingly. This function is part of disj2normal.c*/
int convert_prop(pns* pn_before, matrix* L, int* b, int* LB, int* UB, \
		 matrix* LD, int* CD, pns* pn_after);

/* Given an expression tree, FIND_SUBTREES will find the parents and their 
   children that are the deepest leaves in the tree, returned by an array of 
   structs. Also, an array of leaves is returned, containting the same leaves 
   but with no repetitions. */
int find_subtrees(expression2* root, int* tree_depth,		  \
		  expression2 **tree_structs, int *snodes_number, \
		  inequality2 **unique_leaves, int *uleaves_number);

/* Given the root of an expression tree, get the number of nodes that do not
   have any successor node, and the number of their leaves.*/
void getDeepestNodeCount(expression2 *root, int *curr_depth, int* tree_depth, \
			 int *snode_number, int *sleaves_number);

/* Given the root of an expression tree, get the depth of the tree. Leaves are
   not considered.*/
void getDepth(expression2 *root, int *curr_depth, int *tree_depth);

/* Given the root of an expression tree, return the first leaf of root if it 
   exists, otherwise return the first leaf of the first nodes.*/
inequality2* getFirstLeaf(expression2 *root);

/* Given the root of an expression tree, return the total number of leaves.*/
int getLeafCount(expression2 *root);

/* Given an expression tree and a leaf, return the next leaf on its right,
   which may not be under the same node. curr_leaf_found is used to mark 
   whether the leaf has been found.*/
inequality2* getNextLeaf(expression2 *root, inequality2* current_leaf, \
			 int *curr_leaf_found);

/* Return 0 if the root has no successor node.*/
int isRoot(expression2* root);

/* With the information of struct containing the deepest subtrees and the 
   current PN, MERGE_PROP will construct the new propositions that can be 
   attached to the updated tree. 
   This function is a subroutine of construct_spec*/
inequality2 merge_prop(expression2 *tree_struct, inequality2 **unique_leaves,\
		       int leaves_num, int pnum, variable* v);

/* Replace the node ts with a leaf mp in the expression tree*/
void node2leaf(expression2 *root, expression2* ts, inequality2* mp);

/* Given an expression tree, get the nodes in the deepest layer and store them
   in an array: tree_structs*/
void setTreeStructs(expression2 *root, int *curr_depth, int* tree_depth, \
		    expression2 **tree_structs, int *ni);

int tree2spec(pns* plant1, expression2 *root, char *type, pns* plant2, \
	      matrix *L, int **b)
{
  pns plant0;
  /* if the propositions are state-based interpretation*/
  if (strcmp(type, "state") == 0) {
    construct_spec(plant1, root, plant2, L, b);
  }
  /* if the propositions are dynamic interpretation, then make it state-based first*/
  else if (strcmp(type, "dynamic") == 0) {
    convert_leaves(plant1, &plant0, root);
    construct_spec(&plant0, root, plant2, L, b);
  }
  else {
    return -1;
  }
  printf("Tree constraints converted.\n");
  deallocpn(&plant0);
  return 0;
}


/******************************************************/
/*          Utility Functions and Subroutines         */
/******************************************************/

/* Return 0 if two leaves are identical.*/
int cmpLeaf(inequality2 *l1, inequality2 *l2)
{
  int flag = 0;
  variable *vl1, *vl2;
  if(l1 == l2)
    return 0;
  if(l1->free_term != l2->free_term || l1->lb != l2->lb || l1->ub!=l2->ub)
    return 1;
  vl1 = l1->variable_list;
  vl2 = l2->variable_list;
  while(vl1 && vl2) {
    if(vl1->type != vl2->type || vl1->coefficient != vl2->coefficient \
       || vl1->index != vl2->index)
      return 1;
    vl1 = vl1->next;
    vl2 = vl2->next;
  }
  if(vl1 || vl2)
    return 1;
  else
    return 0;
}

/* Given a plant and a expression tree with state interpretation, 
   CONSTRUCT_SPEC_PROP constructs the new constraints that can be used in 
   LINENF. This function is a subroutine of tree2spec.*/
int construct_spec(pns* plant, expression2 *root, pns* new_plant, \
		   matrix *new_L, int** new_b)
{
  expression2 **tree_structs;
  inequality2 **unique_leaves;
  inequality2 *merged_prop;
  int snodes_number = 0, uleaves_number = 0, sleaves_number = 0, i, j;
  int curr_depth = 1, tree_depth = 1;
  MemoryManager memory;
  matrix L, LD_after, LD_before;
  int *b, *LB, *UB, *CD, firstTime = 1, *old_b;
  variable *vl, *v;
  pns pn_before, pn_after;
  
  memory = CreateMemoryManager(20, 20, 0, 0);
  /* Search for the subtrees that contain the deepest leaves of the current 
     tree and set up an array containing the unique leaves from these leaves.*/
  pn_before = copypn(plant);
  getDepth(root, &curr_depth, &tree_depth);
  if(isRoot(root) == 0) {
    snodes_number = 1;
    sleaves_number = root->n;
  }
  else
    getDeepestNodeCount(root, &curr_depth, &tree_depth, &snodes_number, \
			&sleaves_number);
  tree_structs = mmalloc(&memory, snodes_number * sizeof (expression2*));
  unique_leaves = mmalloc(&memory, sleaves_number * sizeof (inequality2*));
  find_subtrees(root, &tree_depth, tree_structs, &snodes_number, \
		unique_leaves, &uleaves_number);
  /* Get the new constraints recursively by updating the plant and tree.*/
  while(isRoot(root) != 0) {
    /* Get the constraints from unique_leaves.*/
    MAllocateMatrixType(&memory, 2, &L, uleaves_number, pn_before.pnum);
    b = mmalloc(&memory, pn_before.pnum * sizeof(int));
    LB = mmalloc(&memory, pn_before.pnum * sizeof(int));
    UB = mmalloc(&memory, pn_before.pnum * sizeof(int));
    for(i = 0; i < uleaves_number; i++) {
      vl = unique_leaves[i]->variable_list;
      while(vl) {
	SetMatrixEl(&L, i, vl->index, vl->coefficient);
	vl = vl->next;
      }
      b[i] = unique_leaves[i]->free_term;
      LB[i] = unique_leaves[i]->lb;
      UB[i] = unique_leaves[i]->ub;
    }
    /* Update the current PN and get the new set of constraints.*/
    MAllocateMatrixType(&memory, 2, &LD_after, 2 * L.nr, L.nc + L.nr);
    CD = mmalloc(&memory, 2 * L.nr * sizeof(int));
    convert_prop(&pn_before, &L, b, LB, UB, &LD_after, CD, &pn_after);
    /* Update the tree by cutting the deepest leaves and setting new 
       propositions for them.*/
    merged_prop = mmalloc(&memory, snodes_number * sizeof(inequality2));
    for(i = 0; i < snodes_number; i++) {
      v = mmalloc(&memory, \
		  (pn_before.pnum + uleaves_number) * sizeof(variable));
      merged_prop[i] = merge_prop(tree_structs[i], unique_leaves, \
				  uleaves_number, pn_before.pnum, v);
      node2leaf(root, tree_structs[i], &merged_prop[i]);
    }
    /* Update the set of constraits.*/
    if(firstTime) {
      AllocateMatrixType(2, new_L, LD_after.nr, LD_after.nc);
      CopyMatrix(&LD_after, new_L);
      MAllocateMatrixType(&memory, 2, &LD_before, new_L->nr, new_L->nc);
      CopyMatrix(new_L, &LD_before);
      firstTime = 0;
      *new_b = tmalloc(new_L->nr * sizeof(int));
      for(i = 0; i < LD_before.nr; i++) {
	(*new_b)[i] = CD[i];
      }
    }
    else {
      AllocateMatrixType(2, new_L, LD_after.nr, \
			  LD_before.nc + LD_after.nc);  
      CopyBlock(LD_before.nr, LD_before.nc, &LD_before, 0, 0, new_L, 0, 0);
      CopyBlock(LD_after.nr, LD_after.nc, &LD_after, 0, 0, \
		new_L, LD_before.nr, 0);
      *new_b = tmalloc(new_L->nr * sizeof(int));
      for(i = 0; i < LD_before.nr; i++) {
	(*new_b)[i] = old_b[i];
      }
      for(i = LD_before.nr; i < new_L->nr; i++) {
	(*new_b)[i] = CD[i - LD_before.nr];
      }
    }
    /* Update the parameters for next loop.*/
    pn_before = copypn(&pn_after);
    MAllocateMatrixType(&memory, 2, &LD_before, new_L->nr, new_L->nc);  
    CopyMatrix(new_L, &LD_before);
    old_b = *new_b;
    snodes_number = 0;
    uleaves_number = 0;
    sleaves_number = 0;
    curr_depth = 1;
    tree_depth = 1;
    getDepth(root, &curr_depth, &tree_depth);
    if(isRoot(root) == 0) {
      snodes_number = 1;
      sleaves_number = root->n;
    }
    else
      getDeepestNodeCount(root, &curr_depth, &tree_depth, &snodes_number, \
			  &sleaves_number);
    tree_structs = mmalloc(&memory, snodes_number * sizeof (expression2*));
    unique_leaves = mmalloc(&memory, sleaves_number * sizeof (inequality2*));
    find_subtrees(root, &tree_depth, tree_structs, &snodes_number, \
		  unique_leaves, &uleaves_number);
  }
  /* When the tree is updated so that it only constains an operator as a root,
     two cases will be distingished: the oprator is 'OR' or 'AND'.*/
  if(root->type == 1) {
    /* Get the constraints from unique_leaves.*/
    MAllocateMatrixType(&memory, 2, &L, uleaves_number, pn_before.pnum);
    b = mmalloc(&memory, pn_before.pnum * sizeof(int));
    LB = mmalloc(&memory, pn_before.pnum * sizeof(int));
    UB = mmalloc(&memory, pn_before.pnum * sizeof(int));
    for(i = 0; i < uleaves_number; i++) {
      vl = unique_leaves[i]->variable_list;
      while(vl) {
	SetMatrixEl(&L, i, vl->index, vl->coefficient);
	vl = vl->next;
      }
      b[i] = unique_leaves[i]->free_term;
      LB[i] = unique_leaves[i]->lb;
      UB[i] = unique_leaves[i]->ub;
    }
    /* Update the current PN and get the new set of constraints.*/
    MAllocateMatrixType(&memory, 2, &LD_after, 2 * L.nr, L.nc + L.nr);
    CD = mmalloc(&memory, 2 * L.nr * sizeof(int));
    convert_prop(&pn_before, &L, b, LB, UB, &LD_after, CD, &pn_after);
    /* find the additional constraints from the leaves.*/
    merged_prop = mmalloc(&memory, snodes_number * sizeof(inequality2));
    v = mmalloc(&memory, (pn_before.pnum + uleaves_number) * sizeof(variable));
    merged_prop[0] = merge_prop(tree_structs[0], unique_leaves, \
				uleaves_number, pn_before.pnum, v);
    /* update the set of constraits: new_L, new_b, new_plant*/
    AllocateMatrixType(2, new_L, LD_after.nr + LD_before.nr + 1, \
			LD_after.nc);  
    CopyBlock(LD_before.nr, LD_before.nc, &LD_before, 0, 0, new_L, 0, 0);
    CopyBlock(LD_after.nr, LD_after.nc, &LD_after, 0, 0, \
	      new_L, LD_before.nr, 0);
    vl = merged_prop[0].variable_list;
    for(i = 0; i < LD_after.nc; i++) {
      SetMatrixEl(new_L, LD_after.nr + LD_before.nr, i, vl->coefficient);
      vl = vl->next;
    }
    *new_b = tmalloc((new_L->nr + 1) * sizeof(int));
    for(i = 0; i < LD_before.nr; i++) {
      (*new_b)[i] = old_b[i];
    }
    for(i = LD_before.nr; i < new_L->nr - 1; i++) {
      (*new_b)[i] = CD[i - LD_before.nr];
    }
    (*new_b)[new_L->nr - 1] = merged_prop[0].free_term;
    *new_plant = copypn(&pn_after);
  }
  else {
    /* update the set of constraits: new_L, new_b, new_plant*/
    AllocateMatrixType(2, new_L, LD_before.nr + uleaves_number, \
			LD_before.nc);  
    CopyBlock(LD_before.nr, LD_before.nc, &LD_before, 0, 0, new_L, 0, 0);
    for(i = 0; i < uleaves_number; i++) {
      vl = unique_leaves[i]->variable_list;
      while(vl) {
	SetMatrixEl(new_L, LD_before.nr + i, vl->index, vl->coefficient);
	vl = vl->next;
      }
    }
    *new_b = tmalloc((new_L->nr + 1) * sizeof(int));
    for(i = 0; i < LD_before.nr; i++) {
      (*new_b)[i] = old_b[i];
    }
    for(i = 0; i < uleaves_number; i++) {
      (*new_b)[LD_before.nr + i] = unique_leaves[i]->free_term;
    }
    *new_plant = copypn(&pn_after);
  }
  deallocpn(&pn_before);
  deallocpn(&pn_after);
  FreeMemory(&memory);
  return 0;
}

/* Given a plant and a expression tree with dynamic interpretation, 
   CONVERT_LEAVES will convert the original tree and plant to the new tree and
   plant that can be used in CONSTRUCT_SPEC. All the leaves of the original 
   tree will be converted. The root of the new tree is unchanged.
   This function is a subroutine of tree2spec.*/
int convert_leaves(pns* plant1, pns* plant2, expression2 *root)
{
  int i;
  MemoryManager memory;
  int leaf_number;
  inequality2 *first_leaf, *current_leaf, **leaves;
  matrix L, H, L_star;
  int *C, *LB, *UB;
  int curr_leaf_found = 0;
  variable* vl;
  int vl_index;

  /* Get all the leaves of the original tree. Sort out the constraints.*/
  leaf_number = getLeafCount(root);
  first_leaf = getFirstLeaf(root);
  memory = CreateMemoryManager(20, 20, 0, 0);
  MAllocateMatrixType(&memory, 2, &L, leaf_number, plant1->pnum);
  MAllocateMatrixType(&memory, 2, &H, leaf_number, plant1->tnum);
  C = mmalloc(&memory, leaf_number * sizeof(int));
  LB = mmalloc(&memory, leaf_number * sizeof(int));
  UB = mmalloc(&memory, leaf_number * sizeof(int));
  current_leaf = first_leaf;
  for(i = 0; i < leaf_number; i++) {
    vl = current_leaf->variable_list;
    while(vl) {
      if(vl->type == MARKINGV)
	SetMatrixEl(&L, i, vl->index, vl->coefficient);
      else if (vl->type == FIRINGV)
	SetMatrixEl(&H, i, vl->index, vl->coefficient);
      vl = vl->next;
    }
    C[i] = current_leaf->free_term;
    LB[i] = current_leaf->lb;
    UB[i] = current_leaf->ub;
    curr_leaf_found = 0;
    current_leaf = getNextLeaf(root, current_leaf, &curr_leaf_found);
  }
  /* Convert the original constraints to new constraints and get the 
     corresponding plant.*/
  disq2disj(plant1, &L, &H, plant2, &L_star);
  /* Update the contents of the leaves in the original tree to new 
     constraints.*/
  current_leaf = first_leaf;
  for(i = 0; i < leaf_number; i++) {
    vl = current_leaf->variable_list;
    vl_index = 0;
    while(vl) {
      vl->type = MARKINGV;
      vl->index = vl_index++;
      vl->coefficient = GetMatrixEl(&L_star, i, vl->index);
      vl->pn = plant2;
      vl = vl->next;
    }
    curr_leaf_found = 0;
    current_leaf = getNextLeaf(root, current_leaf, &curr_leaf_found);
  }
  FreeMemory(&memory);
  return 0;
} 

/*Given a PN and set of constraints in state-based interpretation, 
  CONVERT_PROP will convert the current constraints to new constraints and 
  update the PN accordingly. This function is part of disj2normal.c*/
int convert_prop(pns* pn_before, matrix* L, int* b, \
		 int* LB, int* UB, matrix* LD, int* CD, pns* pn_after)
{
  int i, j, uniqueflag = 0;
  pns bin;
  pns pn_compose[L->nr+1];
  pns *plant;
  matrix D, l, ld, m0m;
  int* cd;
  int* m0;
  int label0[pn_before->in.nc];
  int c, lb, ub;
  MemoryManager memory;
  memory = CreateMemoryManager(15, 15, 0, 0);
  /* All the transitions in the plant are distinctively labeled from 1 to 
     plant.tnum.*/
  for(i = 0; i < pn_before->tnum; i++) {
    for(j = 0; j < i-1 ; j++) {
      if(pn_before->t[i].l == pn_before->t[j].l) {
	uniqueflag = 1;
	break;
      }
    }
  }
  if(uniqueflag) {
    for(i = 0; i < pn_before->tnum; i++) {
      pn_before->t[i].l = i + 1;
    }
  }
  /* get the new constraints and updated PN*/
  plant = pn_before;
  MAllocateMatrixType(&memory, 2, &D, plant->in.nr, plant->in.nc);
  SubtractMatrix(&plant->in, &plant->out, &D);
  for(i = 0; i < plant->in.nc; i++)
    label0[i] = plant->t[i].l;
  MAllocateMatrixType(&memory, 2, &ld, 2, L->nc + L->nr);
  cd = mmalloc(&memory, 2 * sizeof(int));
  MAllocateMatrixType(&memory, 2, &l, 1, L->nc);
  for(i = 0; i < L->nr; i++) {
    CopyBlock(1, L->nc, L, i, 0, &l, 0, 0);
    c = b[i];
    lb = LB[i];
    ub = UB[i];
    m0m = vector2matrix(plant->marking, plant->in.nr, 1);
    disj2pn(&bin, &ld, cd, &D, &m0m, label0, &l, c, lb, ub, i, L->nr);
    CopyBlock(2, L->nc + L->nr, &ld, 0, 0, LD, i * 2, 0);
    CD[2 * i] = cd[0];
    CD[2 * i + 1] = cd[1];
    if(i == 0)
      pn_compose[i+1] = composepn(plant, &bin);
    else
      pn_compose[i+1] = composepn(&pn_compose[i], &bin);
    deallocpn(&bin);
  }
  *pn_after = copypn(&pn_compose[L->nr]);
  FreeMemory(&memory);
  for(i = 1; i < L->nr+1; i++)
    deallocpn(&pn_compose[i]);
  return 0;
}

/* Given an expression tree, FIND_SUBTREES will find the parents and their 
   children that are the deepest leaves in the tree, returned by an array of 
   structs. Also, an array of leaves is returned, containting the same leaves 
   but with no repetitions. */
int find_subtrees(expression2* root, int* tree_depth, \
		  expression2 **tree_structs, int *snodes_number, \
		  inequality2 **unique_leaves, int *uleaves_number)
{
  int flag, ni = 0, i, j, k, curr_depth = 1;
  /* find the parents(nodes) in the deepest layer. */
  if(isRoot(root) == 0) 
    tree_structs[0] = root;
  else
    setTreeStructs(root, &curr_depth, tree_depth, tree_structs, &ni);
  /* sort out the unique leaves from the deepest leaves*/
  for(i = 0; i < *snodes_number; i++) {
    for(j = 0; j < tree_structs[i]->n; j++) {
      flag = 0;
      for(k = 0; k < *uleaves_number; k++)
	if (!cmpLeaf(tree_structs[i]->leaf[j], unique_leaves[k]))
	  flag = 1;
      if(!flag) unique_leaves[(*uleaves_number)++] = tree_structs[i]->leaf[j];
    }
  }
}

/* Given the root of an expression tree, get the number of nodes that do not
   have any successor node, and the number of their leaves.*/
void getDeepestNodeCount(expression2 *root, int *curr_depth, int* tree_depth, 
			 int *snodes_number, int *sleaves_number)
{
  int i;
  for (i = 0; i < root->n; i++) {
    if(root->successor[i]) {
      (*curr_depth)++;
      if(*curr_depth == *tree_depth) {
	(*snodes_number)++;
	*sleaves_number += root->successor[i]->n;
      }
      else
	getDeepestNodeCount(root->successor[i], curr_depth, tree_depth, \
			    snodes_number, sleaves_number);
      (*curr_depth)--;
    }
  }
}

/* Given the root of an expression tree, get the depth of the tree. Leaves are
   not considered.*/
void getDepth(expression2 *root, int *curr_depth, int *tree_depth)
{
  int i;
  for (i = 0; i < root->n; i++) {
    if(root->successor[i]) {
      (*curr_depth)++;
      if(*curr_depth > *tree_depth)
	*tree_depth = *curr_depth;
      getDepth(root->successor[i], curr_depth, tree_depth);
      (*curr_depth)--;
    }
  }
}

/* Given the root of an expression tree, return the first leaf of root if it 
   exists, otherwise return the first leaf of the first nodes.*/
inequality2* getFirstLeaf(expression2 *root)
{
  int i, sum = 0, expcount = 0;
  for (i = 0; i < root->n; i++) {
    if(root->leaf[i]) {
      return root->leaf[i];
    }
    else
      return getFirstLeaf(root->successor[i]);
  }
}

/* Given the root of an expression tree, return the total number of leaves.*/
int getLeafCount(expression2 *root)
{
  int i, sum = 0, expcount = 0;
  for (i = 0; i < root->n; i++) {
    if(root->successor[i]) {
      sum += getLeafCount(root->successor[i]);
    }
    else
      sum++;
  }
  return sum;
}

/* Given an expression tree and a leaf, return the next leaf on its right,
   which may not be under the same node. curr_leaf_found is used to mark 
   whether the leaf has been found.*/
inequality2* getNextLeaf(expression2 *root, inequality2* current_leaf, \
			 int *curr_leaf_found)
{
  int i;
  inequality2 tmp_leaf;
  inequality2 *lp = &tmp_leaf;
  for(i = 0; i < root->n; i++) {
    if(root->leaf[i]) {
      if (*curr_leaf_found == 0) {
	if (current_leaf == root->leaf[i]) {
	  *curr_leaf_found = 1;
	  continue;
	}
      }
      else {
	return root->leaf[i];
      }
    }
    else {
      lp = getNextLeaf(root->successor[i], current_leaf, curr_leaf_found);
      if(lp) return lp;
    }
  }
  return 0;
}

/* Return 0 if the root has no successor node.*/
int isRoot(expression2* root)
{
  int i, leaf_count = 0;
  for (i = 0; i < root->n; i++) {
    if(root->leaf[i]) {
      leaf_count++;
    }
  }
  if(leaf_count == root->n)
    return 0;
  else
    return 1;
}

/* With the information of struct containing the deepest subtrees and the 
   current PN, MERGE_PROP will construct the new propositions that can be 
   attached to the updated tree. 
   This function is a subroutine of construct_spec*/
inequality2 merge_prop(expression2 *tree_struct, inequality2 **unique_leaves,\
		       int leaves_num, int pnum, variable *v)
{
  int children_num, i, j, ub, lb, c;
  int incert_prop[leaves_num];
  inequality2 mp;
  /* set coefficients to -1 when identical leaves*/
  children_num = getLeafCount(tree_struct);
  for(i = 0; i < leaves_num; i++) 
    incert_prop[i] = 0;
  if(tree_struct->type == 0) {
    for(i = 0; i < leaves_num; i++) {
      for(j = 0; j < children_num; j++) {
	if (cmpLeaf(tree_struct->leaf[j], unique_leaves[i]) == 0)
	  incert_prop[i] = -1;
      }
    }
    ub = 0;
    lb = -children_num;
    c = -children_num;
  }
  else {
    for(i = 0; i < leaves_num; i++) {
      for(j = 0; j < children_num; j++) {
	if (cmpLeaf(tree_struct->leaf[j], unique_leaves[i]) == 0)
	  incert_prop[i] = -1;
      }
    }
    ub = 0;
    lb = -children_num;
    c = -1;
  }
  /* set parameters in the constraint*/
  mp.free_term = c;
  mp.lb = lb;
  mp.ub = ub;
  for(i = 0; i < pnum + leaves_num; i++) {
    v[i].type = MARKINGV;
    if(i < pnum)
      v[i].coefficient = 0;
    else
      v[i].coefficient = incert_prop[i - pnum];
    v[i].index = i;
    if (i == pnum + leaves_num - 1) 
      v[i].next = 0;
    else
      v[i].next = &v[i+1];
  }
  mp.variable_list = v;
  return mp;
}

/* Replace the node ts with a leaf mp in the expression tree*/
void node2leaf(expression2 *root, expression2* ts, inequality2* mp)
{
  int i;
  for (i = 0; i < root->n; i++) {
    if(root->successor[i]) {
      if(root->successor[i] == ts) {
	root->successor[i] = 0;
	root->leaf[i] = mp;
      }
      else
	node2leaf(root->successor[i], ts, mp);
    }
  }  
}

/* Given an expression tree, get the nodes in the deepest layer and store them
   in an array: tree_structs*/
void setTreeStructs(expression2 *root, int *curr_depth, int* tree_depth, \
		    expression2 **tree_structs, int *ni)
{
  int i;
  for (i = 0; i < root->n; i++) {
    if(root->successor[i]) {
      (*curr_depth)++;
      if(*curr_depth == *tree_depth) {
	tree_structs[(*ni)++] = root->successor[i];
      }
      else
	setTreeStructs(root->successor[i], curr_depth, tree_depth, \
		       tree_structs, ni);
      (*curr_depth)--;
    }
  }
}


int satisfied_expr(expression2 *expr) {
/* Returns 1 if the expression is satisfied at the initial marking. Otherwise,
   it returns 0. */
  int i, sum = 0, ft = 0;
  variable *vl;
  pns* p;
  for(i = 0; i < expr->n; i++) {
    if(expr->leaf[i]) { // inequality2
      vl = expr->leaf[i]->variable_list;
      ft = 0;
      while(vl) {
	// marking only. firing and Parikh vector assummed to be 0.
	if(vl->type == MARKINGV && vl->coefficient != 0)
	  ft += vl->coefficient * get_marking(vl->pn, vl->index);
	vl = vl->next;
      }
      if(ft <= expr->leaf[i]->free_term) sum++;
    }
    else {
      sum += satisfied_expr(expr->successor[i]);
    }
  }
  if(expr->type == 1 && sum != 0) return 1;  // OR
  else if(expr->type == 0 && sum == expr->n) return 1;  // AND
  else return 0;
}

