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

Reaction system initialisation based on options.

Browse Source
This commit is contained in:
Artur Meski
2018-02-25 19:47:00 +00:00
parent abdb53ffd5
commit f121ce12fd
15 changed files with 251 additions and 131 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
formrsctl.cc
View File

@@ -189,8 +189,8 @@ bool FormRSCTL::hasOper(Oper op) const
else
{
bool result = false;
if (arg[0] != NULL) result = arg[0]->hasOper(op);
if (!result && arg[1] != NULL) result = arg[1]->hasOper(op);
if (arg[0] != nullptr) result = arg[0]->hasOper(op);
if (!result && arg[1] != nullptr) result = arg[1]->hasOper(op);
return result;
}
}
@@ -249,7 +249,7 @@ bool FormRSCTL::isERSCTL(void) const
std::string FormRSCTL::getActionsStr(void) const
{
if (actions != NULL)
if (actions != nullptr)
{
std::string r = "[ ";
bool firstact = true;
@@ -271,7 +271,7 @@ std::string FormRSCTL::getActionsStr(void) const
r += " ]";
return r;
}
else if (boolCtx != NULL)
else if (boolCtx != nullptr)
{
return "< " + boolCtx->toStr() + " >";
}
@@ -285,11 +285,11 @@ void FormRSCTL::encodeActions(const SymRS *srs)
{
if (RSCTL_COND_ACT(oper))
{
if (actions_bdd != NULL) forgetActionsBDD();
if (actions_bdd != nullptr) forgetActionsBDD();
actions_bdd = new BDD(srs->getBDDfalse());
assert(actions != NULL || boolCtx != NULL);
assert(!(actions != NULL && boolCtx != NULL));
if (actions != NULL)
assert(actions != nullptr || boolCtx != nullptr);
assert(!(actions != nullptr && boolCtx != nullptr));
if (actions != nullptr)
{
for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
{
@@ -302,7 +302,7 @@ void FormRSCTL::encodeActions(const SymRS *srs)
*actions_bdd += single_action;
}
}
else if (boolCtx != NULL)
else if (boolCtx != nullptr)
{
*actions_bdd = boolCtx->getBDD(srs);
}

102
formrsctl.hh
View File

@@ -82,8 +82,8 @@ public:
{
oper = BCTX_PV;
name = varName;
arg[0] = NULL;
arg[1] = NULL;
arg[0] = nullptr;
arg[1] = nullptr;
}
/**
@@ -94,8 +94,8 @@ public:
BoolContexts(bool val) {
oper = BCTX_TF;
tf = val;
arg[0] = NULL;
arg[1] = NULL;
arg[0] = nullptr;
arg[1] = nullptr;
}
/**
@@ -105,7 +105,7 @@ public:
assert(op == BCTX_NOT);
oper = op;
arg[0] = form1;
arg[1] = NULL;
arg[1] = nullptr;
}
/**
@@ -132,12 +132,12 @@ public:
return oper;
}
BoolContexts *getLeftSF(void) const {
assert(arg[0] != NULL);
assert(arg[0] != nullptr);
return arg[0];
}
BoolContexts *getRightSF(void) const {
assert(BCTX_COND_2ARG(oper));
assert(arg[1] != NULL);
assert(arg[1] != nullptr);
return arg[1];
}
};
@@ -162,12 +162,12 @@ public:
FormRSCTL(std::string varName) {
oper = RSCTL_PV;
name = varName;
arg[0] = NULL;
arg[1] = NULL;
bdd = NULL;
actions = NULL;
actions_bdd = NULL;
boolCtx = NULL;
arg[0] = nullptr;
arg[1] = nullptr;
bdd = nullptr;
actions = nullptr;
actions_bdd = nullptr;
boolCtx = nullptr;
}
/**
@@ -178,12 +178,12 @@ public:
FormRSCTL(bool val) {
oper = RSCTL_TF;
tf = val;
arg[0] = NULL;
arg[1] = NULL;
bdd = NULL;
actions = NULL;
actions_bdd = NULL;
boolCtx = NULL;
arg[0] = nullptr;
arg[1] = nullptr;
bdd = nullptr;
actions = nullptr;
actions_bdd = nullptr;
boolCtx = nullptr;
}
/**
@@ -195,41 +195,41 @@ public:
oper = op;
arg[0] = form1;
arg[1] = form2;
bdd = NULL;
actions = NULL;
actions_bdd = NULL;
boolCtx = NULL;
bdd = nullptr;
actions = nullptr;
actions_bdd = nullptr;
boolCtx = nullptr;
}
/**
* @brief Constructor for two-argument formula with action restrictions.
*/
FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) {
assert(acts != NULL);
assert(acts != nullptr);
assert(RSCTL_COND_2ARG(op));
assert(RSCTL_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = form2;
bdd = NULL;
bdd = nullptr;
actions = acts;
actions_bdd = NULL;
boolCtx = NULL;
actions_bdd = nullptr;
boolCtx = nullptr;
}
/**
* @brief Constructor for two-argument formula with Boolean context restrictions.
*/
FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2) {
assert(bctx != NULL);
assert(bctx != nullptr);
assert(RSCTL_COND_2ARG(op));
assert(RSCTL_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = form2;
bdd = NULL;
actions = NULL;
actions_bdd = NULL;
bdd = nullptr;
actions = nullptr;
actions_bdd = nullptr;
boolCtx = bctx;
}
@@ -241,42 +241,42 @@ public:
assert(!RSCTL_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = NULL;
bdd = NULL;
actions = NULL;
actions_bdd = NULL;
boolCtx = NULL;
arg[1] = nullptr;
bdd = nullptr;
actions = nullptr;
actions_bdd = nullptr;
boolCtx = nullptr;
}
/**
* @brief Constructor for one-argument formula with action restrictions.
*/
FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) {
assert(acts != NULL);
assert(acts != nullptr);
assert(RSCTL_COND_1ARG(op));
assert(RSCTL_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = NULL;
bdd = NULL;
arg[1] = nullptr;
bdd = nullptr;
actions = acts;
actions_bdd = NULL;
boolCtx = NULL;
actions_bdd = nullptr;
boolCtx = nullptr;
}
/**
* @brief Constructor for one-argument formula with Boolean context restrictions.
*/
FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1) {
assert(bctx != NULL);
assert(bctx != nullptr);
assert(RSCTL_COND_1ARG(op));
assert(RSCTL_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = NULL;
bdd = NULL;
actions = NULL;
actions_bdd = NULL;
arg[1] = nullptr;
bdd = nullptr;
actions = nullptr;
actions_bdd = nullptr;
boolCtx = bctx;
}
@@ -295,12 +295,12 @@ public:
bool hasOper(Oper op) const;
const BDD *getBDD(void) const {
assert(oper == RSCTL_PV);
assert(bdd != NULL);
assert(bdd != nullptr);
return bdd;
}
const BDD *getActionsBDD(void) const {
assert(RSCTL_COND_ACT(oper));
assert(actions_bdd != NULL);
assert(actions_bdd != nullptr);
return actions_bdd;
}
Oper getOper(void) const {
@@ -308,12 +308,12 @@ public:
return oper;
}
FormRSCTL *getLeftSF(void) const {
assert(arg[0] != NULL);
assert(arg[0] != nullptr);
return arg[0];
}
FormRSCTL *getRightSF(void) const {
assert(RSCTL_COND_2ARG(oper));
assert(arg[1] != NULL);
assert(arg[1] != nullptr);
return arg[1];
}
std::string getActionsStr(void) const;
@@ -324,7 +324,7 @@ public:
void encodeEntities(const SymRS *srs);
void encodeActions(const SymRS *srs);
void forgetActionsBDD(void) {
if (actions_bdd != NULL) delete actions_bdd;
if (actions_bdd != nullptr) delete actions_bdd;
}
bool isERSCTL(void) const;
};

5
macro.hh
View File

@@ -1,6 +1,8 @@
#ifndef __MY_MACROS__
#define __MY_MACROS__
#include <cassert>
#define LINENUM std::cout << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << std::endl;
/* Fatal error */
#define FERROR(s) \
@@ -14,16 +16,19 @@
}
#define VERB(s) \
assert(opts != nullptr); \
if (opts->verbose > 0) { \
std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \
}
#define VERB_L2(s) \
assert(opts != nullptr); \
if (opts->verbose > 1) { \
std::cerr << "ii VERBOSE(2): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \
}
#define VERB_L3(s) \
assert(opts != nullptr); \
if (opts->verbose > 2) { \
std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \
}

40
main.cc
View File

@@ -10,12 +10,10 @@
int main(int argc, char **argv)
{
RctSys rs;
rsin_driver driver(&rs);
rsin_driver driver;
Options *opts = new Options;
driver.setOptions(opts);
bool show_reactions = false;
bool rstl_model_checking = false;
@@ -97,8 +95,6 @@ int main(int argc, char **argv)
}
}
rs.setOptions(opts);
std::string inputfile;
if (optind < argc)
{
@@ -113,9 +109,9 @@ int main(int argc, char **argv)
if (usage_error)
{
cout << endl
<< " **********************************" << endl
<< " **Reaction Systems Model Checker**" << endl
<< " **********************************" << endl
<< " ------------------------------------" << endl
<< " -- Reaction Systems Model Checker --" << endl
<< " ------------------------------------" << endl
<< endl
<< " Version: " << VERSION << endl
<< " Contact: " << AUTHOR << endl
@@ -128,17 +124,19 @@ int main(int argc, char **argv)
<< endl
#endif
<< " Usage: " << argv[0] << " [options] <inputfile>" << endl << endl
<< " -b -- disable bounded model checking (BMC) heuristic" << endl
<< " TASKS:" << endl
<< " -c -- perform RSCTL model checking" << endl
//<< " -f K -- generate SMT input for the depth K" << endl
<< " -p -- show progress (where possible)" << 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
@@ -149,7 +147,7 @@ int main(int argc, char **argv)
if (!(reach_states || reach_states_succ || rstl_model_checking || show_reactions || print_parsed_sys))
{
FERROR("No task specified: -c, -f, -P, -r, or -s needs to be used");
FERROR("No task specified: -c, -P, -r, or -s needs to be used");
}
if (opts->verbose > 0)
@@ -164,6 +162,17 @@ int main(int argc, char **argv)
FERROR("Parse error");
}
//
// Here we retrieve the reaction system from the parser
//
// We decide which RS will be used at the parser level.
// This decision depends on whether we use concentrations,
// context automaton, etc.
//
auto rs = *driver.getReactionSystem();
rs.setOptions(opts); // these need to be passed to the driver
if (show_reactions)
rs.showReactions();
@@ -184,11 +193,16 @@ int main(int argc, char **argv)
if (rstl_model_checking)
{
if (bmc)
{
cout << "Using BDD-based Bounded Model Checking" << endl;
mc.checkRSCTL(driver.getFormRSCTL());
}
else
{
mc.checkRSCTLfull(driver.getFormRSCTL());
}
}
}
if (opts->measure)
{
@@ -197,7 +211,7 @@ int main(int argc, char **argv)
<< "Verification time: " << opts->ver_time << " sec" << endl
<< "Encoding memory: " << opts->enc_mem << " MB" << endl
<< "Memory (total): " << opts->ver_mem << " MB" << endl
<< "TOTAL time: " << opts->enc_time+opts->ver_time << " sec" << endl;
<< "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl;
if (benchmarking)
{
cout << std::setprecision(4)

12
mc.cc
View File

@@ -151,7 +151,7 @@ bool ModelChecker::checkReach(const RctSys::Entities testState)
BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
{
assert(reach != NULL);
assert(reach != nullptr);
Oper oper = form->getOper();
if (oper == RSCTL_PV)
{
@@ -364,7 +364,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
if (opts->measure)
opts->ver_time = cpuTime();
assert(form != NULL);
assert(form != nullptr);
bool result = false;
@@ -378,7 +378,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
form->encodeActions(srs);
VERB("Contexts encoded");
assert(reach == NULL);
assert(reach == nullptr);
reach = new BDD(*initStates);
BDD reach_p = cuddMgr->bddZero();
@@ -437,7 +437,7 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
if (opts->measure)
opts->ver_time = cpuTime();
assert(form != NULL);
assert(form != nullptr);
if (!form->isERSCTL())
{
@@ -456,7 +456,7 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
form->encodeActions(srs);
VERB("Contexts encoded");
assert(reach == NULL);
assert(reach == nullptr);
reach = new BDD(*initStates);
BDD reach_p = cuddMgr->bddZero();
@@ -499,6 +499,6 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
void ModelChecker::cleanup(void)
{
delete reach;
reach = NULL;
reach = nullptr;
}

4
mc.hh
View File

@@ -59,10 +59,10 @@ public:
pv_succ_E = srs->getEncPVsucc_E();
pv_act_E = srs->getEncPVact_E();
trp = srs->getEncPartTrans();
if (trp == NULL) trp_size = 0;
if (trp == nullptr) trp_size = 0;
else trp_size = trp->size();
trm = srs->getEncMonoTrans();
reach = NULL;
reach = nullptr;
}
void printReach(void);

2
memtime.hh
View File

@@ -40,7 +40,7 @@ static inline int memReadStat(void)
pid_t pid = getpid();
sprintf(name, "/proc/%d/statm", pid);
FILE* in = fopen(name, "rb");
if (in == NULL)
if (in == nullptr)
{
return 0;
}

22
rs.cc
View File

@@ -166,7 +166,6 @@ void RctSys::printSystem(void)
showInitialStates();
showActionEntities();
showReactions();
}
bool CtxAut::hasState(std::string name)
@@ -177,6 +176,15 @@ bool CtxAut::hasState(std::string name)
return true;
}
CtxAut::State CtxAut::getStateID(std::string name)
{
if (!hasState(name))
{
FERROR("No such state: " << name);
}
return states_names[name];
}
void CtxAut::addState(std::string name)
{
if (!hasState(name))
@@ -190,12 +198,20 @@ void CtxAut::addState(std::string name)
}
}
void CtxAut::pushContextEntity(std::string entityName)
void CtxAut::pushContextEntity(RctSys::Entity entity_id)
{
tmpEntities.insert(entity_id);
}
void CtxAut::addTransition(std::string srcStateName, std::string dstStateName)
{
VERB_L3("Saving transition");
Transition new_transition;
new_transition.src_state = getStateID(srcStateName);
new_transition.ctx = tmpEntities;
tmpEntities.clear();
new_transition.dst_state = getStateID(dstStateName);
}

23
rs.hh
View File

@@ -95,12 +95,6 @@ class RctSys
void printSystem(void);
};
class RctSysWithCtxAut : private RctSys
{
friend class CtxAut;
};
// Context Automaton
class CtxAut
{
@@ -113,14 +107,13 @@ class CtxAut
RctSys::Entities ctx;
State dst_state;
};
bool hasState(std::string name);
void addState(std::string stateName);
State getStateID(std::string name);
void addTransition(std::string srcStateName, std::string dstStateName);
void pushContextEntity(std::string entityName);
void setOptions(Options *opts)
{
this->opts = opts;
}
void pushContextEntity(RctSys::Entity entity_id);
void setOptions(Options *opts) { this->opts = opts; }
private:
Options *opts;
@@ -129,5 +122,11 @@ class CtxAut
RctSys::Entities tmpEntities;
};
#endif
class RctSysWithCtxAut : public RctSys
{
// friend class CtxAut;
CtxAut ctx_aut;
};
#endif

58
rsin_driver.cc
View File

@@ -1,15 +1,31 @@
#include "rsin_driver.hh"
#include "rsin_parser.hh"
rsin_driver::rsin_driver(void)
: trace_scanning(false), trace_parsing(false)
{
initialise();
}
rsin_driver::rsin_driver(RctSys *rs)
: trace_scanning(false), trace_parsing(false)
{
this->rsctlform = NULL;
initialise();
this->rs = rs;
}
void rsin_driver::initialise(void)
{
this->rs = nullptr;
this->rsctlform = nullptr;
opts = nullptr;
use_ctx_aut = false;
use_concentrations = false;
}
rsin_driver::~rsin_driver ()
{
// placeholder
}
int rsin_driver::parse(const std::string &f)
@@ -33,10 +49,9 @@ void rsin_driver::error(const std::string &m)
std::cerr << m << std::endl;
}
FormRSCTL *rsin_driver::getFormRSCTL(void)
{
if (rsctlform == NULL)
if (rsctlform == nullptr)
{
FERROR("RSCTL formula was not supplied!");
}
@@ -44,3 +59,40 @@ FormRSCTL *rsin_driver::getFormRSCTL(void)
return rsctlform;
}
//
// Checks if we are not too late to be setting any options
//
void rsin_driver::ensureOptionsAllowed(void)
{
if (rs != nullptr)
{
FERROR("Options cannot be set/modified after the reaction system is initialised")
}
}
void rsin_driver::ensureReactionSystemReady(void)
{
if (rs == nullptr)
setupReactionSystem();
}
void rsin_driver::setupReactionSystem(void)
{
assert(rs == nullptr);
if (use_ctx_aut)
{
rs = new RctSysWithCtxAut;
}
else
{
rs = new RctSys;
}
rs->setOptions(opts);
}
RctSys *rsin_driver::getReactionSystem(void)
{
ensureReactionSystemReady();
assert(rs != nullptr);
return rs;
}

25
rsin_driver.hh
View File

@@ -5,6 +5,7 @@
#include "rsin_parser.hh"
#include "rs.hh"
#include "formrsctl.hh"
#include "options.hh"
// Tell Flex the lexer's prototype ...
#define YY_DECL \
@@ -19,12 +20,20 @@ YY_DECL;
class rsin_driver
{
public:
rsin_driver(void);
rsin_driver(RctSys *rs);
virtual ~rsin_driver();
//std::map<std::string, int> variables;
RctSys *rs;
FormRSCTL *rsctlform;
Options *opts;
//
// options in configuration file
//
bool use_ctx_aut;
bool use_concentrations;
// Handling the scanner
void scan_begin();
@@ -35,14 +44,26 @@ public:
std::string file;
bool trace_parsing;
void addFormRSCTL(FormRSCTL *f) { rsctlform = f; }
void setOptions(Options *opts) { this->opts = opts; };
void addFormRSCTL(FormRSCTL *f) { rsctlform = f; };
FormRSCTL *getFormRSCTL(void);
void ensureOptionsAllowed(void);
void useContextAutomaton(void) { ensureOptionsAllowed(); use_ctx_aut = true; };
void useConcentrations(void) { ensureOptionsAllowed(); use_concentrations = true; };
void ensureReactionSystemReady(void);
void setupReactionSystem(void);
RctSys *getReactionSystem(void);
// Error handling.
void error(const yy::location &l, const std::string &m);
void error(const std::string &m);
private:
void initialise(void);
};
#endif

3
rsin_parser.ll
View File

@@ -38,6 +38,9 @@ blank [ \t]
typedef yy::rsin_parser::token token;
%}
"options" return token::OPTIONS;
"use-context-automaton" return token::USE_CTX_AUT;
"use-concentrations" return token::USE_CONCENTRATIONS;
"reactions" return token::REACTIONS;
"initial-contexts" return token::INITIALCONTEXTS;
"context-entities" return token::CONTEXTENTITIES;

26
rsin_parser.yy
View File

@@ -44,6 +44,7 @@ class rsin_driver;
#include "rsin_driver.hh"
}
%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS
%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM
%token CONTEXTAUTOMATON STATES TRANSITIONS
%token LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR
@@ -75,6 +76,7 @@ class rsin_driver;
%start system;
system:
| OPTIONS LCB options RCB system
| REACTIONS LCB reactions RCB system
| INITIALCONTEXTS LCB initstates RCB system
| CONTEXTENTITIES LCB actionentities RCB system
@@ -84,6 +86,14 @@ system:
}
;
options:
| options option SEMICOL
;
option:
| USE_CTX_AUT { }
;
/*
* -------------------------
* REACTIONS
@@ -95,7 +105,7 @@ reactions:
reaction:
| LCB reactionConditions RARR LCB reactionProducts RCB RCB {
driver.rs->commitReaction();
driver.getReactionSystem()->commitReaction();
}
;
@@ -109,7 +119,7 @@ reactants:
;
reactant: IDENTIFIER {
driver.rs->pushReactant(*$1);
driver.getReactionSystem()->pushReactant(*$1);
free($1);
}
;
@@ -121,7 +131,7 @@ inhibitors:
inhibitor:
| IDENTIFIER {
driver.rs->pushInhibitor(*$1);
driver.getReactionSystem()->pushInhibitor(*$1);
free($1);
}
;
@@ -132,7 +142,7 @@ reactionProducts:
;
reactionProduct: IDENTIFIER {
driver.rs->pushProduct(*$1);
driver.getReactionSystem()->pushProduct(*$1);
free($1);
}
;
@@ -141,10 +151,10 @@ reactionProduct: IDENTIFIER {
initstates:
LCB initstate RCB {
driver.rs->commitInitState();
driver.getReactionSystem()->commitInitState();
}
| initstates COMMA LCB initstate RCB {
driver.rs->commitInitState();
driver.getReactionSystem()->commitInitState();
}
;
@@ -154,7 +164,7 @@ initstate:
;
entity: IDENTIFIER {
driver.rs->pushStateEntity(*$1);
driver.getReactionSystem()->pushStateEntity(*$1);
free($1);
}
;
@@ -167,7 +177,7 @@ actionentities:
;
actentity: IDENTIFIER {
driver.rs->addActionEntity(*$1);
driver.getReactionSystem()->addActionEntity(*$1);
free($1);
}
;

2
symrs.cc
View File

@@ -318,7 +318,7 @@ void SymRS::encodeInitStates(void)
#ifndef NDEBUG
if (opts->part_tr_rel)
assert(partTrans != NULL);
assert(partTrans != nullptr);
#endif
initStates = new BDD(BDD_FALSE);

4
symrs.hh
View File

@@ -122,8 +122,8 @@ public:
totalReactions = rs->getReactionsSize();
totalActions = rs->getActionsSize();
partTrans = NULL;
monoTrans = NULL;
partTrans = nullptr;
monoTrans = nullptr;
encode();
}