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 & 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 : *******************************************************************************
24 : */
25 :
26 : #include "Lha-Reader.hpp"
27 : #include "Lha_gmlparser.hpp"
28 : #include "../casesWriter.hpp"
29 :
30 : #include "string.h"
31 :
32 : #include <string>
33 : #include <sstream>
34 : #include <fstream>
35 : #include <set>
36 : #include <algorithm>
37 : #include <list>
38 :
39 :
40 :
41 :
42 : using namespace std;
43 :
44 33 : LhaType::LhaType(GspnType& Mspn) : MyGspn(&Mspn),NbLoc(0),isDeterministic(true) {
45 51 : for (auto it= MyGspn->IntConstant.begin(); it!= MyGspn->IntConstant.end() ; ++it){
46 18 : LhaRealConstant[it->first]=it->second;
47 18 : LhaIntConstant[it->first]=it->second;
48 : }
49 128 : for (auto it= MyGspn->RealConstant.begin(); it!= MyGspn->RealConstant.end() ; ++it){
50 95 : LhaRealConstant[it->first]=it->second;
51 : }
52 33 : }
53 :
54 :
55 33 : Lha_Reader::Lha_Reader(GspnType& mspn,parameters &Q) : MyLha(mspn),P(Q){
56 33 : trace_scanning = false;
57 33 : trace_parsing = false;
58 :
59 33 : }
60 :
61 33 : Lha_Reader::~Lha_Reader() {
62 33 : }
63 :
64 462 : string Lha_Reader::funDecl(const string& funtype) const{
65 462 : return "template<class DEDState>\n"+funtype+ " LHA<DEDState>::";
66 : }
67 :
68 29 : int Lha_Reader::parse(string& expr) {
69 29 : scan_expression(expr);
70 :
71 58 : lha::Lha_parser parser(*this);
72 :
73 29 : parser.set_debug_level(trace_parsing);
74 :
75 29 : int res = parser.parse();
76 29 : scan_end();
77 58 : return res;
78 : }
79 :
80 27 : int Lha_Reader::parse_file(parameters& P) {
81 54 : string str;
82 27 : MyLha.ConfidenceLevel=P.Level;
83 :
84 54 : ifstream file(P.PathLha.c_str(), ios::in);
85 27 : if (file) {
86 :
87 :
88 1753 : while (!file.eof()) {
89 :
90 1726 : string str2;
91 863 : getline(file, str2);
92 863 : str = str + "\n" + str2;
93 : }
94 :
95 27 : int x = parse(str);
96 27 : if (x) cout << "Parsing LHA description file failed" << endl;
97 :
98 :
99 27 : return x;
100 : } else {
101 0 : cout << "Can't open : " << P.PathLha << endl;
102 0 : return 1;
103 : }
104 : }
105 6 : int Lha_Reader::parse_gml_file(parameters& P) {
106 6 : MyLha.ConfidenceLevel=P.Level;
107 12 : ifstream ifile(P.PathLha.c_str());
108 6 : if(ifile){
109 : //cout << "parse GML:" << filename << endl;
110 12 : ModelHandlerPtr handlerPtr(new MyLhaModelHandler(&MyLha,P));
111 12 : ExpatModelParser parser = ExpatModelParser(handlerPtr);
112 6 : parser.parse_file(P.PathLha);
113 : //cout << "end parse GML"<< endl;
114 12 : return 0;
115 : }else{
116 0 : cout << "File " << P.PathLha << " does not exist!" << endl;
117 0 : exit(EXIT_FAILURE);
118 : }
119 :
120 :
121 : }
122 :
123 0 : bool is_simple(const string &s){
124 0 : return (s.find(" ") == string::npos
125 0 : && s.find("+") == string::npos
126 0 : && s.find("*") == string::npos
127 0 : && s.find("/") == string::npos
128 0 : && s.find("-") == string::npos
129 0 : && s.find(",") == string::npos
130 0 : && s.find("(") == string::npos
131 0 : && s.find(")") == string::npos);
132 : }
133 :
134 0 : string Lha_Reader::InvRelOp(const string& str)const {
135 0 : if (str == "<=") return ">=";
136 0 : if (str == ">=") return "<=";
137 0 : cerr << "Fail to inverse RelOp"<< endl;
138 0 : exit(EXIT_FAILURE);
139 : }
140 :
141 : void
142 0 : Lha_Reader::error(const lha::location& l, const std::string& m) {
143 0 : std::cerr << l << ": " << m << std::endl;
144 0 : }
145 :
146 : void
147 0 : Lha_Reader::error(const std::string& m) {
148 0 : std::cerr << m << std::endl;
149 0 : }
150 :
151 0 : void Lha_Reader::view() {
152 :
153 :
154 0 : }
155 :
156 33 : void Lha_Reader::WriteFile(parameters& P)const {
157 66 : string Pref = P.tmpPath;
158 :
159 66 : string loc;
160 :
161 : //loc = Pref + "../SOURCES/Cosmos/LHA.cpp";
162 33 : loc = Pref + "/LHA.cpp";
163 :
164 66 : ofstream LhaCppFile(loc.c_str(), ios::out | ios::trunc);
165 :
166 33 : LhaCppFile << "#include <iostream>" << endl;
167 33 : LhaCppFile << "#include <algorithm>" << endl;
168 33 : LhaCppFile << "#include <vector>" << endl;
169 :
170 33 : LhaCppFile << "using namespace std;" << endl;
171 :
172 33 : LhaCppFile << "#include \"markingImpl.hpp\"" << endl;
173 33 : if(P.modelType == External || P.modelType == GSPN_Simulink){
174 0 : LhaCppFile << "#include \"stateImpl.hpp\"" << endl;
175 : }
176 33 : LhaCppFile << "#include <math.h>" << endl;
177 33 : LhaCppFile << "#include <float.h>" << endl;
178 33 : LhaCppFile << "#include \"LHA.hpp\"" << endl;
179 :
180 185 : for (let it : MyLha.LhaRealConstant) {
181 152 : LhaCppFile << " const double " << it.first << "=" << it.second << ";" << endl;
182 : }
183 :
184 33 : LhaCppFile << "namespace hybridVar {\n";
185 33 : for (let it : MyLha.LhaRealHybrid) {
186 0 : if (MyLha.LhaIntHybrid.find(it.first)!=MyLha.LhaIntHybrid.end()) {
187 0 : LhaCppFile << "\textern int " << it.first << ";\n";
188 : }
189 : else {
190 0 : LhaCppFile << "\textern double " << it.first << ";\n";
191 : }
192 : }
193 33 : LhaCppFile << "};\n";
194 :
195 33 : LhaCppFile << "struct Variables {\n";
196 274 : for(size_t v =0 ; v< MyLha.Vars.type.size(); v++){
197 241 : if(MyLha.Vars.type[v] == COLOR_VARIABLE){
198 2 : LhaCppFile << "\t" << MyLha.MyGspn->colClasses[MyLha.Vars.colorDomain[v]].cname() << " " << MyLha.Vars.label[v] << ";\n";
199 239 : }else if(MyLha.Vars.type[v] == INT_INDEXED_DISC_ARRAY){
200 0 : LhaCppFile << "\tdouble "<< MyLha.Vars.label[v];
201 0 : LhaCppFile << "[ " << MyLha.Vars.colorDomain[v] << " ];" << endl;
202 239 : }else if(MyLha.Vars.colorDomain[v] != UNCOLORED_DOMAIN){
203 0 : LhaCppFile << "\tdouble "<< MyLha.Vars.label[v];
204 0 : colorDomain coldom = MyLha.MyGspn->colDoms[MyLha.Vars.colorDomain[v]];
205 :
206 0 : for (vector<size_t>::const_iterator itcol = coldom.colorClassIndex.begin();
207 0 : itcol != coldom.colorClassIndex.end(); ++itcol ) {
208 0 : LhaCppFile << "[ Color_" << MyLha.MyGspn->colClasses[*itcol].name << "_Total ]";
209 : }
210 0 : LhaCppFile << ";\n";
211 :
212 239 : } else LhaCppFile << "\tdouble "<< MyLha.Vars.label[v] << ";\n";
213 : }
214 33 : LhaCppFile << "};\n";
215 :
216 33 : LhaCppFile << "bool varOrder(const Variables &v1,const Variables &v2){\n";
217 274 : for(size_t v =0 ; v< MyLha.Vars.type.size(); v++){
218 241 : if(MyLha.Vars.type[v] == COLOR_VARIABLE){
219 2 : LhaCppFile << "\tcerr << \"Not yet supported\";\n";
220 239 : }else if(MyLha.Vars.type[v] == INT_INDEXED_DISC_ARRAY){
221 0 : LhaCppFile << "\tfor(unsigned int i =0; i<" << MyLha.Vars.colorDomain[v] << ";i++)";
222 0 : LhaCppFile << "if(v1."<<MyLha.Vars.label[v]<<"[i]<v2."<<MyLha.Vars.label[v]<<"[i])return true;"<< endl;
223 239 : } else LhaCppFile << "\tif(v1."<<MyLha.Vars.label[v]<<"<v2."<<MyLha.Vars.label[v]<<")return true;"<< endl;
224 : }
225 33 : LhaCppFile << "\treturn false;\n};\n";
226 :
227 :
228 33 : LhaCppFile << funDecl("void") << "resetVariables(){\n";
229 274 : for(size_t v= 0 ; v < MyLha.Vars.type.size(); v++){
230 241 : if(MyLha.Vars.type[v] == COLOR_VARIABLE){
231 2 : LhaCppFile << "\tVars->" << MyLha.Vars.label[v] << "= Color_" << MyLha.MyGspn->colClasses[MyLha.Vars.colorDomain[v]].name << "_Total ;\n";
232 239 : }else if(MyLha.Vars.colorDomain[v]==UNCOLORED_DOMAIN)
233 239 : LhaCppFile << "\tVars->"<< MyLha.Vars.label[v] << "= "<< MyLha.Vars.initialValue[v]<<";\n";
234 0 : else LhaCppFile << "\tmemset(Vars->"<< MyLha.Vars.label[v] << ",0 , sizeof(Vars->"<< MyLha.Vars.label[v] << "));\n";
235 : }
236 33 : LhaCppFile << "};\n";
237 :
238 33 : LhaCppFile << funDecl("void") << "printHeader(ostream &s)const{\n";
239 33 : LhaCppFile << "\ts << \"\tLocation\\t";
240 33 : if(P.StringInSpnLHA){
241 20 : for(size_t v= 0 ; v < MyLha.Vars.type.size(); v++)
242 10 : if(MyLha.Vars.isTraced[v])LhaCppFile << MyLha.Vars.label[v] << "\\t";
243 : }
244 33 : LhaCppFile << "\";\n";
245 33 : LhaCppFile << "};\n";
246 :
247 33 : LhaCppFile << funDecl("void") << "printState(ostream &s){\n";
248 33 : LhaCppFile << "\ts << \"\\t\" << LocLabel[CurrentLocation] << \"\\t\";\n";
249 33 : if(P.StringInSpnLHA){
250 20 : for(size_t v= 0 ; v < MyLha.Vars.type.size(); v++)
251 10 : if(MyLha.Vars.isTraced[v]){
252 10 : if(MyLha.Vars.type[v] == INT_INDEXED_DISC_ARRAY){
253 0 : LhaCppFile << "\ts << \"[\";" <<endl;
254 0 : LhaCppFile << "\tfor(unsigned int i=0; i<"<< MyLha.Vars.colorDomain[v] <<"; i++)";
255 0 : LhaCppFile << "s << Vars->"<< MyLha.Vars.label[v] << "[i] << \", \";" << endl;
256 0 : LhaCppFile << "s <<\"] \\t\";\n";
257 : }else{
258 10 : LhaCppFile << "\ts << Vars->"<< MyLha.Vars.label[v] << " << \"\\t\";\n";
259 : }
260 : }
261 : }
262 33 : LhaCppFile << "};\n";
263 :
264 :
265 66 : vector<vector<list<int > > > accedge(MyLha.NbLoc,vector<list<int> >(MyLha.TransitionIndex.size()));
266 142 : for (size_t es =0 ; es < MyLha.NbLoc; es++)
267 2723 : for (auto it : MyLha.TransitionIndex)
268 30711 : for (size_t e = 0; e < MyLha.Edge.size(); e++)
269 56194 : if(MyLha.Edge[e].Source == es
270 28097 : && MyLha.EdgeActions[e].count(it.first)>0)
271 2753 : accedge[es][it.second].push_back(e);
272 :
273 66 : stringstream accstr;
274 33 : size_t maxset =0;
275 33 : accstr << "{"<< endl<< "\t";
276 142 : for (auto &it1 : accedge){
277 2723 : for(auto &it2 : it1){
278 2614 : accstr << it2.size() << " ,";
279 2614 : maxset = max(maxset,it2.size());
280 : }
281 : }
282 165 : while (maxset>0){
283 66 : accstr << endl << "\t";
284 66 : maxset=0;
285 297 : for (auto &it1 : accedge){
286 8924 : for(auto &it2 : it1){
287 8693 : if(it2.size()>0){
288 2753 : accstr << it2.front() << " ,";
289 2753 : it2.pop_front();
290 5940 : }else accstr << "-1,";
291 8693 : maxset = max(maxset,it2.size());
292 : }
293 : }
294 : }
295 33 : accstr << "}";
296 :
297 :
298 :
299 : //LhaCppFile << "/*" << accstr.str() << "*/" << endl;
300 :
301 :
302 33 : LhaCppFile << funDecl("const int") << "ActionEdgesAr[] = " << accstr.str() << ";"<< endl;
303 : /*LhaCppFile << "const int* LHAActionEdgesAr2["<< MyLha.NbLoc
304 : <<"]["<< MyLha.TransitionIndex.size() <<"] = " << accset3.str() << ";"<< endl;
305 : LhaCppFile << "const int* LHAActionEdges = (const int***)LHAActionEdgesAr;"<< endl;
306 : */
307 33 : LhaCppFile << funDecl("") << "LHA():NbLoc(" << MyLha.NbLoc << "),NbTrans(" << MyLha.TransitionIndex.size()<<"),NbVar(" << MyLha.NbVar << "),FinalLoc( " << MyLha.NbLoc << ",false){" << endl;
308 :
309 66 : for (let it : MyLha.InitLoc)
310 33 : LhaCppFile << " InitLoc.insert(" << it << ");" << endl;
311 76 : for (let it : MyLha.FinalLoc)
312 43 : LhaCppFile << " FinalLoc[" << it << "]=true;" << endl;
313 :
314 33 : if(P.CountTrans)
315 0 : LhaCppFile << " EdgeCounter = vector<int>("<<MyLha.Edge.size()<<",0);"<< endl;
316 33 : LhaCppFile << " Edge= vector<LhaEdge>(" << MyLha.Edge.size() << ");" << endl;
317 :
318 33 : if(P.StringInSpnLHA){
319 10 : LhaCppFile << "\n vector<string> vlstr(NbLoc);" << endl;
320 10 : LhaCppFile << " LocLabel= vlstr;" << endl;
321 :
322 40 : for (size_t i = 0; i < MyLha.LocLabel.size(); i++)
323 30 : LhaCppFile << " LocLabel[" << i << "]=\"" << MyLha.LocLabel[i] << "\";" << endl;
324 :
325 10 : LhaCppFile << " VarLabel= vector<string>(NbVar);" << endl;
326 20 : for (size_t v = 0; v < MyLha.Vars.label.size(); v++) {
327 10 : LhaCppFile << " VarLabel[" << v << "]=\"" << MyLha.Vars.label[v] << "\";" << endl;
328 : }
329 : }
330 :
331 243 : for (size_t i = 0; i < MyLha.Edge.size(); i++) {
332 210 : LhaCppFile << " Edge[" << i << "] = LhaEdge(" << MyLha.Edge[i].Index;
333 210 : LhaCppFile << ", " << MyLha.Edge[i].Source;
334 210 : LhaCppFile << ", " << MyLha.Edge[i].Target;
335 210 : if (MyLha.EdgeActions[i].size() < 1)
336 37 : LhaCppFile << ",Auto);" << endl;
337 : else
338 173 : LhaCppFile << ",Synch);" << endl;
339 :
340 : }
341 :
342 33 : LhaCppFile << "\tVars = new Variables;" << endl;
343 33 : LhaCppFile << "\ttempVars = new Variables;" << endl;
344 33 : LhaCppFile << "\tresetVariables();" << endl;
345 :
346 33 : LhaCppFile << " Out_A_Edges =vector< set < int > >(NbLoc);" << endl;
347 243 : for (size_t e = 0; e < MyLha.Edge.size(); e++) {
348 210 : if (MyLha.EdgeActions[e].size() < 1)
349 37 : LhaCppFile << " Out_A_Edges[" << MyLha.Edge[e].Source << "].insert(" << e << ");" << endl;
350 : }
351 :
352 33 : LhaCppFile << " LinForm= vector<double>("<< MyLha.LinearForm.size() <<",0.0);" << endl;
353 33 : LhaCppFile << " OldLinForm=vector<double>("<< MyLha.LinearForm.size() <<",0.0);" << endl;
354 33 : LhaCppFile << " LhaFunc=vector<double>("<< MyLha.LhaFuncArg.size() <<",0.0);" << endl;
355 33 : LhaCppFile << " LhaFuncDefaults=vector<double>("<< MyLha.LhaFuncArg.size() <<",0.0);" << endl;
356 :
357 236 : for (size_t i = 0;i < MyLha.LhaFuncArg.size(); i++) {
358 203 : if (MyLha.LhaFuncType[i] == "Min") {
359 0 : LhaCppFile << " LhaFunc[" << i << "] = DBL_MAX;" << endl;
360 0 : LhaCppFile << " LhaFuncDefaults[" << i << "] = DBL_MAX;" << endl;
361 : }
362 : }
363 :
364 33 : if(P.CountTrans){
365 0 : LhaCppFile << " FormulaVal = vector<double>(" << MyLha.Algebraic.size() + MyLha.Edge.size() << ",0.0);" << endl;
366 : } else {
367 33 : LhaCppFile << " FormulaVal = vector<double>(" << MyLha.Algebraic.size() << ",0.0);" << endl;
368 : }
369 33 : LhaCppFile << " FormulaValQual = vector<bool>(" << MyLha.FinalStateCond.size() << ",false);" << endl;
370 :
371 33 : LhaCppFile << "}\n" << endl;
372 :
373 :
374 33 : LhaCppFile << funDecl("void") << "DoElapsedTimeUpdate(double DeltaT,const DEDState& Marking) {\n";
375 274 : for (size_t v = 0; v < MyLha.Vars.label.size() ; v++) {
376 241 : if(MyLha.Vars.type[v] == CONTINIOUS_VARIABLE )
377 223 : LhaCppFile << "\tVars->"<< MyLha.Vars.label[v] << " += GetFlow("<<v<<", Marking) * DeltaT;\n";
378 : }
379 33 : LhaCppFile << "}\n";
380 :
381 :
382 33 : LhaCppFile << funDecl("double") << "GetFlow(int v, const DEDState& Marking)const{" << endl;
383 66 : casesHandler flowcases("v");
384 274 : for (size_t x = 0; x < MyLha.NbVar; x++) {
385 482 : stringstream newcase;
386 241 : if(MyLha.Vars.type[x] == CONTINIOUS_VARIABLE ){
387 446 : casesHandler flowcases2("CurrentLocation");
388 915 : for (size_t l = 0; l < MyLha.NbLoc; l++) {
389 1384 : stringstream newcase2;
390 692 : if (MyLha.FuncFlow[l][x] != ""){
391 152 : newcase2 << "\t\t\treturn " << MyLha.FuncFlow[l][x] << ";" << endl;
392 540 : }else newcase2 << "\t\treturn 0.0;" << endl;
393 692 : flowcases2.addCase(l, newcase2.str(),MyLha.LocLabel[l]);
394 : }
395 223 : flowcases2.writeCases(newcase);
396 : }
397 241 : flowcases.addCase(x, newcase.str(),MyLha.Vars.label[x]);
398 : }
399 33 : flowcases.writeCases(LhaCppFile);
400 33 : LhaCppFile << "}\n" << endl;
401 :
402 33 : LhaCppFile << funDecl("bool") << "CheckLocation(int loc,const DEDState& Marking)const{" << endl;
403 66 : casesHandler checklock("loc");
404 142 : for (size_t l = 0; l < MyLha.NbLoc; l++) {
405 218 : stringstream newcase;
406 109 : newcase << " return " << MyLha.FuncLocProperty[l] << ";" << endl;
407 109 : checklock.addCase(l, newcase.str(),MyLha.LocLabel[l]);
408 : }
409 33 : checklock.writeCases(LhaCppFile);
410 :
411 33 : LhaCppFile << "}\n" << endl;
412 :
413 33 : LhaCppFile << funDecl("bool") << "CheckEdgeContraints(int ed,size_t ptt,const abstractBinding& b,const DEDState& Marking)const{" << endl;
414 66 : casesHandler checkConstrain("ed");
415 243 : for (size_t e = 0; e < MyLha.Edge.size(); e++){
416 :
417 420 : stringstream newcase;
418 210 : if((MyLha.ConstraintsRelOp[e].size()>0 && MyLha.EdgeActions[e].size() > 0) || MyLha.unTimeEdgeConstraints[e]!="true" ){
419 117 : newcase << "{" << endl;
420 117 : if(MyLha.ConstraintsRelOp[e].size()>0 && MyLha.EdgeActions[e].size() > 0){
421 210 : for (size_t c = 0; c < MyLha.ConstraintsRelOp[e].size(); c++) {
422 105 : size_t k = 0;
423 3932 : for (size_t v = 0; v < MyLha.NbVar; v++)
424 3827 : if (MyLha.ConstraintsCoeffs[e][c][v] != "" /*&& MyLha.Vars.type[v] != CONTINIOUS_VARIABLE*/)k++;
425 105 : if(k>0){
426 105 : newcase << " if(!( ";
427 3932 : for (size_t v = 0; v < MyLha.Vars.label.size(); v++) {
428 3827 : if (MyLha.ConstraintsCoeffs[e][c][v] != "" /*&& MyLha.Vars.type[v] != CONTINIOUS_VARIABLE*/)
429 105 : newcase << "+(" << MyLha.ConstraintsCoeffs[e][c][v] << ")*Vars->" << MyLha.Vars.label[v];
430 :
431 : }
432 105 : newcase << MyLha.ConstraintsRelOp[e][c] << MyLha.ConstraintsConstants[e][c] << ")) return false;" << endl;
433 : }
434 : }
435 : }
436 117 : newcase << "\t\treturn (" << MyLha.unTimeEdgeConstraints[e] << ");" << endl;
437 117 : newcase << " }" << endl;
438 : }else{
439 93 : newcase << "\treturn true;" << endl;
440 : }
441 210 : checkConstrain.addCase(e, newcase.str());
442 : }
443 33 : checkConstrain.writeCases(LhaCppFile);
444 :
445 33 : LhaCppFile << "}\n" << endl;
446 :
447 :
448 33 : LhaCppFile << funDecl("t_interval") << "GetEdgeEnablingTime(int ed,const DEDState& Marking)const{" << endl;
449 66 : casesHandler enablingtime("ed");
450 : // LhaCppFile << " switch(ed){" << endl;
451 243 : for (size_t e = 0; e < MyLha.Edge.size(); e++){
452 420 : stringstream newcase;
453 210 : if(MyLha.ConstraintsRelOp[e].size()>0 && MyLha.EdgeActions[e].size() < 1){
454 : //LhaCppFile << " case " << e << ": //";
455 : //LhaCppFile << MyLha.LocLabel[MyLha.Edge[e].Source] << " -> " << MyLha.LocLabel[MyLha.Edge[e].Target] << endl;
456 :
457 : //LhaCppFile << " return GetEdgeEnablingTime_" << e << "( Marking);" << endl;
458 37 : newcase << " {" << endl;
459 :
460 37 : newcase << " t_interval EnablingT;\n" << endl;
461 37 : newcase << " EnablingT.first=CurrentTime;" << endl;
462 37 : newcase << " EnablingT.second=DBL_MAX;\n" << endl;
463 37 : newcase << " t_interval EmptyInterval;\n" << endl;
464 37 : newcase << " EmptyInterval.first=0;" << endl;
465 37 : newcase << " EmptyInterval.second=-1;\n" << endl;
466 :
467 37 : newcase << " double SumAF;" << endl;
468 37 : newcase << " double SumAX;" << endl;
469 :
470 37 : newcase << "\n" << endl;
471 :
472 74 : for (size_t c = 0; c < MyLha.ConstraintsRelOp[e].size(); c++){
473 37 : size_t k = 0;
474 481 : for (size_t v = 0; v < MyLha.NbVar; v++)
475 444 : if (MyLha.ConstraintsCoeffs[e][c][v] != "" && MyLha.Vars.type[v] == CONTINIOUS_VARIABLE)k++;
476 37 : if(k>0){
477 :
478 37 : newcase << " SumAF=";
479 481 : for (size_t v = 0; v < MyLha.NbVar; v++)
480 444 : if (MyLha.ConstraintsCoeffs[e][c][v] != "" && MyLha.Vars.type[v] == CONTINIOUS_VARIABLE)
481 37 : newcase << "+(" << MyLha.ConstraintsCoeffs[e][c][v] << ")*GetFlow(" << v << ", Marking)";
482 37 : newcase << ";\n SumAX=";
483 481 : for (size_t v = 0; v < MyLha.Vars.label.size(); v++)
484 444 : if (MyLha.ConstraintsCoeffs[e][c][v] != "" && MyLha.Vars.type[v] == CONTINIOUS_VARIABLE)
485 37 : newcase << "+(" << MyLha.ConstraintsCoeffs[e][c][v] << ")*Vars->" << MyLha.Vars.label[v];
486 37 : newcase << ";\n" << endl;
487 :
488 74 : string RelOp = MyLha.ConstraintsRelOp[e][c];
489 :
490 37 : newcase << " if(SumAF==0){" << endl;
491 37 : newcase << " if(!(SumAX" << MyLha.ConstraintsRelOp[e][c] << MyLha.ConstraintsConstants[e][c] << "))" << endl;
492 37 : newcase << " return EmptyInterval;" << endl;
493 37 : newcase << " }" << endl;
494 37 : newcase << " else{" << endl;
495 37 : newcase << " double t=CurrentTime+(" << MyLha.ConstraintsConstants[e][c] << "-SumAX)/(double)SumAF;" << endl;
496 37 : if (RelOp == "==") {
497 :
498 37 : newcase << " if(t>=EnablingT.first && t<=EnablingT.second){" << endl;
499 37 : newcase << " EnablingT.first=t; EnablingT.second=t;" << endl;
500 37 : newcase << " }" << endl;
501 37 : newcase << " else return EmptyInterval;" << endl;
502 :
503 : } else {
504 0 : newcase << " if(SumAF>0){" << endl;
505 0 : if (RelOp == "<=") {
506 0 : newcase << " if(EnablingT.second>t) EnablingT.second=t;" << endl;
507 0 : newcase << " if(EnablingT.second<EnablingT.first) return EmptyInterval;" << endl;
508 :
509 : } else {
510 0 : newcase << " if(EnablingT.first<t) EnablingT.first=t;" << endl;
511 0 : newcase << " if(EnablingT.second<EnablingT.first) return EmptyInterval;" << endl;
512 : }
513 :
514 0 : newcase << " }" << endl;
515 :
516 0 : newcase << " else{" << endl;
517 0 : const auto RelOp2 = InvRelOp(RelOp);
518 0 : if (RelOp2 == "<=") {
519 0 : newcase << " if(EnablingT.second>t) EnablingT.second=t;" << endl;
520 0 : newcase << " if(EnablingT.second<EnablingT.first) return EmptyInterval;" << endl;
521 :
522 : } else {
523 0 : newcase << " if(EnablingT.first<t) EnablingT.first=t;" << endl;
524 0 : newcase << " if(EnablingT.second<EnablingT.first) return EmptyInterval;" << endl;
525 : }
526 :
527 0 : newcase << " }" << endl;
528 : }
529 37 : newcase << " }" << endl;
530 :
531 : }
532 : }
533 :
534 37 : newcase << " return EnablingT;" << endl;
535 37 : newcase << " }"<< endl;
536 :
537 :
538 : //LhaCppFile << " }" << endl;
539 : //LhaCppFile << " break;" << endl;
540 :
541 : }else{
542 173 : newcase << " {" << endl;
543 :
544 173 : newcase << " t_interval EnablingT;\n" << endl;
545 173 : newcase << " EnablingT.first=CurrentTime;" << endl;
546 173 : newcase << " EnablingT.second=DBL_MAX;\n" << endl;
547 173 : newcase << " return EnablingT;" << endl;
548 173 : newcase << " }"<< endl;
549 :
550 : }
551 210 : enablingtime.addCase(e, newcase.str());
552 : }
553 33 : enablingtime.writeCases(LhaCppFile);
554 33 : LhaCppFile << "}\n" << endl;
555 :
556 :
557 :
558 33 : LhaCppFile << funDecl("void") << "DoEdgeUpdates(int ed,const DEDState& Marking, const abstractBinding& b){" << endl;
559 66 : casesHandler edgeUpdateHandler("ed");
560 : //LhaCppFile << " switch(ed){" << endl;
561 243 : for (size_t e = 0; e < MyLha.Edge.size(); e++) {
562 420 : stringstream newcase;
563 210 : int k = 0;
564 210 : for (size_t v = 0; v < MyLha.NbVar; v++)if (MyLha.FuncEdgeUpdates[e][v] != "")k++;
565 210 : if(k>0 || P.CountTrans){
566 : //LhaCppFile << " case " << e << ": // ";
567 : //LhaCppFile << MyLha.LocLabel[MyLha.Edge[e].Source] << " -> " << MyLha.LocLabel[MyLha.Edge[e].Target] << endl;
568 129 : newcase << " {"<< endl;
569 129 : if(P.CountTrans)
570 0 : newcase << " EdgeCounter[" << e << "]++ ;"<< endl;
571 :
572 129 : if (k==1) {
573 307 : for (size_t v = 0; v < MyLha.NbVar; v++)
574 265 : if (MyLha.FuncEdgeUpdates[e][v] != ""){
575 42 : newcase << "\t\tVars->" << MyLha.Vars.label[v];
576 42 : if(MyLha.Vars.type[v] ==INT_INDEXED_DISC_ARRAY)
577 0 : newcase << "[ (int) " << MyLha.FuncEdgeUpdatesIndex[e][v] << "]";
578 42 : newcase << "=" << MyLha.FuncEdgeUpdates[e][v] << ";" << endl;
579 : }
580 87 : } else if (k > 1) {
581 : //newcase << " *tempVars = *Vars;" << endl;
582 3710 : for (size_t v = 0; v < MyLha.NbVar; v++)
583 3623 : if (MyLha.FuncEdgeUpdates[e][v] != ""){
584 177 : if(MyLha.Vars.type[v] ==INT_INDEXED_DISC_ARRAY){
585 0 : newcase << "\t\tconst int tmp_INDEX_" << MyLha.Vars.label[v];
586 0 : newcase << "= " << MyLha.FuncEdgeUpdatesIndex[e][v] << ";"<< endl;
587 : }
588 177 : newcase << "\t\ttempVars->" << MyLha.Vars.label[v];
589 177 : if(MyLha.Vars.type[v] ==INT_INDEXED_DISC_ARRAY)
590 0 : newcase << "[ tmp_INDEX_" << MyLha.Vars.label[v] << "]";
591 177 : newcase << "=" << MyLha.FuncEdgeUpdates[e][v] << ";" << endl;
592 : }/*else{
593 : newcase << " tempVars->" << MyLha.Vars.label[v] << "=Vars->" << MyLha.Vars.label[v] << ";" << endl;
594 : }*/
595 : //newcase << "\t\tstd::swap(Vars,tempVars);\n";
596 3710 : for (size_t v = 0; v < MyLha.NbVar; v++)
597 3623 : if (MyLha.FuncEdgeUpdates[e][v] != ""){
598 177 : newcase << "\t\tVars->" << MyLha.Vars.label[v];
599 177 : if(MyLha.Vars.type[v] ==INT_INDEXED_DISC_ARRAY)
600 0 : newcase << "[ tmp_INDEX_" << MyLha.Vars.label[v] << "]";
601 177 : newcase << " = tempVars->"<< MyLha.Vars.label[v];
602 177 : if(MyLha.Vars.type[v] ==INT_INDEXED_DISC_ARRAY)
603 0 : newcase << "[ tmp_INDEX_" << MyLha.Vars.label[v] << "]";
604 177 : newcase << ";"<<endl;
605 : }
606 : }
607 : //LhaCppFile << " DoEdgeUpdates_" << e << "( Marking);" << endl;
608 129 : newcase << " }"<< endl;
609 : //LhaCppFile << " break;" << endl;
610 : }
611 210 : edgeUpdateHandler.addCase(e, newcase.str());
612 : }
613 33 : edgeUpdateHandler.writeCases(LhaCppFile);
614 : //LhaCppFile << " }" << endl;
615 235 : for (let it : MyLha.LinearForm)
616 202 : if(!MyLha.SimplyUsedLinearForm[it.second]){
617 1 : LhaCppFile << " OldLinForm[" << it.second << "]=LinForm[" << it.second << "];" << endl;
618 :
619 : }
620 :
621 33 : LhaCppFile << "}\n" << endl;
622 :
623 :
624 :
625 : /*for (int e = 0; e < MyLha.Edge.size(); e++) {
626 : LhaCppFile << "void LHA::DoEdgeUpdates_" << e << "(abstractMarking& Marking){" << endl;
627 :
628 : LhaCppFile << " }\n" << endl;
629 : }*/
630 :
631 33 : LhaCppFile << funDecl("void") << "UpdateLinForm(const DEDState& Marking){" << endl;
632 235 : for (let it : MyLha.LinearForm)
633 202 : if(!MyLha.SimplyUsedLinearForm[it.second]){
634 1 : LhaCppFile << " LinForm[" << it.second << "]=" << it.first << ";" << endl;
635 :
636 : }
637 33 : LhaCppFile << " }\n" << endl;
638 :
639 33 : LhaCppFile << funDecl("void") << "UpdateLhaFunc(double& Delta ){" << endl;
640 236 : for (size_t i = 0; i < MyLha.LhaFuncArg.size(); i++) {
641 : /*if (MyLha.LhaFuncType[i] == "Last")
642 : LhaCppFile << " LhaFunc[" << i << "]=LinForm[" << MyLha.LhaFuncArg[i] << "];" << endl;
643 : else {*/
644 203 : if (MyLha.LhaFuncType[i] == "Min")
645 0 : LhaCppFile << " LhaFunc[" << i << "]=min(LhaFunc[" << i << "],LinForm[" << MyLha.LhaFuncArg[i] << "]);" << endl;
646 203 : else if (MyLha.LhaFuncType[i] == "Max")
647 1 : LhaCppFile << " LhaFunc[" << i << "]=Max(LhaFunc[" << i << "],LinForm[" << MyLha.LhaFuncArg[i] << "],OldLinForm[" << MyLha.LhaFuncArg[i] << "]);" << endl;
648 202 : else if (MyLha.LhaFuncType[i] == "Integral")
649 0 : LhaCppFile << " LhaFunc[" << i << "]=Integral(LhaFunc[" << i << "], CurrentTime, Delta, OldLinForm[" << MyLha.LhaFuncArg[i] << "],LinForm[" << MyLha.LhaFuncArg[i] << "]);" << endl;
650 202 : else if (MyLha.LhaFuncType[i] == "Mean")
651 0 : LhaCppFile << " LhaFunc[" << i << "]=Integral(LhaFunc[" << i << "], CurrentTime, Delta, OldLinForm[" << MyLha.LhaFuncArg[i] << "],LinForm[" << MyLha.LhaFuncArg[i] << "]);" << endl;
652 : //}
653 :
654 : }
655 33 : LhaCppFile << "\n }\n" << endl;
656 :
657 33 : LhaCppFile << funDecl("void") << "UpdateFormulaVal(const DEDState& Marking){\n" << endl;
658 236 : for (size_t i = 0; i < MyLha.LhaFuncArg.size(); i++) {
659 203 : if (MyLha.LhaFuncType[i] == "Last" && MyLha.SimplyUsedLinearForm[MyLha.LhaFuncArg[i]]){
660 404 : string str;
661 202 : for( auto it : MyLha.LinearForm) if(it.second== MyLha.LhaFuncArg[i])str=it.first;
662 202 : LhaCppFile << " LhaFunc[" << i << "]= " << str << ";" << endl;
663 1 : }else if (MyLha.LhaFuncType[i] == "Last"){
664 0 : LhaCppFile << " LhaFunc[" << i << "]=LinForm[" << MyLha.LhaFuncArg[i] << "];" << endl;
665 1 : } else if(MyLha.LhaFuncType[i] == "Mean")
666 0 : LhaCppFile << " LhaFunc[" << i << "]=LhaFunc[" << i << "] / CurrentTime ;" << endl;
667 : }
668 :
669 236 : for(size_t i=0;i<MyLha.Algebraic.size();i++){
670 : //haCppFile << " OldFormulaVal=FormulaVal["<<i<<"];" << endl;
671 203 : LhaCppFile << " FormulaVal["<<i<<"]=" << MyLha.Algebraic[i] << ";" << endl;
672 : }
673 33 : if (P.CountTrans) {
674 0 : for(size_t i=0;i<MyLha.Edge.size();i++){
675 0 : size_t j = i+ MyLha.Algebraic.size();
676 0 : LhaCppFile << " FormulaVal["<<j<<"]= EdgeCounter[" << i << "];\n";
677 : }
678 : }
679 33 : for(size_t i = 0; i < MyLha.FinalStateCond.size(); i++){
680 0 : LhaCppFile << " FormulaValQual[" << i << "] = CurrentLocation == " << MyLha.LocIndex.find(MyLha.FinalStateCond[i])->second << ";"<< endl;
681 : }
682 :
683 33 : LhaCppFile << "}\n" << endl;
684 :
685 33 : LhaCppFile << "bool IsLHADeterministic = "<< MyLha.isDeterministic<< ";" << endl;
686 :
687 33 : LhaCppFile << "fullState::fullState():loc(0){\n\tvar= new Variables;\n}\n" << endl;
688 33 : LhaCppFile << "fullState::fullState(int l,const Variables &v):loc(l){\n\tvar= new Variables(v);\n}\n" << endl;
689 33 : LhaCppFile << "fullState::fullState(const fullState &fs):loc(fs.loc){\n\tvar= new Variables(*(fs.var));\n}\n" << endl;
690 33 : LhaCppFile << "fullState::~fullState(){delete var;}\n" << endl;
691 :
692 33 : LhaCppFile << "template class LHA<abstractMarking>;" << endl;
693 33 : if(P.modelType == External /*|| P.modelType == GSPN_Simulink*/){
694 0 : LhaCppFile << "#include \"SKModel.hpp\"" << endl;
695 0 : LhaCppFile << "template class LHA<abstractState>;" << endl;
696 : }
697 : //LhaCppFile << "#include \"MarkovChainState.hpp\"" << endl;
698 :
699 : /*LhaCppFile << "class State{" << endl;
700 : LhaCppFile << " int state;" << endl;
701 : LhaCppFile << " void printSedCmd(std::ostream &of)const{ of << state << \"\t\"; }" << endl;
702 : LhaCppFile << " void printHeader(std::ostream &of)const{ of << state << \"\t\"; }" << endl;
703 : LhaCppFile << " void print(std::ostream &of, double et)const{ of << state << \"\t\"; }" << endl;
704 : LhaCppFile << "};" << endl;
705 : LhaCppFile << "template class LHA<State>;" << endl;*/
706 :
707 :
708 : //LhaCppFile << "template class LHA<State>;" << endl;
709 :
710 33 : LhaCppFile.close();
711 33 : }
712 :
713 :
714 33 : void Lha_Reader::writeDotFile(const string &file)const{
715 66 : ofstream df(file.c_str(), ios::out | ios::trunc);
716 33 : df << "digraph G {" << endl;
717 :
718 142 : for (let l : MyLha.LocLabel ) {
719 109 : df << "\t" << l;
720 109 : df << " [shape=circle];" << endl;
721 : }
722 :
723 243 : for (let e : MyLha.Edge ){
724 210 : df << "\t" << MyLha.LocLabel[e.Source] << "->" << MyLha.LocLabel[e.Target];
725 210 : df << " [label=\"{";
726 210 : if(MyLha.EdgeActions[e.Index].size()>5){df<< "##";}else for(let a :MyLha.EdgeActions[e.Index])df << a << ", ";
727 210 : df<< "}, {";
728 :
729 210 : if((MyLha.ConstraintsRelOp[e.Index].size()>0 && MyLha.EdgeActions[e.Index].size() > 0) || MyLha.unTimeEdgeConstraints[e.Index]!="true" ){
730 117 : if(MyLha.ConstraintsRelOp[e.Index].size()>0 && MyLha.EdgeActions[e.Index].size() > 0){
731 210 : for (size_t c = 0; c < MyLha.ConstraintsRelOp[e.Index].size(); c++) {
732 105 : size_t k = 0;
733 3932 : for (size_t v = 0; v < MyLha.NbVar; v++)
734 3827 : if (MyLha.ConstraintsCoeffs[e.Index][c][v] != "")k++;
735 105 : if(k>0){
736 3932 : for (size_t v = 0; v < MyLha.Vars.label.size(); v++) {
737 3827 : if (MyLha.ConstraintsCoeffs[e.Index][c][v] != "" )
738 105 : df << "(" << MyLha.ConstraintsCoeffs[e.Index][c][v] << ")*" << MyLha.Vars.label[v];
739 :
740 : }
741 105 : df << MyLha.ConstraintsRelOp[e.Index][c] << MyLha.ConstraintsConstants[e.Index][c] << ", ";
742 : }
743 : }
744 : }
745 : }
746 :
747 210 : df << "}, {";
748 4652 : for (size_t v = 0; v < MyLha.NbVar; v++)
749 4442 : if (MyLha.FuncEdgeUpdates[e.Index][v] != ""){
750 219 : df << MyLha.Vars.label[v] << ":=" << MyLha.FuncEdgeUpdates[e.Index][v] << ",";
751 : }
752 210 : df<<"} \"];" << endl;
753 : }
754 33 : df << "}" << endl;
755 138 : }
756 :
757 :
758 :
759 :
760 :
761 :
762 :
763 :
764 :
765 :
|
