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

using namespace std;

class Protocol{
  unsigned Nb_Part;
  unsigned Nb_Rounds;

  ofstream out;

  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;
  Nb_Rounds=N+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::write_honestP(unsigned i){

  out<<"module P"<<i<<"H"<<endl;

  // external variables declaration

  out<<"\t external"<<endl;
  for (unsigned k=1; k<=Nb_Part; k++){
    if((i==Nb_Part && k==Nb_Part-1) || (k==Nb_Part && i!=Nb_Part))
      out<<"\t\t P"<<k<<"_"<<"R_Send : (0.."<<Nb_Rounds<<");"<<endl;
    else if(k!=i)      out<<"\t\t P"<<k<<"_"<<"R_Send,"<<endl;
  }
  out<<"\t\t T_Abort_Send_P"<<i<<","<<endl;		
  out<<"\t\t T_Recovery_Send_P"<<i<<" : bool"<<endl;
  
  // interface variables declaration
  
  out<<"\t interface"<<endl;
  out<<"\t\t P"<<i<<"_"<<"R_Send,"<<endl;  
  out<<"\t\t P"<<i<<"_Recovery  : (0.."<<Nb_Rounds<<");"<<endl;		
  out<<"\t\t P"<<i<<"_stop,"<<endl;
  out<<"\t\t P"<<i<<"_Contr,"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken : bool"<<endl;

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

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

  out<<"\t\t P"<<i<<"_"<<"R_Send,"<<endl;
  out<<"\t\t P"<<i<<"_Recovery,"<<endl;
  out<<"\t\t P"<<i<<"_stop,"<<endl;
  out<<"\t\t P"<<i<<"_Contr,"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken"<<endl;

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

  for (unsigned k=1; k<=Nb_Part; k++){
    if(k!=i)
      out<<"\t\t P"<<k<<"_"<<"R_Send,"<<endl;
  }
  out<<"\t\t T_Abort_Send_P"<<i<<","<<endl;		
  out<<"\t\t T_Recovery_Send_P"<<i<<","<<endl;
  out<<"\t\t P"<<i<<"_Recovery,"<<endl;
  out<<"\t\t P"<<i<<"_"<<"R_Send,"<<endl;
  out<<"\t\t P"<<i<<"_stop,"<<endl;
  out<<"\t\t P"<<i<<"_Contr,"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken"<<endl;

  //init

  out<<"\t init"<<endl;

  out<<"\t\t [] true ->"<<endl;
  out<<"\t\t P"<<i<<"_Recovery':=0;"<<endl;
  out<<"\t\t P"<<i<<"_"<<"R_Send':=0;"<<endl;
  out<<"\t\t P"<<i<<"_stop':=false;"<<endl;
  out<<"\t\t P"<<i<<"_Contr':=false;"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken':=false"<<endl;


  //update

  out<<"\t update"<<endl;

  out<<"\t \t [] ~P"<<i<<"_stop -> "<<endl;
  out<<endl;
  out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_R_Send=0) -> P"<<i<<"_R_Send':=1"<<endl;

  for(unsigned r=1; r<=Nb_Rounds; r++){
    if (r<Nb_Rounds){
      out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_Recovery=0) & (P"<<i<<"_R_Send="<<r<<")"<<endl<<"\t \t \t";
      for(unsigned p=1; p<=Nb_Part; p++)
	if(p!=i)
	  out<<" & (P"<<p<<"_R_Send>="<<r<<")";
      out<< endl <<"\t \t \t -> P"<<i<<"_R_Send':="<<r+1<<endl;
      
      out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_Recovery=0) & P"<<i<<"_R_Send="<<r<<" &"<<endl<<"\t \t \t (";
      for(unsigned p=1; p<=Nb_Part; p++)
	if(p!=i) {
	  out << "P"<<p<<"_R_Send<"<<r;
	  if (!(p==Nb_Part || (p==Nb_Part-1 && i==Nb_Part))) out <<" | ";
	}
      out<<") "<<endl<<"\t \t \t -> P"<<i<<"_Recovery':="<<r<<endl;
    }
    else{ //r==Nb_Rounds
      out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_Recovery=0)"<<endl<<"\t \t \t";
      for(unsigned p=1; p<=Nb_Part; p++)
	if(p==i)
	  out<<" & (P"<<p<<"_R_Send="<<r<<")";
	else
	  out<<" & (P"<<p<<"_R_Send>="<<r<<")";

      out<<endl<<"\t \t \t -> P"<<i<<"_stop':=true; P"<<i<<"_Contr':=true"<<endl;
      
      out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_Recovery=0) & P"<<i<<"_R_Send="<<r<<" &"<<endl<<"\t \t \t (";
      for(unsigned p=1; p<=Nb_Part; p++)
	if(p!=i) {
	  out << "(P"<<p<<"_R_Send<"<<r<<")";
	  if (!(p==Nb_Part || (p==Nb_Part-1 && i==Nb_Part))) out <<" | ";
	}
      out<<") "<<endl<<"\t \t \t -> P"<<i<<"_Recovery':="<<r<<endl;
    }
    out<<endl;
  }

  out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_Recovery>0) & T_Abort_Send_P"<<i<<" -> P"<<i<<"_stop':=true; P"<<i<<"_AbortToken':=true"<<endl;
  
  out<<"\t \t [] ~P"<<i<<"_stop & (P"<<i<<"_Recovery>0) & T_Recovery_Send_P"<<i<<" -> P"<<i<<"_stop':=true; P"<<i<<"_Contr':=true"<<endl;

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


void Protocol::write_dishonestP(unsigned i){

  out<<"module P"<<i<<endl;

  // external variables declaration

  out<<"\t external"<<endl;
  for (unsigned k=1; k<=Nb_Part; k++){
    if((i==Nb_Part && k==Nb_Part-1) || (k==Nb_Part && i!=Nb_Part))
      out<<"\t\t P"<<k<<"_"<<"R_Send : (0.."<<Nb_Rounds<<");"<<endl;
    else if(k!=i)      out<<"\t\t P"<<k<<"_"<<"R_Send,"<<endl;
  }
  out<<"\t\t T_Abort_Send_P"<<i<<","<<endl;		
  out<<"\t\t T_Recovery_Send_P"<<i<<" : bool"<<endl;
  
  // interface variables declaration
  
  out<<"\t interface"<<endl;
  out<<"\t\t P"<<i<<"_"<<"R_Send,"<<endl;  
  out<<"\t\t P"<<i<<"_Recovery  : (0.."<<Nb_Rounds<<");"<<endl;		
  out<<"\t\t P"<<i<<"_stop,"<<endl;
  out<<"\t\t P"<<i<<"_Contr,"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken : bool"<<endl;

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

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

  out<<"\t\t P"<<i<<"_"<<"R_Send,"<<endl;
  out<<"\t\t P"<<i<<"_Recovery,"<<endl;
  out<<"\t\t P"<<i<<"_stop,"<<endl;
  out<<"\t\t P"<<i<<"_Contr,"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken"<<endl;

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

  for (unsigned k=1; k<=Nb_Part; k++){
    if(k!=i)
      out<<"\t\t P"<<k<<"_"<<"R_Send,"<<endl;
  }
  out<<"\t\t T_Abort_Send_P"<<i<<","<<endl;		
  out<<"\t\t T_Recovery_Send_P"<<i<<","<<endl;
  out<<"\t\t P"<<i<<"_Recovery,"<<endl;
  out<<"\t\t P"<<i<<"_"<<"R_Send,"<<endl;
  out<<"\t\t P"<<i<<"_stop,"<<endl;
  out<<"\t\t P"<<i<<"_Contr,"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken"<<endl;

  //init

  out<<"\t init"<<endl;

  out<<"\t\t [] true ->"<<endl;
  out<<"\t\t P"<<i<<"_Recovery':=0;"<<endl;
  out<<"\t\t P"<<i<<"_"<<"R_Send':=0;"<<endl;
  out<<"\t\t P"<<i<<"_stop':=false;"<<endl;
  out<<"\t\t P"<<i<<"_Contr':=false;"<<endl;
  out<<"\t\t P"<<i<<"_AbortToken':=false"<<endl;

  //update

  out<<"\t update"<<endl;

  out<<"\t \t [] ~P"<<i<<"_stop -> "<<endl;
  out<<"\t \t [] ~P"<<i<<"_stop -> P"<<i<<"_stop':=true"<<endl;
  out<<"\t \t [] ~P"<<i<<"_stop -> P"<<i<<"_R_Send':=1"<<endl;
  out<<"\t \t [] ~P"<<i<<"_stop -> P"<<i<<"_Recovery':=1"<<endl;

  for(unsigned r=2; r<=Nb_Rounds; r++){
    out<<"\t \t [] ~P"<<i<<"_stop ";
    for(unsigned p=1; p<=Nb_Part; p++)
      if (p!=i)
	out<<"& (P"<<p<<"_R_Send>="<<r-1<<") ";
    out<<"-> P"<<i<<"_R_Send':="<<r<<endl;

    out<<"\t \t [] ~P"<<i<<"_stop ";
    for(unsigned p=1; p<=Nb_Part; p++)
      if (p!=i)
	out<<"& (P"<<p<<"_R_Send>="<<r-1<<") ";
    out<<"-> P"<<i<<"_Recovery':="<<r<<endl;
  }

  out<<"\t \t [] ~P"<<i<<"_stop ";
  for(unsigned p=1; p<=Nb_Part; p++)
    if (p!=i)
      out<<"& (P"<<p<<"_R_Send>="<<Nb_Rounds<<") ";
  out<<"-> P"<<i<<"_Contr':=true"<<endl;

  out<<"\t \t [] ~P"<<i<<"_stop & T_Abort_Send_P"<<i<<" -> P"<< i <<"_AbortToken':=true"<<endl;
  out<<"\t \t [] ~P"<<i<<"_stop & T_Recovery_Send_P"<<i<<" -> P"<< i <<"_Contr':=true"<<endl;

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

void Protocol::write_T( ){

  out<<"module T"<<endl;

  // external variables declaration
  
  out<<"\t external"<<endl;

  for(unsigned p=1; p<Nb_Part; p++)
    out<<"\t \t P"<<p<<"_Recovery,"<<endl;
  out<<"\t \t P"<<Nb_Part<<"_Recovery : (0.."<<Nb_Rounds<<")"<<endl;

  // interface variables declaration
  
  out<<"\t interface"<<endl;
 
  out<<"\t \t T_Abort : (0.."<<Nb_Rounds<<");"<<endl;

 // for(unsigned p=1; p<Nb_Part; p++)
 //   out<<"\t \t T_Abort_P"<<p<<","<<endl;
 // out<<"\t \t T_Abort_P"<<Nb_Part<<" : (0.."<<Nb_Rounds<<");"<<endl;
    
  for(unsigned p=1; p<=Nb_Part; p++)
    out<<"\t \t T_Abort_Send_P"<<p<<","<<endl;
  
  for(unsigned p=1; p<Nb_Part; p++)
    out<<"\t \t T_Recovery_Send_P"<<p<<","<<endl;
    out<<"\t \t T_Recovery_Send_P"<<Nb_Part<<" : bool"<< endl;
  
  //atom
  out<<"\t atom"<<endl;

  //controls

  out<<"\t controls"<<endl;

 // for(unsigned p=1; p<=Nb_Part; p++)
 //   out<<"\t \t T_Abort_P"<<p<<","<<endl;
   
  out<<"\t \t T_Abort,"<<endl;
   
  for(unsigned p=1; p<=Nb_Part; p++)
    out<<"\t \t T_Abort_Send_P"<<p<<","<<endl;
  
  for(unsigned p=1; p<Nb_Part; p++)
    out<<"\t \t T_Recovery_Send_P"<<p<<","<<endl;
  out<<"\t \t T_Recovery_Send_P"<<Nb_Part<<endl;
    

  //reads
  out<<"\t reads"<<endl;
  for(unsigned p=1; p<=Nb_Part; p++)
    out<<"\t \t P"<<p<<"_Recovery,"<<endl;

  //for(unsigned p=1; p<=Nb_Part; p++)
   // out<<"\t \t T_Abort_P"<<p<<","<<endl;
   out<<"\t \t T_Abort,"<<endl;   
  
  for(unsigned p=1; p<=Nb_Part; p++)
    out<<"\t \t T_Abort_Send_P"<<p<<","<<endl;
  
  for(unsigned p=1; p<Nb_Part; p++)
    out<<"\t \t T_Recovery_Send_P"<<p<<","<<endl;
  out<<"\t \t T_Recovery_Send_P"<<Nb_Part<<endl;


  //init

  out<<"\t init"<<endl;

  out<<"\t\t [] true ->"<<endl;

  //for(unsigned p=1; p<=Nb_Part; p++)
  //  out<<"\t \t T_Abort_P"<<p<<"':=0;"<<endl;
    
    out<<"\t \t T_Abort':=0;"<<endl;
  
  for(unsigned p=1; p<=Nb_Part; p++)
    out<<"\t \t T_Abort_Send_P"<<p<<"':=false;"<<endl;
  
  for(unsigned p=1; p<Nb_Part; p++)
    out<<"\t \t T_Recovery_Send_P"<<p<<"':=false;"<<endl;
  out<<"\t \t T_Recovery_Send_P"<<Nb_Part<<"':=false"<<endl;
  

  //update

  out<<"\t update"<<endl;


  // Recovery_R1

  for(unsigned p=1; p <= Nb_Part; p++){
    out<<"\t \t [] P"<<p<<"_Recovery=1 & ~(T_Abort_Send_P"<<p<<" | T_Recovery_Send_P"<<p<<") & ~";
  out<<"(";
  for(unsigned q=1; q<Nb_Part; q++)
    out << "T_Recovery_Send_P"<<q<<" | ";
  out<<"T_Recovery_Send_P"<<Nb_Part<<") & (T_Abort<1)";
  out<<" -> T_Abort_Send_P"<<p<<"':=true; T_Abort':= 1"<<endl;
// out<<" -> T_Abort_Send_P"<<p<<"':=true; T_Abort_P"<<p<<"':=1"<<endl;
  }

  for(unsigned p=1; p <= Nb_Part; p++){
    out<<"\t \t [] P"<<p<<"_Recovery=1 & ~(T_Abort_Send_P"<<p<<" | T_Recovery_Send_P"<<p<<") & ~";
  out<<"(";
  for(unsigned q=1; q<Nb_Part; q++)
    out << "T_Recovery_Send_P"<<q<<" | ";
  out<<"T_Recovery_Send_P"<<Nb_Part<<") & (T_Abort>=1)";
  out<<" -> T_Abort_Send_P"<<p<<"':=true"<<endl;
// out<<" -> T_Abort_Send_P"<<p<<"':=true; T_Abort_P"<<p<<"':=1"<<endl;
  }
  // Recovery_Ri

  for(unsigned r=2; r <= Nb_Rounds; r++){
    // Abort overturned
    for(unsigned p=1; p <= Nb_Part; p++){
      out<<endl <<"\t \t [] (P"<<p<<"_Recovery="<<r<<") & ~(T_Abort_Send_P"<<p<<" | T_Recovery_Send_P"<<p<<") & ~";
      out<<"(";
      for(unsigned q=1; q<Nb_Part; q++)
	out << "T_Recovery_Send_P"<<q<<" | ";
      out<<"T_Recovery_Send_P"<<Nb_Part<<") & (T_Abort <"<< r-1<<")";
      //out<<" &"<< endl; 
      //out<<"\t \t \t(";      
      //for (unsigned t=1; t< Nb_Part;t++)
      //      out<<"(T_Abort_P"<<t<<"=0|T_Abort_P"<<t<<"<"<<r-1<< ")&";
      //out<<"(T_Abort_P"<<Nb_Part<<"=0|T_Abort_P"<<Nb_Part<<"<"<<r-1<< "))";
      out<<endl<<"\t \t \t -> T_Recovery_Send_P"<<p<<"':=true"<<endl;
      }

    // Abort preserved T_Abort updated 
    for(unsigned p=1; p <= Nb_Part; p++){
      out<<endl<<"\t \t [] (P"<<p<<"_Recovery="<<r<<") & ~(T_Abort_Send_P"<<p<<" | T_Recovery_Send_P"<<p<<") & ~";
      out<<"(";
      for(unsigned q=1; q<Nb_Part; q++)
	out << "T_Recovery_Send_P"<<q<<" | ";
      out<<"T_Recovery_Send_P"<<Nb_Part<<") & (T_Abort ="<< r-1 <<")" ;
      //out<<" &" << endl;
      //out<<"\t \t \t ~(";     
      //for (unsigned t=1; t< Nb_Part;t++)  
      //      out<<"(T_Abort_P"<<t<<"=0|T_Abort_P"<<t<<"<"<<r-1<<")&";  
      //out<<"(T_Abort_P"<<Nb_Part<<"=0|T_Abort_P"<<Nb_Part<<"<"<<r-1<< "))";
     // out<<endl<<"\t \t \t-> T_Abort_Send_P"<<p<<"':=true; T_Abort_P"<<p<<"':="<<r<<endl;
      out<<endl<<"\t \t \t-> T_Abort_Send_P"<<p<<"':=true; T_Abort':="<<r<<endl;
      }
    // Abort preserved T_Abort not updated 
   for(unsigned p=1; p <= Nb_Part; p++){
      out<<endl<<"\t \t [] (P"<<p<<"_Recovery="<<r<<") & ~(T_Abort_Send_P"<<p<<" | T_Recovery_Send_P"<<p<<") & ~";
      out<<"(";
      for(unsigned q=1; q<Nb_Part; q++)
	out << "T_Recovery_Send_P"<<q<<" | ";
      out<<"T_Recovery_Send_P"<<Nb_Part<<") & (T_Abort >"<< r-1 <<")" ;
      //out<<" &" << endl;
      //out<<"\t \t \t ~(";     
      //for (unsigned t=1; t< Nb_Part;t++)  
      //      out<<"(T_Abort_P"<<t<<"=0|T_Abort_P"<<t<<"<"<<r-1<<")&";  
      //out<<"(T_Abort_P"<<Nb_Part<<"=0|T_Abort_P"<<Nb_Part<<"<"<<r-1<< "))";
     // out<<endl<<"\t \t \t-> T_Abort_Send_P"<<p<<"':=true; T_Abort_P"<<p<<"':="<<r<<endl;
      out<<endl<<"\t \t \t-> T_Abort_Send_P"<<p<<"':=true"<<endl;
     }}
  
// Validated preserved
  for(unsigned p=1; p <= Nb_Part; p++){
    out<<"\t \t [] ("<<"P"<<p<<"_Recovery>0)  & ~(T_Abort_Send_P"<<p<<" | T_Recovery_Send_P"<<p<<") & ";
    out<<"(";
    for(unsigned q=1; q<Nb_Part; q++)
      out << "T_Recovery_Send_P"<<q<<" | ";
    out<<"T_Recovery_Send_P"<<Nb_Part<<')';
    out<<" -> T_Recovery_Send_P"<<p<<"':=true"<<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;
}