#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+=")";

    //  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;j<=Nb_Part;j++)
      recoveries[j]=1;
    
    add_recovery(i, recoveries);
    s+=" -> ";
    string rec="P"+si+"_Recovery";
    for (unsigned j=Nb_Part;j>=1;j--){
      if(j!=i){
	string skj(1,'0'+recoveries[j]);
	rec+="_"+skj;
      }
    }
    s+="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(s);

    // (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;
    }
    
    // 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;
    
    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);
  }

  // (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");

    range_interface.push_back("T_h"+si);
    controls.push_back("T_h"+si);
    reads.push_back("T_h"+si);
    init.push_back("T_h"+si+"':=0");

    range_interface.push_back("T_l"+si);
    controls.push_back("T_l"+si);
    reads.push_back("T_l"+si);
    init.push_back("T_l"+si+"':=0");

    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");
      s=guard+"~T_Respond"+si+" & P"+si+"_Abort_Send & ~T_Validated";
      s+=" -> ";
      s+="T_S"+si+"':=true; T_Abort_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_h"+si+"':=0; T_l"+si+"':=1";
      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 & (";

      for (unsigned j=Nb_Part; j>i; j--){
 	string sj(1,'0'+j);
	string recj_minus_1(1, '0'+(ri[j]-1));
 	s5+=" (T_S"+sj+" & T_l"+sj+">"+recj_minus_1+" ) |";
      };
      for (unsigned j=i-1; j>=1; j--){
 	string sj(1,'0'+j);
	string recj_minus_1(1, '0'+ri[j]-1);
 	s5+=" (T_S"+sj+" & T_h"+sj+">"+recj_minus_1+" ) |";
      };

      s5.erase(s5.length()-1,1);
      s5+=") -> T_S"+si+"':=true; T_Abort_Send_P"+si+"':=true; T_Respond"+si+"':=true; ";

      if (i==1){
	string s51=s5;
	string rec_ki_plus_1(1,'0'+ri[i+1]);
	s51+=" T_h"+si+"':="+rec_ki_plus_1+"; ";
	s51+=" T_l"+si+"':=0";
	update.push_back(s51);
      }

      else if (i>1 && ri[i-1]==i-1){
	string s51=s5;
	s51+=" T_h"+si+"':=0; ";
	s51+=" T_l"+si+"':="+si;
	update.push_back(s51);
      }

      else if (i>1 && i<Nb_Part  && ri[i-1]>=i && ri[i-1]<=Nb_Part && ri[i+1] <= ri[i-1]){
	string s51=s5;
	string rec_ki_minus_1(1,'0'+ri[i-1]);
	s51+=" T_h"+si+"':="+rec_ki_minus_1+"; ";
	s51+=" T_l"+si+"':="+rec_ki_minus_1;
	update.push_back(s51);
      }

      else if (i>1 && i<Nb_Part  && ri[i-1]>=i && ri[i-1]<Nb_Part && ri[i+1] > ri[i-1]){
	string s51=s5;
	string rec_ki_minus_1(1,'0'+ri[i-1]);
	string rec_ki_minus_1_plus_1(1,'0'+(ri[i-1]+1));
	s51+=" T_h"+si+"':="+rec_ki_minus_1+"; ";
	s51+=" T_l"+si+"':="+rec_ki_minus_1_plus_1;
	update.push_back(s51);
      }

      else if (i>1 && i<Nb_Part  && ri[i-1]==Nb_Part && ri[i+1]==Nb_Part){
	string s51=s5;
	string s_n(1,'0'+Nb_Part);
	s51+=" T_h"+si+"':="+s_n+"; ";
	s51+=" T_l"+si+"':="+s_n;
	update.push_back(s51);
      }


      else if (i>1 && i<Nb_Part  && ri[i-1]==Nb_Part && ri[i+1]==Nb_Part+1){
	string s51=s5;
	string s_n_plus_1(1,'0'+(Nb_Part+1));
	s51+=" T_h"+si+"':="+s_n_plus_1+"; ";
	s51+=" T_l"+si+"':="+s_n_plus_1;
	update.push_back(s51);
      }


      else if (i==Nb_Part  && ri[i-1]==Nb_Part){
	string s51=s5;
	string s_n_plus_1(1,'0'+(Nb_Part+1));
	s51+=" T_h"+si+"':=0; ";
	s51+=" T_l"+si+"':="+s_n_plus_1;
	update.push_back(s51);
      }
      

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

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

      for (unsigned j=Nb_Part; j>i; j--){
 	string sj(1,'0'+j);
	string recj_minus_1(1, '0'+ri[j]-1);
 	s6+=" (T_S"+sj+" & T_l"+sj+">"+recj_minus_1+" ) |";
      };
      for (unsigned j=i-1; j>=1; j--){
 	string sj(1,'0'+j);
	string recj_minus_1(1, '0'+ri[j]-1);
 	s6+=" (T_S"+sj+" & T_h"+sj+">"+recj_minus_1+" ) |";
      };
      s6.erase(s6.length()-1,1);
      s6+=") -> T_Recovery_Send_P"+si+"':=true; T_Respond"+si+"':=true; T_Validated':=true";
      update.push_back(s6);

      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;
}