#include <stdlib.h>
#include <list>
#include <iostream>
#include <fstream>
#include <string>

using namespace std;

class Protocol{
  unsigned Nb_Part;
  ofstream out;
  
  list<unsigned*> *recs;
  
  list<string> bool_external,range_external, bool_interface, range_interface, controls, reads, init, update;

  void add_recovery(unsigned i, unsigned* r);
  void write_honestP(unsigned i);
  void write_dishonestP(unsigned i);
  void write_T( );
  void write_System(unsigned i);
  
public:
  Protocol(unsigned N, char *fn);
};


Protocol::Protocol(unsigned N, char *fn){
  out.open(fn);
  if (! out.is_open()){
    cerr << "Error opening file" <<endl;
    exit(EXIT_FAILURE);
  }

  Nb_Part=N;
  recs=new list<unsigned*>[Nb_Part+1];
  for(unsigned i=1; i <= Nb_Part; i++){
    write_honestP(i);
    write_dishonestP(i);
  }
  write_T();
  for(unsigned i=1; i <= Nb_Part; i++)
    write_System(i);
  
}

void Protocol::add_recovery(unsigned i, unsigned* r){
  unsigned *x;
  x=new unsigned[Nb_Part+1];
  for(unsigned j=0; j<=Nb_Part; j++)
    if(i!=j){
      x[j]=r[j];
    }
  recs[i].push_back(x);
}


void Protocol::write_honestP(unsigned i){

  string si(1,'0'+i);
  string si_plus_1(1,'0'+i+1);
  string si_minus_1(1,'0'+i-1);
  string si_minus_2(1,'0'+i-2);

  string sn(1,'0'+Nb_Part);
  string sn_plus_1(1,'0'+Nb_Part+1);  
  string sn_minus_1(1,'0'+Nb_Part-1);  

  string not_stop="\t \t [] ~P"+si+"_stop & ~P"+si+"_contacted_T";

  

  // idle action while not stopped
  string s=not_stop + " ->";
  update.push_back("-- idle action while not stopped");
  update.push_back(s);
  
  bool_interface.push_back("P"+si+"_stop");
  controls.push_back("P"+si+"_stop");
  reads.push_back("P"+si+"_stop");
  init.push_back("P"+si+"_stop':=false");

  bool_interface.push_back("P"+si+"_contacted_T");
  controls.push_back("P"+si+"_contacted_T");
  reads.push_back("P"+si+"_contacted_T");
  init.push_back("P"+si+"_contacted_T':=false");
  
  // (1) wait for higher recursive levels to start
  update.push_back("-- (1) wait for higher recursive levels to start");
  if(i!=Nb_Part){
    s=not_stop;
    for(unsigned j=Nb_Part; j>=1; j--)
      if(j!=i){
	string sj(1,'0'+j);
	s+=" & Pr_"+si+"_"+sj+"_L=0";
      }
    s+=" & ~(";
    for(unsigned j=Nb_Part; j>i; j--){
      string sj(1,'0'+j);
      s+=" Pr_"+sj+"_"+si+"_L>0 ";
      s+="&";
      range_external.push_back("Pr_"+sj+"_"+si+"_L");
      reads.push_back("Pr_"+sj+"_"+si+"_L");
    }
    s.erase(s.length()-1,1);
    s+=") -> P"+si+"_stop':=true";
    update.push_back(s); 
  }

  // (2) start recursive level i
  update.push_back("-- (2) start recursive level i");
  if(i!=1){  
    s=not_stop;
    for(unsigned j=Nb_Part; j>i; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+sj+"_"+si+"_L>0";
    };

    for(unsigned j=Nb_Part; j>i; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
    }
    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
      range_interface.push_back("Pr_"+si+"_"+sj+"_L");
      controls.push_back("Pr_"+si+"_"+sj+"_L");
      reads.push_back("Pr_"+si+"_"+sj+"_L");
      init.push_back("Pr_"+si+"_"+sj+"_L':=0");
    };
    s+=" -> ";
    for(unsigned j=i-1; j>1; j--){
      string sj(1,'0'+j);
      s+="Pr_"+si+"_"+sj+"_L':=1; ";
    };
    s+="Pr_"+si+"_1_L':=1";
    update.push_back(s); 
 }

  // (3) Wait for recursive level (i-1) to finish
  update.push_back("-- (3) Wait for recursive level (i-1) to finish");
  if(i!=1){
    s=not_stop;
    for(unsigned j=Nb_Part; j>i; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
    };
    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=1";
    };
    s+=" & ~(";
    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" Pr_"+sj+"_"+si+"_L>"+si_minus_2;
      s+="&";
      range_external.push_back("Pr_"+sj+"_"+si+"_L");
      reads.push_back("Pr_"+sj+"_"+si+"_L");
    }
    s.erase(s.length()-1,1);
    s+=")";
    s+=" -> P"+si+"_Abort_Send':=true; P"+si+"_contacted_T':=true";
    bool_interface.push_back("P"+si+"_Abort_Send");
    controls.push_back("P"+si+"_Abort_Send");
    reads.push_back("P"+si+"_Abort_Send");
    init.push_back("P"+si+"_Abort_Send':=false");
    update.push_back(s);
  }

  // (4) Send (i) level promises to all lower parties
  update.push_back("-- (4) Send (i) level promises to all lower parties");
  if(i!=1){
    s=not_stop;
    for(unsigned j=Nb_Part; j>i; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
    };

    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=1";
    };
    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+sj+"_"+si+"_L>"+si_minus_2;
    }
    s+=" -> ";
    for(unsigned j=i-1; j>1; j--){
      string sj(1,'0'+j);
      s+="Pr_"+si+"_"+sj+"_L':="+si+"; ";
    }
    s+="Pr_"+si+"_1_L':="+si;
    update.push_back(s); 
  }

  // (5) Finish recursive level i when i-level promises are received
  update.push_back("-- (5) Finish recursive level i when i-level promises are received");
  if(i!=1){
    unsigned *recoveries=new unsigned[Nb_Part+1];
    for(unsigned j=Nb_Part; j>i; j--)
      recoveries[j]=1;
    for(unsigned j=i-1; j>=1; j--)
      recoveries[j]=i-1;
    add_recovery(i, recoveries);
    
    s=not_stop;
    for(unsigned j=Nb_Part; j>i; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
    }
    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L="+si;
    }
    s+=" & ~(";
    for(unsigned j=i-1; j>0; j--){
      string sj(1,'0'+j);
      s+=" Pr_"+sj+"_"+si+"_L>"+si_minus_1;
      s+=" &";
    }
    s.erase(s.length()-1,1);
    s+=") -> ";
    string rec="P"+si+"_Recovery";
    for(unsigned j=Nb_Part; j>i; j--)
      {
	string s1(1,'1');     
	rec+="_"+s1;
      };
    for(unsigned j=i-1; j>0; j--)
      {
	rec+="_"+si_minus_1;
      };

    bool_interface.push_back(rec);
    controls.push_back(rec);
    reads.push_back(rec);
    init.push_back(rec+"':=false");
    s+="P"+si+"_contacted_T':=true; "+rec+"':=true";
    
    update.push_back(s);   
  }


  // (6) Complete all higher recursive levels
  update.push_back("-- (6) Complete all higher recursive levels");
  for (unsigned a=i+1; a<=Nb_Part; a++){
    string sa(1,'0'+a);
    string sa_minus_1(1,'0'+a-1);
    string sa_minus_2(1,'0'+a-2);

    // (6.1)
    update.push_back("-- (6.1) - a="+sa);
    s=not_stop;

    for (unsigned j=Nb_Part; j>=a; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
    }    
    for (unsigned j=a-1; j>=1; j--){
    string sj(1,'0'+j);
      if(j!=i)
	s+=" & Pr_"+si+"_"+sj+"_L="+sa_minus_1;
    }

    for (unsigned j=1; j<a; j++){
    string sj(1,'0'+j);
      if(j!=i)
	s+=" & Pr_"+sj+"_"+si+"_L>"+sa_minus_2;
    }    

    for (unsigned j=a; j<=Nb_Part; j++){
    string sj(1,'0'+j);
	s+=" & Pr_"+sj+"_"+si+"_L>0";
    }    
    s+=" -> Pr_"+si+"_"+sa+"_L':="+sa_minus_1;

    range_interface.push_back("Pr_"+si+"_"+sa+"_L");
    controls.push_back("Pr_"+si+"_"+sa+"_L");
    reads.push_back("Pr_"+si+"_"+sa+"_L");
    init.push_back("Pr_"+si+"_"+sa+"_L':=0");
    update.push_back(s);

    // (6.2)
    update.push_back("-- (6.2) - a="+sa);
    s=not_stop;
    for (unsigned j=Nb_Part; j>a; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L=0";
    }    
    for (unsigned j=a; j>=1; j--){
    string sj(1,'0'+j);
      if(j!=i)
	s+=" & Pr_"+si+"_"+sj+"_L="+sa_minus_1;
    }
    s+=" & ~(";
    for(unsigned j=a; j>=i+1; j--){
      string sj(1,'0'+j);
      s+=" Pr_"+sj+"_"+si+"_L>"+sa_minus_1;
      s+=" &";
    }
    s.erase(s.length()-1,1);
    s+=")";

    // considering all different possibilities for recovery at 6.2
    unsigned *recoveries=new unsigned[Nb_Part+1];
    for (unsigned j=1; j<i; j++)
      recoveries[j]=a-1;
    for (unsigned j=i+1; j<a; j++)
      recoveries[j]=a-1;
    for (unsigned j=a+1;j<=Nb_Part;j++)
      recoveries[j]=1;
    

    bool ok=true;
    while (ok) {

      // this possibility for recovery[a]=1
      string s1=s;
      recoveries[a]=1;
      
      for (unsigned j=Nb_Part;j>=1;j--){
	if(j!=i){
	  string sj(1,'0'+j);
	  string skj_minus_1(1,'0'+recoveries[j]-1);
	  s1+=" & Pr_"+sj+"_"+si+"_L>"+skj_minus_1;
	}
      }
      add_recovery(i, recoveries);
      s1+=" ->";
      string rec="P"+si+"_Recovery";
      for (unsigned j=Nb_Part;j>=1;j--){
	if(j!=i){
	  string skj(1,'0'+recoveries[j]);
	  rec+="_"+skj;
	}
      }
      s1+="P"+si+"_contacted_T':=true; "+rec+"':=true";
      bool_interface.push_back(rec);
      controls.push_back(rec);
      reads.push_back(rec);
      init.push_back(rec+"':=false");
      update.push_back(s1);


      // this possibility for recovery[a]=a
      if (i+1 <=a-1){
	s1=s;
	recoveries[a]=a;
	for (unsigned j=Nb_Part;j>=1;j--){
	  if(j!=i){
	    string sj(1,'0'+j);
	    string skj_minus_1(1,'0'+recoveries[j]-1);
	    s1+=" & Pr_"+sj+"_"+si+"_L>"+skj_minus_1;
	  }
	}
	add_recovery(i, recoveries);
	s1+=" ->";
	rec="P"+si+"_Recovery";
	for (unsigned j=Nb_Part;j>=1;j--){
	  if(j!=i){
	    string skj(1,'0'+recoveries[j]);
	    rec+="_"+skj;
	  }
	}
	s1+="P"+si+"_contacted_T':=true; "+rec+"':=true";
	bool_interface.push_back(rec);
	controls.push_back(rec);
	reads.push_back(rec);
	init.push_back(rec+"':=false");
	update.push_back(s1);
      }
      // generate next possible recovery
      unsigned j=i+1;
      while(j<a && recoveries[j]==a){
	recoveries[j]--;
	j++;
      }
      recoveries[j]++;
      
      // test if last possibility
      j=i+1;
      ok=false;
      while(j<a && !ok)
	ok=(recoveries[j++]==a-1);
    } //end while(OK)

    if (a-1 >= i+1){
      string s1=s;
      recoveries[a]=1;
      for (unsigned j=Nb_Part;j>=1;j--){
	if(j!=i){
	  string sj(1,'0'+j);
	  string skj_minus_1(1,'0'+recoveries[j]-1);
	  s1+=" & Pr_"+sj+"_"+si+"_L>"+skj_minus_1;
	}
      }
      add_recovery(i, recoveries);
      s1+=" ->";
      string rec="P"+si+"_Recovery";
      for (unsigned j=Nb_Part;j>=1;j--){
	if(j!=i){
	  string skj(1,'0'+recoveries[j]);
	  rec+="_"+skj;
	}
      }
      s1+="P"+si+"_contacted_T':=true; "+rec+"':=true";
      bool_interface.push_back(rec);
      controls.push_back(rec);
      reads.push_back(rec);
      init.push_back(rec+"':=false");
      update.push_back(s1);
    }
    // (6.3)
    update.push_back("-- (6.3) - a="+sa);
    if(i!=1){
      s=not_stop;

      for (unsigned j=Nb_Part; j>a; j--){
	string sj(1,'0'+j);
	s+=" & Pr_"+si+"_"+sj+"_L=0";
      }    
      for (unsigned j=a; j>=1; j--){
	string sj(1,'0'+j);
	if(j!=i)
	  s+=" & Pr_"+si+"_"+sj+"_L="+sa_minus_1;
      }

      for (unsigned j=a; j>=i+1; j--){
	string sj(1,'0'+j);      
	s+=" & Pr_"+sj+"_"+si+"_L>"+sa_minus_1;
      }
      for (unsigned j=i-1; j>=1; j--){
	string sj(1,'0'+j);      
	s+=" & Pr_"+sj+"_"+si+"_L>"+sa_minus_2;
      }
      s+=" -> ";
      for (unsigned j=i-1; j>1; j--){
	string sj(1,'0'+j);      
	s+="Pr_"+si+"_"+sj+"_L':="+sa+"; ";
      }
      s+="Pr_"+si+"_1_L':="+sa;
      update.push_back(s);
    }
    // (6.4)
    update.push_back("-- (6.4) - a="+sa);
    if (i!=1){
      s=not_stop;

      for (unsigned j=Nb_Part; j>a; j--){
	string sj(1,'0'+j);
	s+=" & Pr_"+si+"_"+sj+"_L=0";
      }    
      for (unsigned j=a; j>i; j--){
	string sj(1,'0'+j);
	if(j!=i)
	  s+=" & Pr_"+si+"_"+sj+"_L="+sa_minus_1;
      }
      for (unsigned j=i-1; j>=1; j--){
	string sj(1,'0'+j);
	if(j!=i)
	  s+=" & Pr_"+si+"_"+sj+"_L="+sa;
      }


      for (unsigned j=Nb_Part; j>a; j--){
	string sj(1,'0'+j);
	s+=" & Pr_"+sj+"_"+si+"_L>0";
      }

      for (unsigned j=a; j>i; j--){
	string sj(1,'0'+j);
	s+=" & Pr_"+sj+"_"+si+"_L>"+sa_minus_1;
      }

      s+=" & ~(";
      for(unsigned j=i-1; j>=1; j--){
	string sj(1,'0'+j);
	s+=" Pr_"+sj+"_"+si+"_L>"+sa_minus_1;
	s+=" &";
      }
      s.erase(s.length()-1,1);
      s+=")";
      
      // recovery at 6.4
      
      unsigned *recoveries=new unsigned[Nb_Part+1];
      for(unsigned j=Nb_Part; j>a; j--)
	recoveries[j]=1;
      for(unsigned j=a; j>i; j--)
	recoveries[j]=a;
      for(unsigned j=i-1; j>=1; j--)
	recoveries[j]=a-1;
      add_recovery(i, recoveries);
      string rec="P"+si+"_Recovery";
      for(unsigned j=Nb_Part; j>a; j--)
	{
	  string s1(1,'1');     
	  rec+="_"+s1;
	};
      for(unsigned j=a; j>i; j--)
	{
	  rec+="_"+sa;
	};

      for(unsigned j=i-1; j>0; j--)
	{
	  rec+="_"+sa_minus_1;
	};

      bool_interface.push_back(rec);
      controls.push_back(rec);
      reads.push_back(rec);
      init.push_back(rec+"':=false");
      s+=" -> P"+si+"_contacted_T':=true; "+rec+"':=true";
    
      update.push_back(s);   
    } // end if (i!=1)

    // (6.5)
    update.push_back("-- (6.5) - a="+sa);
    if(i!=Nb_Part){
      s=not_stop;
      for (unsigned j=Nb_Part; j>a; j--){
	string sj(1,'0'+j);
	s+=" & Pr_"+si+"_"+sj+"_L=0";
      }    
      for (unsigned j=a; j>i; j--){
	string sj(1,'0'+j);
	if(j!=i)
	  s+=" & Pr_"+si+"_"+sj+"_L="+sa_minus_1;
      }
      for (unsigned j=i-1; j>=1; j--){
	string sj(1,'0'+j);
	if(j!=i)
	  s+=" & Pr_"+si+"_"+sj+"_L="+sa;
      }

      for (unsigned j=Nb_Part; j>a; j--){
	string sj(1,'0'+j);      
	s+=" & Pr_"+sj+"_"+si+"_L>0";
      }
      for (unsigned j=a; j>=1; j--){
	if (j!=i){
	  string sj(1,'0'+j);      
	  s+=" & Pr_"+sj+"_"+si+"_L>"+sa_minus_1;
	}
      }
      s+=" -> ";
      for (unsigned j=a; j>i+1; j--){
	string sj(1,'0'+j);      
	s+="Pr_"+si+"_"+sj+"_L':="+sa+"; ";
      }
      s+="Pr_"+si+"_"+si_plus_1+"_L':="+sa;
      update.push_back(s);
    }
  }

  // (7) receive n+1-level promises from higher participants, else recover
  update.push_back("-- (7) receive n+1-level promises from higher participants, else recover");
  if (i!=Nb_Part){
    s=not_stop;
    unsigned *recoveries=new unsigned[Nb_Part+1];

    for (unsigned j=Nb_Part; j>=1; j--){
      if (j!=i){
	string sj(1,'0'+j);
	s+=" & Pr_"+si+"_"+sj+"_L="+sn;
      }
    }

    s+=" & ~(";
    for(unsigned j=Nb_Part; j>=i+1; j--){
      string sj(1,'0'+j);
      s+=" Pr_"+sj+"_"+si+"_L>"+sn;
      s+=" &";
    }
    s.erase(s.length()-1,1);
    s+=")";
    
    for (unsigned j=i-1; j>=1; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+sj+"_"+si+"_L>"+sn_minus_1;
    }
    
    // considering all different possibilities for recovery at 7
    for (unsigned j=1; j<i; j++)
      recoveries[j]=Nb_Part;
    for (unsigned j=i+1; j<=Nb_Part; j++)
      recoveries[j]=Nb_Part;
    
    bool ok=true;
    while (ok) {
      string s1=s;
      for (unsigned j=Nb_Part;j>=1;j--){
	if(j!=i){
	  string sj(1,'0'+j);
	  string skj_minus_1(1,'0'+recoveries[j]-1);
	  s1+=" & Pr_"+sj+"_"+si+"_L>"+skj_minus_1;
	}
      }
      s1+=" -> ";
      string rec="P"+si+"_Recovery";
      for (unsigned j=Nb_Part;j>=1;j--){
	if(j!=i){
	  string skj(1,'0'+recoveries[j]);
	  rec+="_"+skj;
	}
      }
      s1+="P"+si+"_contacted_T':=true; "+rec+"':=true";
      bool_interface.push_back(rec);
      controls.push_back(rec);
      reads.push_back(rec);
      init.push_back(rec+"':=false");
      update.push_back(s1);
      add_recovery(i, recoveries);
      
      unsigned j=i+1;
      while(j<=Nb_Part && recoveries[j]==Nb_Part+1){
	recoveries[j]--;
	j++;
      }
      recoveries[j]++;
	
      // test if last possibility
      j=i+1;
      ok=false;
      while(j<=Nb_Part && !ok)
	ok=(recoveries[j++]==Nb_Part);
    }
  }

  // (8) send n+1 level promises to everybody
  update.push_back("-- (8) send n+1 level promises to everybody");
  s=not_stop;
  for (unsigned j=Nb_Part; j>=i+1; j--){
    string sj(1,'0'+j);
    s+=" & Pr_"+sj+"_"+si+"_L>"+sn;
  }
  for (unsigned j=i-1; j>=1; j--){
    string sj(1,'0'+j);
    s+=" & Pr_"+sj+"_"+si+"_L>"+sn_minus_1;
  }
  for (unsigned j=Nb_Part; j>=1; j--)
    if (j!=i){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L="+sn;
    }
  s+=" ->";
  for (unsigned j=Nb_Part; j>=1; j--)
    if (j!=i){
      string sj(1,'0'+j);
      s+=" Pr_"+si+"_"+sj+"_L':="+sn_plus_1+";";
    }
  s.erase(s.length()-1,1);
  update.push_back(s);

  // (9) receive n+1 level promoises from lower participants, else recover
  update.push_back("-- (9) receive n+1 level promoises from lower participants, else recover");
  if (i!=1){
    s=not_stop;
    unsigned *recoveries=new unsigned[Nb_Part+1];

    for (unsigned j=Nb_Part; j>=1; j--){
      if (j!=i){
	string sj(1,'0'+j);
	s+=" & Pr_"+si+"_"+sj+"_L="+sn_plus_1;
      }
    }

    for (unsigned j=Nb_Part; j>=i+1; j--){
      string sj(1,'0'+j);
      s+=" & Pr_"+sj+"_"+si+"_L>"+sn;
    }

    s+=" & ~(";
    for(unsigned j=Nb_Part; j>=1; j--){
      if(j !=i){
	string sj(1,'0'+j);
	s+=" Pr_"+sj+"_"+si+"_L>"+sn;
	s+=" &";
      }
    }
    s.erase(s.length()-1,1);
    s+=")";
    
    
    // recovery at 9
    for (unsigned j=1; j<i; j++)
      recoveries[j]=Nb_Part;
    for (unsigned j=i+1; j<=Nb_Part; j++)
      recoveries[j]=Nb_Part+1;
    
    string s1=s;
    for (unsigned j=Nb_Part;j>=1;j--){
      if(j!=i){
	string sj(1,'0'+j);
	string skj_minus_1(1,'0'+recoveries[j]-1);
	s1+=" & Pr_"+sj+"_"+si+"_L>"+skj_minus_1;
      }
    }
    s1+=" -> ";
    string rec="P"+si+"_Recovery";
    for (unsigned j=Nb_Part;j>=1;j--){
      if(j!=i){
	string skj(1,'0'+recoveries[j]);
	rec+="_"+skj;
      }
    }
    s1+="P"+si+"_contacted_T':=true; "+rec+"':=true";
    bool_interface.push_back(rec);
    controls.push_back(rec);
    reads.push_back(rec);
    init.push_back(rec+"':=false");
    update.push_back(s1);
    add_recovery(i, recoveries);
  }

  // receiving signatures and stopping ...
  update.push_back("-- receiving signatures and stopping ...");

  for (unsigned j=Nb_Part; j>=1; j--){
    if (j!=i){
      s=not_stop;
      string sj(1,'0'+j);
      s+=" & Pr_"+sj+"_"+si+"_L="+sn_plus_1+" -> P"+si+"_S"+sj+"':=true" ;
      bool_interface.push_back("P"+si+"_S"+sj);
      controls.push_back("P"+si+"_S"+sj);
      reads.push_back("P"+si+"_S"+sj);
      init.push_back("P"+si+"_S"+sj+"':=false");
      update.push_back(s);
    }
  }
  
  s=not_stop;
  for (unsigned j=Nb_Part; j>=1; j--){
    if (j!=i){
      string sj(1,'0'+j);
      s+=" & Pr_"+si+"_"+sj+"_L="+sn_plus_1;
    }
  }
  for (unsigned j=Nb_Part; j>=1; j--){
    if (j!=i){
      string sj(1,'0'+j);
      s+=" & P"+si+"_S"+sj;
    }
  }
  s+=" -> P"+si+"_stop':=true";
  update.push_back(s);

  //receiving abort or recovery from T
  update.push_back("-- receiving abort ot recovery token");
  s="\t \t [] ~P"+si+"_stop & P"+si+"_contacted_T";
  s+=" & T_Abort_Send_P"+si+" -> P"+si+"_AbortToken':=true; P"+si+"_stop':=true";
  bool_external.push_back("T_Abort_Send_P"+si);
  reads.push_back("T_Abort_Send_P"+si);
  bool_interface.push_back("P"+si+"_AbortToken");
  controls.push_back("P"+si+"_AbortToken");
  reads.push_back("P"+si+"_AbortToken");
  init.push_back("P"+si+"_AbortToken':=false");
  update.push_back(s);

  s="\t \t [] ~P"+si+"_stop & P"+si+"_contacted_T";
  s+=" & T_Recovery_Send_P"+si+" -> ";

  for (unsigned j=Nb_Part; j>=1; j--)
    if (j!=i){
      string sj(1,'0'+j);
      s+="P"+si+"_S"+sj+"':=true; " ;
    }
  s+="P"+si+"_stop':=true"; 

  bool_external.push_back("T_Recovery_Send_P"+si);
  reads.push_back("T_Recovery_Send_P"+si);
  update.push_back(s);

  
  //dumping
  list<string> tmp;
  out<<"module P"<<i<<"H"<<endl;
  out<<"\t external"<<endl;

  tmp=range_external;
  while (range_external.size()>1){
    out<<" \t \t "<<range_external.front()<<","<<endl;
    range_external.pop_front();
  }
  if (range_external.size()==1){
    out<<" \t \t "<<range_external.front()<<" : (0.." << Nb_Part+1<<")";
    range_external.pop_front();
  }
  range_external=tmp;
  tmp=bool_external;
  if (bool_external.size()>0)
    out<<";";
  out<<endl;

  while (bool_external.size()>1){
    out<<" \t \t "<<bool_external.front()<<","<<endl;
    bool_external.pop_front();
  }
  if (bool_external.size()==1){
    out<<" \t \t "<<bool_external.front()<<" : bool" <<endl;
    bool_external.pop_front();
  }
  out<<endl;
  bool_external=tmp;
  
  // interface variables declaration
  
  out<<"\t interface"<<endl;
  tmp=range_interface;
  while (range_interface.size()>1){
    out<<" \t \t "<<range_interface.front()<<","<<endl;
    range_interface.pop_front();
  }
  if (range_interface.size()==1){
    out<<" \t \t "<<range_interface.front()<<" : (0.." << Nb_Part+1<<")";
    range_interface.pop_front();
  }
  range_interface=tmp;
  tmp=bool_interface;
  if (bool_interface.size()>0)
    out<<";";
  out<<endl;

  while (bool_interface.size()>1){
    out<<" \t \t "<<bool_interface.front()<<","<<endl;
    bool_interface.pop_front();
  }
  if (bool_interface.size()==1){
    out<<" \t \t "<<bool_interface.front()<<" : bool" <<endl;
    bool_interface.pop_front();
  }
  out<<endl;
  bool_interface=tmp;

  //atom
  out<<"\t atom"<<endl;

  //controls
  out<<"\t controls"<<endl;
  tmp=controls;
  while (controls.size()>1){
    out<<" \t \t "<<controls.front()<<","<<endl;
    controls.pop_front();
  }
  if (controls.size()==1){
    out<<" \t \t "<<controls.front();
    controls.pop_front();
  }
  out<<endl;
  controls=tmp;

  //reads
  out<<"\t reads"<<endl;
  tmp=reads;
  while (reads.size()>1){
    out<<" \t \t "<<reads.front()<<","<<endl;
    reads.pop_front();
  }
  if (reads.size()==1){
    out<<" \t \t "<<reads.front()<<endl;
    reads.pop_front();
  }
  out<<endl;
  reads=tmp;

  //init

  out<<"\t init"<<endl;
  tmp=init;
  out<<"\t\t [] true ->"<<endl;
  while (init.size()>1){
    out<<"\t \t \t "<<init.front()<<";"<<endl;
    init.pop_front();
  }
  if (init.size()==1){
    out<<"\t \t \t "<<init.front() <<endl;
    init.pop_front();
  }
  init=tmp;
  //update

  out<<"\t update"<<endl;
  while (update.size()>0){
    out<<update.front()<<endl;
    update.pop_front();
  }
  out<<endl;

  //endatom
    out<<"\t endatom"<<endl;
  //endmodule
    out<<"endmodule"<<endl<<endl<<endl;
}



void Protocol::write_dishonestP(unsigned i){

  string si(1,'0'+i);
  string si_plus_1(1,'0'+i+1);
  string si_minus_1(1,'0'+i-1);
  string si_minus_2(1,'0'+i-2);

  string sn(1,'0'+Nb_Part);
  string sn_plus_1(1,'0'+Nb_Part+1);  
  string sn_minus_1(1,'0'+Nb_Part-1);  

  string not_stop="\t \t [] ~P"+si+"_stop";

  // idle action and stop
  string s=not_stop + " ->";
  update.push_back("-- idle action and stop");
  update.push_back(s);
  update.push_back(s+" P"+si+"_stop':=true");

  //sending out promises
  update.push_back("-- sending out promises");
  for(unsigned j=1; j<i; j++){
    string sj(1,'0'+j);
    for(unsigned l=1; l<=Nb_Part+1; l++){
      string sl(1,'0'+l);
      s=not_stop+" & Pr_"+si+"_"+sj+"_L<"+sl+" ->";
      s+="Pr_"+si+"_"+sj+"_L':="+sl;
      update.push_back(s);
    }
  }

  for(unsigned j=i+1; j<=Nb_Part; j++){
    string sj(1,'0'+j);
    for(unsigned l=i; l<=Nb_Part+1; l++){
      string sl(1,'0'+l);
      s=not_stop+" & Pr_"+si+"_"+sj+"_L<"+sl+" ->";
      s+="Pr_"+si+"_"+sj+"_L':="+sl;
      update.push_back(s);
    }
  }

  //sending abort
  update.push_back("-- sending abort");
  if(i!=1){
    s=not_stop+" -> P"+si+"_Abort_Send':=true";
    update.push_back(s);
  }

  //sending recoveries
   update.push_back("-- sending recoveries");
   list<unsigned *> recs_i=recs[i];
   while (recs_i.size()>0){
     unsigned *ri=recs_i.front();
     s=not_stop;
     for (unsigned j=Nb_Part; j>=1; j--){
       if(j!=i){
 	 string sj(1,'0'+j);
 	 string sl(1,'0'+ri[j]-1);
 	 s+=" & Pr_"+sj+"_"+si+"_L>"+sl;
       }
     }
     s+=" -> P"+si+"_Recovery";
     for (unsigned j=Nb_Part; j>=1; j--)
       if(j!=i){
	 string sl(1,'0'+ri[j]);
	 s+="_"+sl;
       }
     s+="':=true";
     update.push_back(s);
     recs_i.pop_front();
   }




  // receiving signatures ...
  update.push_back("-- receiving signatures and stopping ...");

  for (unsigned j=Nb_Part; j>=1; j--){
    if (j!=i){
      s=not_stop;
      string sj(1,'0'+j);
      s+=" & Pr_"+sj+"_"+si+"_L="+sn_plus_1+" -> P"+si+"_S"+sj+"':=true" ;
      update.push_back(s);
    }
  }
  

  //receiving abort or recovery from T
  update.push_back("-- receiving abort ot recovery token");
  s=not_stop;
  s+=" & T_Abort_Send_P"+si+" -> P"+si+"_AbortToken':=true";
  update.push_back(s);

  s=not_stop;
  s+=" & T_Recovery_Send_P"+si+" ->";

  for (unsigned j=Nb_Part; j>=1; j--)
    if (j!=i){
      string sj(1,'0'+j);
      s+=" P"+si+"_S"+sj+"':=true;" ;
    }
  s.erase(s.length()-1,1);
  update.push_back(s);



  //dumping
  out<<"module P"<<i<<endl;
  out<<"\t external"<<endl;

  while (range_external.size()>1){
    out<<" \t \t "<<range_external.front()<<","<<endl;
    range_external.pop_front();
  }
  if (range_external.size()==1){
    out<<" \t \t "<<range_external.front()<<" : (0.." << Nb_Part+1<<")";
    range_external.pop_front();
  }
  if (bool_external.size()>0)
    out<<";";
  out<<endl;

  while (bool_external.size()>1){
    out<<" \t \t "<<bool_external.front()<<","<<endl;
    bool_external.pop_front();
  }
  if (bool_external.size()==1){
    out<<" \t \t "<<bool_external.front()<<" : bool" <<endl;
    bool_external.pop_front();
  }
  out<<endl;
  
  // interface variables declaration
  
  out<<"\t interface"<<endl;
  while (range_interface.size()>1){
    out<<" \t \t "<<range_interface.front()<<","<<endl;
    range_interface.pop_front();
  }
  if (range_interface.size()==1){
    out<<" \t \t "<<range_interface.front()<<" : (0.." << Nb_Part+1<<")";
    range_interface.pop_front();
  }
  if (bool_interface.size()>0)
    out<<";";
  out<<endl;

  while (bool_interface.size()>1){
    out<<" \t \t "<<bool_interface.front()<<","<<endl;
    bool_interface.pop_front();
  }
  if (bool_interface.size()==1){
    out<<" \t \t "<<bool_interface.front()<<" : bool" <<endl;
    bool_interface.pop_front();
  }
  out<<endl;

  //atom
  out<<"\t atom"<<endl;

  //controls
  out<<"\t controls"<<endl;
  while (controls.size()>1){
    out<<" \t \t "<<controls.front()<<","<<endl;
    controls.pop_front();
  }
  if (controls.size()==1){
    out<<" \t \t "<<controls.front();
    controls.pop_front();
  }
  out<<endl;

  //reads
  out<<"\t reads"<<endl;
  while (reads.size()>1){
    out<<" \t \t "<<reads.front()<<","<<endl;
    reads.pop_front();
  }
  if (reads.size()==1){
    out<<" \t \t "<<reads.front()<<endl;
    reads.pop_front();
  }
  out<<endl;

  //init

  out<<"\t init"<<endl;
  out<<"\t\t [] true ->"<<endl;
  while (init.size()>1){
    out<<"\t \t \t "<<init.front()<<";"<<endl;
    init.pop_front();
  }
  if (init.size()==1){
    out<<"\t \t \t "<<init.front() <<endl;
    init.pop_front();
  }
  //update

  out<<"\t update"<<endl;
  while (update.size()>0){
    out<<update.front()<<endl;
    update.pop_front();
  }
  out<<endl;

  //endatom
    out<<"\t endatom"<<endl;
  //endmodule
    out<<"endmodule"<<endl<<endl<<endl;
}

void Protocol::write_T( ){

  string guard="\t \t []";
  string s;
  
  bool_interface.push_back("T_Validated");
  controls.push_back("T_Validated");
  reads.push_back("T_Validated");
  init.push_back("T_Validated':=false");

  for (unsigned i=1; i<=Nb_Part; i++){
    string si(1,'0'+i);

    update.push_back("-- treating requests from "+si);

    bool_interface.push_back("T_Respond"+si);
    controls.push_back("T_Respond"+si);
    reads.push_back("T_Respond"+si);
    init.push_back("T_Respond"+si+"':=false");

    bool_interface.push_back("T_F"+si);
    controls.push_back("T_F"+si);
    reads.push_back("T_F"+si);
    init.push_back("T_F"+si+"':=false");

    bool_interface.push_back("T_S"+si);
    controls.push_back("T_S"+si);
    reads.push_back("T_S"+si);
    init.push_back("T_S"+si+"':=false");

    bool_interface.push_back("T_Recovery_Send_P"+si);
    controls.push_back("T_Recovery_Send_P"+si);
    reads.push_back("T_Recovery_Send_P"+si);
    init.push_back("T_Recovery_Send_P"+si+"':=false");

    bool_interface.push_back("T_Abort_Send_P"+si);
    controls.push_back("T_Abort_Send_P"+si);
    reads.push_back("T_Abort_Send_P"+si);
    init.push_back("T_Abort_Send_P"+si+"':=false");


    // Abort Request
    if (i!=1){
      update.push_back("-- treating abort from "+si);      
      update.push_back("-- case not validated and "+si+" > max(Sm)");
      s=guard+"~T_Respond"+si+" & P"+si+"_Abort_Send & ~T_Validated";
      for(unsigned j=Nb_Part; j>i; j--){
	string sj(1,'0'+j);
	s+=" & ~T_S"+sj;
      }
      s+=" -> ";
      for(unsigned j=Nb_Part; j>=1; j--){
	string sj(1,'0'+j);	
	s+="T_F"+sj+"':=false; ";
      }
      s+="T_S"+si+"':=true; T_Abort_Send_P"+si+"':=true; T_Respond"+si+"':=true";
      update.push_back(s);


      if (i!=Nb_Part){
	update.push_back("-- case not validated and "+si+" < max(Sm)");
	s=guard+"~T_Respond"+si+" & P"+si+"_Abort_Send & ~T_Validated & (";
	for(unsigned j=Nb_Part; j>i; j--){
	  string sj(1,'0'+j);
	  s+=" T_S"+sj+" |";
	}
	s.erase(s.length()-1,1);
	s+=")";	
	s+=" -> ";
	s+="T_S"+si+"':=true; T_Abort_Send_P"+si+"':=true; T_Respond"+si+"':=true";
	update.push_back(s);
      }
      

      update.push_back("-- case validated before");
      s=guard+"~T_Respond"+si+" & P"+si+"_Abort_Send & T_Validated ";
      s+=" -> ";
      s+="T_S"+si+"':=true; T_Recovery_Send_P"+si+"':=true; T_Respond"+si+"':=true";
      update.push_back(s);
      
      bool_external.push_back("P"+si+"_Abort_Send");
      reads.push_back("P"+si+"_Abort_Send");
    }
    
    //Recovery Request
    update.push_back("-- treating recovery from "+si);
    list<unsigned *> recs_i=recs[i];
    while (recs_i.size()>0){
      unsigned *ri=recs_i.front();
      string rec="P"+si+"_Recovery";
      for(unsigned j=Nb_Part; j>=1; j--)
	if (j!=i){
	  string skj(1,'0'+ri[j]);
	  rec+="_"+skj;
	};

      bool_external.push_back(rec);
      reads.push_back(rec);

      // Recovery 

      update.push_back("-- treating recovery "+rec);
      
      update.push_back("-- if first request");

      s=guard+" "+rec+" & ";
      for(unsigned j=Nb_Part; j>=1; j--){
	string sj(1,'0'+j);
	s+=" ~T_Respond"+sj+" &";
      };
      s.erase(s.length()-1,1);
      s+=" -> T_Recovery_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_Validated':=true";
      update.push_back(s);

      
      update.push_back("-- if validated before ");
      s=guard+" "+rec+" & "+"~T_Respond"+si+" & T_Validated";
      s+=" -> T_Recovery_Send_P"+si+"':=true; T_Respond"+si+"':=true";
      update.push_back(s);


      update.push_back("-- not first request, not validated");

      string s5=guard+" "+rec+" & ~T_Respond"+si+" & (";
      for(unsigned j=Nb_Part; j>=1; j--){
 	string sj(1,'0'+j);
 	s5+=" T_Respond"+sj+" |";
      };

      s5.erase(s5.length()-1,1);
      s5+=") & ~T_Validated";

      update.push_back("-- "+si+" not in Fm");
      
      string s5_1=s5+" & ~T_F"+si;
      string s5_1_1= s5_1+" & ";
      bool ok=false;
      for(unsigned l=1;l<=Nb_Part;l++)
	if (l!=i){
	  string sl(1,'0'+l);
	  for(unsigned j=1;j<=Nb_Part;j++)
	    if(j!=i && j>ri[l]){
	      if (!ok){
		ok=true; s5_1_1+="( ";
	      }
	      string sj(1,'0'+j);
	      s5_1_1+=" ( T_S"+sl+" & T_S"+sj+" ) |";
	    }
	}
      if (ok){
	s5_1_1.erase(s5_1_1.length()-1,1);
	s5_1_1+=")";

	if(i!=Nb_Part){
	  update.push_back("-- abort and max Sm > "+si);
	  for(unsigned j=Nb_Part; j>i; j--){
	    string sj(1,'0'+j);
	    string s5_1_1a=s5_1_1;	      
	    for(unsigned k=Nb_Part; k>j; k--){
	      string sk(1,'0'+k);
	      s5_1_1a+=" & ~T_S"+sk;
	    }
	    s5_1_1a+=" & T_S"+sj+" -> ";
	    for(unsigned l=1; l<=Nb_Part; l++)
	      if(ri[l]==j-1){
		string sl(1,'0'+l);
		s5_1_1a+="T_F"+sl+"':=true; ";
	      }
	    s5_1_1a+="T_S"+si+"':=true; T_Respond"+si+"':=true; T_Abort_Send_P"+si+"':=true";
	    update.push_back(s5_1_1a);
	  }
	}
	update.push_back("-- abort and max Sm < "+si);
	string s5_1_1b=s5_1_1;
	for(unsigned j=Nb_Part; j>i; j--){
	  string sj(1,'0'+j);
	  s5_1_1b+=" & ~T_S"+sj;
	}
	s5_1_1b+=" -> ";
	for(unsigned j=Nb_Part; j>=1; j--){
	  string sj(1,'0'+j);
	  s5_1_1b+="T_F"+sj+"':=false; ";
	}
	s5_1_1b+="T_S"+si+"':=true; T_Respond"+si+"':=true; T_Abort_Send_P"+si+"':=true";
	update.push_back(s5_1_1b);
      }

      update.push_back("-- overturn");
      string s5_1_2= s5_1;
      for(unsigned l=1;l<=Nb_Part;l++)
	if (l!=i){
	  string sl(1,'0'+l);
	  for(unsigned j=1;j<=Nb_Part;j++)
	    if(j!=i && j>ri[l]){
		string sj(1,'0'+j);
		s5_1_2+=" & ( ~T_S"+sl+" | ~T_S"+sj+" )";
	    }
	}
      s5_1_2+=" -> T_Recovery_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_Validated':=true";
      update.push_back(s5_1_2);

      //i in Fm
      update.push_back("-- i in Fm");
      string s5_2=s5+" & T_F"+si;

      for(unsigned a=Nb_Part; a>=1; a--)
	if (a!=i){
	  string s5_2_1= s5_2;
	  string sa(1,'0'+a);
	  for(unsigned b=Nb_Part; b>a; b--){
	    if (b!=i){
	      string sb(1,'0'+b);
	      s5_2_1+=" & ~T_S"+sb;
	    }
	  }
	  s5_2_1+=" & T_S"+sa;
	  bool ok=true;
	  for(unsigned j=i+1; j<=a && ok; j++)
	    ok=ri[j]>a;
	  for(unsigned j=1; j<i && ok; j++)
	    ok=ri[j]>=a;
	  if (ok){
	    update.push_back("-- overturn");
	    s5_2_1+=" -> T_Recovery_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_Validated':=true";
	    update.push_back(s5_2_1);
	  }
	  else{
	    if (a>i){
	      update.push_back("-- abort with i< max Sm");
	      s5_2_1+=" -> ";
	      for (unsigned j=1; j<=Nb_Part; j++)
		if (ri[j]==a-1){
		  string sj(1,'0'+j);
		  s5_2_1+="T_F"+sj+"':=true; ";
		}
	      s5_2_1+="T_Abort_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_S"+si+"':=true";
	      update.push_back(s5_2_1);
	    }
	    else{
	      update.push_back("-- abort with i > max Sm");
	      s5_2_1+=" -> ";
	      for (unsigned j=1; j<=Nb_Part; j++){
		string sj(1,'0'+j);
		s5_2_1+="T_F"+sj+"':=false; ";
	      }
	      s5_2_1+="T_Abort_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_S"+si+"':=true";
	      update.push_back(s5_2_1);
	    } 
	  }
	}
      
      recs_i.pop_front();
    }
    
  }





    


  //dumping
  out<<"module T"<<endl;
  out<<"\t external"<<endl;
  unsigned ln=range_external.size();
  while (range_external.size()>1){
    out<<" \t \t "<<range_external.front()<<","<<endl;
    range_external.pop_front();
  }
  if (range_external.size()==1){
    out<<" \t \t "<<range_external.front()<<" : (0.." << Nb_Part+1<<")";
    range_external.pop_front();
  }
  if (bool_external.size()>0 && ln>0)
    out<<";";
  out<<endl;

  while (bool_external.size()>1){
    out<<" \t \t "<<bool_external.front()<<","<<endl;
    bool_external.pop_front();
  }
  if (bool_external.size()==1){
    out<<" \t \t "<<bool_external.front()<<" : bool" <<endl;
    bool_external.pop_front();
  }
  out<<endl;
  
  // interface variables declaration
  
  out<<"\t interface"<<endl;
  ln=range_interface.size();
  while (range_interface.size()>1){
    out<<" \t \t "<<range_interface.front()<<","<<endl;
    range_interface.pop_front();
  }
  if (range_interface.size()==1){
    out<<" \t \t "<<range_interface.front()<<" : (0.." << Nb_Part+1<<")";
    range_interface.pop_front();
  }
  if (bool_interface.size()>0 && ln >0)
    out<<";";
  out<<endl;

  while (bool_interface.size()>1){
    out<<" \t \t "<<bool_interface.front()<<","<<endl;
    bool_interface.pop_front();
  }
  if (bool_interface.size()==1){
    out<<" \t \t "<<bool_interface.front()<<" : bool" <<endl;
    bool_interface.pop_front();
  }
  out<<endl;

  //atom
  out<<"\t atom"<<endl;

  //controls
  out<<"\t controls"<<endl;
  while (controls.size()>1){
    out<<" \t \t "<<controls.front()<<","<<endl;
    controls.pop_front();
  }
  if (controls.size()==1){
    out<<" \t \t "<<controls.front();
    controls.pop_front();
  }
  out<<endl;

  //reads
  out<<"\t reads"<<endl;
  while (reads.size()>1){
    out<<" \t \t "<<reads.front()<<","<<endl;
    reads.pop_front();
  }
  if (reads.size()==1){
    out<<" \t \t "<<reads.front()<<endl;
    reads.pop_front();
  }
  out<<endl;

  //init

  out<<"\t init"<<endl;
  out<<"\t\t [] true ->"<<endl;
  while (init.size()>1){
    out<<"\t \t \t "<<init.front()<<";"<<endl;
    init.pop_front();
  }
  if (init.size()==1){
    out<<"\t \t \t "<<init.front() <<endl;
    init.pop_front();
  }
  //update

  out<<"\t update"<<endl;
  while (update.size()>0){
    out<<update.front()<<endl;
    update.pop_front();
  }
  out<<endl;

  //endatom
    out<<"\t endatom"<<endl;
  //endmodule
    out<<"endmodule"<<endl<<endl<<endl;
}


void Protocol::write_System(unsigned i){
  out<<"System_"<<i<<"H := T";
  for(unsigned p=1; p<=Nb_Part; p++)
    if (p==i) out<<" || P"<<p<<"H";
    else out<<" || P"<<p;
  out<<endl;
}


int main(int argc, char **argv){
  if(argc!=3)
    cerr <<"Usage : ./a.out <number of participants> <output file>"<<endl;
  else{
    Protocol P(*argv[1]-'0', argv[2]);
  }
  return EXIT_SUCCESS;
}