/******* BENCHMARK GENERATION ******/

fml GenerateModalClause(integer depth);

fml GenerateModalLiteral(integer depth)
{
  fml L;

  if (depth>0 && Random01(ProbModal))
    L=Box(Rel(ONE),GenerateModalClause(depth-1));
  else 
    L=Var(Random1To(MaxVariables));

  if (Random01(ProbNegated)) 
    L=Not(L);

  return L;
}

fml GenerateModalClause(integer depth)
{
  sequent C;
  fml L;
  integer num_literals,failed_literals;

  C=EMPTY_SEQUENT;
  num_literals=0;
  failed_literals=0;
  while (num_literals<MaxLiterals) {
    L=GenerateModalLiteral(depth);
    if (!flag_test) {
      num_literals++;
      C=AddFml(L,C);
      failed_literals=0;
    }
    else if (!FindTwinFml(L,C,EqualFml) && !FindTwinFml(L,C,NegateFml)) {
      num_literals++;
      C=WithFml(L,C);
      failed_literals=0;
    }
    else {
      DeleteFml(L);
      failed_literals++;
      if (failed_literals>MaxFailures) {
	fprintf(stderr,"\n WARNING - Too many failures - WARNING \n");
	fprintf(stderr,"There might not be enough different formulae\n");
	fprintf(stderr,"With these parameters\n");
	exit(1);
      }
    }
  }

  return Or(C);
}


sequent GenerateFormulae()
{
  sequent S;
  fml A;  
  integer num_clauses,failed_clauses;

  S=EMPTY_SEQUENT;
  failed_clauses=0;
  num_clauses=0;
  while (num_clauses<MaxClauses) {
    failed_clauses++;
    A=GenerateModalClause(MaxDepth);
    if (!flag_test || !FindTwinFml(A,S,EqualFml)) {
      num_clauses++;
      failed_clauses=0;
      S=WithFml(A,S);
    }
    else {
      failed_clauses++;
      DeleteFml(A);
      if (failed_clauses>MaxFailures) {
	fprintf(stderr,"\n WARNING - Too many failures - WARNING \n");
	fprintf(stderr,"There might not be enough different formulae\n");
	fprintf(stderr,"With these parameters\n");
	exit(1);
      }
    }
  }
  return S;
}