#include <iostream>
#include <string>
#include <stdio.h>
#include <stdlib.h>
#include <fstream>
#include <vector>

using namespace std;

ofstream *out;

void print(string str)
{
    (*out)<<str<<endl;
}

/*
string int2string(const int i){
  char chr[256];
  string str;
  sprintf(chr,"%i",i);
  str=chr;
  return str;
}*/

void spilt(std::string& sr, std::string delim, std::vector< std::string >* ret)
{
  size_t last = 0;
  string s=sr;
  size_t index = s.find(delim, last);
  while (index != std::string::npos)
  {
    //cout<<"begin:"<<last<<endl;
    //cout<<"end:"<<index<<endl;
    //cout<<s.substr(last, index - last)<<endl;
    ret->push_back(s.substr(last, index - last));
    last = index + delim.length() ;
    s=s.substr(last,s.size()-last);
    last=0;
    index = s.find(delim, last);
  }
  if (index - last>0)
  {
    ret->push_back(s);
    //ret->push_back(s.substr(last, index - last));
  }
}

string trim(string& s){
  const string drop=" ";
  s.erase(s.find_last_not_of(drop)+1);
  s[s.find_last_not_of(drop)+1]='\0';
  return s.erase(0,s.find_first_not_of(drop));
}

int main()
{

    int N;
    cout<<"Please input the number of cars:"<<endl;
    cin>>N;
    out=new ofstream("motorcar_"+to_string(N)+".xml");
    string head="<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n<sspaceex xmlns=\"http://www-verimag.imag.fr/xml-namespaces/sspaceex\" version=\"0.2\" math=\"SpaceEx\">";
    string foot="</sspaceex>";
    print(head);
    print("\t<component id=\"motorcar_template\">");
    for(unsigned i=0;i<N;i++)
    {
        string name="x_"+to_string(i+1);
        print("\t\t<param name=\""+name+"\" type=\"real\" local=\"false\" d1=\"1\" d2=\"1\" dynamics=\"any\" />");
    }

    for(unsigned i=0;i<3*(N-1);i++)
    {
        print("\t\t<param name=\"e"+to_string(i+1)+"\" type=\"label\" local=\"false\" />");
    }

    //loc 1
    {
        print("\t\t<location id=\"1\" name=\"v1\">");
        string invariant="";
        string flow="";
        for(unsigned i=0;i<N-1;i++){
            string name1="x_"+to_string(i+1);
            string name2="x_"+to_string(i+2);
            string tmp=name1+"-"+name2+"&gt;=2 &amp; "+name1+"-"+name2+"&lt;=10";
            if(invariant=="")
                invariant=tmp;
            else
                invariant=invariant+" &amp; "+tmp;
        }

        for(unsigned i=0;i<N;i++)
        {
            string name="x_"+to_string(i+1);
            string tmp=name+"'&lt;=10 &amp; "+name+"'&gt;=8";
            if(flow=="")
                flow=tmp;
            else
                flow=flow+" &amp; "+tmp;
        }
        print("\t\t\t<invariant>"+invariant+"</invariant>");
        print("\t\t\t<flow>"+flow+"</flow>");
        print("\t\t</location>");
    }
    //loc 2-N
    for(unsigned i=1;i<N;i++){
        print("\t\t<location id=\""+to_string(i+1)+"\" name=\"v"+to_string(i+1)+"\">");
        string invariant="";
        string flow="";
        for(unsigned j=0;j<N-1;j++){
            string name1="x_"+to_string(j+1);
            string name2="x_"+to_string(j+2);
            string tmp=name1+"-"+name2+"&gt;=0 &amp; "+name1+"-"+name2+"&lt;=10";
            if(invariant=="")
                invariant=tmp;
            else
                invariant=invariant+" &amp; "+tmp;
        }

        for(unsigned j=0;j<i;j++)
        {
            string name="x_"+to_string(j+1);
            string tmp=name+"'==12";
            if(flow=="")
                flow=tmp;
            else
                flow=flow+" &amp; "+tmp;
        }
        {
            string name="x_"+to_string(i+1);
            string tmp=name+"'==10";
            if(flow=="")
                flow=tmp;
            else
                flow=flow+" &amp; "+tmp;
        }
        for(unsigned j=i+1;j<N;j++)
        {
            string name="x_"+to_string(j+1);
            string tmp=name+"'&lt;=10 &amp; "+name+"'&gt;=8";
            if(flow=="")
                flow=tmp;
            else
                flow=flow+" &amp; "+tmp;
        }
        print("\t\t\t<invariant>"+invariant+"</invariant>");
        print("\t\t\t<flow>"+flow+"</flow>");
        print("\t\t</location>");
    }
    {
        print("\t\t<location id=\""+to_string(N+1)+"\" name=\"v"+to_string(N+1)+"\">");
        string flow="";


        for(unsigned i=0;i<N;i++)
        {
            string name="x_"+to_string(i+1);
            string tmp=name+"'==0";
            if(flow=="")
                flow=tmp;
            else
                flow=flow+" &amp; "+tmp;
        }
        print("\t\t\t<flow>"+flow+"</flow>");
        print("\t\t</location>");
    }
    int count=1;
   for(unsigned i=1;i<N;i++){


        string name1="x_"+to_string(i);
        string name2="x_"+to_string(i+1);
         print("\t\t<transition source=\"1\" target=\""+to_string(i+1)+"\">");
         print("\t\t\t<label>e"+to_string(count++)+"</label>");
         print("\t\t\t<guard>"+name1+"-"+name2+"&lt;=4</guard>");
         print("\t\t</transition>");

         print("\t\t<transition source=\""+to_string(i+1)+"\" target=\"1\">");
         print("\t\t\t<label>e"+to_string(count++)+"</label>");
         print("\t\t\t<guard>"+name1+"-"+name2+"&gt;=4</guard>");
         print("\t\t</transition>");

         print("\t\t<transition source=\""+to_string(i+1)+"\" target=\""+to_string(N+1)+"\">");
         print("\t\t\t<label>e"+to_string(count++)+"</label>");
         print("\t\t\t<guard>"+name1+"-"+name2+"&lt;=1</guard>");
         print("\t\t</transition>");
    }

    print("\t</component>");

    print("\t<component id=\"system\">");
    for(unsigned i=0;i<N;i++)
    {
        string name="x_"+to_string(i+1);
        print("\t\t<param name=\""+name+"\" type=\"real\" local=\"false\" d1=\"1\" d2=\"1\" dynamics=\"any\" />");
    }

    for(unsigned i=0;i<3*(N-1);i++)
    {
        print("\t\t<param name=\"e"+to_string(i+1)+"\" type=\"label\" local=\"false\" />");
    }
    print("\t\t<bind component=\"motorcar_template\" as=\"motorcar_"+to_string(N)+"\">");
    for(unsigned i=0;i<N;i++)
    {
        string name="x_"+to_string(i+1);
         print("\t\t\t<map key=\""+name+"\">"+name+"</map>");
    }
    for(unsigned i=0;i<3*(N-1);i++)
    {
        print("\t\t\t<map key=\"e"+to_string(i+1)+"\">e"+to_string(i+1)+"</map>");
    }

    print("\t\t</bind>");
    print("\t</component>");
    print(foot);
    out->close();
    /*
    out=new ofstream("/home/xefox/BACH/examples/motorcar_"+to_string(N)+".cfg");

    print("# analysis options");
    print("system = \"system\"");
    string init="";
    int v=20;
    for(int i=N-1;i>=0;i--)
    {
        string name="x_"+to_string(i+1);
        string tmp=name+"=="+to_string(v);
        v+=5;
        if(init=="")
            init=tmp;
        else
            init=tmp+" & "+init;
    }
    print("initially = \""+init+" & loc()==v1\"");
    print("forbidden=\"loc()==v"+to_string(N+1)+"\"");

    print("scenario = \"phaver\"");
    print("directions = \"uni32\"");
    print("sampling-time = 0.1");
    print("time-horizon = 40000");
    print("iter-max = 10");

    print("rel-err = 1.0e-12");
    print("abs-err = 1.0e-13");

    out->close();
    */
    return 0;
}