diff --git a/main.cc b/main.cc index afc90f7..25b3aa8 100644 --- a/main.cc +++ b/main.cc @@ -34,7 +34,7 @@ int main(int argc, char **argv) int c; int option_index = 0; - while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxz", long_options, &option_index)) != -1) + while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxzh", long_options, &option_index)) != -1) { switch (c) { case 0: @@ -90,8 +90,12 @@ int main(int argc, char **argv) opts->reorder_reach = true; opts->reorder_trans = true; break; + case 'h': + usage_error = true; + break; default: usage_error = true; + break; } } @@ -108,40 +112,7 @@ int main(int argc, char **argv) if (usage_error) { - cout << endl - << " ------------------------------------" << endl - << " -- Reaction Systems Model Checker --" << endl - << " ------------------------------------" << endl - << endl - << " Version: " << VERSION << endl - << " Contact: " << AUTHOR << endl - << endl -#ifndef PUBLIC_RELEASE - << " ###################################" << endl - << " THIS IS A PRIVATE VERSION OF RSMC " << endl - << " PLEASE, DO NOT DISTRIBUTE " << endl - << " ###################################" << endl - << endl -#endif - << " Usage: " << argv[0] << " [options] " << endl << endl - << " TASKS:" << endl - << " -c -- perform RSCTL model checking" << endl - //<< " -f K -- generate SMT input for the depth K" << endl - << " -P -- print parsed system" << endl - << " -r -- print reactions" << endl - << " -s -- print the set of all the reachable states" << endl - << " -t -- print the set of all the reachable states with their successors" << endl - << endl << " OTHER:" << endl - << " -b -- disable bounded model checking (BMC) heuristic" << endl - << " -x -- use partitioned transition relation (may use less memory)" << endl - << " -z -- use reordering of the BDD variables" << endl - << " -v -- verbose (can be used more than once to increase verbosity)" << endl - << " -p -- show progress (where possible)" << endl - << endl - << " Benchmarking options:" << endl - << " -m -- measure and display time and memory usage" << endl - << " -B -- display an easy to parse summary (enables -m)" << endl - << endl; + print_help(std::string(argv[0])); return 100; } @@ -233,4 +204,43 @@ int main(int argc, char **argv) return 0; } +void print_help(std::string path_str) +{ + cout << endl + << " ------------------------------------" << endl + << " -- Reaction Systems Model Checker --" << endl + << " ------------------------------------" << endl + << endl + << " Version: " << VERSION << endl + << " Contact: " << AUTHOR << endl + << endl +#ifndef PUBLIC_RELEASE + << " ###################################" << endl + << " THIS IS A PRIVATE VERSION OF RSMC " << endl + << " PLEASE, DO NOT DISTRIBUTE " << endl + << " ###################################" << endl + << endl +#endif + << " Usage: " << path_str << " [options] " << endl << endl + << " TASKS:" << endl + << " -c -- perform RSCTL model checking" << endl + //<< " -f K -- generate SMT input for the depth K" << endl + << " -P -- print parsed system" << endl + << " -r -- print reactions" << endl + << " -s -- print the set of all the reachable states" << endl + << " -t -- print the set of all the reachable states with their successors" << endl + << endl << " OTHER:" << endl + << " -b -- disable bounded model checking (BMC) heuristic" << endl + << " -x -- use partitioned transition relation (may use less memory)" << endl + << " -z -- use reordering of the BDD variables" << endl + << " -v -- verbose (can be used more than once to increase verbosity)" << endl + << " -p -- show progress (where possible)" << endl + << endl + << " Benchmarking options:" << endl + << " -m -- measure and display time and memory usage" << endl + << " -B -- display an easy to parse summary (enables -m)" << endl + << endl; +} + /** EOF **/ + diff --git a/main.hh b/main.hh index 5a7b11b..5d95f44 100644 --- a/main.hh +++ b/main.hh @@ -22,9 +22,11 @@ #include "options.hh" #include "memtime.hh" -#define VERSION "1.0alpha" -#define AUTHOR "Artur Męski " +#define VERSION "2.0 ALPHA" +#define AUTHOR "Artur Meski " using std::cout; using std::endl; +void print_help(std::string path_str); + #endif diff --git a/rs.cc b/rs.cc index 5df678a..4b844f4 100644 --- a/rs.cc +++ b/rs.cc @@ -65,6 +65,7 @@ void RctSys::setCurrentProcess(std::string processName) } current_proc_id = getProcessID(processName); + current_process_defined = true; } void RctSys::addProcess(std::string processName) @@ -79,7 +80,7 @@ void RctSys::addProcess(std::string processName) processes_names[processName] = new_proc_id; // reactions for the new process - proc_reactions.push_back(Reactions()); + proc_reactions[new_proc_id] = Reactions(); assert(proc_reactions.size() == new_proc_id+1); } } @@ -132,6 +133,10 @@ void RctSys::pushProduct(std::string entityName) void RctSys::addReactionForCurrentProcess(Reaction reaction) { + if (!current_process_defined) + { + FERROR("Internal error. Current process is not set!"); + } proc_reactions[current_proc_id].push_back(reaction); } @@ -176,7 +181,6 @@ void RctSys::showReactions(void) << "I={" << entitiesToStr(r.inhib) << "}," << "P={" << entitiesToStr(r.prod) << "})" << endl; } - } cout << endl; } diff --git a/rsin_parser.ll b/rsin_parser.ll index ba2cbf8..8ecb732 100644 --- a/rsin_parser.ll +++ b/rsin_parser.ll @@ -55,6 +55,7 @@ blank [ \t] ")" return token::RRB; "[" return token::LSB; "]" return token::RSB; +"=" return token::EQ; "<" return token::LAB; ">" return token::RAB; ":" return token::COL; diff --git a/rsin_parser.yy b/rsin_parser.yy index c947743..02458e7 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -47,7 +47,7 @@ class rsin_driver; %token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS %token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS -%token LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR +%token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR %token AND OR XOR IMPLIES NOT %token EX EU EF EG AX AU AF AG E A X U F G EMPTY @@ -110,10 +110,6 @@ reactionsets: ; processname: IDENTIFIER { - //driver.getReactionSystem()->ctxAutAddState(*$1); - // - // Set the current process name for which we are saving reactions... - // driver.getReactionSystem()->setCurrentProcess(*$1); free($1); } @@ -231,12 +227,18 @@ auttransitions: | auttrans SEMICOL auttransitions ; -auttrans: LCB contextset RCB COL IDENTIFIER RARR IDENTIFIER { +auttrans: LCB proc_contextset RCB COL IDENTIFIER RARR IDENTIFIER { driver.getReactionSystem()->ctxAutAddTransition(*$5, *$7); free($5); free($7); } ; + +proc_contextset: IDENTIFIER EQ LCB contextset RCB { + driver.getReactionSystem()->setCurrentProcess(*$1); + free($1); + } + ; contextset: ctxentity diff --git a/types.hh b/types.hh index cfaf789..b431fa0 100644 --- a/types.hh +++ b/types.hh @@ -21,8 +21,13 @@ struct Reaction { Entities inhib; Entities prod; }; + +typedef unsigned int Process; +typedef std::vector ProcessesById; +typedef std::map ProcessesByName; + typedef std::vector Reactions; -typedef std::vector ReactionsForProc; +typedef std::map ReactionsForProc; typedef std::vector EntitiesById; typedef std::map EntitiesByName; @@ -32,9 +37,7 @@ typedef unsigned int State; typedef std::vector StatesById; typedef std::map StatesByName; -typedef unsigned int Process; -typedef std::vector ProcessesById; -typedef std::map ProcessesByName; +typedef std::map EntitiesForProc; struct ReactionCond { Entities rctt;