File preview

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