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

Optimisations

Browse Source
This commit is contained in:
Artur Meski
2018-07-22 20:20:14 +01:00
parent 18e840ce17
commit 07171c6d60
5 changed files with 22 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
drs_benchmark.sh
View File

@@ -2,9 +2,9 @@
TMPINPUT="tmp_$RANDOM$RANDOM.rs" TMPINPUT="tmp_$RANDOM$RANDOM.rs"
CMD="./reactics -z -b -B" CMD="./reactics -zxbB"
for i in `seq 2 20`;do for i in `seq 2 9`;do
echo "[i] n=$i; generating input file" echo "[i] n=$i; generating input file"
in/gen_drs_mutex.py $i > $TMPINPUT in/gen_drs_mutex.py $i > $TMPINPUT

6
formrsctlk.hh
View File

@@ -40,8 +40,8 @@
#define RSCTLK_AF_ACT 44 #define RSCTLK_AF_ACT 44
#define RSCTLK_TF 50 // true/false #define RSCTLK_TF 50 // true/false
#define RSCTLK_UK 60 // Epistemic operators #define RSCTLK_NK 61 // Epistemic operators
#define RSCTLK_NK 61 #define RSCTLK_UK 71
/* For Boolean contexts: */ /* For Boolean contexts: */
#define BCTX_PV 80 #define BCTX_PV 80
@@ -57,7 +57,7 @@
#define RSCTLK_COND_ACT(a) ((a) > 30 && (a) < 45) #define RSCTLK_COND_ACT(a) ((a) > 30 && (a) < 45)
#define RSCTLK_IS_VALID(a) (RSCTLK_COND_1ARG(a) || RSCTLK_COND_2ARG(a) || (a) == RSCTLK_PV || (a) == RSCTLK_TF) #define RSCTLK_IS_VALID(a) (RSCTLK_COND_1ARG(a) || RSCTLK_COND_2ARG(a) || (a) == RSCTLK_PV || (a) == RSCTLK_TF)
#define RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45)) #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_1ARG(a) ((a) == BCTX_NOT)
#define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR) #define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR)

13
mc.cc
View File

@@ -75,6 +75,7 @@ inline BDD ModelChecker::getSucc(const BDD &states)
if (opts->part_tr_rel) { if (opts->part_tr_rel) {
for (const auto &trans : *trp) { for (const auto &trans : *trp) {
q *= states * trans; q *= states * trans;
reorder();
} }
} }
else { else {
@@ -101,6 +102,7 @@ inline BDD ModelChecker::getPreE(const BDD &states)
if (opts->part_tr_rel) { if (opts->part_tr_rel) {
for (const auto &trans : *trp) { for (const auto &trans : *trp) {
q *= x * trans; q *= x * trans;
reorder();
} }
} }
else { else {
@@ -123,6 +125,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
if (opts->part_tr_rel) { if (opts->part_tr_rel) {
for (const auto &trans : *trp) { for (const auto &trans : *trp) {
q *= x * trans; q *= x * trans;
reorder();
} }
q *= *contexts; q *= *contexts;
} }
@@ -619,6 +622,16 @@ bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
return result; return result;
} }
void ModelChecker::reorder(void)
{
if (opts->reorder_trans) {
VERB_L2("Reordering START");
// Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 100000);
cuddMgr->ReduceHeap(CUDD_REORDER_GROUP_SIFT);
VERB_L2("Reordering DONE");
}
}
void ModelChecker::cleanup(void) void ModelChecker::cleanup(void)
{ {
delete reach; delete reach;

2
mc.hh
View File

@@ -66,6 +66,8 @@ class ModelChecker
void cleanup(void); void cleanup(void);
void reorder(void);
public: public:
ModelChecker(SymRS *srs, Options *opts); ModelChecker(SymRS *srs, Options *opts);

3
symrs.cc
View File

@@ -946,7 +946,8 @@ void SymRS::reorder(void)
{ {
if (opts->reorder_trans) { if (opts->reorder_trans) {
VERB_L2("Reordering START"); VERB_L2("Reordering START");
Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); // Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
cuddMgr->ReduceHeap(CUDD_REORDER_GROUP_SIFT);
VERB_L2("Reordering DONE"); VERB_L2("Reordering DONE");
} }
} }