Commit 6a677577 authored by Benoit Barbot's avatar Benoit Barbot

improve unfolding

parent b2126e3a
Pipeline #1051 passed with stages
in 13 minutes and 54 seconds
......@@ -18,7 +18,15 @@ test_cosmos "Philosopher color" "philo.grml" "--loop 1000" "--use-setdomain-imp
("MeanToken_Wait" , 7.96561444752);
("MeanToken_Eat" , 0.0105564222604);
("MeanToken_Fork" , 0.0132727079572);
]
];;
test_cosmos "Philosopher color unfold" "philo.grml" "" "--const N=8 --unfold philo_unfold.grml" [];;
test_cosmos "Philosopher color unfold " "philo_unfold.grml" "--loop 1000" "--max-run 20000"
[("Throughput_takeLeft_philo_IC_1",0.0132773335/.8.) ;
("Throughput_takeRight_philo_IC_1", 0.0052773335/.8.) ;
("Throughput_backToThink_philo_IC_1", 0.0052773335/.8.);
("MeanToken_Think_philo_IC_1", 0.0238291302177/.8.);
("MeanToken_Wait_philo_IC_1" , 7.96561444752/.8.);
("MeanToken_Eat_philo_IC_1" , 0.0105564222604/.8.);
("MeanToken_Fork_philo_IC_1" , 0.0132727079572/.8.);
];;
\ No newline at end of file
......@@ -49,6 +49,30 @@ void unfolder::export_grml(ofstream& fout){
fout << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" << endl;
fout << "<model formalismUrl=\"http://formalisms.cosyverif.org/sptgd-net.fml\" xmlns=\"http://cosyverif.org/ns/model\">" << endl;
fout << "\t<attribute name=\"declaration\"><attribute name=\"constants\">" << endl;
fout << "\t\t<attribute name=\"intConsts\">" <<endl;
for( let ci : IntConstant){
fout << "\t\t\t<attribute name=\"intConst\"><attribute name=\"name\">"<< endl;
fout << "\t\t\t\t" << ci.first << endl;
fout << "\t\t\t</attribute><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
fout << "\t\t\t\t" << ci.second << endl;
fout << "\t\t\t</attribute></attribute></attribute>" << endl;
}
fout << "\t\t</attribute>" << endl;
fout << "\t\t<attribute name=\"realConsts\">" <<endl;
for( let ci : RealConstant){
fout << "\t\t\t<attribute name=\"realConst\"><attribute name=\"name\">"<< endl;
fout << "\t\t\t\t" << ci.first << endl;
fout << "\t\t\t</attribute><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
fout << "\t\t\t\t" << ci.second << endl;
fout << "\t\t\t</attribute></attribute></attribute>" << endl;
}
fout << "\t\t</attribute>" << endl;
fout << "\t</attribute></attribute>" << endl;
for(let p: placeStruct)export_place_grml(fout,p);
for(let t: transitionStruct)export_transition_grml(fout,t);
......@@ -65,7 +89,7 @@ void unfolder::export_place_grml(ofstream &fout,const place &p){
fout << "\t<node id=\"" << get_uid("place"+str) << "\" nodeType=\"place\">"<< endl;
fout << "\t\t<attribute name=\"name\">" << str << "</attribute>" << endl;
fout << "\t\t<attribute name=\"marking\"><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
if(p.Marking.t == Int && p.Marking.intVal==0){
if((p.Marking.t == Int && p.Marking.intVal==0) || p.initMarking.empty()){
fout << "\t\t\t0" << endl;
} else if(p.colorDom != UNCOLORED_DOMAIN) {
fout << "\t\t\t1" << endl;
......@@ -87,15 +111,9 @@ void unfolder::export_transition_grml(ofstream &fout, const transition &t){
fout << "\t\t\t<attribute name=\"type\">" << t.dist.name ;
fout << "</attribute>" << endl;
for(auto &sparam : t.dist.Param){
fout << "\t\t\t<attribute name=\"param\"><attribute name=\"expr\">";
if(!sparam.is_concrete()){
fout << "<attribute name=\"numValue\">"<< endl;
fout << "\t\t\t\t" << sparam/*MyGspn.RealConstant.find(sparam)->second*/ << endl;
} else {
fout << "<attribute name=\"numValue\">" << endl;
fout << "\t\t\t\t" << sparam << endl;
}
fout << "\t\t\t</attribute></attribute></attribute>"<< endl;
fout << "\t\t\t<attribute name=\"param\">";
fout << sparam;
fout << "\t\t\t</attribute>"<< endl;
}
fout << "\t\t</attribute>" << endl;
fout << "\t</node>" << endl;
......@@ -108,9 +126,9 @@ void unfolder::print_arc(ofstream &fout,size_t arcuid,size_t truid, size_t pluid
if(dir){
fout << pluid << "\" target=\"" << truid << "\">";
}else fout << truid << "\" target=\"" << pluid << "\">";
fout << "<attribute name=\"valuation\"><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
fout << "<attribute name=\"valuation\">" << endl;
fout << "\t\t" << val << endl;
fout << "\t</attribute></attribute></attribute></arc>" << endl;
fout << "\t</attribute></arc>" << endl;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment