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 Gspn-Grml-Output.cpp *
24 : * Created by Benoit Barbot on 02/11/2015. *
25 : *******************************************************************************
26 : */
27 :
28 : #include "Gspn-Grml-Output.hpp"
29 :
30 : using namespace std;
31 : using namespace xml_output;
32 :
33 : namespace xml_output {
34 0 : ostream& operator<<(ostream & os, GspnGrmlOutput& gspn){
35 0 : os << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" << endl;
36 0 : os << "<model formalismUrl=\"http://formalisms.cosyverif.org/sptgd-net.fml\" xmlns=\"http://cosyverif.org/ns/model\">" << endl;
37 :
38 0 : os << "\t<attribute name=\"declaration\">" << endl;
39 0 : os << "\t\t<attribute name=\"constants\">" << endl;
40 0 : if(!gspn.IntConstant.empty()){
41 0 : os << "\t\t\t<attribute name=\"intConsts\">"<< endl;
42 0 : for(let n: gspn.IntConstant){
43 0 : os << "\t\t\t\t<attribute name=\"intConst\"><attribute name=\"name\">";
44 0 : os << n.first << "</attribute><attribute name=\"expr\"><attribute name=\"numValue\">";
45 0 : os << n.second << "</attribute></attribute></attribute>" << endl;
46 : }
47 0 : os << "\t\t\t</attribute>"<< endl;
48 : }
49 0 : if(!gspn.RealConstant.empty()){
50 0 : os << "\t\t\t<attribute name=\"realConsts\">"<< endl;
51 0 : for(let n: gspn.RealConstant){
52 0 : os << "\t\t\t\t<attribute name=\"realConst\"><attribute name=\"name\">";
53 0 : os << n.first << "</attribute><attribute name=\"expr\"><attribute name=\"numValue\">";
54 0 : os << n.second << "</attribute></attribute></attribute>" << endl;
55 : }
56 0 : os << "\t\t\t</attribute>"<< endl;
57 : }
58 0 : os << "\t\t</attribute>" << endl;
59 :
60 :
61 0 : for(let c: gspn.colClasses){
62 0 : os << "\t\t<attribute name=\"classDeclaration\">";
63 0 : os << "<attribute name=\"name\">" << c.name << "</attribute>" << endl;
64 0 : os << "\t\t\t<attribute name=\"classType\">";
65 0 : if(c.intIntervalName.empty()){
66 0 : os << "<attribute name=\"classEnum\">"<< endl;;
67 0 : for(let cc :c.colors)os << "<attribute name=\"enumValue\">"<< cc.name << "</attribute>";
68 : }else{
69 0 : os << "<attribute name=\"classIntInterval\">"<< endl;;
70 0 : os << "\t\t\t\t<attribute name=\"lowerBound\">" << expr(1) << "</attribute>" << endl;
71 0 : os << "\t\t\t\t<attribute name=\"higherBound\">" << expr((int)c.colors.size()) << "</attribute>" << endl;
72 0 : os << "\t\t\t</attribute></attribute>" << endl;
73 : }
74 0 : os << "\t\t\t<attribute name=\"circular\">" << boolalpha << (c.type == ColorClassType::Cyclic) << "</attribute>"<<endl;
75 0 : os << "\t\t</attribute>" << endl;
76 : }
77 :
78 0 : for(let v: gspn.colVars){
79 0 : os << "\t\t<attribute name=\"variableDeclaration\">";
80 0 : os << "<attribute name=\"name\">" << v.name << "</attribute>" << endl;
81 0 : os << "<attribute name=\"type\">" << gspn.colDoms[v.type].name << "</attribute>" << endl;
82 0 : os << "\t\t</attribute>" << endl;
83 : }
84 :
85 0 : os << "\t</attribute>" << endl;
86 :
87 0 : for(let p: gspn.placeStruct)gspn.printPlace(os,p);
88 0 : for(let t: gspn.transitionStruct)gspn.printTransition(os,t);
89 0 : for(let inarc : gspn.inArcsStruct)
90 0 : gspn.printArc(os, make_pair(
91 0 : gspn.get_uid("P_"+to_string(inarc.first.second)),
92 0 : gspn.get_uid("T_"+to_string(inarc.first.first))),
93 0 : inarc.second, false, gspn.placeStruct[inarc.first.first].colorDom);
94 0 : for(let outarc : gspn.outArcsStruct)
95 0 : gspn.printArc(os, make_pair(
96 0 : gspn.get_uid("T_"+to_string(outarc.first.first)),
97 0 : gspn.get_uid("P_"+to_string(outarc.first.second))),
98 0 : outarc.second, false,gspn.placeStruct[outarc.first.first].colorDom);
99 0 : for(let inhibarc : gspn.inhibArcsStruct)
100 0 : gspn.printArc(os, make_pair(
101 0 : gspn.get_uid("P_"+to_string(inhibarc.first.second)),
102 0 : gspn.get_uid("T_"+to_string(inhibarc.first.first))),
103 0 : inhibarc.second, true, gspn.placeStruct[inhibarc.first.first].colorDom);
104 0 : os << "</model>" << endl;
105 0 : return os;
106 : }
107 :
108 :
109 0 : ostream& operator<<(ostream & os, const Distribution& d){
110 0 : os << "\t\t<attribute name=\"distribution\">" << endl;
111 0 : os << "\t\t\t<attribute name=\"type\">" << d.name << "</attribute>"<< endl;
112 0 : for( let p : d.Param){
113 0 : os << "\t\t\t<attribute name=\"param\">" << p << "</attribute>"<< endl;
114 : }
115 0 : os << "\t\t</attribute>"<< endl;
116 0 : return os;
117 : }
118 : }
119 :
120 0 : void GspnGrmlOutput::printToken(ostream& os, const coloredToken& c,size_t cd){
121 0 : if( c.mult.is_zero())return;
122 0 : os << "\t\t\t<attribute name=\"token\">" << endl;
123 0 : os << "\t\t\t\t<attribute name=\"occurs\">" << c.mult << "</attribute>" << endl;
124 0 : if(cd != UNCOLORED_DOMAIN){
125 0 : os << "\t\t\t\t<attribute name=\"tokenProfile\"><attribute name=\"expr\">"<<endl;
126 0 : if(c.hasAll){
127 0 : os << "\t\t\t\t\t<attribute name=\"function\"><attribute name=\"all\"><attribute name=\"type\">";
128 0 : os << colDoms[cd].name;
129 0 : os << "</attribute></attribute></attribute>" << endl;
130 : }else{
131 0 : os << "\t\t\t\t\t<attribute name=\"expr\">" << endl;
132 0 : for(size_t i =0 ; i < c.field.size(); i++)
133 0 : switch (c.Flags[i]){
134 : case CT_VARIABLE:
135 0 : if( c.varIncrement[i] == 0 ){
136 0 : os << "\t\t\t\t\t<attribute name=\"name\">";
137 0 : os << colVars[c.field[i].intVal].name;
138 0 : os << "</attribute>"<<endl;
139 : }else{
140 0 : os << "\t\t\t\t\t<attribute name=\"function\"><attribute name=\"++\">" << endl;
141 0 : os << "\t\t\t\t\t\t<attribute name=\"name\">";
142 0 : os << colVars[c.field[i].intVal].name;
143 0 : os << "</attribute>"<< endl;
144 0 : os << "\t\t\t\t\t\t<attribute name=\"intValue\">";
145 0 : os << c.varIncrement[i];
146 0 : os << "</attribute>"<< endl;
147 0 : os << "\t\t\t\t\t</attribute></attribute>"<< endl;
148 : }
149 0 : break;
150 : default:
151 0 : os << "<FAILFAIL>";
152 : }
153 0 : os << "\t\t\t\t\t</attribute>"<< endl;
154 : }
155 0 : os << "\t\t\t\t</attribute></attribute>"<<endl;
156 : }
157 0 : os << "\t\t\t</attribute>" << endl;
158 : }
159 :
160 0 : void GspnGrmlOutput::printArc(ostream& os, const pair<size_t,size_t>& p, const arc& a, bool isInhib, size_t cd){
161 0 : os << "\t<arc id=\""<< GspnType::new_uid("Arc") << "\" ";
162 0 : os << "arcType=\"" <<(isInhib? "inhibitorarc":"arc") << "\" ";
163 0 : os << "source=\"" << p.first << "\" ";
164 0 : os << "target=\"" << p.second << "\" ";
165 0 : os << ">"<<endl;
166 0 : os << "\t\t<attribute name=\"valuation\">";
167 0 : if(!a.isColored){
168 0 : os << "<attribute name=\"numValue\">" << a.coloredVal[0].mult << "</attribute>"<<endl;
169 : } else {
170 0 : os << endl;
171 0 : for (let t: a.coloredVal) {
172 0 : printToken(os, t, cd);
173 : }
174 : }
175 0 : os << "\t\t</attribute>" << endl;
176 0 : os << "\t</arc>"<< endl;
177 0 : }
178 :
179 0 : void GspnGrmlOutput::printTransition(ostream& os, const transition& t){
180 0 : os << "\t<node id=\""<< GspnType::get_uid("T_"+ to_string(t.id)) << "\" nodeType=\"transition\">"<<endl;
181 0 : os << "\t\t<attribute name=\"name\">" + t.name + "</attribute>"<< endl;
182 0 : os << "\t\t<attribute name=\"weight\">" << t.weight << "</attribute>" << endl;
183 0 : os << "\t\t<attribute name=\"guard\">" << t.guard << "</attribute>" << endl;
184 0 : os << "\t\t<attribute name=\"priority\">" << t.priority << "</attribute>" << endl;
185 0 : os << "\t\t<attribute name=\"service\">" << expr(t.nbServers) << "</attribute>" << endl;
186 0 : os << t.dist ;
187 0 : os << "\t</node>"<< endl;
188 0 : }
189 :
190 :
191 0 : void GspnGrmlOutput::printPlace(ostream& os, const place& p){
192 0 : os << "\t<node id=\""<< GspnType::get_uid("P_"+ to_string(p.id)) << "\" nodeType=\"place\">"<<endl;
193 0 : os << "\t\t<attribute name=\"name\">" + p.name + "</attribute>"<< endl;
194 0 : if(p.colorDom != UNCOLORED_DOMAIN){
195 0 : os << "\t\t<attribute name=\"domain\"><attribute name=\"type\">";
196 0 : os << colDoms[p.colorDom].name;
197 0 : os << "</attribute></attribute>" << endl;
198 : }
199 0 : os << "\t\t<attribute name=\"marking\">";
200 0 : if(p.colorDom == UNCOLORED_DOMAIN){
201 0 : os << "<attribute name=\"numValue\">" << p.initMarking[0].mult << "</attribute>"<<endl;
202 : } else {
203 0 : os << endl;
204 0 : for (let t: p.initMarking) {
205 0 : printToken(os, t,p.colorDom);
206 : }
207 : }
208 0 : os << "\t\t</attribute>" << endl;
209 0 : os << "\t</node>"<< endl;
210 105 : }
|
