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 parameters.cpp *
24 : * Created by Benoit Barbot on 08/02/12. *
25 : *******************************************************************************
26 : */
27 :
28 : #include "parameters.hpp"
29 :
30 : #include <iostream>
31 : #include <cstdlib>
32 : #include <getopt.h>
33 : #include <string.h>
34 : #include <unistd.h>
35 : #include <sys/types.h>
36 : #include <sys/ioctl.h>
37 : #include <stdio.h>
38 :
39 : using namespace std;
40 :
41 : #define BUILD_VERSION "Cosmos 1.6"
42 :
43 : #ifdef __APPLE__
44 : #include <mach-o/dyld.h>
45 : void findBinaryPath(parameters& P) {
46 : char path[1024];
47 : uint32_t size = sizeof(path);
48 : if (_NSGetExecutablePath(path, &size) != 0){
49 : printf("buffer too small; need size %u\n", size);
50 : exit(EXIT_FAILURE);
51 : }
52 :
53 : P.Path=path;
54 : std::string::size_type t = P.Path.find_last_of("/");
55 : P.Path = P.Path.substr(0, t);
56 : P.Path.append("/");
57 : }
58 : #elif __linux__
59 0 : void findBinaryPath(parameters& P) {
60 : char path[1024];
61 : char link[512];
62 0 : sprintf(link, "/proc/%d/exe", getpid());
63 0 : int sz = readlink(link, path, 1024);
64 0 : if (sz >= 0) {
65 0 : path[sz] = 0;
66 0 : P.Path = path;
67 0 : std::string::size_type t = P.Path.find_last_of("/");
68 0 : P.Path = P.Path.substr(0, t);
69 0 : P.Path.append("/");
70 : }
71 0 : }
72 : #else
73 : #error "Operating system not supported"
74 : #endif
75 :
76 :
77 : /**
78 : * Constructor for parameters, set all default values
79 : */
80 63 : parameters::parameters() :
81 : commandLine(""),
82 : verbose(2),
83 : interactive(false),
84 : updatetime(100),
85 : seed(0),
86 : randomGen(MT19937),
87 : Njob(1),
88 :
89 : epsilon(0.000001),
90 : continuousStep(1),
91 : Level(0.99),
92 : Width(0.001),
93 : Batch(1000),
94 : MaxRuns(2000000),
95 : sequential(true),
96 : relative(false),
97 : chernoff(false),
98 :
99 : comp_uuid("tmpuuid"),
100 : tmpPath("tmp"),
101 : tmpStatus((TmpStat)(TS_GEN | TS_BUILD | TS_RUN | TS_DESTROY)),
102 : reuse(false),
103 : modelType(GSPN),
104 : lhaType(DET),
105 : Path(""),
106 : PathGspn(""),
107 : PathLha(""),
108 : constants(),
109 : generateLHA(NoGen),
110 : loopLHA(0.0),
111 : loopTransientLHA(0.0),
112 : CSLformula(""),
113 : externalHASL(""),
114 :
115 : localTesting(false),
116 : RareEvent(false),
117 : DoubleIS(false),
118 : BoundedRE(0),
119 : horizon(100),
120 : BoundedContinuous(false),
121 :
122 : CountTrans(false),
123 : StringInSpnLHA(false),
124 :
125 :
126 : GMLinput(false),
127 : computeStateSpace(0),
128 : lumpStateSpace(false),
129 : alligatorMode(false),
130 : guiGreatSpnMode(false),
131 : unfold(""),
132 : isTTY(true),
133 : terminalWidth(80),
134 : graceFullEnding(0),
135 :
136 : gcccmd(CPP_COMPILER),
137 : boostpath(BOOST_PATH),
138 : gccflags("-Wno-return-type -std=gnu++11"),
139 : boostlib(BOOST_LIB),
140 : lightSimulator(false),
141 :
142 : prismPath(""),
143 : dataoutput(""),
144 : dataraw(""),
145 : datatrace(""),
146 : sampleResol(0.0),
147 : dataPDFCDF(""),
148 : gnuplotDriver(""),
149 : tracedPlace(),
150 : dotfile(""),
151 : magic_values(""),
152 : use_magic_print(false),
153 : is_domain_impl_set(false),
154 :
155 : HaslFormulas(vector<HaslFormulasTop*>(0)),
156 : HaslFormulasname(vector<string>(0)),
157 : nbAlgebraic(0),
158 : nbQualitatif(0),
159 63 : nbPlace(0)
160 : //prismPath = "/import/barbot/prism-4.0.1-linux64/bin/prism";
161 : {
162 63 : tracedPlace.insert(pair<string, int>("ALL",0));
163 63 : isTTY = isatty(fileno(stdout));
164 : struct winsize ws;
165 63 : if(isTTY && ioctl(fileno(stdout), TIOCGWINSZ, &ws)>=0){
166 0 : if(ws.ws_col == 0){
167 0 : isTTY=false;
168 : }else{
169 0 : terminalWidth=ws.ws_col;
170 : }
171 : }
172 :
173 63 : const char *env = getenv("FROM_GUI");
174 63 : guiGreatSpnMode = (env != nullptr && 0 == strcmp(env, "1"))>0;
175 63 : if(guiGreatSpnMode){
176 0 : isTTY = true;
177 0 : terminalWidth =120;
178 0 : verbose=1;
179 : }
180 :
181 63 : }
182 :
183 : /**
184 : * Display the usage text
185 : */
186 0 : void parameters::usage() {
187 0 : cout << "usage: Cosmos [-ghsr] [-vb arg] ";
188 0 : cout << "[--alligator-mode] ";
189 0 : cout << "[--level arg] [--width arg] [--batch arg] [--max-run arg] ";
190 0 : cout << "[--set-Horizon arg] [--njob arg] ";
191 0 : cout << "gspn_file lha_file" << endl;
192 :
193 0 : cout << "General options:" << endl;
194 0 : cout << "\t--version\tdisplay version number" << endl;
195 0 : cout << "\t-v,--verbose arg\tset the verbose level" << endl;
196 0 : cout << "\t-i,--interactive \tAsk the user to choose next transition" << endl;
197 0 : cout << "\t--update-time\t set the time in second beetween two updates of the display" << endl;
198 0 : cout << "\t-h,--help \tdisplay this message" << endl;
199 0 : cout << "\t--njob \tset the number of parralel thread" << endl;
200 0 : cout << "\t--gppcmd \tset the C++ compiler (default g++)" << endl;
201 0 : cout << "\t--gppflags\tset the C++ compiler flags (default -O3)" << endl;
202 0 : cout << "\t--reuse\ttry to load previous simulation and save simulations" << endl;
203 0 : cout << "\t--use-domainset\tuse the Set implementation on Places and Transitions" << endl;
204 :
205 0 : cout << "Option of simulation:" << endl;
206 0 : cout << "\t--level \tset the confidence level for the simulation (default=0.99)" << endl;
207 0 : cout << "\t--width \tset the width of the confidence interval (default=0.001)" << endl;
208 0 : cout << "\t--batch \tset the size of batch of simulation (default=1000)" << endl;
209 0 : cout << "\t--max-run \tset the maximal number of run (default=2000000)" << endl;
210 0 : cout << "\t--relative \tUse relative confidence interval instead of absolute one" << endl;
211 0 : cout << "\t--chernoff (level | width | nbrun)\tuse chernoff-hoeffding bound to compute the number of simulation" << endl;
212 0 : cout << "\t--seed \tSpecify the seed for the random generator, 0 allow to take a random value" << endl;
213 0 : cout << "\t--local-test \tUse local testing faster on big net" << endl;
214 0 : cout << "\t--const \toverride constant value of the model" << endl;
215 0 : cout << "\t--random-generator (MT19937 | VDC | Kronecker) \tUse a pseudo random number generator" << endl;
216 :
217 0 : cout << "Rare event options:" << endl;
218 0 : cout << "\t-r \tUnbounded rare event mode" << endl;
219 0 : cout << "\t-b arg \tDiscrete bounded rare event mode, arg is the method to use to stop vector" << endl;
220 0 : cout << "\t--set-Horizon arg \tSet the horizon for bounded rare event mode arg must be an integer in discrete bounded case" << endl;
221 0 : cout << "\t-c \tContinuous bounded rare event mode." << endl;
222 0 : cout << "\t--epsilon arg \tError level of the fox glynn algorithme" << endl;
223 0 : cout << "\t--step-continuous arg \tSize of step of the continuous method" << endl;
224 :
225 :
226 0 : cout << "Miscellaneous options:" << endl;
227 0 : cout << "\t-g,--grmlinput \tforce use of grml file format for input file" << endl;
228 0 : cout << "\t--alligator-mode \toutput easy to parse result" << endl;
229 0 : cout << "\t--unfold arg \tUnfold the GSPN given as input" << endl;
230 0 : cout << "\t--output-model arg \tReturn the GSPN file given as input" << endl;
231 0 : cout << "\t--count-transition \tAdd a Hasl formula for wich count the number of time each transition occurs" << endl;
232 0 : cout << "\t--tmp-path arg \tPath to the temporary directory by default ./tmp/" << endl;
233 0 : cout << "\t--bin-path arg \tPath to the binary of cosmos (guess automatically)" << endl;
234 0 : cout << "\t--tmp-status arg \tDo not remove or do not rebuild tmp directory: 0 default->rebuild,destroy; 1->do not build;2->do not destroy;3-> do not build nor destroy" << endl;
235 0 : cout << "\t--debug-string \tAdd transition and place name to the compile file for debuging" << endl;
236 0 : cout << "\t-d,--outputdata \tOutput successive result in the blank separated file format" << endl;
237 0 : cout << "\t--output-raw \tOutput the result of each trajectory in a file for debug purpose" << endl;
238 0 : cout << "\t--output-trace arg resol \tOutput the trace each trajectory in the file arg with a resolution of resol" << endl;
239 0 : cout << "\t--output-graph \tOutput the result of CDF or PDF formula in gnuplot file format" << endl;
240 0 : cout << "\t--output-dot \tOutput the Petri net in a dot file" << endl;
241 0 : cout << "\t--gnuplot-driver terminal\tRun gnuplot on the output datafile to produce graph use the given terminal for gnuplot" << endl;
242 0 : cout << "\t--trace-pt arg\tSpecify which place to trace in all the output file, arg is a comma separated list of places and transitions name" << endl;
243 0 : cout << "\t--HASL-expression \tAllow to define an HASL formula from the command line" << endl;
244 0 : cout << "\t--loop t1 [--transtient t2] \tGenerate an LHA that loop for t1 times unit and then t2 time unit. The --transient option alone do not do anything" << endl;
245 0 : cout << "\t--sampling t1 t2 \tGenerate an LHA that loop for t1 times unit and sample the average number of token each t2 time units" << endl;
246 0 : cout << "\t--formula f\t specify a CSL formula to use instead of an automata" << endl;
247 0 : cout << "\t--prism \tExport the state space and launch prism." << endl;
248 0 : cout << "\t-s,--state-space \tExport the state space." << endl;
249 0 : cout << "\t--lump-state-space \tLump the state space before exporting." << endl;
250 0 : cout << "\t--no-magic-print\tIgnore magic_print when using custom C code in models" << endl;
251 :
252 :
253 0 : }
254 :
255 :
256 215 : Poption parameters::parsersingleOpt(int i)const{
257 215 : switch (i) {
258 : case 'g':
259 0 : return CO_grml_input;
260 : case 'i':
261 0 : return CO_interactive;
262 : case 'h':
263 0 : return CO_help;
264 : case 's':
265 1 : return CO_state_space;
266 : case 'c':
267 2 : return CO_boundedcountiniouceRE;
268 : case 'r':
269 1 : return CO_rareevent;
270 : case 'b':
271 5 : return CO_boundedRE;
272 : case 'v':
273 0 : return CO_verbose;
274 : case 'p':
275 0 : return CO_prism;
276 : case 'd':
277 0 : return CO_output_data;
278 : default:
279 206 : return (Poption)i;
280 : }
281 : }
282 :
283 : /**
284 : * Parse the command line and set the parameter structure
285 : * with the option set by the user
286 : */
287 34 : void parameters::parseCommandLine(int argc, char** argv) {
288 :
289 : //Find the path to the directory containing Cosmos binary.
290 67 : string st = argv[0];
291 34 : if (st == "./Cosmos"){Path = "";} //local directory
292 34 : else if(st.length()>6){Path=st.substr(0,st.length()-6);} //direct Path to Cosmos
293 0 : else findBinaryPath(*this); //Ask the system where Cosmos is (System dependant)
294 :
295 :
296 34 : commandLine = argv[0];
297 460 : for (int i = 1; i<argc; i++){
298 426 : commandLine += " ";
299 426 : commandLine += argv[i];
300 : }
301 :
302 : int c;
303 :
304 : while (1) {
305 : static struct option long_options[] ={
306 : /* Options for the simulator*/
307 : {"level", required_argument, 0, CO_level},
308 : {"width", required_argument, 0, CO_width},
309 : {"batch", required_argument, 0, CO_batch},
310 : {"max-run", required_argument, 0, CO_max_run},
311 : {"seed", required_argument, 0, CO_seed},
312 : {"local-test", no_argument , 0, CO_local_test},
313 : {"sampling", required_argument, 0, CO_sampling},
314 : {"loop", required_argument, 0, CO_loop},
315 : {"transient", required_argument, 0, CO_transient},
316 : {"formula", required_argument, 0, CO_formula},
317 : {"chernoff", required_argument, 0, CO_chernoff},
318 : {"relative", no_argument , 0, CO_relative},
319 : {"const", required_argument, 0, CO_const},
320 : {"reuse", no_argument , 0, CO_reuse},
321 : {"use-van-der-corput",no_argument, 0, CO_VDC},
322 : {"random-generator",required_argument, 0, CO_RandomGen},
323 : {"gracefull-ending", no_argument, 0, CO_gracefull_ending},
324 :
325 : /* Options for the rare event engine */
326 : {"rareevent", no_argument , 0, CO_rareevent},
327 : {"boundedcountiniousRE", no_argument, 0, CO_boundedcountiniouceRE},
328 : {"boundedRE", required_argument, 0, CO_boundedRE},
329 : {"step-continuous", required_argument, 0, CO_step_continuous},
330 : {"epsilon", required_argument, 0, CO_epsilon},
331 : {"set-Horizon", required_argument, 0, CO_set_Horizon},
332 : {"state-space", no_argument , 0, CO_state_space},
333 : {"lump-state-space", no_argument , 0, CO_lump},
334 : {"prism", no_argument , 0, CO_prism},
335 : {"normalize-IS", no_argument , 0, CO_normalize_IS},
336 :
337 : /* CosyVerif Options */
338 : {"gmlinput", no_argument , 0, CO_grml_input},
339 : {"grml-input", no_argument , 0, CO_grml_input},
340 : {"alligator-mode", no_argument , 0, CO_alligator_mode},
341 : {"gui-greatSPN-mode",no_argument , 0, CO_gui_greatSPN_mode},
342 :
343 : /* Output function */
344 : {"verbose", required_argument, 0, CO_verbose},
345 : {"interactive", no_argument , 0, CO_interactive},
346 : {"update-time", required_argument, 0, CO_update_time},
347 : {"outputdata", required_argument, 0, CO_output_data},
348 : {"output-data", required_argument, 0, CO_output_data},
349 : {"output-raw", required_argument, 0, CO_output_raw},
350 : {"output-trace", required_argument, 0, CO_output_trace},
351 : {"output-PDFCDF", required_argument, 0, CO_output_graph},
352 : {"output-graph", required_argument, 0, CO_output_graph},
353 : {"output-dot", required_argument , 0, CO_output_dot},
354 : {"gnuplot-driver", required_argument, 0, CO_gnuplot_driver},
355 : {"trace-place", required_argument, 0, CO_trace_pt},
356 : {"trace-pt", required_argument, 0, CO_trace_pt},
357 :
358 :
359 : /* Miscellaneous options */
360 : {"not-gspn", no_argument , 0, CO_not_gspn},
361 : {"force-TTY", no_argument , 0, CO_force_TTY},
362 : {"unfold", required_argument, 0, CO_unfold},
363 : {"output-model", required_argument,0, CO_output_model},
364 : {"HASL-formula", required_argument, 0, CO_HASL_formula},
365 : {"HASL-expression", required_argument, 0, CO_HASL_formula},
366 : {"njob", required_argument, 0, CO_njob},
367 : {"gppcmd", required_argument, 0, CO_gppcmd},
368 : {"gppflags", required_argument, 0, CO_gppflags},
369 : {"light-simulator", no_argument , 0, CO_light_simulator},
370 : {"help", no_argument , 0, CO_help},
371 : {"count-transition", no_argument , 0, CO_count_transition},
372 : {"debug-string", no_argument , 0, CO_debug_string},
373 : {"tmp-path", required_argument, 0, CO_tmp_path},
374 : {"tmp-status", required_argument, 0, CO_tmp_status},
375 : {"bin-path", required_argument, 0, CO_bin_path},
376 : {"prism-path", required_argument, 0, CO_prism_path},
377 : {"magic-values", required_argument,0, CO_magic_values},
378 : {"no-magic-print", no_argument, 0, CO_use_magic_print},
379 : {"use-setdomain-impl", no_argument, 0, CO_domain_impl},
380 : {"use-domainset", no_argument, 0, CO_domain_impl},
381 : {"version", no_argument , 0, CO_version},
382 :
383 : {0, 0, 0, 0}
384 : };
385 : /* getopt_long stores the option index here. */
386 248 : int option_index = 0;
387 :
388 : c = getopt_long(argc, argv, "gihspcrb:v:d:",
389 248 : long_options, &option_index);
390 :
391 : /* Detect the end of the options. */
392 248 : if (c == -1)
393 33 : break;
394 :
395 215 : switch (parsersingleOpt(c)) {
396 : case CO_help:
397 0 : usage();
398 0 : exit(EXIT_SUCCESS);
399 : break;
400 :
401 0 : case CO_verbose:verbose = atoi(optarg);
402 0 : if (verbose >= 4)StringInSpnLHA = true;
403 0 : break;
404 :
405 : case CO_interactive:
406 0 : interactive = true;
407 0 : StringInSpnLHA = true;
408 0 : break;
409 :
410 0 : case CO_update_time:updatetime = chrono::duration_cast<chrono::milliseconds>(chrono::duration<double> (atof(optarg)));
411 0 : break;
412 :
413 0 : case CO_grml_input:GMLinput = true;
414 0 : break;
415 :
416 : case CO_rareevent:
417 1 : RareEvent = true;
418 1 : StringInSpnLHA = true; // Need to know the name of place to find
419 : // place begining with "RE_"
420 1 : localTesting = false; //Need to unfire transition not implemented for local testing
421 1 : relative = true;
422 1 : break;
423 :
424 : case CO_relative:
425 0 : relative = true;
426 0 : break;
427 :
428 : case CO_normalize_IS:
429 0 : DoubleIS = true;
430 0 : break;
431 :
432 : case CO_gracefull_ending:
433 45 : graceFullEnding = 1;
434 45 : break;
435 :
436 5 : case CO_boundedRE:BoundedRE = atoi(optarg);
437 5 : StringInSpnLHA = true;
438 5 : RareEvent = true;
439 5 : relative = true;
440 5 : break;
441 :
442 2 : case CO_boundedcountiniouceRE:BoundedContinuous = true;
443 2 : RareEvent = true;
444 2 : break;
445 :
446 5 : case CO_set_Horizon :horizon = atof(optarg);
447 5 : break;
448 :
449 1 : case CO_state_space:computeStateSpace = 2;
450 1 : StringInSpnLHA = true;
451 1 : localTesting = false; //Need to unfire transition, not implemented for local testing
452 1 : break;
453 :
454 0 : case CO_lump: lumpStateSpace = true;
455 0 : break;
456 :
457 2 : case CO_prism:computeStateSpace = 1;
458 2 : StringInSpnLHA = true;
459 2 : localTesting = false; //Need to unfire transition, not implemented for local testing
460 2 : break;
461 :
462 0 : case CO_alligator_mode:alligatorMode = true;
463 0 : verbose = 0;
464 0 : break;
465 :
466 0 : case CO_force_TTY : isTTY = true; break;
467 :
468 : case CO_gui_greatSPN_mode:
469 0 : guiGreatSpnMode =true;
470 0 : isTTY = true;
471 0 : terminalWidth=120;
472 0 : break;
473 :
474 1 : case CO_unfold:unfold = optarg;
475 1 : break;
476 0 : case CO_output_model:outputModel =optarg;
477 0 : break;
478 :
479 43 : case CO_level:Level = atof(optarg);
480 43 : break;
481 : case CO_width:
482 : {
483 0 : double w = atof(optarg);
484 0 : if(w==0.0)sequential=false;
485 0 : Width = w;
486 : }
487 0 : break;
488 8 : case CO_batch: Batch = atol(optarg);
489 8 : break;
490 24 : case CO_max_run: MaxRuns = atol(optarg);
491 24 : break;
492 : case CO_chernoff:
493 0 : chernoff = true;
494 0 : sequential = false;
495 0 : if (strcmp(optarg, "level") == 0)Level = 0;
496 0 : else if (strcmp(optarg, "width") == 0)Width = 0;
497 0 : else if (strcmp(optarg, "nbrun") == 0)MaxRuns = (unsigned long)-1;
498 : else {
499 0 : cerr << "Required one of (level | width | nbrun) to specify which ";
500 0 : cerr << "parameter should be computed" << endl;
501 0 : usage();
502 0 : exit(EXIT_FAILURE);
503 : }
504 0 : break;
505 0 : case CO_local_test: localTesting = !localTesting;
506 0 : break;
507 1 : case CO_njob: Njob = atoi(optarg);
508 1 : break;
509 0 : case CO_epsilon: epsilon = atof(optarg);
510 0 : break;
511 0 : case CO_step_continuous: continuousStep = atoi(optarg);
512 0 : break;
513 1 : case CO_output_data: dataoutput = optarg;
514 1 : break;
515 1 : case CO_output_raw: dataraw = optarg;
516 1 : break;
517 0 : case CO_output_dot: dotfile = optarg;
518 0 : break;
519 0 : case CO_magic_values: magic_values = optarg;
520 0 : use_magic_print = true;
521 0 : break;
522 0 : case CO_use_magic_print: use_magic_print = false;
523 0 : break;
524 4 : case CO_domain_impl: is_domain_impl_set = true;
525 4 : break;
526 : case CO_output_trace:
527 1 : datatrace = optarg;
528 1 : StringInSpnLHA = true;
529 1 : if (optind == argc) {
530 0 : usage();
531 0 : exit(EXIT_FAILURE);
532 : }
533 1 : sampleResol = atof(argv[optind]);
534 1 : optind++;
535 1 : break;
536 :
537 0 : case CO_output_graph: dataPDFCDF = optarg;
538 0 : break;
539 0 : case CO_count_transition: CountTrans = true;
540 0 : break;
541 0 : case CO_debug_string: StringInSpnLHA = true;
542 0 : break;
543 0 : case CO_tmp_path: tmpPath = optarg;
544 0 : break;
545 0 : case CO_bin_path: Path = optarg;
546 0 : break;
547 : case CO_tmp_status:
548 : {
549 1 : int order = 0;
550 1 : if (strcmp(optarg, "full") == 0) order = 0;
551 1 : else if (strcmp(optarg, "keep") == 0)order = 2;
552 1 : else if (strcmp(optarg, "reuse") == 0)order = 3;
553 1 : else if (strcmp(optarg, "only-build") == 0)order = 5;
554 1 : else if (strcmp(optarg, "only-gen") == 0)order = 6;
555 0 : else { order = atoi(optarg);};
556 1 : switch (order) {
557 : case 0:
558 0 : tmpStatus = (TmpStat)( TS_GEN | TS_BUILD | TS_RUN | TS_DESTROY);
559 0 : break;
560 : case 1:
561 0 : tmpStatus = (TmpStat)( TS_RUN | TS_DESTROY);
562 0 : break;
563 : case 2:
564 0 : tmpStatus = (TmpStat)( TS_GEN | TS_BUILD | TS_RUN );
565 0 : break;
566 : case 3:
567 0 : tmpStatus = (TmpStat)( TS_RUN );
568 0 : break;
569 : case 4:
570 0 : tmpStatus = (TmpStat)( TS_BUILD | TS_RUN );
571 : case 5:
572 0 : tmpStatus = (TmpStat)( TS_GEN | TS_BUILD );
573 0 : break;
574 : case 6:
575 1 : tmpStatus = (TmpStat)( TS_GEN );
576 1 : break;
577 :
578 : default:
579 0 : tmpStatus = (TmpStat)atoi(optarg);
580 0 : break;
581 : }
582 1 : break;
583 : }
584 : case CO_reuse:
585 0 : tmpStatus = (TmpStat)(tmpStatus & (TS_GEN | TS_BUILD | TS_RUN));
586 0 : reuse = true;
587 0 : break;
588 0 : case CO_gppcmd: gcccmd = optarg;
589 0 : break;
590 46 : case CO_gppflags: gccflags = optarg;
591 46 : break;
592 : case CO_light_simulator:
593 0 : lightSimulator = true;
594 0 : break;
595 0 : case CO_seed: seed = atoi(optarg);
596 0 : break;
597 0 : case CO_VDC: randomGen = VDC;
598 0 : break;
599 : case CO_RandomGen:
600 0 : if( strcmp(optarg,"VDC")==0) randomGen = VDC;
601 0 : if( strcmp(optarg,"Kronecker")==0) randomGen = VDC;
602 0 : break;
603 2 : case CO_HASL_formula: externalHASL = optarg;
604 2 : break;
605 : case CO_loop:
606 11 : if(optarg[0]!='#'){
607 11 : loopLHA = atof(optarg);
608 11 : generateLHA = TimeLoop;
609 : }else{
610 0 : const auto st = string(optarg);
611 0 : loopLHA = stod(st.substr(1,st.length()-1));
612 0 : generateLHA = ActionLoop;
613 : }
614 11 : PathLha = "LOOP";
615 11 : break;
616 : case CO_sampling:
617 0 : loopLHA = atof(optarg);
618 0 : generateLHA = SamplingLoop;
619 0 : PathLha = "SAMPLING";
620 0 : if (optind == argc) {
621 0 : usage();
622 0 : exit(EXIT_FAILURE);
623 : }
624 0 : loopTransientLHA = atof(argv[optind]);
625 0 : optind++;
626 0 : break;
627 1 : case CO_transient: loopTransientLHA = atof(optarg);
628 1 : break;
629 3 : case CO_formula: CSLformula = optarg;
630 3 : generateLHA = CSL_LHA;
631 3 : break;
632 :
633 0 : case CO_gnuplot_driver: gnuplotDriver = optarg;
634 0 : break;
635 :
636 : case CO_trace_pt:
637 : {
638 1 : tracedPlace.clear();
639 2 : const string st = optarg;
640 1 : for(size_t i=0 ; i< st.length();){
641 0 : auto j = st.find(',',i+1);
642 0 : tracedPlace.insert(pair<string, int>(st.substr(i,j-i),i));
643 0 : if(j == string::npos)break;
644 0 : i=j+1;
645 : }
646 1 : break;
647 : }
648 0 : case CO_prism_path: prismPath = optarg;
649 0 : break;
650 :
651 : case CO_const: // const
652 : {
653 8 : string conststr = optarg;
654 : size_t index, index2;
655 4 : index2 = conststr.find('=', 0) + 1;
656 8 : for (index = 0; index != string::npos; index2 = conststr.find('=', index) + 1) {
657 8 : string varname = conststr.substr(index, index2 - index - 1);
658 4 : index = conststr.find(',', index2);
659 8 : string varvalue;
660 4 : if (index == string::npos) {
661 4 : varvalue = conststr.substr(index2, conststr.length() - index2);
662 : } else {
663 0 : varvalue = conststr.substr(index2, index - index2);
664 0 : index++;
665 : }
666 4 : constants[varname] = varvalue;
667 : }
668 :
669 4 : break;
670 : }
671 :
672 : case CO_not_gspn:
673 : {
674 0 : modelType = External;
675 0 : break;
676 : }
677 :
678 : case CO_version:
679 1 : cout << "Source Version:" << GIT_REVISION << endl;
680 1 : cout << BUILD_VERSION << " Build Date:" << __DATE__ " at " << __TIME__ << endl;
681 1 : cout << "Compiled with ";
682 : #ifdef CMAKE_VERSION
683 : cout << "cmake " << CMAKE_VERSION ;
684 : #else
685 : #ifdef XCODE_VERSION
686 : cout << "Xcode " << XCODE_VERSION ;
687 : #else
688 1 : cout << "automake" ;
689 : #endif
690 : #endif
691 1 : cout <<" : " << CPP_COMPILER << " " << BOOST_PATH << endl;
692 1 : cout << "Default flags: " << gccflags << endl;
693 1 : cout << "Library: " << BOOST_LIB << " " << endl;
694 1 : cout << "Binary Path: " << Path << endl;
695 1 : exit(0);
696 :
697 : default:
698 0 : usage();
699 0 : exit(EXIT_FAILURE);
700 : }
701 :
702 214 : }
703 :
704 :
705 : //Additionnal parameter handling.
706 :
707 : //MaxRuns =0 mean no run.
708 33 : if(MaxRuns==0)tmpStatus= (TmpStat)(tmpStatus & (~TS_RUN));
709 :
710 33 : if (lightSimulator && (tmpStatus & TS_RUN))StringInSpnLHA=true;
711 :
712 33 : if(interactive)Njob=1;
713 :
714 : //Batch must be smaller than maxRuns
715 33 : if (Batch != 0)Batch = min(Batch,MaxRuns);
716 :
717 33 : if(prismPath.empty())prismPath="prism";
718 :
719 : //If no LHA is required only set the path for the GSPN.
720 : //if (optind + 1 == argc && (loopLHA > 0.0 || !CSLformula.empty() || !unfold.empty() || lightSimulator)) {
721 33 : if (optind + 1 == argc) {
722 15 : PathGspn = argv[optind];
723 15 : if(generateLHA == NoGen) generateLHA = EmptyLoop;
724 18 : } else if (optind + 2 == argc) {
725 18 : PathGspn = argv[optind];
726 18 : PathLha = argv[optind + 1];
727 : } else {
728 0 : if (optind + 1 > argc) {
729 0 : cout << "Model file is required." << endl;
730 : } else {
731 0 : cout << "Unrecognize option:" << argv[optind + 2] << endl;
732 : }
733 :
734 0 : usage();
735 0 : exit(EXIT_FAILURE);
736 : }
737 :
738 33 : if( ! (tmpStatus & TS_GEN)){
739 0 : PathLha = tmpPath+"/LHA.cpp";
740 : }
741 :
742 222 : }
743 :
744 :
|
