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

Includes, clean-up

Browse Source 
We are trying to avoid including stuff whenever possible.
Forward declarations are prefered in most cases, just in case...
This commit is contained in:
Artur Meski
2018-09-22 20:05:35 +01:00
parent d4ac425963
commit a36ed9651f
15 changed files with 103 additions and 153 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
bdd_macro.hh
View File

@@ -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())

5
ctx_aut.cc
View File

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

10
ctx_aut.hh
View File

@@ -12,15 +12,17 @@
#include <vector>
#include <string>
#include <cstdlib>
#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);

28
formrsctlk.cc
View File

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

107
formrsctlk.hh
View File

@@ -12,9 +12,11 @@
#include <iostream>
#include <string>
#include <cassert>
#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<Entity_f> Action_f;
// typedef vector<Action_f> ActionsVec_f;
typedef std::set<std::string> 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));

2
macro.hh
View File

@@ -2,6 +2,8 @@
#define __MY_MACROS__
#include <cassert>
#include <iostream>
#define LINENUM std::cout << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << std::endl;
/* Fatal error */

4
memtime.hh
View File

@@ -28,6 +28,8 @@
#include <unistd.h>
#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")
}
}

9
rs.cc
View File

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

2
rs.hh
View File

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

2
rsin_driver.cc
View File

@@ -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)
{

5
rsin_driver.hh
View File

@@ -3,7 +3,7 @@
#include <string>
#include <map>
#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
{

49
rsin_parser.yy
View File

@@ -7,6 +7,8 @@
#include <string>
#include <set>
#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 <ent> f_entity
// %type <act> action
// %type <actionsVec> actions
%type <fboolctx> bool_contexts
%type <fstc> 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);
}
;

14
symrs.cc
View File

@@ -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...");

15
symrs.hh
View File

@@ -13,11 +13,12 @@
#include <algorithm>
#include <map>
#include <cassert>
#include <iostream>
#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

2
types.hh
View File

@@ -15,6 +15,8 @@
#include <string>
#include "cudd.hh"
typedef unsigned char Oper;
typedef std::vector<BDD> BDDvec;
typedef unsigned int Entity;