artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Context automaton with augmented context: parsing

Browse Source
This commit is contained in:
Artur Meski
2018-03-28 20:46:19 +01:00
parent 753b217721
commit c90a87875a
6 changed files with 71 additions and 49 deletions
Download Patch File Download Diff File Expand all files Collapse all files

80
main.cc
View File

@@ -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] <inputfile>" << 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] <inputfile>" << 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 **/

6
main.hh
View File

@@ -22,9 +22,11 @@
#include "options.hh"
#include "memtime.hh"
#define VERSION "1.0alpha"
#define AUTHOR "Artur Męski <meski@ipipan.waw.pl>"
#define VERSION "2.0 ALPHA"
#define AUTHOR "Artur Meski <meski@ipipan.waw.pl>"
using std::cout;
using std::endl;
void print_help(std::string path_str);
#endif

8
rs.cc
View File

@@ -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;
}

1
rsin_parser.ll
View File

@@ -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;

14
rsin_parser.yy
View File

@@ -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,13 +227,19 @@ 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
| contextset COMMA ctxentity

11
types.hh
View File

@@ -21,8 +21,13 @@ struct Reaction {
Entities inhib;
Entities prod;
};
typedef unsigned int Process;
typedef std::vector<std::string> ProcessesById;
typedef std::map<std::string, Process> ProcessesByName;
typedef std::vector<Reaction> Reactions;
typedef std::vector<Reactions> ReactionsForProc;
typedef std::map<Process, Reactions> ReactionsForProc;
typedef std::vector<std::string> EntitiesById;
typedef std::map<std::string, Entity> EntitiesByName;
@@ -32,9 +37,7 @@ typedef unsigned int State;
typedef std::vector<std::string> StatesById;
typedef std::map<std::string, State> StatesByName;
typedef unsigned int Process;
typedef std::vector<std::string> ProcessesById;
typedef std::map<std::string, Process> ProcessesByName;
typedef std::map<Process, Entities> EntitiesForProc;
struct ReactionCond {
Entities rctt;