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

Building of stateconstr.o; prelim. methods for ctx and state BDD enc.

Browse Source
This commit is contained in:
Artur Meski
2018-09-22 22:55:00 +01:00
parent a36ed9651f
commit 206996a700
4 changed files with 21 additions and 73 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
Makefile
View File

@@ -4,13 +4,13 @@ CUDD_INCLUDE=cudd/lib/libcudd.a
INCLUDES=-Icudd/include
CPPFLAGS_SILENT = $(INCLUDES)
CPPFLAGS = -Wall $(CPPFLAGS_SILENT) #-Werror
#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG
#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG
CXXFLAGS_SILENT = -O3 -g
CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
#CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
LDLIBS = $(CUDD_INCLUDE)
LDLIBS = $(CUDD_INCLUDE)
OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctlk.o
OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctlk.o stateconstr.o
all: reactics
@@ -44,7 +44,7 @@ rsin_parser.lex.cc: rsin_parser.ll
mv lex.yy.c rsin_parser.lex.cc
style:
astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh
astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh
commit: style
git commit -a

65
formrsctlk.cc
View File

@@ -8,71 +8,6 @@
#include "formrsctlk.hh"
std::string StateConstr::toStr(void) const
{
if (oper == STC_PV) {
return proc_name + "." + entity_name;
}
else if (oper == STC_TF) {
if (tf) {
return "true";
}
else {
return "false";
}
}
else if (oper == STC_AND) {
return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
}
else if (oper == STC_OR) {
return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
}
else if (oper == STC_XOR) {
return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
}
else if (oper == STC_NOT) {
return "~" + arg[0]->toStr();
}
else {
return "??";
assert(0);
}
}
BDD StateConstr::getBDD(const SymRS *srs) const
{
if (oper == STC_PV) {
return srs->encActStrEntity(proc_name, entity_name);
}
else if (oper == STC_TF) {
if (tf) {
return srs->getBDDtrue();
}
else {
return srs->getBDDfalse();
}
}
else if (oper == STC_AND) {
return arg[0]->getBDD(srs) * arg[1]->getBDD(srs);
}
else if (oper == STC_OR) {
return arg[0]->getBDD(srs) + arg[1]->getBDD(srs);
}
else if (oper == STC_XOR) {
return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs);
}
else if (oper == STC_NOT) {
return !arg[0]->getBDD(srs);
}
else {
assert(0);
FERROR("Undefined operator used in Boolean context definition. This should not happen.");
return srs->getBDDfalse();
}
}
std::string FormRSCTLK::toStr(void) const
{
if (oper == RSCTLK_PV) {

13
stateconstr.cc
View File

@@ -7,6 +7,10 @@
*/
#include "stateconstr.hh"
#include "types.hh"
#include "cudd.hh"
#include "bdd_macro.hh"
#include "symrs.hh"
std::string StateConstr::toStr(void) const
{
@@ -40,7 +44,13 @@ std::string StateConstr::toStr(void) const
}
}
BDD StateConstr::getBDD(const SymRS *srs) const
BDD StateConstr::getBDDforState(const SymRS *srs) const
{
assert(0);
// return BDD_FALSE;
}
BDD StateConstr::getBDDforContext(const SymRS *srs) const
{
if (oper == STC_PV) {
return srs->encActStrEntity(proc_name, entity_name);
@@ -71,4 +81,3 @@ BDD StateConstr::getBDD(const SymRS *srs) const
return srs->getBDDfalse();
}
}

8
stateconstr.hh
View File

@@ -11,7 +11,7 @@
#include "types.hh"
/* For Boolean contexts: */
/* For state constraints: */
#define STC_PV 80
#define STC_AND 81
#define STC_OR 82
@@ -87,7 +87,11 @@ class StateConstr
std::string toStr(void) const;
BDD getBDD(const SymRS *srs) const;
BDD getBDD(const SymRS *srs) const {
return getBDDforContext(srs);
}
BDD getBDDforContext(const SymRS *srs) const;
BDD getBDDforState(const SymRS *srs) const;
Oper getOper(void) const
{