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 Generator.cpp *
24 : * Created by Benoit Barbot on 21/01/2014. *
25 : *******************************************************************************
26 : */
27 :
28 :
29 : #include <fstream>
30 : #include <iostream>
31 : #include <string>
32 : #include <utility>
33 : #include <exception>
34 :
35 : #include "Generator.hpp"
36 : #include "parameters.hpp"
37 : #include "LhaParser/Lha-Reader.hpp"
38 : #include "GspnParser/Gspn-model.hpp"
39 : #include "GspnParser/Gspn-Writer.hpp"
40 : #include "GspnParser/Gspn-Writer-Color.hpp"
41 :
42 :
43 : using namespace std;
44 :
45 34 : shared_ptr<GspnType> ParseGSPN() {
46 :
47 : // initialize an empty structure for the model.
48 68 : Gspn_Reader gReader(P);
49 :
50 34 : if (P.verbose > 0)cout << "Start Parsing " << P.PathGspn << endl;
51 : int parseresult;
52 :
53 : try {
54 : // Check the extension of the model file to call the correct parser
55 102 : if (!P.GMLinput
56 102 : && P.PathGspn.substr(P.PathGspn.length() - 4, 4) != "grml"
57 45 : && P.PathGspn.substr(P.PathGspn.length() - 3, 3) != "gml"
58 113 : && P.PathGspn.substr(P.PathGspn.length() - 4, 4) != "gspn"){
59 0 : if(P.verbose>0)cerr << "Input file not in GrML try to use convertor."<< endl;
60 0 : auto outspt = P.tmpPath + "/generatedspt";
61 0 : stringstream cmd;
62 0 : cmd << P.Path << "modelConvert --grml ";
63 0 : if(P.lightSimulator)cmd << "--light ";
64 0 : cmd << P.PathGspn << " " << outspt;
65 0 : if (P.verbose > 0)cout << cmd.str() << endl;
66 0 : if (system(cmd.str().c_str()) != 0) {
67 0 : cerr << "Fail to Convert from input language to GrML!" << endl;
68 0 : return nullptr;
69 : }
70 0 : P.PathGspn = outspt+".grml";
71 : }
72 :
73 68 : if (P.GMLinput
74 34 : || (P.PathGspn.compare(P.PathGspn.length() - 4, 4, "grml") == 0)
75 45 : || (P.PathGspn.compare(P.PathGspn.length() - 3, 3, "gml") == 0)) {
76 23 : parseresult = gReader.parse_gml_file(P);
77 : } else {
78 11 : parseresult = gReader.parse_file(P.PathGspn);
79 : }
80 34 : P.nbPlace = gReader.spn->pl;
81 :
82 :
83 34 : if(parseresult==1 || !gReader.spn)return nullptr;
84 :
85 : //The following code modify the internal representation of the
86 : //SPN according to options.
87 :
88 : //When using multimodel with simulink and a gspn add a synchronisation transition to the GSPN
89 34 : if(P.modelType == GSPN_Simulink){
90 0 : auto &spn = gReader.spn;
91 0 : transition trans(spn->transitionStruct.size(), "Synctrans", expr(0.0), true);
92 0 : trans.dist.name = "SYNC";
93 0 : spn->transitionStruct.push_back(trans);
94 0 : spn->TransList.insert(trans.name);
95 0 : spn->TransId["Synctrans"]=spn->tr;
96 0 : spn->tr++;
97 0 : for (size_t t = 0; t < spn->tr-1; t++)
98 0 : if(spn->transitionStruct[t].dist.name == "SYNC")
99 0 : for(auto outarc= spn->outArcsStruct.lower_bound(make_pair(t, 0));
100 0 : outarc != spn->outArcsStruct.end() && outarc->first.first==t; ++outarc){
101 0 : spn->outArcsStruct.insert(make_pair(make_pair(spn->tr-1, outarc->first.second) , outarc->second));
102 : }
103 : }
104 :
105 : //Set the isTraced flag for places, transitions and hybrid var
106 34 : if (P.tracedPlace.count("ALL") == 0 && P.tracedPlace.count("ALLCOLOR")==0 ) {
107 2 : P.nbPlace = 0;
108 54 : for (size_t i = 0; i < gReader.spn->pl; i++) {
109 52 : if (P.tracedPlace.count(gReader.spn->placeStruct[i].name)>0) {
110 0 : gReader.spn->placeStruct[i].isTraced = true;
111 0 : P.nbPlace++;
112 : } else {
113 52 : gReader.spn->placeStruct[i].isTraced = false;
114 : }
115 : }
116 44 : for (size_t i = 0; i < gReader.spn->tr; i++) {
117 42 : if ( P.tracedPlace.count(gReader.spn->transitionStruct[i].name)>0 ) {
118 0 : gReader.spn->transitionStruct[i].isTraced = true;
119 : } else {
120 42 : gReader.spn->transitionStruct[i].isTraced = false;
121 : }
122 : }
123 2 : for (auto &v: gReader.spn->hybridVars) {
124 0 : if ( P.tracedPlace.count(v.name)>0 ) {
125 0 : v.isTraced = true;
126 : } else {
127 0 : v.isTraced = false;
128 : }
129 : }
130 : }
131 :
132 : //Apply Law of mass action for MASSACTION distribution:
133 547 : for (size_t t = 0; t < gReader.spn->tr; t++) {
134 513 : ProbabiliteDistribution *trDistr = &gReader.spn->transitionStruct[t].dist;
135 513 : if (trDistr->name.compare("MASSACTION") == 0) {
136 30 : gReader.spn->transitionStruct[t].markingDependant = true;
137 690 : for (size_t p = 0; p < gReader.spn->pl; p++) {
138 660 : if (!gReader.spn->access(gReader.spn->inArcsStruct, t, p).isEmpty) {
139 80 : expr exponent = gReader.spn->access(gReader.spn->inArcsStruct, t, p).exprVal;
140 : /*if (gReader.spn->access(gReader.spn->inArcsStruct, t, p).isMarkDep) {
141 : exponent = expr(gReader.spn->access(gReader.spn->inArcsStruct, t, p).stringVal);
142 : } else {
143 : exponent = expr((int) gReader.spn->access(gReader.spn->inArcsStruct, t, p).intVal);
144 : }*/
145 80 : expr pl = expr(PlaceName, gReader.spn->placeStruct[p].name);
146 80 : expr mult = expr(Pow, pl, exponent);
147 80 : expr dist = expr(Times, trDistr->Param[0], mult);
148 :
149 40 : trDistr->Param[0] = dist;
150 : }
151 : }
152 : }
153 : }
154 :
155 34 : if(P.is_domain_impl_set){
156 : //rewrite color variable guard
157 30 : for(auto &tr : gReader.spn->transitionStruct){
158 152 : tr.guard.rewrite( [](expr &e){
159 100 : if(e.t == ColorVarName){
160 20 : e.t = UnParsed;
161 20 : e.stringVal = " itVar_" +e.stringVal + " ";
162 : }
163 126 : });
164 : }
165 : }
166 :
167 : //Print the internal representation
168 : { using namespace text_output;
169 34 : if(P.verbose >=3)cout << *(gReader.spn);}
170 :
171 0 : } catch (GrmlInputException& e) {
172 0 : cerr << "The following exception append during model import: " << e.what() << endl;
173 0 : return nullptr;
174 : }
175 :
176 34 : return gReader.spn;
177 : }
178 :
179 0 : bool ParseLHA(){
180 0 : GspnType emptyGSPN;
181 0 : emptyGSPN.tr =1;
182 0 : transition trans;
183 0 : trans.id = 0;
184 0 : trans.name = "DummyTrans";
185 0 : trans.type = Timed;
186 0 : trans.priority = expr(1);
187 0 : trans.weight = expr(1.0);
188 0 : trans.singleService = true;
189 0 : trans.markingDependant = false;
190 0 : trans.ageMemory = false;
191 0 : trans.nbServers = 1;
192 :
193 0 : emptyGSPN.transitionStruct.push_back(trans);
194 0 : emptyGSPN.TransId["DummyTrans"]=0;
195 0 : return ParseLHA(emptyGSPN);
196 : }
197 :
198 33 : bool ParseLHA(GspnType &spn){
199 : // Intialize an empty structure for the automaton
200 66 : Lha_Reader lReader(spn, P);
201 33 : auto &A = lReader.MyLha;
202 :
203 : int parseresult;
204 :
205 : //Copy name of transition and place required for synchronization.
206 33 : A.TransitionIndex = spn.TransId;
207 33 : A.PlaceIndex = spn.PlacesId;
208 33 : A.ConfidenceLevel = P.Level;
209 :
210 33 : if (P.verbose > 0)cout << "Start Parsing " << P.PathLha << endl;
211 :
212 : try {
213 33 : switch (P.generateLHA) {
214 : case CSL_LHA:
215 : {
216 : // If the automaton need to be generated from a formula
217 : // call the generating tool.
218 3 : P.PathLha = P.tmpPath + "/generatedlha.lha";
219 3 : stringstream cmd;
220 : cmd << "echo \"" << P.CSLformula << "\" | " << P.Path <<
221 3 : "automataGen >" << P.PathLha;
222 3 : if (P.verbose > 0)cout << cmd.str() << endl;
223 3 : if (system(cmd.str().c_str()) != 0) {
224 0 : cerr << "Fail to Generate the Automaton!" << endl;
225 0 : return false;
226 : }
227 3 : break;
228 : }
229 : case TimeLoop:
230 : case ActionLoop:
231 12 : generateLoopLHA(spn);
232 12 : break;
233 : case SamplingLoop:
234 0 : generateSamplingLHA(spn);
235 0 : break;
236 : case EmptyLoop:
237 0 : generateEmptyLHA();
238 0 : break;
239 : case NoGen:
240 18 : break;
241 : }
242 :
243 :
244 : //check the type of the LHA file
245 : //First check if it is not C++ code
246 33 : if (P.PathLha.compare(P.PathLha.length() - 3, 3, "cpp") != 0) {
247 :
248 33 : if (P.PathLha.compare(P.PathLha.length() - 4, 4, "grml") == 0) {
249 : //The LHA is in the GRML file format
250 6 : parseresult = lReader.parse_gml_file(P);
251 6 : if(! A.isDeterministic )P.lhaType= NOT_DET;
252 : } else {
253 : //The LHA is in the LHA file format
254 27 : parseresult = lReader.parse_file(P);
255 27 : if(! A.isDeterministic )P.lhaType= NOT_DET;
256 : }
257 :
258 : //Add external HASL formula to the lha.
259 33 : if (P.externalHASL.compare("") != 0)
260 2 : lReader.parse(P.externalHASL);
261 :
262 : //Set the isTraced flag for variables
263 33 : if (P.tracedPlace.count("ALL")==0 && P.tracedPlace.count("ALLCOLOR")==0) {
264 6 : for (size_t i = 0; i < A.NbVar; i++) {
265 4 : if ( P.tracedPlace.count(A.Vars.label[i])>0){
266 0 : A.Vars.isTraced[i] = true;
267 : } else {
268 4 : A.Vars.isTraced[i] = false;
269 : }
270 : }
271 : }
272 :
273 : //If everythink work correctly, copy the HASL formula and generate the code
274 33 : if (!parseresult && A.NbLoc > 0) {
275 33 : P.HaslFormulasname = A.HASLname;
276 33 : P.HaslFormulas = vector<HaslFormulasTop*>(A.HASLtop);
277 33 : P.nbAlgebraic = A.Algebraic.size();
278 33 : P.nbQualitatif = A.FinalStateCond.size();
279 :
280 : //If the countTrans option is set then add HASL formula counting the occurance of each transition of the LHA.
281 33 : if (P.CountTrans) {
282 0 : for (size_t tr = 0; tr < A.Edge.size(); tr++) {
283 0 : P.nbAlgebraic++;
284 0 : std::stringstream transname;
285 0 : transname << "P_";
286 0 : transname << A.LocLabel[A.Edge[tr].Source];
287 0 : transname << "->";
288 0 : transname << A.LocLabel[A.Edge[tr].Target];
289 0 : P.HaslFormulasname.push_back(transname.str());
290 0 : P.HaslFormulas.push_back(new HaslFormulasTop(A.Algebraic.size() + tr));
291 : }
292 : }
293 :
294 : //some cleaning:
295 33 : A.SimplyUsedLinearForm = vector<bool>(A.LinearForm.size(),true);
296 236 : for( size_t i = 0; i< A.LhaFuncArg.size();++i)
297 203 : if(A.LhaFuncType[i]!="Last")
298 1 : A.SimplyUsedLinearForm[A.LhaFuncArg[i]] = false;
299 :
300 :
301 : //Generate the code for the LHA
302 33 : lReader.WriteFile(P);
303 33 : lReader.writeDotFile(P.tmpPath + "/templateLHA.dot");
304 :
305 : } else {
306 0 : return false;
307 : }
308 :
309 : //If the LHA is already C++ code just copy it to temporary
310 : //and add external HASL formula
311 0 : } else if (P.PathLha.compare(P.PathLha.length() - 3, 3, "cpp") == 0) {
312 : //The code for the LHA is provided by the user
313 0 : A.ConfidenceLevel = P.Level;
314 : //Add external HASL formula
315 0 : if (P.externalHASL.compare("") == 0) {
316 0 : P.HaslFormulasname.push_back("preComputedLHA");
317 0 : HaslFormulasTop *ht = new HaslFormulasTop((size_t) 0);
318 0 : P.HaslFormulas.push_back(ht);
319 0 : P.nbAlgebraic = 1;
320 : } else {
321 0 : parseresult = lReader.parse(P.externalHASL);
322 0 : if (!parseresult) {
323 0 : P.HaslFormulasname = A.HASLname;
324 0 : P.HaslFormulas = vector<HaslFormulasTop*>(A.HASLtop);
325 0 : P.nbAlgebraic = A.Algebraic.size();
326 : } else
327 0 : cerr << "Fail to parse extra Hasl Formula" << endl;
328 : }
329 :
330 : //Copy the code into the temporary directory
331 0 : if( P.PathLha != P.tmpPath + "/LHA.cpp"){
332 0 : string cmd = "cp " + P.PathLha + " " + P.tmpPath + "/LHA.cpp";
333 0 : if (P.verbose > 2)cout << cmd << endl;
334 0 : if (system(cmd.c_str()) != 0) {
335 0 : cerr << "Fail to copy LHA to temporary" << endl;
336 0 : return false;
337 : }
338 : }
339 : }
340 0 : } catch (GrmlInputException& e) {
341 0 : cerr << "The following exception append during LHA import: " << e.what() << endl;
342 0 : return false;
343 : }
344 :
345 66 : string cmd;
346 :
347 33 : if (P.RareEvent) {
348 : //If rareevent handling is require copy the lumping function and table of value to the temporary directory
349 6 : if (P.BoundedRE == 0)cmd = "cp muFile " + P.tmpPath + "/muFile";
350 5 : else cmd = "cp matrixFile " + P.tmpPath + "/matrixFile";
351 6 : if (system(cmd.c_str())) return false;
352 6 : cmd = "cp lumpingfun.cpp " + P.tmpPath + "/lumpingfun.cpp";
353 6 : if (system(cmd.c_str())) return false;
354 :
355 : //Rewrite part of probabilistic operator to apply Rare event handling
356 : //First case for Continuous bounded rare event.
357 6 : if (P.BoundedContinuous) {
358 12 : for (vector<HaslFormulasTop*>::iterator it = P.HaslFormulas.begin();
359 8 : it != P.HaslFormulas.end(); ++it)
360 2 : if ((*it)->TypeOp == EXPECTANCY) {
361 2 : (*it)->TypeOp = RE_Continuous;
362 2 : (*it)->Value = P.continuousStep;
363 2 : (*it)->Value2 = P.epsilon;
364 :
365 : }
366 : } else { // Second case Unbounded rare event.
367 8 : vector<HaslFormulasTop*> tmpRE;
368 8 : vector<string> tmpREName;
369 24 : for (vector<HaslFormulasTop*>::iterator it = P.HaslFormulas.begin();
370 16 : it != P.HaslFormulas.end(); ++it)
371 4 : if ((*it)->TypeOp == EXPECTANCY) {
372 4 : (*it)->TypeOp = RE_AVG;
373 4 : HaslFormulasTop *HaslCopy = new HaslFormulasTop(**it);
374 4 : HaslCopy->TypeOp = RE_Likelyhood;
375 4 : tmpRE.push_back(HaslCopy);
376 4 : tmpREName.push_back("Likelyhood_" + P.HaslFormulasname[it - P.HaslFormulas.begin() ]);
377 : }
378 24 : for (vector<HaslFormulasTop*>::iterator it = tmpRE.begin();
379 16 : it != tmpRE.end(); ++it) {
380 4 : P.HaslFormulas.push_back(*it);
381 4 : P.HaslFormulasname.push_back(tmpREName[it - tmpRE.begin()]);
382 : }
383 : }
384 : }
385 :
386 : //generateMain();
387 :
388 33 : return true;
389 :
390 : }
391 :
392 33 : void generateMain() {
393 63 : string loc;
394 :
395 33 : loc = P.tmpPath + "/main.cpp";
396 63 : ofstream mF(loc.c_str(), ios::out | ios::trunc);
397 :
398 33 : mF << "#include \"BatchR.hpp\"" << endl;
399 33 : mF << "#include \"clientsim.hpp\"" << endl;
400 : /*mF << "#include \"Simulator.hpp\"" << endl;
401 : mF << "#include \"SimulatorRE.hpp\"" << endl;
402 : mF << "#include \"SimulatorBoundedRE.hpp\"" << endl;
403 : mF << "#include \"SimulatorContinuousBounded.hpp\"" << endl;*/
404 33 : mF << "#include <sys/types.h>" << endl;
405 33 : mF << "#include <unistd.h>" << endl;
406 33 : mF << "#include <signal.h>" << endl;
407 33 : if( P.modelType == GSPN_Simulink){
408 0 : mF << "#include \"MultiModel.hpp\"" << endl;
409 0 : mF << "#include \"SKModel.hpp\"" << endl;
410 0 : mF << "#include \"multimodel.cpp\"" << endl;
411 : }
412 :
413 33 : mF << "int main(int argc, char** argv) {" << endl;
414 33 : mF << " signal(SIGHUP, signalHandler);" << endl;
415 33 : mF << " signal(SIGINT, signalHandler);" << endl;
416 33 : mF << " {const string tmppath(argv[1]);" << endl;
417 33 : mF << " ifstream ifs(tmppath+\"/parameters.txt\");" << endl;
418 33 : mF << " readParameters(ifs);}" << endl;
419 33 : if( P.computeStateSpace>0){
420 3 : mF << "stateSpace states;" << endl;
421 3 : mF << "states.exploreStateSpace();" << endl;
422 3 : mF << "states.buildTransitionMatrix();" << endl;
423 3 : if(P.computeStateSpace==1){
424 2 : mF << "states.outputPrism();" << endl;
425 2 : mF << "states.launchPrism(\""<< P.prismPath <<"\");" << endl;
426 2 : mF << "states.importPrism();" << endl;
427 2 : mF << "states.outputVect();" << endl;
428 2 : mF << "states.outputTmpLumpingFun();" << endl;
429 2 : mF << "double prResult = states.returnPrismResult();" << endl;
430 2 : mF << "BatchR dummR(1,0);" << endl;
431 2 : mF << "SimOutput sd;" << endl;
432 2 : mF << "sd.accept=true;" << endl;
433 2 : mF << "sd.quantR.push_back(prResult);" << endl;
434 2 : mF << "dummR.addSim(sd);" << endl;
435 : } else{
436 : //states.uniformizeMatrix();
437 1 : mF << "states.outputMat();" << endl;
438 1 : mF << "states.outputTmpLumpingFun();" << endl;
439 1 : mF << "BatchR dummR(0,0);" << endl;
440 : }
441 3 : mF << "dummR.outputR(cout);" << endl;
442 3 : mF << "cerr << \"Finish Exporting\" << endl;" << endl;
443 3 : mF << "exit(EXIT_SUCCESS);" << endl;
444 3 : mF << "}" << endl;
445 3 : return;
446 : }
447 :
448 : // Instantiate EventQueue
449 30 : const auto eqt = (P.is_domain_impl_set ? "EventsQueueSet" :"EventsQueue");
450 :
451 : // Instantiate DEDS
452 30 : if (P.BoundedRE > 0 || P.BoundedContinuous) {
453 5 : mF << " SPN_BoundedRE N(false);" << endl;
454 25 : } else if (P.RareEvent) {
455 1 : mF << " SPN_RE N("<< P.DoubleIS <<");" << endl;
456 : } else {
457 24 : mF << " SPN_orig<" << eqt << "> N(0);" << endl;
458 : }
459 :
460 30 : if(P.modelType == GSPN_Simulink){
461 0 : mF << " SKModel<" << eqt <<"> N2(N.tr);" << endl;
462 0 : mF << " MultiModel<"<< eqt <<",typeof N, typeof N2> mm(N,N2);" << endl;
463 : }
464 30 : const auto model = ((P.modelType == GSPN_Simulink)? "mm" : "N");
465 :
466 : // Instantiade LHA
467 30 : if( P.lhaType == DET){
468 30 : mF << " LHA_orig<typename decltype(N)::stateType> A;"<< endl;
469 : }else{
470 0 : mF << " NLHA<typename decltype(N)::stateType> A;"<< endl;
471 : }
472 :
473 : // Instantiate Simulator
474 30 : if (P.BoundedContinuous){
475 2 : mF << " SimulatorContinuousBounded<SPN_BoundedRE> sim(N,A,"<<
476 4 : P.BoundedRE << ", "<< P.epsilon << ", " << P.continuousStep << ");" << endl;
477 2 : mF << " sim.initVectCo("<< P.horizon <<");" << endl;
478 28 : }else if (P.BoundedRE > 0) {
479 3 : mF << " SimulatorBoundedRE<SPN_BoundedRE> sim(N,A,"<< P.BoundedRE <<");" << endl;
480 3 : mF << " sim.initVect("<< (int)P.horizon <<");" << endl;
481 25 : } else if (P.RareEvent) {
482 1 : mF << " SimulatorRE<SPN_RE> sim(N,A);" << endl;
483 1 : mF << " sim.initVect();" << endl;
484 : } else {
485 24 : mF << " Simulator<"<< eqt << ",typeof "<< model << "> sim("<< model <<",A);" << endl;
486 : }
487 :
488 :
489 30 : if( !P.dataraw.empty()) mF << " sim.logValue(\"" << P.dataraw << "\");" <<endl;
490 30 : if( !P.datatrace.empty()){
491 1 : mF << " sim.logTrace(\"" << P.datatrace << "\","<< P.sampleResol << ");" <<endl;
492 1 : mF << " bool singleBatch = true;"<< endl;
493 29 : } else mF << " bool singleBatch = false;"<< endl;
494 30 : if( !P.dotfile.empty()) mF << " sim.dotFile = \"" << P.dotfile << "\";" << endl;
495 :
496 30 : mF << " sim.SetBatchSize(" << P.Batch << ");" << endl;
497 :
498 30 : mF << " setSimulator(sim,argc,argv,P);" << endl;
499 :
500 30 : mF << " if((P.verbose>=4) | singleBatch )sim.RunBatch();" << endl;
501 30 : mF << " else while( !cin.eof() && P.graceFullEnding <= 1 ){" << endl;
502 30 : mF << " BatchR batchResult = sim.RunBatch(); //simulate a batch of trajectory" << endl;
503 30 : mF << " batchResult.outputR(cout);// output the result on the standart output" << endl;
504 30 : mF << " }" << endl;
505 30 : mF << " return (EXIT_SUCCESS);" << endl;
506 30 : mF << "}" << endl << endl;
507 :
508 30 : mF.close();
509 : }
510 :
511 31 : bool compileSource(const std::vector<std::string> &sources){
512 62 : string bcmd = P.gcccmd + " " + P.gccflags;
513 :
514 31 : bool first = true;
515 62 : string cmd;
516 106 : for(let file : sources){
517 75 : if(first){ first = false; cmd += " ";
518 : } else {
519 44 : cmd += "&";
520 : }
521 :
522 75 : cmd += "(" + bcmd + " -c -I" + P.Path + "../include " + (P.modelType== External || P.modelType==GSPN_Simulink ? (P.boostpath +" -I./ ") : "");
523 75 : cmd += " -o " + P.tmpPath + "/" + file +".o " + P.tmpPath + "/" + file +".cpp" + " )\\\n";
524 : }
525 31 : cmd += " & wait";
526 31 : if (P.verbose > 2)cout << cmd << endl;
527 31 : if (system(cmd.c_str())) return false;
528 31 : return true;
529 : }
530 :
531 :
532 31 : bool build() {
533 : const bool generateMain =
534 56 : P.RareEvent || P.computeStateSpace >0
535 22 : || P.is_domain_impl_set
536 18 : || P.modelType == External || P.modelType == GSPN_Simulink
537 49 : || P.lhaType == NOT_DET;
538 :
539 62 : string bcmd = P.gcccmd + " " + P.gccflags;
540 :
541 31 : if (P.verbose > 0) {
542 31 : cout << "Parsing OK.\n" << endl;
543 31 : cout << "Start building ... " << endl;
544 : }
545 :
546 62 : auto sources = vector<string>();
547 :
548 : //Compile the SPN
549 31 : if(P.modelType==GSPN || P.modelType == GSPN_Simulink )sources.push_back("spn");
550 :
551 : //Compile the LHA
552 31 : if(!P.lightSimulator)sources.push_back("LHA");
553 :
554 : //Compile main
555 31 : if( generateMain)sources.push_back("main");
556 :
557 31 : if(P.modelType == GSPN_Simulink){
558 0 : if(system(("cp " + P.tmpPath + "/../SKModel.cpp "+ P.tmpPath+"/SKModel.cpp").c_str()) !=0){
559 0 : cerr << "Fail to copy files to temporary directory" << endl;
560 0 : exit(EXIT_FAILURE);
561 : }
562 :
563 0 : sources.push_back("SKModel");
564 : //sources.push_back("multimodel");
565 : }
566 :
567 31 : compileSource(sources);
568 :
569 : //Link SPN and LHA with the library
570 62 : string cmd = bcmd + " -o " + P.tmpPath + "/ClientSim ";
571 31 : for(let file : sources)cmd += P.tmpPath + "/" + file + ".o ";
572 31 : if(P.lightSimulator){
573 0 : cmd += P.Path + "../lib/libClientSimLight.a ";
574 : } else {
575 :
576 31 : if(P.modelType == External || P.modelType == GSPN_Simulink)cmd += P.Path + "../lib/libClientSimSK.a ";
577 31 : if(generateMain){
578 13 : cmd += P.Path + "../lib/libClientSim.a ";
579 : } else {
580 18 : cmd += P.Path + "../lib/libClientSimMain.a ";
581 : }
582 31 : cmd += P.Path + "../lib/libClientSimBase.a ";
583 : };
584 31 : cmd += " " + P.boostlib + " ";
585 :
586 :
587 31 : if (P.verbose > 2)cout << cmd << endl;
588 31 : if (system(cmd.c_str())) return false;
589 :
590 31 : if (P.verbose > 0)cout << "Building OK.\n" << endl;
591 :
592 31 : return true;
593 : }
594 :
595 0 : void generateSamplingLHA(GspnType &spn) {
596 : //bool allcolor = false;
597 : //if (P.tracedPlace == "ALLCOLOR")allcolor= true;
598 0 : P.sampleResol = P.loopTransientLHA;
599 0 : size_t nbsample = static_cast<size_t> (ceil((P.loopLHA / P.sampleResol)));
600 :
601 0 : P.PathLha = P.tmpPath + "/samplelha.lha";
602 0 : ofstream lhastr(P.PathLha.c_str(), ios::out | ios::trunc);
603 :
604 : //lhastr << "NbVariables = "<<1+gReader.spn->tr + P.nbPlace <<";\nNbLocations = 3;\n";
605 0 : lhastr << "const double T=" << P.loopLHA << ";\n";
606 0 : lhastr << "const double invT=" << P.sampleResol << ";\n";
607 0 : lhastr << "const double invT2=" << 1 / P.sampleResol << ";\n";
608 :
609 0 : lhastr << "VariablesList = {time,time2, DISC counter";
610 0 : for (const auto &itt : spn.placeStruct)if (itt.isTraced) {
611 0 : lhastr << ", PLVARACC_" << itt.name;
612 0 : lhastr << ", DISC PLVAR_" << itt.name << "[" << nbsample << "]";
613 : //if(allcolor && itt.colorDom != UNCOLORED_DOMAIN){
614 : // gReader.iterateDom("", "_", "","","","" ,gReader.spn->colDoms[itt.colorDom], 0, [&] (const string &str,const string&){
615 : // lhastr << ", PLVAR_" + itt.name + str;
616 : // });
617 :
618 : //}
619 : }
620 0 : lhastr << "} ;\nLocationsList = {l0,";
621 : //for (size_t i = 0; i < nbsample ; ++i ) lhastr << "l" << i << ", ";
622 0 : lhastr << "l2 };\n";
623 :
624 0 : for (const auto &itt : spn.placeStruct) {
625 0 : if (itt.isTraced)for (size_t i = 0; i < nbsample; ++i) {
626 0 : lhastr << "MeanToken_" << itt.name << "$GRAPH$" << (double) i * P.sampleResol << "$" << (double) (i + 1) * P.sampleResol << "$= AVG(Last( PLVAR_" << itt.name << "[" << i << "]));\n";
627 : /*if(allcolor && itt.colorDom != UNCOLORED_DOMAIN){
628 : gReader.iterateDom("", "_", "","","","" ,gReader.spn->colDoms[itt.colorDom], 0, [&] (const string &str,const string&){
629 : lhastr << "MeanToken_" << itt.name << str << "= AVG(Last( PLVAR_" << itt.name<< str <<"));\n";
630 : });
631 : }*/
632 : }
633 : }
634 0 : lhastr << P.externalHASL << endl;
635 0 : lhastr << "InitialLocations={l0};\nFinalLocations={l2};\n";
636 0 : lhastr << "Locations={" << endl;
637 : //for (size_t i = 0; i < nbsample ; ++i ) {
638 0 : lhastr << "(l" << 0 << ", TRUE , (time:1,time2:1";
639 0 : for (const auto &itt : spn.placeStruct)
640 0 : if (itt.isTraced) {
641 0 : lhastr << ", PLVARACC_" << itt.name << ": " << itt.name << "* invT2 ";
642 : /*if(allcolor && itt.colorDom != UNCOLORED_DOMAIN){
643 : gReader.iterateDom("", "_", "","","","," ,gReader.spn->colDoms[itt.colorDom], 0, [&] (const string &str,const string &str2){
644 : lhastr << ", PLVAR_" << itt.name << str << ": " << itt.name << "[" << str2 <<"]* invT ";
645 : });
646 : }*/
647 : }
648 0 : lhastr << "));" << endl;
649 : //}
650 0 : lhastr << "(l2, TRUE , (time:1,time2:1));};\n";
651 0 : lhastr << "Edges={";
652 : //for (size_t i = 0; i < nbsample ; ++i ) {
653 0 : lhastr << "((l0,l0),ALL,time<= invT ,#);";
654 0 : lhastr << "((l0,l0),#,time=invT ,{time=0,counter=counter+1";
655 0 : for (const auto &itt : spn.placeStruct)if (itt.isTraced) {
656 0 : lhastr << ", PLVARACC_" << itt.name << " = 0.0 ";
657 0 : lhastr << ", PLVAR_" << itt.name << "[" << "counter" << "]=PLVARACC_" << itt.name;
658 : }
659 0 : lhastr << "});" << endl;
660 0 : lhastr << "((l0,l2),# , time2 >= " << P.loopLHA + P.sampleResol * 0.001 << ",#);";
661 :
662 : //}
663 :
664 0 : lhastr << "};";
665 0 : lhastr.close();
666 :
667 0 : }
668 :
669 0 : void generateEmptyLHA(){
670 0 : P.PathLha = P.tmpPath + "/emptylha.lha";
671 0 : ofstream lhastr(P.PathLha.c_str(), ios::out | ios::trunc);
672 :
673 0 : lhastr << "VariablesList = {time};" <<endl;
674 0 : lhastr << "LocationsList = {l0, l1};" <<endl;
675 0 : lhastr << "PROB;" << endl;
676 0 : lhastr << "InitialLocations={l0};" << endl;
677 0 : lhastr << "FinalLocations={l1};" << endl;
678 0 : lhastr << "Locations={ (l0, TRUE); (l1, TRUE); };" << endl;
679 0 : lhastr << "Edges={ ((l0,l0),ALL, # ,#);} ;" << endl;
680 :
681 0 : lhastr.close();
682 :
683 0 : }
684 :
685 12 : void generateLoopLHA(GspnType &spn) {
686 : //If the automaton need to be generated to mesure simple perfomance indices generate it
687 : //An automaton is produce with two loop the first make time elapse until transient time
688 : //elapse and then compute the mean number of token in each place and the throughput
689 : //of each transition
690 12 : bool allcolor = false;
691 12 : if (P.tracedPlace.count("ALLCOLOR")>0.0)allcolor = true;
692 :
693 :
694 12 : P.PathLha = P.tmpPath + "/looplha.lha";
695 24 : ofstream lhastr(P.PathLha.c_str(), ios::out | ios::trunc);
696 :
697 12 : if(P.generateLHA ==TimeLoop){
698 12 : lhastr << "const double T=" << P.loopLHA << ";\n";
699 12 : lhastr << "const double invT=" << 1 / P.loopLHA << ";\n";
700 : } else {
701 0 : lhastr << "const double TDiscr=" << P.loopLHA << ";\n";
702 0 : lhastr << "const double invT= 1.0 ;\n";
703 : }
704 12 : lhastr << "const double Ttrans=" << P.loopTransientLHA << ";\n";
705 12 : lhastr << "VariablesList = {time,DISC countT";
706 136 : for (let itt : spn.transitionStruct)
707 124 : if (itt.isTraced)lhastr << ", " << itt.name;
708 :
709 165 : for (let itt : spn.placeStruct) {
710 153 : if (itt.isTraced) {
711 101 : lhastr << ", PLVAR_" << itt.name;
712 101 : if (allcolor && itt.colorDom != UNCOLORED_DOMAIN) {
713 0 : spn.iterateDom("", "_", "", "", "", "", spn.colDoms[itt.colorDom], 0, [&] (const string &str, const string&) {
714 0 : lhastr << ", PLVAR_" + itt.name + str;
715 0 : });
716 : }
717 : }
718 : }
719 12 : lhastr << "} ;\nLocationsList = {l0, l1,l2};\n";
720 :
721 12 : auto nbHASL = 0;
722 136 : for (let itt : spn.transitionStruct)
723 124 : if (itt.isTraced){
724 82 : nbHASL++;
725 82 : lhastr << "Throughput_" << itt.name << "= AVG(Last(" << itt.name << "));\n";
726 : }
727 165 : for (let itt : spn.placeStruct)
728 153 : if (itt.isTraced) {
729 101 : nbHASL++;
730 101 : lhastr << "MeanToken_" << itt.name << "= AVG(Last( PLVAR_" << itt.name << "));\n";
731 101 : if (allcolor && itt.colorDom != UNCOLORED_DOMAIN) {
732 0 : spn.iterateDom("", "_", "", "", "", "", spn.colDoms[itt.colorDom], 0, [&] (const string &str, const string&) {
733 0 : lhastr << "MeanToken_" << itt.name << str << "= AVG(Last( PLVAR_" << itt.name << str << "));\n";
734 0 : });
735 : }
736 : }
737 12 : lhastr << P.externalHASL << endl;
738 12 : if(P.externalHASL.empty() && nbHASL==0)
739 2 : lhastr << "PROB;" << endl;
740 :
741 12 : const auto stopcond = (P.generateLHA == TimeLoop ? "time<=T," : "countT<=TDiscr -1,");
742 :
743 12 : lhastr << "InitialLocations={l0};\nFinalLocations={l2};\n";
744 12 : lhastr << "Locations={\n(l0, TRUE, (time:1));\n(l1, TRUE, (time:1 ";
745 165 : for (let itt : spn.placeStruct)
746 153 : if (itt.isTraced) {
747 101 : lhastr << ", PLVAR_" << itt.name << ": " << itt.name << "* invT ";
748 101 : if (allcolor && itt.colorDom != UNCOLORED_DOMAIN) {
749 0 : spn.iterateDom("", "_", "", "", "", ",", spn.colDoms[itt.colorDom], 0, [&] (const string &str, const string & str2) {
750 0 : lhastr << ", PLVAR_" << itt.name << str << ": " << itt.name << "[" << str2 << "]* invT ";
751 0 : });
752 : }
753 : }
754 :
755 12 : lhastr << "));\n(l2, TRUE);\n};\n";
756 12 : lhastr << "Edges={\n((l0,l0),ALL,time<= Ttrans ,#);\n((l0,l1),#,time=Ttrans ,{time=0});\n";
757 12 : size_t nbplntr = 0;
758 136 : for (let itt : spn.transitionStruct) {
759 124 : if (itt.isTraced) {
760 82 : lhastr << "((l1,l1),{" << itt.name << "}," << stopcond;
761 82 : if(P.loopLHA>0.0){
762 82 : lhastr << "{" << itt.name << " = " << itt.name << " + invT, countT = countT+1 });\n";
763 : }else{
764 0 : lhastr << "{" << itt.name << " = " << itt.name << " + 1, countT = countT+1 });\n";
765 : }
766 42 : } else nbplntr++;
767 : }
768 12 : if (nbplntr > 0) {
769 2 : lhastr << "((l1,l1),{";
770 2 : nbplntr = 0;
771 44 : for (let itt : spn.transitionStruct)
772 42 : if (!itt.isTraced) {
773 42 : if (nbplntr > 0)lhastr << ",";
774 42 : lhastr << itt.name;
775 42 : nbplntr++;
776 : }
777 2 : lhastr << "}," << stopcond;
778 2 : lhastr << " # );" << endl;
779 : }
780 12 : if (P.generateLHA == TimeLoop){
781 12 : lhastr << "((l1,l2),#,time=T ,#);\n};";
782 0 : }else lhastr << "((l1,l2),ALL,countT=TDiscr ,#);\n};";
783 12 : lhastr.close();
784 117 : }
|
