Line data Source code
1 : /*******************************************************************************
2 : * *
3 : * Cosmos:(C)oncept et (O)utils (S)tatistique pour les (Mo)deles *
4 : * (S)tochastiques *
5 : * *
6 : * Copyright (C) 2009-2012 LSV & LACL *
7 : * Authors: Paolo Ballarini Benoît Barbot & Hilal Djafri *
8 : * Website: http://www.lsv.ens-cachan.fr/Software/cosmos *
9 : * *
10 : * This program is free software; you can redistribute it and/or modify *
11 : * it under the terms of the GNU General Public License as published by *
12 : * the Free Software Foundation; either version 3 of the License, or *
13 : * (at your option) any later version. *
14 : * *
15 : * This program is distributed in the hope that it will be useful, *
16 : * but WITHOUT ANY WARRANTY; without even the implied warranty of *
17 : * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *
18 : * GNU General Public License for more details. *
19 : * *
20 : * You should have received a copy of the GNU General Public License along *
21 : * with this program; if not, write to the Free Software Foundation, Inc., *
22 : * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *
23 : * file unfolder.cpp created by Benoit Barbot on 10/01/14. *
24 : *******************************************************************************
25 : */
26 :
27 : #include <stdlib.h>
28 :
29 : #include "unfolder.hpp"
30 :
31 : using namespace std;
32 : using namespace xml_output;
33 :
34 384 : string unfolder::str_of_vect(const vector<color> &v,const string &smid)const {
35 384 : string acc;
36 768 : for( let s : v){
37 384 : acc += smid;
38 384 : acc += s.name;
39 : }
40 384 : return acc;
41 : }
42 :
43 0 : string unfolder::cleanstr(const string &str)const {
44 0 : if(str[0] == '(' && str[str.length()-1]==')') return str.substr(1,str.length()-2);
45 0 : return str;
46 : }
47 :
48 1 : void unfolder::export_grml(ofstream& fout){
49 1 : fout << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" << endl;
50 1 : fout << "<model formalismUrl=\"http://formalisms.cosyverif.org/sptgd-net.fml\" xmlns=\"http://cosyverif.org/ns/model\">" << endl;
51 :
52 1 : fout << "\t<attribute name=\"declaration\"><attribute name=\"constants\">" << endl;
53 :
54 1 : fout << "\t\t<attribute name=\"intConsts\">" <<endl;
55 2 : for( let ci : IntConstant){
56 1 : fout << "\t\t\t<attribute name=\"intConst\"><attribute name=\"name\">"<< endl;
57 1 : fout << "\t\t\t\t" << ci.first << endl;
58 1 : fout << "\t\t\t</attribute><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
59 1 : fout << "\t\t\t\t" << ci.second << endl;
60 1 : fout << "\t\t\t</attribute></attribute></attribute>" << endl;
61 : }
62 1 : fout << "\t\t</attribute>" << endl;
63 :
64 1 : fout << "\t\t<attribute name=\"realConsts\">" <<endl;
65 5 : for( let ci : RealConstant){
66 4 : fout << "\t\t\t<attribute name=\"realConst\"><attribute name=\"name\">"<< endl;
67 4 : fout << "\t\t\t\t" << ci.first << endl;
68 4 : fout << "\t\t\t</attribute><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
69 4 : fout << "\t\t\t\t" << ci.second << endl;
70 4 : fout << "\t\t\t</attribute></attribute></attribute>" << endl;
71 : }
72 1 : fout << "\t\t</attribute>" << endl;
73 :
74 1 : fout << "\t</attribute></attribute>" << endl;
75 :
76 1 : for(let p: placeStruct)export_place_grml(fout,p);
77 :
78 1 : for(let t: transitionStruct)export_transition_grml(fout,t);
79 :
80 1 : for(let t: transitionStruct)export_arc_grml(fout, t);
81 :
82 1 : fout << "</model>" << endl;
83 1 : cout << "Number of Places:" << nbPlace << "\tNumber of Transitions:" << nbTrans << "\tNumber of Arcs:" << nbArc << endl;
84 1 : }
85 :
86 4 : void unfolder::export_place_grml(ofstream &fout,const place &p){
87 40 : iterateDom(p.name, "_", "", "", "_", "", colDoms[p.colorDom], 0, [&](const string& str,const string&){
88 64 : nbPlace++;
89 192 : fout << "\t<node id=\"" << get_uid("place"+str) << "\" nodeType=\"place\">"<< endl;
90 32 : fout << "\t\t<attribute name=\"name\">" << str << "</attribute>" << endl;
91 32 : fout << "\t\t<attribute name=\"marking\"><attribute name=\"expr\"><attribute name=\"numValue\">" << endl;
92 48 : if((p.Marking.t == Int && p.Marking.intVal==0) || p.initMarking.empty()){
93 16 : fout << "\t\t\t0" << endl;
94 16 : } else if(p.colorDom != UNCOLORED_DOMAIN) {
95 16 : fout << "\t\t\t1" << endl;
96 : } else {
97 0 : fout << "\t\t\t" << p.Marking;
98 : }
99 32 : fout << "\t\t</attribute></attribute></attribute>" << endl;
100 32 : fout << "\t</node>" << endl;
101 :
102 36 : });
103 4 : }
104 :
105 3 : void unfolder::export_transition_grml(ofstream &fout, const transition &t){
106 30 : iterateVars(t.name , "_", "", t.varDomain , 0, [&](const string& str){
107 48 : nbTrans++;
108 240 : fout << "\t<node id=\"" << get_uid("transition"+str) << "\" nodeType=\"transition\">"<< endl;
109 24 : fout << "\t\t<attribute name=\"name\">" << str << "</attribute>" << endl;
110 24 : fout << "\t\t<attribute name=\"distribution\">" << endl;
111 72 : fout << "\t\t\t<attribute name=\"type\">" << t.dist.name ;
112 24 : fout << "</attribute>" << endl;
113 48 : for(auto &sparam : t.dist.Param){
114 24 : fout << "\t\t\t<attribute name=\"param\">";
115 24 : fout << sparam;
116 24 : fout << "\t\t\t</attribute>"<< endl;
117 : }
118 24 : fout << "\t\t</attribute>" << endl;
119 24 : fout << "\t</node>" << endl;
120 27 : });
121 3 : }
122 :
123 128 : void unfolder::print_arc(ofstream &fout,size_t arcuid,size_t truid, size_t pluid, bool dir, const expr &val){
124 128 : fout << "\t<arc id=\"" << arcuid;
125 128 : fout << "\" arcType=\"arc\" source=\"";
126 128 : if(dir){
127 40 : fout << pluid << "\" target=\"" << truid << "\">";
128 88 : }else fout << truid << "\" target=\"" << pluid << "\">";
129 128 : fout << "<attribute name=\"valuation\">" << endl;
130 128 : fout << "\t\t" << val << endl;
131 128 : fout << "\t</attribute></arc>" << endl;
132 128 : }
133 :
134 :
135 64 : void unfolder::export_coltoken(ofstream &fout,const vector<color> &vec,
136 : const coloredToken &coltoken,const transition &t,const place &p,bool dir){
137 64 : size_t truid = get_uid("transition"+t.name+str_of_vect(vec, "_"));
138 128 : vector<color> vec2;
139 128 : for ( size_t i =0 ; i != coltoken.field.size(); ++i) {
140 128 : colorClass cc = colClasses[vec[coltoken.field[i].intVal].cc];
141 : size_t col;
142 64 : if(coltoken.Flags[i] == CT_SINGLE_COLOR){
143 0 : col = coltoken.field[i].intVal;
144 64 : }else col = (vec[coltoken.field[i].intVal].id + coltoken.varIncrement[i] + cc.colors.size()) % cc.colors.size();
145 64 : vec2.push_back(cc.colors[col]);
146 : }
147 64 : size_t pluid = get_uid("place"+p.name+str_of_vect(vec2, "_"));
148 64 : nbArc++;
149 64 : size_t arcuid = get_uid("arcpre_"+t.name+str_of_vect(vec, "_")+"_"+p.name);
150 :
151 64 : print_arc(fout, arcuid, truid, pluid, dir, coltoken.mult);
152 64 : }
153 :
154 72 : void unfolder::export_multcoltok(ofstream &fout,const vector<color> &vec,const transition &t,const place &p, bool dir, const arc inoutarc){
155 72 : if (!inoutarc.isColored && !inoutarc.isEmpty) {
156 0 : size_t truid = get_uid("transition"+t.name+str_of_vect(vec, "_"));
157 0 : size_t pluid = get_uid("place"+p.name);
158 0 : size_t arcuid = get_uid("arcpre_"+t.name+str_of_vect(vec, "_")+"_"+p.name);
159 0 : print_arc(fout,arcuid,truid,pluid,dir,to_string(inoutarc.exprVal.intVal));
160 0 : return;
161 : }
162 144 : auto toklist = inoutarc.coloredVal;
163 72 : if(toklist.size() == 1 && !toklist[0].hasAll){
164 64 : export_coltoken(fout,vec,toklist[0],t,p,dir);
165 8 : } else if(toklist.size()>0){
166 16 : vector<color> iteratevec;
167 80 : iterateDomVec(iteratevec, colDoms[p.colorDom], 0, [&](const vector<color> &v){
168 128 : expr mult(0);
169 192 : for (auto coltoken: toklist) {
170 128 : bool match = true;
171 256 : for ( size_t i =0 ; i != coltoken.field.size(); ++i) {
172 128 : if(coltoken.Flags[i]!=CT_ALL){
173 128 : if(coltoken.Flags[i] != CT_SINGLE_REAL){
174 896 : colorClass cc = colClasses[vec[coltoken.field[i].intVal].cc];
175 : size_t col;
176 128 : if(coltoken.Flags[i] == CT_SINGLE_COLOR){
177 0 : col = coltoken.field[i].intVal;
178 256 : }else col = (vec[coltoken.field[i].intVal].id + coltoken.varIncrement[i] + cc.colors.size()) % cc.colors.size();
179 128 : if(col != v[i].id)match=false;
180 : }else{
181 0 : cerr << "Cannot unfold unbounded domain";
182 0 : exit(EXIT_FAILURE);
183 : }
184 : }
185 : }
186 128 : if(match)mult = expr(Plus,mult,coltoken.mult);
187 : }
188 64 : mult.eval();
189 64 : if(!mult.empty() || (mult.t == Int && mult.intVal != 0) ){
190 64 : nbArc++;
191 256 : size_t truid = get_uid("transition"+t.name+str_of_vect(vec, "_"));
192 192 : size_t pluid = get_uid("place"+p.name+str_of_vect(v, "_"));
193 256 : size_t arcuid = get_uid("arcpre_"+t.name+str_of_vect(vec, "_")+"_"+p.name);
194 128 : print_arc(fout,arcuid,truid,pluid,dir,mult);
195 : }
196 72 : });
197 : }
198 : }
199 :
200 :
201 3 : void unfolder::export_arc_grml(ofstream &fout, const transition &t){
202 6 : vector<color> iteratevec;
203 30 : iterateVars(iteratevec , t.varDomain , 0, [&](const vector<color> &vec){
204 384 : for(const auto &p: placeStruct){
205 456 : auto a = access(inArcsStruct,t.id,p.id);
206 208 : if (!a.isEmpty)export_multcoltok(fout,vec,t,p,true,a);
207 384 : auto b = access(outArcsStruct,t.id,p.id);
208 128 : if (!b.isEmpty)export_multcoltok(fout,vec,t,p,false,b);
209 : }
210 27 : });
211 108 : }
212 :
213 :
214 :
215 :
|
