From a36ed9651f7e49853aa98ed024ba34e34b8270d6 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sat, 22 Sep 2018 20:05:35 +0100 Subject: [PATCH] Includes, clean-up We are trying to avoid including stuff whenever possible. Forward declarations are prefered in most cases, just in case... --- bdd_macro.hh | 2 + ctx_aut.cc | 5 ++- ctx_aut.hh | 10 +++-- formrsctlk.cc | 28 ++++++------- formrsctlk.hh | 107 ++++--------------------------------------------- macro.hh | 2 + memtime.hh | 4 +- rs.cc | 9 ++++- rs.hh | 2 + rsin_driver.cc | 2 + rsin_driver.hh | 5 ++- rsin_parser.yy | 49 ++++++++++++---------- symrs.cc | 14 ++++++- symrs.hh | 15 +++---- types.hh | 2 + 15 files changed, 103 insertions(+), 153 deletions(-) diff --git a/bdd_macro.hh b/bdd_macro.hh index dee04e3..c39bf1e 100644 --- a/bdd_macro.hh +++ b/bdd_macro.hh @@ -1,6 +1,8 @@ #ifndef __BDD_MACRO_HH__ #define __BDD_MACRO_HH__ +#include "cudd.hh" + #define BDD_IFF(p,q) (!(p+q)+(p*q)) #define BDD_TRUE (cuddMgr->bddOne()) #define BDD_FALSE (cuddMgr->bddZero()) diff --git a/ctx_aut.cc b/ctx_aut.cc index 3e2abf9..def9d3c 100644 --- a/ctx_aut.cc +++ b/ctx_aut.cc @@ -1,5 +1,8 @@ #include "ctx_aut.hh" +#include "rs.hh" +#include "macro.hh" +#include "stateconstr.hh" CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys) { @@ -94,7 +97,7 @@ void CtxAut::saveCurrentContextSet(Process proc_id) tmpEntities.clear(); } -void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) +void CtxAut::addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr) { VERB_L3("Saving transition"); diff --git a/ctx_aut.hh b/ctx_aut.hh index e756dad..66bb489 100644 --- a/ctx_aut.hh +++ b/ctx_aut.hh @@ -12,15 +12,17 @@ #include #include #include -#include "rs.hh" +// #include "rs.hh" #include "types.hh" -#include "macro.hh" -#include "options.hh" +// #include "options.hh" +// #include "stateconstr.hh" using std::cout; using std::endl; class RctSys; +class Options; +class StateConstr; class CtxAut { @@ -36,7 +38,7 @@ class CtxAut std::string getStateName(State state_id); void printAutomaton(void); void showStates(void); - void addTransition(std::string srcStateName, std::string dstStateName); + void addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr); void showTransitions(void); void pushContextEntity(Entity entity_id); void saveCurrentContextSet(Process proc_id); diff --git a/formrsctlk.cc b/formrsctlk.cc index 044cc38..6dc82fa 100644 --- a/formrsctlk.cc +++ b/formrsctlk.cc @@ -9,12 +9,12 @@ #include "formrsctlk.hh" -std::string BoolContexts::toStr(void) const +std::string StateConstr::toStr(void) const { - if (oper == BCTX_PV) { + if (oper == STC_PV) { return proc_name + "." + entity_name; } - else if (oper == BCTX_TF) { + else if (oper == STC_TF) { if (tf) { return "true"; } @@ -22,16 +22,16 @@ std::string BoolContexts::toStr(void) const return "false"; } } - else if (oper == BCTX_AND) { + else if (oper == STC_AND) { return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")"; } - else if (oper == BCTX_OR) { + else if (oper == STC_OR) { return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")"; } - else if (oper == BCTX_XOR) { + else if (oper == STC_XOR) { return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")"; } - else if (oper == BCTX_NOT) { + else if (oper == STC_NOT) { return "~" + arg[0]->toStr(); } @@ -41,12 +41,12 @@ std::string BoolContexts::toStr(void) const } } -BDD BoolContexts::getBDD(const SymRS *srs) const +BDD StateConstr::getBDD(const SymRS *srs) const { - if (oper == BCTX_PV) { + if (oper == STC_PV) { return srs->encActStrEntity(proc_name, entity_name); } - else if (oper == BCTX_TF) { + else if (oper == STC_TF) { if (tf) { return srs->getBDDtrue(); } @@ -54,16 +54,16 @@ BDD BoolContexts::getBDD(const SymRS *srs) const return srs->getBDDfalse(); } } - else if (oper == BCTX_AND) { + else if (oper == STC_AND) { return arg[0]->getBDD(srs) * arg[1]->getBDD(srs); } - else if (oper == BCTX_OR) { + else if (oper == STC_OR) { return arg[0]->getBDD(srs) + arg[1]->getBDD(srs); } - else if (oper == BCTX_XOR) { + else if (oper == STC_XOR) { return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs); } - else if (oper == BCTX_NOT) { + else if (oper == STC_NOT) { return !arg[0]->getBDD(srs); } else { diff --git a/formrsctlk.hh b/formrsctlk.hh index b9b94c0..474ea5f 100644 --- a/formrsctlk.hh +++ b/formrsctlk.hh @@ -12,9 +12,11 @@ #include #include #include -#include "rs.hh" +// #include "rs.hh" #include "symrs.hh" #include "cudd.hh" +#include "types.hh" +#include "stateconstr.hh" #define RSCTLK_PV 0 // propositional variable #define RSCTLK_AND 1 @@ -43,15 +45,6 @@ #define RSCTLK_NK 61 // Epistemic operators #define RSCTLK_UK 71 -/* For Boolean contexts: */ -#define BCTX_PV 80 -#define BCTX_AND 81 -#define BCTX_OR 82 -#define BCTX_XOR 83 -#define BCTX_NOT 84 -#define BCTX_TF 90 - - #define RSCTLK_COND_1ARG(a) ((a) == RSCTLK_NOT || (a) == RSCTLK_EG || (a) == RSCTLK_EF || (a) == RSCTLK_EX || (a) == RSCTLK_AG || (a) == RSCTLK_AF || (a) == RSCTLK_AX || (a) == RSCTLK_EG_ACT || (a) == RSCTLK_EF_ACT || (a) == RSCTLK_EX_ACT || (a) == RSCTLK_AG_ACT || (a) == RSCTLK_AF_ACT || (a) == RSCTLK_AX_ACT || (a) == RSCTLK_UK || (a) == RSCTLK_NK) #define RSCTLK_COND_2ARG(a) ((a) == RSCTLK_AND || (a) == RSCTLK_OR || (a) == RSCTLK_XOR || (a) == RSCTLK_IMPL || (a) == RSCTLK_EU || (a) == RSCTLK_AU || (a) == RSCTLK_EU_ACT || (a) == RSCTLK_AU_ACT) #define RSCTLK_COND_ACT(a) ((a) > 30 && (a) < 45) @@ -59,101 +52,15 @@ #define RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45) || ((a) > 70 && (a) < 75)) -#define BCTX_COND_1ARG(a) ((a) == BCTX_NOT) -#define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR) -#define BCTX_IS_VALID(a) (BCTX_COND_1ARG(a) || BCTX_COND_2ARG(a) || (a) == BCTX_PV || (a) == BCTX_TF) - using std::cout; using std::endl; -typedef unsigned char Oper; - // typedef std::string Entity_f; // typedef std::set Action_f; // typedef vector ActionsVec_f; typedef std::set Agents_f; -class BoolContexts -{ - Oper oper; - BoolContexts *arg[2]; - std::string entity_name; - std::string proc_name; - bool tf; - - public: - - BoolContexts(std::string procName, std::string varName) - { - oper = BCTX_PV; - entity_name = varName; - proc_name = procName; - arg[0] = nullptr; - arg[1] = nullptr; - } - - /** - * @brief Constructor for true/false. - * - * @param val value of the logical constant - */ - BoolContexts(bool val) - { - oper = BCTX_TF; - tf = val; - arg[0] = nullptr; - arg[1] = nullptr; - } - - /** - * @brief Constructor for one-argument formula. - */ - BoolContexts(Oper op, BoolContexts *form1) - { - assert(op == BCTX_NOT); - oper = op; - arg[0] = form1; - arg[1] = nullptr; - } - - /** - * @brief Constructor for two-argument formula. - */ - BoolContexts(Oper op, BoolContexts *form1, BoolContexts *form2) - { - assert(BCTX_COND_2ARG(op)); - oper = op; - arg[0] = form1; - arg[1] = form2; - } - - ~BoolContexts() - { - delete arg[0]; - delete arg[1]; - } - - std::string toStr(void) const; - - BDD getBDD(const SymRS *srs) const; - - Oper getOper(void) const - { - assert(BCTX_IS_VALID(oper)); - return oper; - } - BoolContexts *getLeftSF(void) const - { - assert(arg[0] != nullptr); - return arg[0]; - } - BoolContexts *getRightSF(void) const - { - assert(BCTX_COND_2ARG(oper)); - assert(arg[1] != nullptr); - return arg[1]; - } -}; +class StateConstr; class FormRSCTLK { @@ -165,7 +72,7 @@ class FormRSCTLK BDD *bdd; // ActionsVec_f *actions; BDD *actions_bdd; - BoolContexts *boolCtx; + StateConstr *boolCtx; Agents_f agents; public: /** @@ -240,7 +147,7 @@ class FormRSCTLK /** * @brief Constructor for two-argument formula with Boolean context restrictions. */ - FormRSCTLK(Oper op, BoolContexts *bctx, FormRSCTLK *form1, FormRSCTLK *form2) + FormRSCTLK(Oper op, StateConstr *bctx, FormRSCTLK *form1, FormRSCTLK *form2) { assert(bctx != nullptr); assert(RSCTLK_COND_2ARG(op)); @@ -290,7 +197,7 @@ class FormRSCTLK /** * @brief Constructor for one-argument formula with Boolean context restrictions. */ - FormRSCTLK(Oper op, BoolContexts *bctx, FormRSCTLK *form1) + FormRSCTLK(Oper op, StateConstr *bctx, FormRSCTLK *form1) { assert(bctx != nullptr); assert(RSCTLK_COND_1ARG(op)); diff --git a/macro.hh b/macro.hh index 1e86fac..b4305a7 100644 --- a/macro.hh +++ b/macro.hh @@ -2,6 +2,8 @@ #define __MY_MACROS__ #include +#include + #define LINENUM std::cout << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << std::endl; /* Fatal error */ diff --git a/memtime.hh b/memtime.hh index d257276..af6a286 100644 --- a/memtime.hh +++ b/memtime.hh @@ -28,6 +28,8 @@ #include #include "macro.hh" +using namespace std; + typedef long long int64; static inline double cpuTime(void) @@ -52,7 +54,7 @@ static inline int memReadStat(void) for (int field = 0; field >= 0; --field) { if (fscanf(in, "%d", &value) == EOF) { - FERROR("EOF"); + FERROR("EOF") } } diff --git a/rs.cc b/rs.cc index 5f9bf71..67f734f 100644 --- a/rs.cc +++ b/rs.cc @@ -322,7 +322,14 @@ void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateName) { assert(ctx_aut != nullptr); - ctx_aut->addTransition(srcStateName, dstStateName); + ctx_aut->addTransition(srcStateName, dstStateName, nullptr); +} + +void RctSys::ctxAutAddTransition(std::string srcStateName, + std::string dstStateName, StateConstr *stateConstr) +{ + assert(ctx_aut != nullptr); + ctx_aut->addTransition(srcStateName, dstStateName, stateConstr); } void RctSys::ctxAutPushNamedContextEntity(std::string entityName) diff --git a/rs.hh b/rs.hh index 1ac89b2..66389f2 100644 --- a/rs.hh +++ b/rs.hh @@ -25,6 +25,7 @@ using std::cout; using std::endl; class CtxAut; +class StateConstr; class RctSys { @@ -87,6 +88,7 @@ class RctSys void ctxAutAddState(std::string stateName); void ctxAutSetInitState(std::string stateName); void ctxAutAddTransition(std::string srcStateName, std::string dstStateName); + void ctxAutAddTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr); void ctxAutPushNamedContextEntity(std::string entity_name); void ctxAutSaveCurrentContextSet(std::string processName); diff --git a/rsin_driver.cc b/rsin_driver.cc index 952fa51..66c8403 100644 --- a/rsin_driver.cc +++ b/rsin_driver.cc @@ -1,6 +1,8 @@ #include "rsin_driver.hh" #include "rsin_parser.hh" +#include "rs.hh" + rsin_driver::rsin_driver(void) : trace_scanning(false), trace_parsing(false) { diff --git a/rsin_driver.hh b/rsin_driver.hh index 49002b4..381c3c4 100644 --- a/rsin_driver.hh +++ b/rsin_driver.hh @@ -3,7 +3,7 @@ #include #include #include "rsin_parser.hh" -#include "rs.hh" +// #include "rs.hh" #include "formrsctlk.hh" #include "options.hh" @@ -16,6 +16,9 @@ // ... and declare it for the parser's sake. YY_DECL; +class RctSys; +class CtxAut; + // Conducting the whole scanning an parsing of RS class rsin_driver { diff --git a/rsin_parser.yy b/rsin_parser.yy index 81bfb68..c87bbff 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -7,6 +7,8 @@ #include #include #include "formrsctlk.hh" +#include "rs.hh" +// #include "stateconstr.hh" using std::set; using std::string; @@ -37,7 +39,7 @@ class rsin_driver; // Entity_f *ent; // Action_f *act; // ActionsVec_f *actionsVec; - BoolContexts *fboolctx; + StateConstr *fstc; }; %code { @@ -64,7 +66,7 @@ class rsin_driver; // %type f_entity // %type action // %type actions -%type bool_contexts +%type state_constr //%printer { yyoutput << *$$; } "identifier" %destructor { delete $$; } "identifier" @@ -235,6 +237,11 @@ auttrans: LCB proc_ctxsets RCB COL IDENTIFIER RARR IDENTIFIER { free($5); free($7); } + | LCB proc_ctxsets RCB COL IDENTIFIER RARR IDENTIFIER COL state_constr { + driver.getReactionSystem()->ctxAutAddTransition(*$5, *$7, $9); + free($5); + free($7); + } ; proc_ctxsets: @@ -260,25 +267,25 @@ ctxentity: IDENTIFIER { /* formulae */ -bool_contexts: IDENTIFIER DOT IDENTIFIER { - $$ = new BoolContexts(*$1, *$3); +state_constr: IDENTIFIER DOT IDENTIFIER { + $$ = new StateConstr(*$1, *$3); free($1); free($3); } - | NOT bool_contexts { - $$ = new BoolContexts(BCTX_NOT, $2); + | NOT state_constr { + $$ = new StateConstr(STC_NOT, $2); } - | LRB bool_contexts RRB { + | LRB state_constr RRB { $$ = $2; } - | bool_contexts AND bool_contexts { - $$ = new BoolContexts(BCTX_AND, $1, $3); + | state_constr AND state_constr { + $$ = new StateConstr(STC_AND, $1, $3); } - | bool_contexts OR bool_contexts { - $$ = new BoolContexts(BCTX_OR, $1, $3); + | state_constr OR state_constr { + $$ = new StateConstr(STC_OR, $1, $3); } - | bool_contexts XOR bool_contexts { - $$ = new BoolContexts(BCTX_XOR, $1, $3); + | state_constr XOR state_constr { + $$ = new StateConstr(STC_XOR, $1, $3); } ; @@ -404,28 +411,28 @@ rsctlk_form: // } /* contexts as boolean formulae */ - | E LAB bool_contexts RAB X rsctlk_form { + | E LAB state_constr RAB X rsctlk_form { $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6); } - | E LAB bool_contexts RAB U LRB rsctlk_form COMMA rsctlk_form RRB { + | E LAB state_constr RAB U LRB rsctlk_form COMMA rsctlk_form RRB { $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9); } - | E LAB bool_contexts RAB F rsctlk_form { + | E LAB state_constr RAB F rsctlk_form { $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6); } - | E LAB bool_contexts RAB G rsctlk_form { + | E LAB state_constr RAB G rsctlk_form { $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6); } - | A LAB bool_contexts RAB X rsctlk_form { + | A LAB state_constr RAB X rsctlk_form { $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6); } - | A LAB bool_contexts RAB U LRB rsctlk_form COMMA rsctlk_form RRB { + | A LAB state_constr RAB U LRB rsctlk_form COMMA rsctlk_form RRB { $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9); } - | A LAB bool_contexts RAB F rsctlk_form { + | A LAB state_constr RAB F rsctlk_form { $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6); } - | A LAB bool_contexts RAB G rsctlk_form { + | A LAB state_constr RAB G rsctlk_form { $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6); } ; diff --git a/symrs.cc b/symrs.cc index 1258e90..b6cafbf 100644 --- a/symrs.cc +++ b/symrs.cc @@ -4,7 +4,8 @@ */ #include "symrs.hh" - +#include "rs.hh" +#include "bdd_macro.hh" SymRS::SymRS(RctSys *rs, Options *opts) { @@ -35,6 +36,17 @@ SymRS::SymRS(RctSys *rs, Options *opts) encode(); } +bool SymRS::usingContextAutomaton(void) +{ + return rs->ctx_aut != nullptr; +} + + +BDD SymRS::encEntity(std::string proc_name, std::string entity_name) const +{ + return encEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name)); +} + void SymRS::encode(void) { VERB("Encoding..."); diff --git a/symrs.hh b/symrs.hh index 4023eb7..aa275af 100644 --- a/symrs.hh +++ b/symrs.hh @@ -13,11 +13,12 @@ #include #include #include +#include #include "cudd.hh" #include "types.hh" #include "macro.hh" #include "bdd_macro.hh" -#include "rs.hh" +// #include "rs.hh" #include "options.hh" #include "memtime.hh" @@ -27,6 +28,8 @@ using std::endl; using std::vector; using std::map; +class RctSys; + class SymRS { friend class ModelChecker; @@ -87,10 +90,7 @@ class SymRS { return totalRctSysStateVars; } - BDD encEntity(std::string proc_name, std::string entity_name) const - { - return encEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name)); - } + BDD encEntity(std::string proc_name, std::string entity_name) const; BDD encActStrEntity(std::string proc_name, std::string entity_name) const; BDD getBDDtrue(void) const { @@ -106,10 +106,7 @@ class SymRS * * @return True if CA is used */ - bool usingContextAutomaton(void) - { - return rs->ctx_aut != nullptr; - } + bool usingContextAutomaton(void); /** * @brief Encodes a context automaton's state diff --git a/types.hh b/types.hh index 8cb55c8..f0a5054 100644 --- a/types.hh +++ b/types.hh @@ -15,6 +15,8 @@ #include #include "cudd.hh" +typedef unsigned char Oper; + typedef std::vector BDDvec; typedef unsigned int Entity;