fml TwoFixedBox(fml A)
{
  return Box(Rel(ONE),Box(Rel(TWO),A));
}

 
fml TwoFixedPos(fml A)
{
  return Pos(Rel(ONE),Pos(Rel(TWO),A));
}


fml GenerateModalVariable(ident var)
{
  integer i,j;

  fml A[3],Qi,NQi;

  if (flag_Kenc) {
    Qi=TwoFixedPos(Var(ONE));
    for (j=1; j<var; j++)
      Qi=TwoFixedPos(Qi);
    A[2]=TwoFixedPos(And(WithFml(Not(Var(ONE)),WithFml(Qi,EMPTY_SEQUENT))));
  }
  else {
    for (i=0;i<2;i++) {
      Qi=TwoFixedPos(TwoFixedBox(Var(ONE)));
      for (j=1; j<var;j++)
	Qi=TwoFixedPos(And(WithFml(Var(ONE),
			    WithFml(TwoFixedPos(And(WithFml(Not(Var(ONE)),
					     WithFml(Qi,EMPTY_SEQUENT)))),
			    EMPTY_SEQUENT))));

      NQi=TwoFixedBox(TwoFixedPos(Not(Var(ONE))));
      for (j=1; j<=var;j++)
	NQi=TwoFixedBox(Or(WithFml(Not(Var(ONE)),
		       WithFml(TwoFixedBox(Or(WithFml(Var(ONE),
				       WithFml(NQi,EMPTY_SEQUENT)))),
		       EMPTY_SEQUENT))));
    
      A[i]=TwoFixedPos(And(WithFml(Qi,WithFml(NQi,EMPTY_SEQUENT))));
    }
    A[2]=And(WithFml(TwoFixedPos(A[0]),
	     WithFml(TwoFixedBox(Or(WithFml(Not(A[1]),
			     WithFml(TwoFixedPos(TwoFixedBox(Not(Var(ONE)))),
			     EMPTY_SEQUENT)))),
	     EMPTY_SEQUENT)));
  }
  return A[2];
}

prg ModalizePrg(prg);

fml ModalizeFml(fml A)
{
  sequent Asub;
  fml MA;

  if (A==NOT_EXISTS_FML) {
    fprintf(stderr,"\nERROR - Formula do not exists - ERROR\n");
    exit(1);
  }

  switch (A->op) {
  case UNKNOWN:
  case FALSE: 
  case TRUE:
    break;
  case VAR:
    MA=GenerateModalVariable(A->name);
    DeleteFml(A);
    A=MA;
    break;
  case NOT:
  case AND:
  case OR:
  case XOR:
  case EQUIV:
  case IMP:
    for (Asub=A->subfml; Asub!=EMPTY_SEQUENT; Asub = Asub->rest)
      Asub->first=ModalizeFml(Asub->first);
    break;
  case BOX:
  case POS:
    A->subprg->first=ModalizePrg(A->subprg->first);
    for (Asub=A->subfml; Asub!=EMPTY_SEQUENT; Asub = Asub->rest)
      Asub->first=ModalizeFml(Asub->first);
    break;
  }
  return A;
}


prg ModalizePrg(prg P)
{
  pool Psub;

  if (P==NOT_EXISTS_PRG) {
    fprintf(stderr,"\nERROR - Program does not exists - ERROR\n");
    exit(1);
  }

  switch (P->op) {
  case UNKNOWN:
  case REL:
    break;
  case INVERSE:
  case UNION:
  case SEQUENCE:
  case STAR:
    for (Psub=P->subprg; Psub!=EMPTY_POOL; Psub = Psub->rest)
      Psub->first=ModalizePrg(Psub->first);
    break;
  case TEST:
    P->subfml->first=ModalizeFml(P->subfml->first);
    break;

  }
  return P;
}


sequent ModalizeFormulae(sequent S)
{
  sequent NS;
  
  for (NS=S;NS!=EMPTY_SEQUENT;NS=NS->rest)
    NS->first=ModalizeFml(NS->first);

  return S;
}