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

fml GenerateModalLiteral(integer depth)
{
  fml L;
  integer i;

  L=Var(Random1To(MaxVariables));
  if (Random01(ProbNegated)) 
    L=Not(L);
  
  for (i=0;i<depth;i++)
    L=Box(Rel(ONE),L);

  return L;
}


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

  C=EMPTY_SEQUENT;
  num_literals=0;
  failed_literals=0;
  while (num_literals<MaxLiterals) {
    if (num_literals==0)
      L=GenerateModalLiteral(0);
    else if (num_literals==1)
      L=GenerateModalLiteral(depth);
    else
      L=GenerateModalLiteral(Random1To(depth+1)-1);
    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=GeneratePeriodicClause(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;
}