/*
 *  Copyright (C) 2003
 *  Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
 *
 *  This program is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU General Public License
 *  as published by the Free Software Foundation; either version 2
 *  of the License, or (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
 *
 ------------------------------------------------------------------------------
 Compiling and using the program:
  
   1. Uncompress the lbtt sources (version >= 1.0.0, available at
      <http://www.tcs.hut.fi/Software/lbtt/releases>) into a directory
      (${LBTT_DIR} in the following) and run the `configure' script as
      detailed in the instructions.
  
   2. Compile this file with the command

        c++ -I${LBTT_DIR} -I${LBTT_DIR}/src test-distribution.cc \
          ${LBTT_DIR}/src/BitArray.cc $LBTT_DIR/src/FormulaRandomizer.cc \
          ${LBTT_DIR}/src/LtlFormula.cc -o test-distribution

      to produce an executable file `test-distribution' (replace `c++' with
      the name of an appropriate C++ compiler if necessary).

   3. Run the produced executable:

        ./test-distribution
             [formula size]
             [sum of the relative priorities of all unary operators]
             [sum of the relative priorities of all binary operators]
             [common absolute priority of all unary operators]
             [common absolute priority of all binary operators]
             [number of formulas]
             [random seed]

      (The number of formulas and the random seed need not be specified.
      Their default values are 1000000 and 0, respectively.)

      The common absolute priority of unary/binary operators can be
      calculated by dividing the absolute priority of an operator by its
      relative priority.

      The program generates [number of formulas] random formulas and then
      displays the actual operator distribution.
 ------------------------------------------------------------------------------
 */

#include <climits>
#include <cmath>
#include <cstring>
#include <iostream>
#include <map>
#include "Alloc.h"
#include "FormulaRandomizer.h"
#include "LtlFormula.h"
#include "Random.h"

bool user_break;

using namespace Ltl;

enum { NOT = 0, NEXT, FINALLY, GLOBALLY, AND, OR, IMPLY, EQUIV, XOR, UNTIL,
       WEAK_UNTIL, RELEASE, STRONG_RELEASE, BEFORE };

int indexToLtlSymbol(int sym)
{
  switch (sym)
  {
    case 0 : return LTL_NEGATION;
    case 1 : return LTL_NEXT;
    case 2 : return LTL_FINALLY;
    case 3 : return LTL_GLOBALLY;
    case 4 : return LTL_CONJUNCTION;
    case 5 : return LTL_DISJUNCTION;
    case 6 : return LTL_IMPLICATION;
    case 7 : return LTL_EQUIVALENCE;
    case 8 : return LTL_XOR;
    case 9 : return LTL_UNTIL;
    case 10 : return LTL_WEAK_UNTIL;
    case 11 : return LTL_V;
    case 12 : return LTL_STRONG_RELEASE;
    default : return LTL_BEFORE;
  }
}

int main(int argc, char* argv[])
{
  if (argc < 6 || argc > 8)
  {
    cerr << "Usage: "
	 << argv[0] 
	 << " [formula size] [sum of relative priorities for unary ops] "
            "[sum of relative priorities for binary ops] [unary priority] "
            "[binary priority] [number of formulas] [random seed]"
	 << endl;
    exit(0);
  }

  int formula_size = atoi(argv[1]);
  int number_of_unary_ops = atoi(argv[2]);
  int number_of_binary_ops = atoi(argv[3]);
  int unary_priority = atoi(argv[4]);
  int binary_priority = atoi(argv[5]);
  int number_of_formulas;
  int seed;

  if (argc >= 7)
    number_of_formulas = atoi(argv[6]);
  else
    number_of_formulas = 1000000;

  if (argc == 8)
    seed = atoi(argv[7]);
  else
    seed = 0;

  SRAND(seed);

  if (formula_size <= 0 || number_of_unary_ops < 0 || number_of_binary_ops < 0
      || (number_of_unary_ops == 0)
      || (number_of_unary_ops > 0 && unary_priority <= 0)
      || (number_of_binary_ops > 0 && binary_priority <= 0)
      || number_of_formulas <= 0)
  {
    cerr << argv[0] << ": error in command line parameters" << endl;
    exit(1);
  }

  int pri[14];
  for (int i = 0; i < 14; i++)
    pri[i] = 0;

  cout << "Formula size: " << formula_size << endl
       << "Sum of relative priorities of unary operators: "
       << number_of_unary_ops << endl
       << "Sum of relative priorities of binary operators: "
       << number_of_binary_ops << endl
       << "Formulas to generate: " << number_of_formulas << endl
       << "Random seed: " << seed << endl;

  for (int i = 0; i < number_of_unary_ops; i++)
    pri[i % 4] += unary_priority;
  for (int i = 0; i < number_of_binary_ops; i++)
    pri[(i % 10) + 4] += binary_priority;

  cout << "Expected relative distribution:" << endl;
  for (int i = 0; i < 14; i++)
  {
    if (pri[i] > 0)
      cout << "  "
	   << (i < 4 ? "Unary operator" : "Binary operator")
	   << ' '
	   << (i < 4 ? i + 1 : i - 3)
	   << ": "
	   << (i < 4 ? " " : "")
	   << pri[i] / (i < 4 ? unary_priority : binary_priority)
	   << endl;
  }

  FormulaRandomizer formula_randomizer;
  formula_randomizer.number_of_available_variables = 1;
  formula_randomizer.size = formula_randomizer.max_size = formula_size;
  formula_randomizer.useSymbol(LTL_ATOM, 1);
  formula_randomizer.useShortOperator(LTL_NEGATION, pri[NOT]);
  formula_randomizer.useShortOperator(LTL_NEXT, pri[NEXT]);
  formula_randomizer.useShortOperator(LTL_FINALLY, pri[FINALLY]);
  formula_randomizer.useShortOperator(LTL_GLOBALLY, pri[GLOBALLY]);
  formula_randomizer.useLongOperator(LTL_NEGATION, pri[NOT]);
  formula_randomizer.useLongOperator(LTL_NEXT, pri[NEXT]);
  formula_randomizer.useLongOperator(LTL_FINALLY, pri[FINALLY]);
  formula_randomizer.useLongOperator(LTL_GLOBALLY, pri[GLOBALLY]);
  formula_randomizer.useLongOperator(LTL_CONJUNCTION, pri[AND]);
  formula_randomizer.useLongOperator(LTL_DISJUNCTION, pri[OR]);
  formula_randomizer.useLongOperator(LTL_IMPLICATION, pri[IMPLY]);
  formula_randomizer.useLongOperator(LTL_EQUIVALENCE, pri[EQUIV]);
  formula_randomizer.useLongOperator(LTL_XOR, pri[XOR]);
  formula_randomizer.useLongOperator(LTL_UNTIL, pri[UNTIL]);
  formula_randomizer.useLongOperator(LTL_WEAK_UNTIL, pri[WEAK_UNTIL]);
  formula_randomizer.useLongOperator(LTL_V, pri[RELEASE]);
  formula_randomizer.useLongOperator(LTL_STRONG_RELEASE, pri[STRONG_RELEASE]);
  formula_randomizer.useLongOperator(LTL_BEFORE, pri[BEFORE]);

  cout << "Generating random formulas ["
       << string(40, ' ')
       << ']'
       << string(41, '\b');
  cout.flush();

  double progress = 0.0;
  double progress_step = 40.0 / static_cast<double>(number_of_formulas);
  int progress_indicator = 0;

  LtlFormula* f;
  for (int i = 0; i < number_of_formulas; i++)
  {
    progress = progress_step * i;
    if (static_cast<int>(progress) > progress_indicator)
    {
      while (static_cast<int>(progress) > progress_indicator
	     && progress_indicator < 40)
      {
	cout << '.';
	++progress_indicator;
      }
      cout.flush();
    }

    f = formula_randomizer.generate();
    LtlFormula::destruct(f);
  }

  while (progress_indicator < 40)
  {
    cout << '.';
    ++progress_indicator;
  }
  cout << endl;

  typedef const map<int, unsigned long int, less<int>,
                    ALLOC(unsigned long int) >
    Statistics;

  Statistics& stats(formula_randomizer.symbolStatistics());

  cout << "Actual distribution:" << endl;

  unsigned long long int total = 0;
  for (Statistics::const_iterator s = stats.begin(); s != stats.end(); ++s)
  {
    if (s->first != LTL_ATOM)
      total += s->second;
  }

  double unit = static_cast<double>(total)
                  / static_cast<double>
                      (number_of_unary_ops + number_of_binary_ops);

  double max_error = 0.0;

  cout << "  Unit: " << unit << endl;

  for (int i = 0; i < 14; i++)
  {
    if (pri[i] > 0)
    {
      double ratio = static_cast<double>
 	               (stats.find(indexToLtlSymbol(i))->second) / unit;

      cout << "  "
	   << (i < 4 ? "Unary operator" : "Binary operator")
	   << ' '
	   << (i < 4 ? i + 1 : i - 3)
	   << ": "
	   << (i < 4 ? " " : "")
	   << stats.find(indexToLtlSymbol(i))->second << " ("
	   << ratio
	   << " units)" << endl;

      unsigned long int pr = pri[i] / (i < 4
				       ? unary_priority
				       : binary_priority);

      if (abs(static_cast<double>(pr) - ratio) > max_error)
	max_error = abs(static_cast<double>(pr) - ratio);
    }
  }

  cout << "  Maximum absolute deviation from expected distribution: "
       << max_error
       << " units"
       << endl;

  exit(0);
}