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

Formatting

Browse Source
This commit is contained in:
Artur Meski
2018-12-29 22:07:26 +00:00
parent 53504d6514
commit e4f5b7271e
11 changed files with 93 additions and 72 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
ctx_aut.cc
View File

@@ -121,9 +121,11 @@ void CtxAut::showTransitions(void)
cout << " * [" << getStateName(t.src_state) << " -> " << getStateName( cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(
t.dst_state) t.dst_state)
<< "]: { " << parent_rctsys->procEntitiesToStr(t.ctx) << "}"; << "]: { " << parent_rctsys->procEntitiesToStr(t.ctx) << "}";
if (t.state_constr != nullptr) { if (t.state_constr != nullptr) {
cout << " " << t.state_constr->toStr(); cout << " " << t.state_constr->toStr();
} }
cout << endl; cout << endl;
} }
} }
@@ -134,16 +136,17 @@ void CtxAut::makeProgressive(void)
assert(!made_progressive); assert(!made_progressive);
std::string special_loc = "T"; std::string special_loc = "T";
while (hasState(special_loc))
{ while (hasState(special_loc)) {
special_loc += "T"; special_loc += "T";
} }
addState(special_loc); addState(special_loc);
State special_loc_id = getLastStateID(); State special_loc_id = getLastStateID();
std::map<State, StateConstr *> constrs; std::map<State, StateConstr *> constrs;
for (State s = 0; s < states_ids.size(); ++s)
{ for (State s = 0; s < states_ids.size(); ++s) {
if (s == special_loc_id) { if (s == special_loc_id) {
continue; continue;
} }
@@ -157,22 +160,23 @@ void CtxAut::makeProgressive(void)
for (const auto &t : transitions) { for (const auto &t : transitions) {
State curr_st = t.src_state; State curr_st = t.src_state;
if (t.state_constr != nullptr)
{ if (t.state_constr != nullptr) {
constrs[curr_st] = new StateConstr( constrs[curr_st] = new StateConstr(
STC_OR, constrs[curr_st], t.state_constr); STC_OR, constrs[curr_st], t.state_constr);
} }
} }
for (const auto &s : states_ids) for (const auto &s : states_ids) {
{ StateConstr *state_constr = nullptr;
StateConstr *state_constr = nullptr;
if (!constrs[getStateID(s)]->isTrue()) { if (!constrs[getStateID(s)]->isTrue()) {
state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]); state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]);
addTransition(s, special_loc, state_constr); addTransition(s, special_loc, state_constr);
} }
} }
addTransition(special_loc, special_loc, nullptr); addTransition(special_loc, special_loc, nullptr);
made_progressive = true; made_progressive = true;

5
ctx_aut.hh
View File

@@ -35,7 +35,10 @@ class CtxAut
void setInitState(std::string stateName); void setInitState(std::string stateName);
State getInitState(void); State getInitState(void);
State getStateID(std::string name); State getStateID(std::string name);
State getLastStateID(void) { return states_ids.size(); } State getLastStateID(void)
{
return states_ids.size();
}
std::string getStateName(State state_id); std::string getStateName(State state_id);
void printAutomaton(void); void printAutomaton(void);
void showStates(void); void showStates(void);

17
formrsctlk.cc
View File

@@ -263,23 +263,28 @@ std::string FormRSCTLK::getAgentsStr(void) const
{ {
std::string r = ""; std::string r = "";
bool first = true; bool first = true;
for (const auto &a : agents)
{ for (const auto &a : agents) {
if (first) if (first) {
first = false; first = false;
else }
else {
r += " "; r += " ";
}
r += a; r += a;
} }
return r; return r;
} }
ProcSet FormRSCTLK::getAgentsAsProcSet(RctSys *rs) const ProcSet FormRSCTLK::getAgentsAsProcSet(RctSys *rs) const
{ {
ProcSet processes; ProcSet processes;
for (auto &a : agents)
{ for (auto &a : agents) {
processes.insert(rs->getProcessID(a)); processes.insert(rs->getProcessID(a));
} }
return processes; return processes;
} }

14
in/scripts/gen_tgc_sc.py
View File

@@ -3,7 +3,7 @@
from sys import argv,exit from sys import argv,exit
OPTIONS_STR = """ OPTIONS_STR = """
options { use-context-automaton; make-progressive; } options { use-context-automaton; make-progressive; };
""" """
PROC_STR = """ PROC_STR = """
@@ -18,16 +18,16 @@ PROC_STR = """
CA_STR = """ CA_STR = """
context-automaton {{ context-automaton {{
states {{ init, green, red }} states {{ init, green, red }};
init-state {{ init }} init-state {{ init }};
transitions {{ transitions {{
{:s} {:s}
}} }};
}} }};
""" """
PROPERTY_STR = """ PROPERTY_STR = """
rsctlk-property {{ {:s} : {:s} }} rsctlk-property {{ {:s} : {:s} }};
""" """
@@ -47,7 +47,7 @@ out += OPTIONS_STR
out += "reactions {\n" out += "reactions {\n"
for i in range(n): for i in range(n):
out += PROC_STR.format(i) out += PROC_STR.format(i)
out += "}\n" out += "};\n"
transitions = "" transitions = ""

18
mc.cc
View File

@@ -127,6 +127,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
q *= x * trans; q *= x * trans;
reorder(); reorder();
} }
q *= *contexts; q *= *contexts;
} }
else { else {
@@ -367,13 +368,11 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
auto proc_set = form->getAgentsAsProcSet(srs->rs); auto proc_set = form->getAgentsAsProcSet(srs->rs);
return *reach - (statesNE(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach); return *reach - (statesNE(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
} }
else if (oper == RSCTLK_NC) else if (oper == RSCTLK_NC) {
{
auto proc_set = form->getAgentsAsProcSet(srs->rs); auto proc_set = form->getAgentsAsProcSet(srs->rs);
return statesNC(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_set) * *reach; return statesNC(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_set) * *reach;
} }
else if (oper == RSCTLK_UC) else if (oper == RSCTLK_UC) {
{
auto proc_set = form->getAgentsAsProcSet(srs->rs); auto proc_set = form->getAgentsAsProcSet(srs->rs);
return *reach - (statesNC(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach); return *reach - (statesNC(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
} }
@@ -475,8 +474,7 @@ BDD ModelChecker::statesNE(const BDD &states, ProcSet processes)
{ {
BDD x = BDD_FALSE; BDD x = BDD_FALSE;
for (auto const &proc_id : processes) for (auto const &proc_id : processes) {
{
x += states.ExistAbstract(getIthOnly(proc_id)); x += states.ExistAbstract(getIthOnly(proc_id));
} }
@@ -488,14 +486,14 @@ BDD ModelChecker::statesNC(const BDD &states, ProcSet processes)
BDD x = BDD_FALSE; BDD x = BDD_FALSE;
BDD x_p = *reach; BDD x_p = *reach;
while (x != x_p) while (x != x_p) {
{
x_p = x; x_p = x;
BDD t = BDD_FALSE; BDD t = BDD_FALSE;
for (auto const &proc_id : processes)
{ for (auto const &proc_id : processes) {
t += x.ExistAbstract(getIthOnly(proc_id)); t += x.ExistAbstract(getIthOnly(proc_id));
} }
x = t; x = t;
} }

12
memtime.hh
View File

@@ -69,16 +69,18 @@ static inline int64 memUsedInt64()
#if defined(__APPLE__) #if defined(__APPLE__)
static inline double memUsed() { static inline double memUsed()
malloc_statistics_t t; {
malloc_zone_statistics(NULL, &t); malloc_statistics_t t;
return (double)t.max_size_in_use / (1024*1024); } malloc_zone_statistics(NULL, &t);
return (double)t.max_size_in_use / (1024 * 1024);
}
#else #else
static inline double memUsed() static inline double memUsed()
{ {
return memUsedInt64() / (1024*1024); return memUsedInt64() / (1024 * 1024);
} }
#endif #endif

32
reactics.cc
View File

@@ -124,7 +124,7 @@ int main(int argc, char **argv)
if (optind < argc) { if (optind < argc) {
inputfile = argv[optind]; inputfile = argv[optind];
} }
else if (!dump_help_message) { else if (!dump_help_message) {
cout << "Missing input file" << endl; cout << "Missing input file" << endl;
dump_help_message = true; dump_help_message = true;
} }
@@ -217,10 +217,12 @@ int main(int argc, char **argv)
int ret_val; int ret_val;
if (result) if (result) {
ret_val = 0; ret_val = 0;
else }
else {
ret_val = 1; ret_val = 1;
}
return ret_val; return ret_val;
} }
@@ -244,25 +246,25 @@ void print_help(std::string path_str)
#endif #endif
<< " Usage: " << path_str << " [options] <input file>" << endl << endl << " Usage: " << path_str << " [options] <input file>" << endl << endl
<< " TASKS:" << endl << " TASKS:" << endl
<< " -c -- perform RSCTLK model checking" << endl << " -c form -- perform RSCTLK model checking (form: formula identifier)" << endl
//<< " -f K -- generate SMT input for the depth K" << endl //<< " -f K -- generate SMT input for the depth K" << endl
<< " -P -- print parsed system" << endl << " -P -- print parsed system" << endl
<< " -r -- print reactions" << endl << " -r -- print reactions" << endl
<< " -s -- print the set of all the reachable states" << endl << " -s -- print all the reachable states" << endl
<< " -t -- print the set of all the reachable states with their successors" << " -t -- print all the reachable states with their successors"
<< endl << endl
<< endl << " OTHER:" << endl << endl << " OTHER:" << endl
<< " -b -- disable bounded model checking (BMC) heuristic" << endl << " -b -- disable bounded model checking (BMC) heuristic" << endl
<< " -x -- use partitioned transition relation (may use less memory)" << << " -x -- use partitioned transition relation" <<
endl endl
<< " -z -- use reordering of the BDD variables" << endl << " -z -- use reordering of the BDD variables" << endl
<< " -v -- verbose (can be used more than once to increase verbosity)" << << " -v -- verbose (use more than once to increase verbosity)" <<
endl endl
<< " -p -- show progress (where possible)" << endl << " -p -- show progress (where possible)" << endl
<< endl << endl
<< " Benchmarking options:" << endl << " Benchmarking options:" << endl
<< " -m -- measure and display time and memory usage" << endl << " -m -- measure and display time and memory usage" << endl
<< " -B -- display an easy to parse summary (enables -m)" << endl << " -B -- display an easy to parse summary (enables -m)" << endl
<< endl; << endl;
} }

3
rs.cc
View File

@@ -363,8 +363,9 @@ void RctSys::ctxAutSaveCurrentContextSet(std::string processName)
void RctSys::ctxAutFinalise(void) void RctSys::ctxAutFinalise(void)
{ {
if (gen_ctxaut_progressive_closure) if (gen_ctxaut_progressive_closure) {
ctx_aut->makeProgressive(); ctx_aut->makeProgressive();
}
} }
/** EOF **/ /** EOF **/

7
rsin_driver.cc
View File

@@ -110,12 +110,11 @@ void rsin_driver::useContextAutomaton(void)
void rsin_driver::makeProgressive(void) void rsin_driver::makeProgressive(void)
{ {
make_progressive = true; make_progressive = true;
if (use_ctx_aut)
{ if (use_ctx_aut) {
getReactionSystem()->ctxAutEnableProgressiveClosure(); getReactionSystem()->ctxAutEnableProgressiveClosure();
} }
else else {
{
FERROR("Context automaton not enabled"); FERROR("Context automaton not enabled");
} }
} }

18
stateconstr.cc
View File

@@ -57,10 +57,12 @@ BDD StateConstr::getBDDforContext(const SymRS *srs) const
BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
{ {
if (oper == STC_PV) { if (oper == STC_PV) {
if (encode_context) if (encode_context) {
return srs->encActStrEntity(proc_name, entity_name); return srs->encActStrEntity(proc_name, entity_name);
else }
else {
return srs->encEntity(proc_name, entity_name); return srs->encEntity(proc_name, entity_name);
}
} }
else if (oper == STC_TF) { else if (oper == STC_TF) {
if (tf) { if (tf) {
@@ -91,22 +93,26 @@ BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
bool StateConstr::isFalse(void) const bool StateConstr::isFalse(void) const
{ {
if (oper == STC_TF && tf == false) if (oper == STC_TF && tf == false) {
return true; return true;
}
if (oper == STC_NOT && arg[0]->isTrue()) if (oper == STC_NOT && arg[0]->isTrue()) {
return true; return true;
}
return false; return false;
} }
bool StateConstr::isTrue(void) const bool StateConstr::isTrue(void) const
{ {
if (oper == STC_TF && tf == true) if (oper == STC_TF && tf == true) {
return true; return true;
}
if (oper == STC_NOT && arg[0]->isFalse()) if (oper == STC_NOT && arg[0]->isFalse()) {
return true; return true;
}
return false; return false;
} }

7
symrs.cc
View File

@@ -773,7 +773,7 @@ void SymRS::encodeTransitions(void)
VERB("Using partitioned transition relation encoding"); VERB("Using partitioned transition relation encoding");
if (usingContextAutomaton()) { if (usingContextAutomaton()) {
partTrans = new BDDvec(numberOfProc+1); partTrans = new BDDvec(numberOfProc + 1);
} }
else { else {
partTrans = new BDDvec(numberOfProc); partTrans = new BDDvec(numberOfProc);
@@ -789,8 +789,7 @@ void SymRS::encodeTransitions(void)
VERB_LN(3, "Entity production encoding for all the processes and their products"); VERB_LN(3, "Entity production encoding for all the processes and their products");
if (opts->part_tr_rel) if (opts->part_tr_rel) {
{
for (const auto &proc_products : usedProducts) { for (const auto &proc_products : usedProducts) {
auto proc_id = proc_products.first; auto proc_id = proc_products.first;
@@ -949,9 +948,11 @@ void SymRS::encodeCtxAutTrans(void)
BDD enc_dst = encCtxAutStateSucc(t.dst_state); BDD enc_dst = encCtxAutStateSucc(t.dst_state);
BDD enc_ctx = compContext(encContext(t.ctx)); BDD enc_ctx = compContext(encContext(t.ctx));
BDD enc_drs_state = BDD_TRUE; BDD enc_drs_state = BDD_TRUE;
if (t.state_constr != nullptr) { if (t.state_constr != nullptr) {
enc_drs_state = t.state_constr->getBDDforState(this); enc_drs_state = t.state_constr->getBDDforState(this);
} }
BDD new_trans = enc_src * enc_drs_state * enc_ctx * enc_dst; BDD new_trans = enc_src * enc_drs_state * enc_ctx * enc_dst;
*tr_ca += new_trans; *tr_ca += new_trans;