//---------------------------------------------------------------------------
#include <stdio.h>  // printf
#include <stdlib.h> // atoi, random
#include <string.h>
#include <time.h>
#include <sys\timeb.h>
#include <sys\types.h>
#include <sys\stat.h>
#include <math.h>

#include "tboolfnct.h"
#include "boom.h"
#include "tpfnct.h"

#define POCET_POKUSU_OUTPUT 1
#define DELKA_NAZVU_STAVU 16
#define VYPIS_CASU
//#define LADICI_HLASENI
//#define LADICI_HLASENI2
//#define VYPIS_TERMU
//#define VYPIS_CHYBEJICICH_TERMU
//#define VYPIS_GRAFU_STAVU
//#define VYPIS_TERMU_NA_STAV
#define random(n)	(rand()%(n))

//---------------------------------------------------------------------------




class THash_Polozka
{
public:
  TPfnct * fnct;                // Budu pouzivat Tpfcnt fyzicky z TBoolfcnt kvuli mistu.
  THash_Polozka * next;
  THash_Polozka();
private:
};


class THash_Seznam_Polozek
{
public:
  THash_Seznam_Polozek* next;
  long index;  // index do Thash_Tabulka->tabulka[]  -- kvuli DeleteTerm. pokud budem mazat prvni, tak abychom mohli zmenit primo tabulka[]
  THash_Seznam_Polozek();
  ~THash_Seznam_Polozek();
};


class THash_Tabulka
{
public:
  long pocet;
  int bitu;
  long polozek;

private:
  THash_Polozka **tabulka;
  void Push(TPfnct * ff,long kam);
  TBoolFnct *parent;
  void AddItemPrivate(TPfnct * ff, int pozice, long kam);
  THash_Seznam_Polozek* Vrat_SeznamPrivate(TPfnct * ff,THash_Seznam_Polozek* pol, int pozice,long kde);  // Vrati ukazatel na seznam kam (by patril)/patri term ff.

public:
  THash_Tabulka(int bits,TBoolFnct *parent);
  ~THash_Tabulka();
  THash_Polozka* VratPolozkuZTabulky(long index);
  void THash_Tabulka::UlozPolozkuDoTabulky(THash_Polozka *pol,long index);
  void AddItem(TPfnct * ff);
  THash_Seznam_Polozek* Vrat_Seznam(TPfnct * ff);  // Vrati ukazatel na seznam kam (by patril)/patri term ff.
  void DeleteTerm(TPfnct *ff);
  void Print();
};


class GenerateInfo
{
public:
  int bits;
  char *onmpla;
  char *onminf;
  int iv;
  int ov;
  int t;
  int mask;
  int type;  // 0 fd 1 fr
  double idc;      // prumerny
  double odc;
  double idt;
  double odt;
  double sidc;     // prvni term
  double sodc;
  double sidt;
  double sodt;
  double glidc;    // posledni term
  double glodc;
  double glidt;
  double glodt;
  int filt;
  int dupl;
  int timeout;
  int pocet_output;   // pocet navic opakovanych zkousek outputu pri generovani
  THash_Tabulka *hashtab;
  TBoolFnct *fn;
  int *tab;   // tabulka s idc,idt,idf,odc,odt,odf pro kazdy term. Pro pocitani granularity.
  GenerateInfo(int terms);
  ~GenerateInfo();
};

class Tuzel
{
  public:
  int cislo;
  Tuzel *next;
};

class TPrechod
{
  public:
  int src;
  int dst;
  float vaha;
  TPrechod *next;

};


class StateInfo
{
public:
  int origpocet;                        // kolik stavu
  int pocet;                            // kolik trid ekvivalence
  int inpvars;
  int outvars;
  int reset;
  int dosazitelnost;
  int spojitost;
  int koncovost;
  int terms;
  int termakt;
  int deterministic;
  int full;
  int pseudo;
  int deadlock;

  int *trida_uzlu;
  Tuzel *uzly;
  TPrechod *hrany;

  int *trida_ekviv;                     // do jake tridy bude stav [i] lezet
  int **seznm_ekviv;                    // seznam stavu ve tride [i]
  int *pocet_ekviv;                     // pocet stavu v tride [i]
  char **names;                         // nazev stavu [i]
  int *pocet_termu_na_ekviv;            // pole s pocet termu na 1 ekvivalentni stav
  TPrechod **prechody;                   // seznam predtvorenych hran.
  int *pprechodu;                       // kolik vede hran z jednotlivych trid ekvivalenci
  int *zprechodu;                       // kolik vede hran do jednotlivych trid ekvivalenci
  int SaveFnctAsKISS2(char * filn);
  void Dodelej_ekviv_stavy();            // Okopiruje termy z tridy ekvivalence pro vsechny souvisejici stavy
                                        // a premeni cilove prechody na nahodny stav z dane tridy ekvivalence
  void Dodelej_pseudo_stavy();            // Doplni pseudo stavy
  TPfnct **fnct_array;                  // pole ukazatelu na termy odpovidajici kazdemu stavu
  void Init(GenerateInfo * gi);                          // Inicializuje a predpocita vsechny nalezitosti ( spojitost, atd...)
  void Dopln_Stavy(GenerateInfo * gi,int state);
                                        // Doplni k vygenerovanym termum odpovidajici tridy ekvivalence podle prepripravenych hran, zbyle nahodne...
  void Zarad_do_seznamu_hran(TPrechod *hr); // zaradi hranu na spravne misto zarazaeneho seznamu hrany
  void Print_termy_na_ekviv();
  void Print_graf_ekviv();
  StateInfo();
  ~StateInfo();
};

void StateInfo::Print_termy_na_ekviv() {
	int i;
	for (i=0;i<this->pocet;i++) {
		printf("%2d - %2d | ",i,this->pocet_termu_na_ekviv[i]);
	}
	printf("\n");
}

void StateInfo::Print_graf_ekviv() {
	TPrechod *hr;
	int i;
	for (i=0;i<this->pocet;i++) {
		printf("%2d ->",i);
		hr = this->prechody[i];
		while (hr!=NULL) {
			printf("%2d,",hr->dst);
			hr=hr->next;
		}
		printf("\n");
	}
	
}

void StateInfo::Zarad_do_seznamu_hran(TPrechod *hr)
{
    TPrechod * tmp,*tmp2;
    if (this->hrany==NULL) {
      this->hrany=hr;
      hr->next=NULL;
      return;
      }
    tmp2 = NULL;
    tmp = this->hrany;
    while ((tmp!=NULL) && (tmp->vaha < hr->vaha)) {
      tmp2 = tmp;
      tmp=tmp->next;
      }
    if (tmp2==NULL) {
      this->hrany = hr;
      hr->next=tmp;
      }
    else {
      tmp2->next = hr;
      hr->next = tmp;
      }
}



void StateInfo::Dodelej_ekviv_stavy(void)
{
    int i;
    TPfnct *fnct2,*fnct4;
    for (i=this->pocet;i<this->origpocet;++i) {
      fnct4 = this->fnct_array[i]= new TPfnct;
      fnct2 = this->fnct_array[this->trida_ekviv[i]];
      while (fnct2 != NULL) {
        *fnct4 = *fnct2;
        fnct4->tmp = i;
        fnct4->tmp2 = fnct2->tmp2;
        fnct4->tmp2 = this->seznm_ekviv[fnct4->tmp2][random(this->pocet_ekviv[fnct4->tmp2])];
        fnct2 = fnct2->next;
        if (fnct2!= NULL) {
          fnct4->next = new TPfnct;
          fnct4=fnct4->next;
        }
        else fnct4->next = NULL;
      }
    }
    for (i=0;i<this->pocet;++i) {		// prepisem nahodne stavy jakymkoliv jinym z ekvivalentnich.
      fnct2=this->fnct_array[i];
      while (fnct2 != NULL) {
        fnct2->tmp2 = this->seznm_ekviv[fnct2->tmp2][random(this->pocet_ekviv[fnct2->tmp2])];
        fnct2=fnct2->next;
      }
    }




}

void StateInfo::Dodelej_pseudo_stavy(void) {
  int i,v;
  TPfnct *ff;
  if (this->fnct_array != NULL)
    for (i=0;i<this->origpocet;++i) {
      ff = this->fnct_array[i];
      while ( ff != NULL ) {
		v=random(100);
		if (v < this->pseudo) ff->tmp2 = this->origpocet;
	    ff = ff->next;
      }
    }
}

void StateInfo::Dopln_Stavy(GenerateInfo * gi,int state)
{
  TPfnct * fnct2;
  TPrechod * temp;
  fnct2 = this->fnct_array[state]= gi->fn->fnct;
  gi->fn->fnct = NULL;
  temp=this->prechody[state];
  while (fnct2 != NULL) {
        fnct2->tmp = state;
        if (temp == NULL) fnct2->tmp2 = random(this->pocet);
        else {
            fnct2->tmp2 = temp->dst;
            temp=temp->next;
        }
        fnct2=fnct2->next;
  }
}


void StateInfo::Init(GenerateInfo * gi)
{

  int i,z,j,k,x,y;
  TPrechod *tmp,*tmp2;
  Tuzel *tp;
	long int zmax = (long int) pow((double)2,gi->iv);
  if (this->pocet == -1) this->pocet = this->origpocet;

  this->trida_ekviv = (int *) malloc(sizeof(int) * this->origpocet);		// do jake tridyu ekvivalence stav i patri
  this->pocet_ekviv = (int *) malloc(sizeof(int) * this->pocet);			// kolik ma ekviv trida i ekviv stavu
  this->pocet_termu_na_ekviv = (int *) malloc(sizeof(int) * this->pocet);	// kolik ma ekviv trida i termu
  this->pprechodu = (int *) malloc(sizeof(int) * this->pocet);
  this->zprechodu = (int *) malloc(sizeof(int) * this->pocet);
  this->prechody = (TPrechod * *) malloc(sizeof(TPrechod *) * this->pocet);
  this->fnct_array = (TPfnct * *) malloc(sizeof(TPfnct *) * this->origpocet);
  this->seznm_ekviv = (int * *) malloc(sizeof(int *) * this->pocet);

  // alokace a pojmenovani stavu
  this->names = (char * *) malloc(sizeof(char *) * (this->origpocet+1));	
  for (i=0;i< this->origpocet+1;++i) {
        this->fnct_array[i] = NULL;
		this->names[i] = (char *) malloc(sizeof(char) * DELKA_NAZVU_STAVU);
        sprintf( this->names[i], "state%i", i);
  }
  sprintf( this->names[this->origpocet], "*");
  if (reset) {
    sprintf( this->names[0], "RESET");
    sprintf( this->names[this->origpocet], "  *  ");
  }
  else sprintf( this->names[0], "START");

// resime do jake tridy ekvivalence budou stavy nalezet a pocitame kolik stavu v dane tride;

  for (i=0;i< this->pocet;++i) {
        this->prechody[i]=NULL;
        this->pprechodu[i]=0;
        this->zprechodu[i]=0;
        this->pocet_termu_na_ekviv[i] = 0;
        this->trida_ekviv[i] = i;
        this->pocet_ekviv[i] = 1;
  }
  for (i=this->pocet;i<this->origpocet;++i) {
		z = random(this->pocet);
        this->trida_ekviv[i]=z;
        this->pocet_ekviv[z]++;
  }

// zaalokujeme seznam ekvivalentnich stavu a vynulujemem pocet- pouzijeme jako polu zarazek pri vyplnovani
  for (i=0;i< this->pocet;++i) {
        this->seznm_ekviv[i] = (int *) malloc(sizeof(int) * this->pocet_ekviv[i]);
        this->pocet_ekviv[i] = 0;
  }
// vyplnime seznam ekvivalentnich stavu
  for (i=0;i<this->origpocet;++i) {
        z=this->trida_ekviv[i];
        this->seznm_ekviv[z][this->pocet_ekviv[z]++] = i;
  }


// spojitost dosazitelnost a koncovost resime na tridach ekvivalence.... a rovnou pocitame termakt..
// nahodna spojitost pres kostru. Z kazdeho uzlu sqrt(n)+1 orient hran do ostatnich (1 z toho bud do
// nasledujiciho nebo do uzlu s vetsim cislem) s nahodnou vahou a pak primuv alg na kostru...
  if (this->spojitost == 1) {
    this->trida_uzlu = (int *) malloc(sizeof(int) * this->pocet);
    this->uzly = (Tuzel * ) malloc(sizeof(Tuzel) * this->pocet);
    k = (int) ceil(sqrt((float)this->pocet));
    this->trida_uzlu = (int *) malloc(sizeof(int) * this->pocet);
    this->uzly = (Tuzel * ) malloc(sizeof(Tuzel) * this->pocet);
    k = (int) ceil(sqrt((float)this->pocet));
    for (i=0;i< this->pocet;++i) {
        this->trida_uzlu[i] = i;
        this->uzly[i].cislo = i;
        this->uzly[i].next = NULL;
        tmp = new TPrechod;
        tmp->src = i;
        if (i==this->pocet-1) tmp->dst=(random(this->pocet-1)); // pokud zdrojova hrana zacina na poslednim tak nahodnej jinej
        else {
          if (random(2)) tmp->dst = i+1;                // 50% nasledujici
          else tmp->dst = random(this->pocet-i-1)+i+1;         // 50% nahodny vyssi
          }
        if (tmp->dst >= this->pocet) tmp->dst= this->pocet-1;		// nemelo by nastat..
        tmp->vaha=(float) rand();
        this->Zarad_do_seznamu_hran(tmp);		// zarazujeme 1 hranu ktera je vzdy na na vyssi stav.. - zarucime spojitost..
        for ( j=0;j<k;++j) {					// dalsi hrany dodelavame nahodne na kterykoliv jiny stav.
          tmp = new TPrechod;
          tmp->src = i;
          z=random(this->pocet-1);
          tmp->dst = i<=z?z+1:z;
          if (tmp->dst >= this->pocet) tmp->dst= this->pocet-1;		// nemelo by nastat.
          tmp->vaha = (float) rand();
          this->Zarad_do_seznamu_hran(tmp);
        }
    }

    // mame pripraveny hrany.. ted jen predelat ty tridy uzlu... (spojime vsechny disjunktni skupiny do jedne) - vytvorime kostru)
    i =1;
    tmp = this->hrany;
    while (i<this->pocet) {
        if (this->trida_uzlu[tmp->src] != this->trida_uzlu[tmp->dst]) {
            // rozdilna trida spojujeme tridu a pridavame hranu do prechody,upravime pprechod zprechod
            i++;
            this->pprechodu[tmp->src]++;
            this->zprechodu[tmp->dst]++;
            this->pocet_termu_na_ekviv[tmp->src]++;
            this->termakt += this->pocet_ekviv[tmp->src];
            tmp2=new TPrechod;
            tmp2->src = tmp->src;
            tmp2->dst = tmp->dst;
            tmp2->vaha = tmp->vaha;
            tmp2->next = this->prechody[tmp2->src];
            this->prechody[tmp2->src] = tmp2;
            // spojime tridy
            x = tmp->src<tmp->dst?tmp->src:tmp->dst;  // mensi cislo
            y = tmp->src<tmp->dst?tmp->dst:tmp->src;  // vesti cislo
            k = this->trida_uzlu[x];
            z = this->trida_uzlu[y]; // trida uzlu vyssiho
            tp = &this->uzly[x];
            while (tp->next != NULL) tp=tp->next;  // dojedeme
            tp->next=&this->uzly[z];
            tp=tp->next;
            while( tp!=NULL) {
                this->trida_uzlu[tp->cislo]=k;
                tp=tp->next;
                }
            }
        tmp=tmp->next;

    }  // konec prolejzani hran

    tmp=this->hrany;
    while (tmp != NULL) {
      tmp2=tmp->next;
      delete tmp;
      tmp=tmp2;
    }
    delete[] this->uzly;
    delete[] this->trida_uzlu;

  } // konec spojitosti
#ifdef VYPIS_GRAFU_STAVU
	printf("Mame spojitost skupin\n");
  this->Print_graf_ekviv();
#endif
#ifdef VYPIS_TERMU_NA_STAV
	this->Print_termy_na_ekviv();
#endif

  if (this->dosazitelnost == 1) { // res aby do kazdeho stavu vedla alespon jedna hrana , ne sama od sebe
    for (i=0;i<this->pocet;++i) {
      if (this->zprechodu[i]==0) {
        tmp = new TPrechod;
        z=random(this->pocet-1);
        tmp->src = i<=z?z+1:z;
        if (tmp->src >= this->pocet) tmp->src= this->pocet-1;
        tmp->dst = i;
        tmp->vaha =(float) rand();
        this->pprechodu[tmp->src]++;
        this->zprechodu[tmp->dst]++;
        this->pocet_termu_na_ekviv[tmp->src]++;
        this->termakt += this->pocet_ekviv[tmp->src];

        tmp->next = this->prechody[tmp->src];
        this->prechody[tmp->src] = tmp;
      };
    }
  }
#ifdef VYPIS_GRAFU_STAVU
	printf("Mame dosazitelnost\n");	
  this->Print_graf_ekviv();
#endif
#ifdef VYPIS_TERMU_NA_STAV
	this->Print_termy_na_ekviv();
#endif

  if (this->koncovost == 1) { // z kazdeho musi vest alespon 1 hrana ne do sebe.
    for (i=0;i<this->pocet;++i) {
      if (this->pprechodu[i]==0) {
        tmp = new TPrechod;

        z=random(this->pocet-1);
        tmp->dst = i<=z?z+1:z;
        if (tmp->dst >= this->pocet) tmp->dst= this->pocet-1;
        tmp->src = i;
        tmp->vaha =(float) rand();
        this->pprechodu[tmp->src]++;
        this->zprechodu[tmp->dst]++;
        this->pocet_termu_na_ekviv[tmp->src]++;
        this->termakt += this->pocet_ekviv[tmp->src];

        tmp->next = this->prechody[tmp->src];
        this->prechody[tmp->src] = tmp;
      };
    }
  }	// konec koncovosti
#ifdef VYPIS_GRAFU_STAVU
  printf("Mame koncovost\n");
  this->Print_graf_ekviv();
#endif
#ifdef VYPIS_TERMU_NA_STAV
	this->Print_termy_na_ekviv();
#endif

	// jeste zarucime ze ze startu vede alespon 1 hrana nekam jinam nez na sebe.
  if (this->pprechodu[0] == 0) {
      tmp = new TPrechod;
	  tmp->src = 0;
      z=random(this->pocet-1)+1;
      tmp->dst = z;
      tmp->vaha =(float) rand();
      this->pprechodu[tmp->src]++;
      this->zprechodu[tmp->dst]++;
      this->termakt += this->pocet_ekviv[tmp->src];
      this->pocet_termu_na_ekviv[tmp->src]++;
      tmp->next = this->prechody[tmp->src];
      this->prechody[tmp->src] = tmp;
  }
  else {
	  tmp = this->prechody[0];
	  while ((tmp != NULL) && (tmp->dst == 0)) tmp=tmp->next;
	  if (tmp==NULL) {
        tmp = new TPrechod;
        tmp->src = 0;
        z=random(this->pocet-1)+1;
        tmp->dst = z;
        tmp->vaha =(float) rand();
        this->pprechodu[tmp->src]++;
        this->zprechodu[tmp->dst]++;
        this->termakt += this->pocet_ekviv[tmp->src];
        this->pocet_termu_na_ekviv[tmp->src]++;
        tmp->next = this->prechody[tmp->src];
        this->prechody[tmp->src] = tmp;
	  }
  }

#ifdef VYPIS_GRAFU_STAVU
	printf("Mame minimalni splnenej graf\n");
  this->Print_graf_ekviv();
#endif
#ifdef VYPIS_TERMU_NA_STAV
	this->Print_termy_na_ekviv();
#endif






// pripravime tabulku s poctem termu na vsechny tridy ekvivalence.
	if (this->full) {
		for (i=0;i<this->pocet;++i) {
			this->pocet_termu_na_ekviv[i]=zmax;
		}
	}
	else{			
	  while (this->termakt<this->terms) {
		z = random(this->pocet);
        if (this->pocet_termu_na_ekviv[z]>=zmax) continue;
		this->pocet_termu_na_ekviv[z]++;
        this->termakt += this->pocet_ekviv[z];

#ifdef VYPIS_TERMU_NA_STAV
	this->Print_termy_na_ekviv();
#endif

	  }
	  if (this->termakt<this->terms) this->terms=this->termakt;
	}
	for (i=0;i<this->pocet;++i) {
		if (this->pocet_termu_na_ekviv[i]>zmax) { this->deadlock=1; break; }
	}
}

StateInfo::StateInfo()
{
  this->origpocet = -1;
  this->deterministic = 1;
  this->pocet = -1;
  this->inpvars = -1;
  this->outvars = -1;
  this->terms = -1;
  this->termakt = 0;
  this->reset = 0;
  this->spojitost = 1;
  this->dosazitelnost = 1;
  this->koncovost = 1;
  this->fnct_array = NULL;
  this->trida_ekviv = NULL;
  this->seznm_ekviv = NULL;
  this->pocet_ekviv = NULL;
  this->names = NULL;
  this->pocet_termu_na_ekviv = NULL;
  this->prechody = NULL;
  this->pprechodu = NULL;
  this->trida_uzlu = NULL;
  this->uzly = NULL;
  this->hrany = NULL;
  this->full = 0;
  this->pseudo = 0;
  this->deadlock=0;
}

StateInfo::~StateInfo()
{
  TPfnct * fnct2,*fnct3;
  TPrechod * temp;
  int i;
  if (this->fnct_array != NULL)
    for (i=0;i<this->origpocet;++i) {
      fnct2=this->fnct_array[i];
      while ( fnct2 != NULL ) {
        delete[] fnct2->iv;
        delete[] fnct2->ov;
        fnct2->DeleteCovs();
        fnct3 = fnct2->next;
        delete fnct2;
        fnct2 = fnct3;
      }
    }
  delete this->fnct_array;
  delete this->trida_ekviv;
  delete this->pocet_ekviv;
  for (i=0;i<this->origpocet;++i) delete this->names[i];
  delete this->names;
  for (i=0;i<this->pocet;++i) delete this->seznm_ekviv[i];
  delete this->seznm_ekviv;
  delete this->pocet_termu_na_ekviv;


  delete this->pprechodu;
  for (i=0;i<this->pocet;++i) {
    while (this->prechody[i]!=NULL) {
        temp=this->prechody[i]->next;
        delete this->prechody[i];
        this->prechody[i]=temp;
    }
  }
  delete this->prechody;
}

int StateInfo::SaveFnctAsKISS2( char * filn)
{
  FILE * f;
  TPfnct * ff;
  int i;

  if ( filn != 0 ) fopen_s(&f,filn, "wt" );
  else f = stdout;
  if (this->reset)
    fprintf( f, ".i %i\n", this->inpvars+1 );
  else
    fprintf( f, ".i %i\n", this->inpvars );
    fprintf( f, ".o %i\n", this->outvars );
  if (this->reset)
    fprintf( f, ".p %i\n", this->termakt+1 );
  else
    fprintf( f, ".p %i\n", this->termakt );
  fprintf( f, ".s %i\n", this->origpocet );
  fprintf( f, ".r %s\n", this->names[0] );
  if (this->fnct_array != NULL)
    for (i=0;i<this->origpocet;++i) {
      ff = this->fnct_array[i];
      while ( ff != NULL ) {
        ff->iv[this->inpvars] = 0;
        ff->ov[this->outvars] = 0;
        if (this->reset)
          fprintf( f, "0%s %7s %7s %s\n", ff->iv,this->names[ff->tmp],this->names[ff->tmp2],ff->ov );
        else
          fprintf( f, "%s %7s %7s %s\n", ff->iv,this->names[ff->tmp],this->names[ff->tmp2],ff->ov );
        ff = ff->next;
      }
    }
  if (this->reset) {
    fprintf( f, "1");
    for (i=0;i<this->inpvars;++i) fprintf( f, "-");
    fprintf( f, " %7s %7s ", "-----",this->names[0]);
    for (i=0;i<this->outvars;++i) fprintf( f, "-");
    fprintf( f ,"\n");
    }
	fprintf( f ,".e\n");

  if (f!=stdout) fclose( f );
  return 0;
}


GenerateInfo::GenerateInfo(int terms)
{
  int i;
  this->tab = (int *) malloc(sizeof(long) * 6 * terms);  // alokuju pole
  for (i=0;i<terms;i++)
  {
    this->tab[i*6]=this->tab[i*6+1]=this->tab[i*6+2]=this->tab[i*6+3]=this->tab[i*6+4]=this->tab[i*6+5]=0;
  }
}

GenerateInfo::~GenerateInfo()
{
  delete this->tab;
}



THash_Polozka* THash_Tabulka::VratPolozkuZTabulky(long index)
{
  return this->tabulka[index];
}


void THash_Tabulka::UlozPolozkuDoTabulky(THash_Polozka *pol,long index)
{
  this->tabulka[index] = pol;
}


THash_Seznam_Polozek::THash_Seznam_Polozek()
{
 this->next = NULL;
 this->index = 0;
}


THash_Seznam_Polozek::~THash_Seznam_Polozek()
{
  if ( this == NULL ) return;
  if ( this->next != NULL )
  {
    delete this->next;
  }
}


THash_Polozka::THash_Polozka()
{
  this->next = NULL;
  this->fnct = NULL;
}


THash_Tabulka::THash_Tabulka(int bits,TBoolFnct *parent)
{
  long i;
  this->bitu=bits;
  this->parent=parent;
  this->polozek=1 << bits;
  this->pocet=0;
  this->tabulka = (THash_Polozka * *) malloc(sizeof(THash_Polozka *) * polozek);  // alokuju pole
  for (i=0;i<polozek;++i)
  {
    this->tabulka[i]=NULL;
  }
}


THash_Tabulka::~THash_Tabulka()         // Znici jen strukturu THash_Tabulka, fnct zustanou v TBoolfnct
{
  THash_Polozka * pol, * pol2;
  long i;
  if ( this == NULL ) return;
  for (i=0;i<this->polozek;++i)
  {
    pol = this->tabulka[i];
    while ( pol != 0 )
    {
      pol2 = pol->next;
      delete pol;
      pol = pol2;
    }
  }
}


void THash_Tabulka::Push(TPfnct * ff,long kam)
{
	THash_Polozka *novy;
	novy = new THash_Polozka;
	novy->fnct = ff;
	novy->next = this->tabulka[kam];
  this->tabulka[kam]=novy;
  this->pocet++;
}


void THash_Tabulka::AddItem(TPfnct * ff )
{
  this->AddItemPrivate(ff,0,0);
}


void THash_Tabulka::AddItemPrivate(TPfnct * ff, int pozice, long kam)
{
  if ((pozice == this->parent->inpvars ) || (pozice==this->bitu))
  {
    this->Push(ff,kam);
  }
  else
  {
    kam = kam << 1;
    if (ff->iv[pozice]=='-')
    {
      this->AddItemPrivate(ff,pozice+1,kam);
      this->AddItemPrivate(ff,pozice+1,kam+1);
    }
    else if (ff->iv[pozice]=='0') { this->AddItemPrivate(ff,pozice+1,kam); }
    else if (ff->iv[pozice]=='1') { this->AddItemPrivate(ff,pozice+1,kam+1); }
  }
}


THash_Seznam_Polozek* THash_Tabulka::Vrat_Seznam(TPfnct * ff)
{
  THash_Seznam_Polozek* pol;
  pol=NULL;
  pol = this->Vrat_SeznamPrivate(ff,pol,0,0);
  return pol;
}



THash_Seznam_Polozek* THash_Tabulka::Vrat_SeznamPrivate(TPfnct * ff,THash_Seznam_Polozek* pol, int pozice, long kde)
{
  THash_Seznam_Polozek* pol2;
  if ((pozice == this->parent->inpvars) || (pozice==this->bitu))
  {
    pol2 = new THash_Seznam_Polozek;
    pol2->next = pol;
    pol2->index=kde;
    return pol2;
  }
  else
  {
    kde = kde << 1;
    if (ff->iv[pozice]=='-')
    {
      pol = this->Vrat_SeznamPrivate(ff,pol,pozice+1,kde);
      pol = this->Vrat_SeznamPrivate(ff,pol,pozice+1,kde+1);
    }
    else if (ff->iv[pozice]=='0') { pol = this->Vrat_SeznamPrivate(ff,pol,pozice+1,kde); }
    else if (ff->iv[pozice]=='1') { pol = this->Vrat_SeznamPrivate(ff,pol,pozice+1,kde+1); }
  }
  return pol;
}




void THash_Tabulka::DeleteTerm(TPfnct *ff)

{

    THash_Seznam_Polozek *ff1,*ff1n;

    THash_Polozka *ff2,*ff2n,*ff3,*ff4;
    int brk;

    ff1=NULL;
    ff1n=ff1=this->Vrat_Seznam(ff);
    while (ff1!=NULL)
    {
        ff2n=ff2=this->VratPolozkuZTabulky(ff1->index);
        brk=0;
        while ((ff2!=NULL) && (brk==0))
        {
          if (ff2->fnct == ff)
          {
            brk=1;
            if ( ff2n == ff2 )
            {
              this->tabulka[ff1->index] = ff2->next;
              ff2->next = NULL;
              delete ff2;
              ff2 = this->tabulka[ff1->index];
              ff3 = ff2;
              this->pocet--;
            }
            else
            {
              ff4 = ff2->next;
              ff2->next = NULL;
              delete ff2;
              ff3->next = ff4;
              ff2 = ff4;
              this->pocet--;
            }
          }
          else
          {
            ff3=ff2;
            ff2=ff2->next;
          }
        }
        ff1=ff1->next;
    }
    delete ff1n;
}


void THash_Tabulka::Print()

{
  THash_Polozka * pol;
  int i;
  for (i=0;i<this->polozek;++i)
  {
    pol = this->tabulka[i];
    printf ("%d - ",i);
    while ( pol != 0 )
    {
      printf("%s*%s",pol->fnct->iv,pol->fnct->ov);
      pol = pol->next;
      if (pol) printf(",");
    }
    printf("\n");
  }
}



int NewGauge( char * name, int max, int context )
{
  return 0;
}

void CloseGauge()
{
}

int GaugeStep( int val, int context )
{
  return 0;
}

void help()
{
  fprintf_s( stderr, "syntax: \n");
  fprintf_s( stderr, " Genstate -i n -o n -t n -s n [-idc n] [-odc n] [-idt n] [-odt n] [-se n] [-sp n] [-sr] [-sNS] [-sND] [-sNK] [-sD] [-NC] [-timeout n] [file_name]\n" );
  fprintf_s( stderr, " Necessary parameters:\n\n");
  fprintf( stderr, "   -i n        Specify the number of inputs\n" );
  fprintf( stderr, "   -o n        Specify the number of outputs\n" );
  fprintf( stderr, "   -t n        Specify the number of defined terms\n" );
  fprintf( stderr, "   -s n        Specify the number of states\n" );
  fprintf_s( stderr, " Optional parameters:\n\n");
  fprintf( stderr, "   -idc n      Specify the percentage of input don't cares. 0 is default\n" );
  fprintf( stderr, "   -odc n      Specify the percentage of output don't cares. 0 is default\n" );
  fprintf( stderr, "   -idt n      Specify the percentage of input ones. 50 is default\n" );
  fprintf( stderr, "   -odt n      Specify the percentage of output ones. 50 is default\n" );
  fprintf( stderr, "   -timeout n  The timeout limit, in seconds. 1000s is the default\n" );
  fprintf( stderr, "   -se n       Specify the effective states (number of equivalence classes)\n" );
  fprintf( stderr, "   -sp n       Specify the percentage of pseudo states\n" );
  fprintf( stderr, "   -sr         Enable state RESET (it doesnt count to n states and n terms)\n" );
  fprintf( stderr, "   -NC         The consistency check on each state is not performed\n" );
  fprintf( stderr, "   -ND         The duplicity chceck on each state is not performed\n" );
  fprintf( stderr, "   -NS         The continuity check is not performed.\n" );
  fprintf( stderr, "   -NZ         The accesibility check is not performed.\n" );
  fprintf( stderr, "   -NK         The ending check is not performed.\n" );
  fprintf( stderr, "   -NT         The deterministic check is not performed\n" );
}

void RandomFillOneFnct(THash_Tabulka *htab, TBoolFnct *srcf, TPfnct *ff, double r, double r2, int mask)
{
    int i,v;

    ff->dim=0;
    if ((mask & 1) == 1)
    {
      for (i = 0; i < srcf->inpvars; i++)
      {
        v = random(100);
        if (v < r) {
            ff->iv[i] = '-';
            ff->dim++;
        } else {
            v = random(100);
            if (v<r2) { ff->iv[i] = '1'; }
            else ff->iv[i] = '0';
        }
      }

    }
    if ((mask &2) == 2) for (i=0; i<srcf->outvars; i++) {
        v=random(100);
        if (v<r) {
                ff->ov[i]='-';
        } else {
            v = random(100);
            if (v<r2) { ff->ov[i] = '1'; }
            else ff->ov[i] = '0';
        }
    }
}

int DoPostChecks(THash_Tabulka *htab, TBoolFnct *fn, TPfnct *ffl,int filt,int dupl,int det)   // dela kontrolu validity 0-OK, 1-dupl,2-inkonzistent,3-nondeterministic
{
  THash_Seznam_Polozek *ff1,*ffn;
  THash_Polozka* ff2;
  int i,brk;

  if ((filt==0) && (dupl==0) && (det==0)) {
	return 0;
  }
  brk=0;
  ff1=ffn=NULL;
  if (ffl!=NULL)
  {
    ffn=ff1=htab->Vrat_Seznam(ffl);
      while (ff1!=NULL)
      {
        ff2=htab->VratPolozkuZTabulky(ff1->index);
        while (ff2!=NULL)
        {
          if (ff2->fnct->valid==1) {
            // duplicity
			if ((dupl) && (strcmp(ffl->iv,ff2->fnct->iv)==0) && (strcmp(ffl->ov,ff2->fnct->ov)==0) ) {
				return 1;
			}
			if (det) {
				brk=1;
	            for (i=0; i<fn->inpvars; i++)	
	            {
					if (ffl->iv[i]!=ff2->fnct->iv[i] && ffl->iv[i]!='-' && ff2->fnct->iv[i]!='-')
					{
	                    brk=0;
						break;
					}
				}
				if (brk) return 3;
			}
			if (filt) {
				brk=1;
	            for (i=0; i<fn->inpvars; i++) {
	                if (ffl->iv[i]!=ff2->fnct->iv[i] && ffl->iv[i]!='-' && ff2->fnct->iv[i]!='-') {
						brk=0;
						break;
					}
				}
				if (brk)
				{
					for (i=0; i<fn->outvars; i++)
					{
						if (ffl->ov[i]!=ff2->fnct->ov[i] && ffl->ov[i]!='-' && ff2->fnct->ov[i]!='-')
						{
							return 2;
						}
					}
				}
            }
          }
          ff2=ff2->next;
        }
        ff1=ff1->next;
      }
    delete ffn;
  }
  return 0;
}

int RndConFillFnct( GenerateInfo *gi, int det )
//THash_Tabulka * htab,TBoolFnct *fn, int mask, int irnd, int ornd,int idt,int odt, int filt, int to)
/*
    Randomly fills a function fn. Terms must be defined.
    mask: bit 0 == 1 -> fill input
    mask: bit 1 == 1 -> fill output
    irnd: % of input DCs
    ornd: % of input DCs
    filt == 0 -> no checks, just fill it
    filt == 1 -> consistent fill (no inconsistencies)
    to: # of seconds until timeout
    returns true if succeeded
*/
{
    int zbyvajicich=0,brk,k,j;
    TPfnct *ff, *ffl;
    struct timeb t2, t1;

    ftime(&t2);

    RandomFillOneFnct(gi->hashtab, gi->fn, gi->fn->fnct, gi->idc, gi->idt, gi->mask & 1);
       #ifdef LADICI_HLASENI
        gi->hashtab->Print();
        gi->fn->Print();
       #endif
    RandomFillOneFnct(gi->hashtab, gi->fn, gi->fn->fnct, gi->odc, gi->odt, gi->mask & 2);
       #ifdef LADICI_HLASENI
        gi->hashtab->Print();
        gi->fn->Print();
       #endif
        ffl = ff = gi->fn->fnct;
        gi->hashtab->AddItem(ff);
        ff=ff->next;
        j=1;
        ftime(&t1);

        while (j < gi->t && t1.time-t2.time < gi->timeout)
        {
          if (zbyvajicich != gi->t-j)
          {
            zbyvajicich = gi->t-j;
           #ifdef VYPIS_CHYBEJICICH_TERMU
            printf("Zbyva %d termu\n",zbyvajicich);
           #endif
          }
         #ifdef LADICI_HLASENI
          gi->hashtab->Print();
          gi->fn->Print();
         #endif
		  RandomFillOneFnct(gi->hashtab, gi->fn, ff, gi->idc, gi->idt, gi->mask & 1);
          gi->hashtab->AddItem(ff);
         #ifdef LADICI_HLASENI
          gi->hashtab->Print();
          gi->fn->Print();
         #endif
          RandomFillOneFnct(gi->hashtab, gi->fn, ff, gi->odc, gi->odt, gi->mask & 2);
         #ifdef LADICI_HLASENI
          gi->hashtab->Print();
          gi->fn->Print();
         #endif
          ff->valid=0;
		  brk=DoPostChecks(gi->hashtab, gi->fn, ff,gi->filt,gi->dupl,det); // zkouma validitu termu ff vuci termum v hashtabulce
          k=gi->pocet_output;
          if (det) k=0;
		  while ((brk) && (k>0) && ((gi->mask & 2)==2)) { // pokud mame jeste pokusy a zajima nas output  tak zkousime menit output
            --k;
            RandomFillOneFnct(gi->hashtab, gi->fn, ff, gi->odc, gi->odt, gi->mask & 2);
           #ifdef LADICI_HLASENI
            gi->hashtab->Print();
            gi->fn->Print();
           #endif
		  brk=DoPostChecks(gi->hashtab, gi->fn, ff,gi->filt,gi->dupl,det); // zkouma validitu termu ff vuci termum v hashtabulce
		  }
           #ifdef LADICI_HLASENI2
			gi->hashtab->Print();
			printf("%s*%s\n",ff->iv,ff->ov);
			printf("vysledek kontrol %d\n",brk);
           #endif
		  if (brk) {      // brk1 inconsistent => mazeme z hash a budem zkouset znovu
            gi->hashtab->DeleteTerm(ff);
          }
          else {
            ff->valid=1;
            ffl=ff;
            ff=ff->next;
            j++;
          }
          ftime(&t1);
        }

    return (j == gi->t);
}

int FullStateFillFnct( GenerateInfo *gi )
{
    TPfnct *ff, *ffl;
	int i,j,k,v;
	ff=gi->fn->fnct;
	for(j=0;j<=gi->t;++j) {
		k=j;
		for (i = 0; i < gi->fn->inpvars; ++i) {
            ff->iv[i] = '0'+k%2;
			k=k>>1;
        }
		for (i = 0; i < gi->fn->outvars; ++i) {
			v=random(100);
			if (v<gi->odc) {
				ff->ov[i]='-';
			} else {
				v = random(100);
				if (v<gi->odt) { ff->ov[i] = '1'; }
				else ff->ov[i] = '0';
			}
		}
		ff=ff->next;
	}

	return 1;
}
int main( int argc, char * argv[] )
{
  int i;
  int cas,load,info,ready,stav;
  struct timeb t2, t1;

  ftime(&t2);

  Boom * boominst;
  GenerateInfo *gi,*gg;
  StateInfo *stavy;

  boominst = new Boom();
  boominst->gauge.NewGauge = NewGauge;
  boominst->gauge.CloseGauge = CloseGauge;
  boominst->gauge.GaugeStep = GaugeStep;

  cas=((int) t2.time)*1000+t2.millitm;
  srand(cas);
  stavy = new StateInfo;
  gi = new GenerateInfo(0);
  gi->pocet_output = POCET_POKUSU_OUTPUT;
  gi->bits = 0;
  gi->onmpla = 0;
  gi->onminf = 0;
  gi->iv = -1;
  gi->ov = -1;
  gi->t = -1;
  gi->idc = 0;
  gi->odc = 0;
  gi->idt = 50;
  gi->odt = 50;
  gi->glidc = -1;
  gi->glodc = -1;
  gi->glidt = -1;
  gi->glodt = -1;
  gi->filt = 1;
  gi->timeout = 1000;
  gi->mask = 3;

  i = 1;
  load = 0;
  info = 0;
  ready = 0;
  stav = 0;

  fprintf( stderr, "STATE Generator 0.91, (c) May 2008\n\n" );
  while ( i != argc )
  {
    if ( argv[i] [0] == '-' )
	{
		if ( strcmp(argv[i], "-i") == 0) {
            gi->iv = atoi( argv[++i] );
			stavy->inpvars=gi->iv;
		}
		else if ( strcmp(argv[i], "-o") == 0) {
            gi->ov = atoi( argv[++i] );
			stavy->outvars=gi->ov;
		}
		else if ( strcmp(argv[i], "-t") == 0) {
            gi->t = atoi( argv[++i] );
			stavy->terms=gi->t;
		}
        else if ( strcmp(argv[i], "-h") == 0) {
            gi->bits = atoi( argv[++i] );
            gi->bits=gi->bits>16?16:gi->bits;
        }
        else if ( strcmp(argv[i], "-p") == 0)
            gi->pocet_output = atoi( argv[++i] );
		else if ( strcmp(argv[i], "-idc") == 0) {
            gi->idc = atoi( argv[++i] );
			gi->sidc = gi->idc;
		}
		else if ( strcmp(argv[i], "-odc") == 0) {
            gi->odc = atoi( argv[++i] );
			gi->sodc = gi->odc;
		}
		else if ( strcmp(argv[i], "-idt") == 0) {
            gi->idt = atoi( argv[++i] );
			gi->sidt = gi->idt;
		}
		else if ( strcmp(argv[i], "-odt") == 0) {
            gi->odt = atoi( argv[++i] );
			gi->sodt = gi->odt;
		}
        else if ( strcmp(argv[i], "-timeout") == 0)
            gi->timeout = atoi( argv[++i] );
        else if ( strcmp(argv[i], "-s") == 0) {
            stavy->origpocet = atoi( argv[++i] );
            }
        else if ( strcmp(argv[i], "-se") == 0)
            stavy->pocet = atoi( argv[++i] );
		else if ( strcmp(argv[i], "-sp") == 0) {
            stavy->pseudo = atoi( argv[++i] );
		}
        else if ( strcmp(argv[i], "-sr") == 0)
            stavy->reset = 1;
        else if ( strcmp(argv[i], "-NC") == 0)
            gi->filt = 0;
        else if ( strcmp(argv[i], "-ND") == 0)
            gi->dupl = 0;
        else if ( strcmp(argv[i], "-NS") == 0)
            stavy->spojitost = 0;
        else if ( strcmp(argv[i], "-NZ") == 0)
            stavy->dosazitelnost = 0;
        else if ( strcmp(argv[i], "-NK") == 0)
            stavy->koncovost = 0;
        else if ( strcmp(argv[i], "-NT") == 0)
            stavy->deterministic = 0;
        else {
            fprintf( stderr, "Unknown parameter %s\n", argv[i] );
            exit( 1 );
        }
    }
    else  gi->onmpla = argv[i];
    i++;
  }



  if (( stavy->origpocet == -1 || gi->iv == -1 || gi->ov == -1 || gi->t == -1 ) && (load==0)) help();
  else
  {
	if (stavy->pocet > stavy->origpocet) {
		fprintf( stderr, "Number of equivalence classes must be equal or lower to number of states !" );
		exit( 1 );
	}

	long int zmax = (long int) pow((double)2,gi->iv);
	if ((gi->t>zmax*stavy->origpocet)&&(stavy->deterministic)) {
		if (gi->t>=zmax*stavy->origpocet) fprintf( stderr, "Number of terms is bigger than terms in full deterministic autamat! Number of terms is modified.\n" );
		gi->t=zmax*stavy->origpocet;
		stavy->full;
		stavy->terms=gi->t;
	}

//  resime stavy
      stavy->Init(gi);
	  if (stavy->deadlock) { 
	            fprintf( stderr, "Number of terms for one state is bigger, than its possible. Deadlock will occur. Try run again with more inputs.\n" );
		        return 8;
	  }
      for (i=0;i<stavy->pocet;++i) {
       if (stavy->pocet_termu_na_ekviv[i]!=0) {
        gi->fn = new TBoolFnct( gi->iv, gi->ov, stavy->pocet_termu_na_ekviv[i] , gi->filt );
        gi->fn->FillEmptyFnct();
        gi->t= stavy->pocet_termu_na_ekviv[i];
        gi->hashtab = new THash_Tabulka(gi->bits,gi->fn);
		if (stavy->full && stavy->deterministic) {
			if ( FullStateFillFnct(gi)){
				stavy->Dopln_Stavy(gi,i);
	        }
		}
		else {
			if ( RndConFillFnct( gi,stavy->deterministic)) {
				stavy->Dopln_Stavy(gi,i);
			}
	        else {
	            fprintf( stderr, "Timeout\n" );
		        return 1;
			}
		}
        delete gi->hashtab;
        delete gi->fn;
       }
      }
      stavy->Dodelej_ekviv_stavy();
	  stavy->Dodelej_pseudo_stavy();
      stavy->SaveFnctAsKISS2(gi->onmpla);
    
  }
  delete gi;
  ftime(&t1);
  cas=((int) t1.time)*1000+t1.millitm-((int)t2.time)*1000-t2.millitm;
#ifdef VYPIS_CASU
  printf("Program was running: %.3f sekund.",(float)cas/1000);
#endif
  return 0;
}


