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

RSCTL -> RSCTLK

Browse Source
This commit is contained in:
Artur Meski
2018-04-21 19:33:32 +01:00
parent 09578a075f
commit d2a9b5733c
12 changed files with 266 additions and 266 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@@ -10,7 +10,7 @@ CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
#CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
LDLIBS = $(CUDD_INCLUDE)
OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctl.o
OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctlk.o
all: main

88
formrsctl.cc → formrsctlk.cc
View File

@@ -6,7 +6,7 @@
without the author's permission is strictly prohibited.
*/
#include "formrsctl.hh"
#include "formrsctlk.hh"
std::string BoolContexts::toStr(void) const
@@ -73,12 +73,12 @@ BDD BoolContexts::getBDD(const SymRS *srs) const
}
}
std::string FormRSCTL::toStr(void) const
std::string FormRSCTLK::toStr(void) const
{
if (oper == RSCTL_PV) {
if (oper == RSCTLK_PV) {
return proc_name + "." + entity_name;
}
else if (oper == RSCTL_TF) {
else if (oper == RSCTLK_TF) {
if (tf) {
return "true";
}
@@ -86,69 +86,69 @@ std::string FormRSCTL::toStr(void) const
return "false";
}
}
else if (oper == RSCTL_AND) {
else if (oper == RSCTLK_AND) {
return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
}
else if (oper == RSCTL_OR) {
else if (oper == RSCTLK_OR) {
return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
}
else if (oper == RSCTL_XOR) {
else if (oper == RSCTLK_XOR) {
return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
}
else if (oper == RSCTL_IMPL) {
else if (oper == RSCTLK_IMPL) {
return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
}
else if (oper == RSCTL_NOT) {
else if (oper == RSCTLK_NOT) {
return "~" + arg[0]->toStr();
}
else if (oper == RSCTL_EX) {
else if (oper == RSCTLK_EX) {
return "EX(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_EG) {
else if (oper == RSCTLK_EG) {
return "EG(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_EU) {
else if (oper == RSCTLK_EU) {
return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
}
else if (oper == RSCTL_EF) {
else if (oper == RSCTLK_EF) {
return "EF(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_AX) {
else if (oper == RSCTLK_AX) {
return "AX(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_AG) {
else if (oper == RSCTLK_AG) {
return "AG(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_AU) {
else if (oper == RSCTLK_AU) {
return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
}
else if (oper == RSCTL_AF) {
else if (oper == RSCTLK_AF) {
return "AF(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_EX_ACT) {
else if (oper == RSCTLK_EX_ACT) {
return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_EG_ACT) {
else if (oper == RSCTLK_EG_ACT) {
return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_EU_ACT) {
else if (oper == RSCTLK_EU_ACT) {
return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
+ ")";
}
else if (oper == RSCTL_EF_ACT) {
else if (oper == RSCTLK_EF_ACT) {
return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_AX_ACT) {
else if (oper == RSCTLK_AX_ACT) {
return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_AG_ACT) {
else if (oper == RSCTLK_AG_ACT) {
return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
}
else if (oper == RSCTL_AU_ACT) {
else if (oper == RSCTLK_AU_ACT) {
return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
+ ")";
}
else if (oper == RSCTL_AF_ACT) {
else if (oper == RSCTLK_AF_ACT) {
return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
}
@@ -158,7 +158,7 @@ std::string FormRSCTL::toStr(void) const
}
}
bool FormRSCTL::hasOper(Oper op) const
bool FormRSCTLK::hasOper(Oper op) const
{
if (oper == op) {
return true;
@@ -178,28 +178,28 @@ bool FormRSCTL::hasOper(Oper op) const
}
}
void FormRSCTL::encodeEntities(const SymRS *srs)
void FormRSCTLK::encodeEntities(const SymRS *srs)
{
if (RSCTL_COND_1ARG(oper)) {
if (RSCTLK_COND_1ARG(oper)) {
arg[0]->encodeEntities(srs);
}
else if (RSCTL_COND_2ARG(oper)) {
else if (RSCTLK_COND_2ARG(oper)) {
arg[0]->encodeEntities(srs);
arg[1]->encodeEntities(srs);
}
else if (oper == RSCTL_PV) {
else if (oper == RSCTLK_PV) {
bdd = new BDD(srs->encEntity(proc_name, entity_name));
}
}
bool FormRSCTL::isERSCTL(void) const
bool FormRSCTLK::isERSCTLK(void) const
{
if (oper == RSCTL_PV) {
if (oper == RSCTLK_PV) {
return true;
}
if (oper == RSCTL_NOT) {
if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF) {
if (oper == RSCTLK_NOT) {
if (arg[0]->getOper() == RSCTLK_PV || arg[0]->getOper() == RSCTLK_TF) {
return true;
}
else {
@@ -207,16 +207,16 @@ bool FormRSCTL::isERSCTL(void) const
}
}
if (RSCTL_COND_IS_UNIVERSAL(oper)) {
if (RSCTLK_COND_IS_UNIVERSAL(oper)) {
return false;
}
if (RSCTL_COND_1ARG(oper)) {
return arg[0]->isERSCTL();
if (RSCTLK_COND_1ARG(oper)) {
return arg[0]->isERSCTLK();
}
if (RSCTL_COND_2ARG(oper)) {
return arg[0]->isERSCTL() && arg[1]->isERSCTL();
if (RSCTLK_COND_2ARG(oper)) {
return arg[0]->isERSCTLK() && arg[1]->isERSCTLK();
}
assert(0);
@@ -224,7 +224,7 @@ bool FormRSCTL::isERSCTL(void) const
return false;
}
std::string FormRSCTL::getActionsStr(void) const
std::string FormRSCTLK::getActionsStr(void) const
{
// if (actions != nullptr) {
// std::string r = "[ ";
@@ -267,9 +267,9 @@ std::string FormRSCTL::getActionsStr(void) const
}
}
void FormRSCTL::encodeActions(const SymRS *srs)
void FormRSCTLK::encodeActions(const SymRS *srs)
{
if (RSCTL_COND_ACT(oper)) {
if (RSCTLK_COND_ACT(oper)) {
if (actions_bdd != nullptr) {
forgetActionsBDD();
}
@@ -300,11 +300,11 @@ void FormRSCTL::encodeActions(const SymRS *srs)
}
}
if (RSCTL_COND_1ARG(oper)) {
if (RSCTLK_COND_1ARG(oper)) {
arg[0]->encodeActions(srs);
}
if (RSCTL_COND_2ARG(oper)) {
if (RSCTLK_COND_2ARG(oper)) {
arg[0]->encodeActions(srs);
arg[1]->encodeActions(srs);
}

134
formrsctl.hh → formrsctlk.hh
View File

@@ -6,8 +6,8 @@
without the author's permission is strictly prohibited.
*/
#ifndef RS_FORMRSCTL_HH
#define RS_FORMRSCTL_HH
#ifndef RS_FORMRSCTLK_HH
#define RS_FORMRSCTLK_HH
#include <iostream>
#include <string>
@@ -16,32 +16,32 @@
#include "symrs.hh"
#include "cudd.hh"
#define RSCTL_PV 0 // propositional variable
#define RSCTL_AND 1
#define RSCTL_OR 2
#define RSCTL_XOR 3
#define RSCTL_NOT 4
#define RSCTL_IMPL 5
#define RSCTL_EG 11 // Existential...
#define RSCTL_EU 12
#define RSCTL_EX 13
#define RSCTL_EF 14
#define RSCTL_AG 21 // Universal...
#define RSCTL_AU 22
#define RSCTL_AX 23
#define RSCTL_AF 24
#define RSCTL_EG_ACT 31 // Existential...
#define RSCTL_EU_ACT 32
#define RSCTL_EX_ACT 33
#define RSCTL_EF_ACT 34
#define RSCTL_AG_ACT 41 // Universal...
#define RSCTL_AU_ACT 42
#define RSCTL_AX_ACT 43
#define RSCTL_AF_ACT 44
#define RSCTL_TF 50 // true/false
#define RSCTLK_PV 0 // propositional variable
#define RSCTLK_AND 1
#define RSCTLK_OR 2
#define RSCTLK_XOR 3
#define RSCTLK_NOT 4
#define RSCTLK_IMPL 5
#define RSCTLK_EG 11 // Existential...
#define RSCTLK_EU 12
#define RSCTLK_EX 13
#define RSCTLK_EF 14
#define RSCTLK_AG 21 // Universal...
#define RSCTLK_AU 22
#define RSCTLK_AX 23
#define RSCTLK_AF 24
#define RSCTLK_EG_ACT 31 // Existential...
#define RSCTLK_EU_ACT 32
#define RSCTLK_EX_ACT 33
#define RSCTLK_EF_ACT 34
#define RSCTLK_AG_ACT 41 // Universal...
#define RSCTLK_AU_ACT 42
#define RSCTLK_AX_ACT 43
#define RSCTLK_AF_ACT 44
#define RSCTLK_TF 50 // true/false
#define RSCTL_UK 60 // Epistemic operators
#define RSCTL_NK 61
#define RSCTLK_UK 60 // Epistemic operators
#define RSCTLK_NK 61
/* For Boolean contexts: */
#define BCTX_PV 80
@@ -52,12 +52,12 @@
#define BCTX_TF 90
#define RSCTL_COND_1ARG(a) ((a) == RSCTL_NOT || (a) == RSCTL_EG || (a) == RSCTL_EF || (a) == RSCTL_EX || (a) == RSCTL_AG || (a) == RSCTL_AF || (a) == RSCTL_AX || (a) == RSCTL_EG_ACT || (a) == RSCTL_EF_ACT || (a) == RSCTL_EX_ACT || (a) == RSCTL_AG_ACT || (a) == RSCTL_AF_ACT || (a) == RSCTL_AX_ACT || (a) == RSCTL_UK || (a) == RSCTL_NK)
#define RSCTL_COND_2ARG(a) ((a) == RSCTL_AND || (a) == RSCTL_OR || (a) == RSCTL_XOR || (a) == RSCTL_IMPL || (a) == RSCTL_EU || (a) == RSCTL_AU || (a) == RSCTL_EU_ACT || (a) == RSCTL_AU_ACT)
#define RSCTL_COND_ACT(a) ((a) > 30 && (a) < 45)
#define RSCTL_IS_VALID(a) (RSCTL_COND_1ARG(a) || RSCTL_COND_2ARG(a) || (a) == RSCTL_PV || (a) == RSCTL_TF)
#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)
#define RSCTLK_IS_VALID(a) (RSCTLK_COND_1ARG(a) || RSCTLK_COND_2ARG(a) || (a) == RSCTLK_PV || (a) == RSCTLK_TF)
#define RSCTL_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))
#define BCTX_COND_1ARG(a) ((a) == BCTX_NOT)
#define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR)
@@ -155,10 +155,10 @@ class BoolContexts
}
};
class FormRSCTL
class FormRSCTLK
{
Oper oper;
FormRSCTL *arg[2];
FormRSCTLK *arg[2];
std::string entity_name;
std::string proc_name;
bool tf;
@@ -174,9 +174,9 @@ class FormRSCTL
* @param varName variable name used mostly for printing the variable.
* @param varBDD the BDD describing the set where the variable holds.
*/
FormRSCTL(std::string procName, std::string varName)
FormRSCTLK(std::string procName, std::string varName)
{
oper = RSCTL_PV;
oper = RSCTLK_PV;
proc_name = procName;
entity_name = varName;
arg[0] = nullptr;
@@ -192,9 +192,9 @@ class FormRSCTL
*
* @param val value of the logical constant
*/
FormRSCTL(bool val)
FormRSCTLK(bool val)
{
oper = RSCTL_TF;
oper = RSCTLK_TF;
tf = val;
arg[0] = nullptr;
arg[1] = nullptr;
@@ -207,10 +207,10 @@ class FormRSCTL
/**
* @brief Constructor for two-argument formula.
*/
FormRSCTL(Oper op, FormRSCTL *form1, FormRSCTL *form2)
FormRSCTLK(Oper op, FormRSCTLK *form1, FormRSCTLK *form2)
{
assert(RSCTL_COND_2ARG(op));
assert(!RSCTL_COND_ACT(op));
assert(RSCTLK_COND_2ARG(op));
assert(!RSCTLK_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = form2;
@@ -223,11 +223,11 @@ class FormRSCTL
/**
* @brief Constructor for two-argument formula with action restrictions.
*/
// FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2)
// FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1, FormRSCTLK *form2)
// {
// assert(acts != nullptr);
// assert(RSCTL_COND_2ARG(op));
// assert(RSCTL_COND_ACT(op));
// assert(RSCTLK_COND_2ARG(op));
// assert(RSCTLK_COND_ACT(op));
// oper = op;
// arg[0] = form1;
// arg[1] = form2;
@@ -240,11 +240,11 @@ class FormRSCTL
/**
* @brief Constructor for two-argument formula with Boolean context restrictions.
*/
FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2)
FormRSCTLK(Oper op, BoolContexts *bctx, FormRSCTLK *form1, FormRSCTLK *form2)
{
assert(bctx != nullptr);
assert(RSCTL_COND_2ARG(op));
assert(RSCTL_COND_ACT(op));
assert(RSCTLK_COND_2ARG(op));
assert(RSCTLK_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = form2;
@@ -257,10 +257,10 @@ class FormRSCTL
/**
* @brief Constructor for one-argument formula.
*/
FormRSCTL(Oper op, FormRSCTL *form1)
FormRSCTLK(Oper op, FormRSCTLK *form1)
{
assert(RSCTL_COND_1ARG(op));
assert(!RSCTL_COND_ACT(op));
assert(RSCTLK_COND_1ARG(op));
assert(!RSCTLK_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = nullptr;
@@ -273,11 +273,11 @@ class FormRSCTL
/**
* @brief Constructor for one-argument formula with action restrictions.
*/
// FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1)
// FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1)
// {
// assert(acts != nullptr);
// assert(RSCTL_COND_1ARG(op));
// assert(RSCTL_COND_ACT(op));
// assert(RSCTLK_COND_1ARG(op));
// assert(RSCTLK_COND_ACT(op));
// oper = op;
// arg[0] = form1;
// arg[1] = nullptr;
@@ -290,11 +290,11 @@ class FormRSCTL
/**
* @brief Constructor for one-argument formula with Boolean context restrictions.
*/
FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1)
FormRSCTLK(Oper op, BoolContexts *bctx, FormRSCTLK *form1)
{
assert(bctx != nullptr);
assert(RSCTL_COND_1ARG(op));
assert(RSCTL_COND_ACT(op));
assert(RSCTLK_COND_1ARG(op));
assert(RSCTLK_COND_ACT(op));
oper = op;
arg[0] = form1;
arg[1] = nullptr;
@@ -304,9 +304,9 @@ class FormRSCTL
boolCtx = bctx;
}
FormRSCTL(Oper op, Agents_f agents_set, FormRSCTL *form1)
FormRSCTLK(Oper op, Agents_f agents_set, FormRSCTLK *form1)
{
assert(RSCTL_COND_1ARG(op));
assert(RSCTLK_COND_1ARG(op));
oper = op;
arg[0] = form1;
arg[1] = nullptr;
@@ -318,7 +318,7 @@ class FormRSCTL
/**
* @brief Destructor.
*/
~FormRSCTL()
~FormRSCTLK()
{
delete arg[0];
delete arg[1];
@@ -331,36 +331,36 @@ class FormRSCTL
bool hasOper(Oper op) const;
const BDD *getBDD(void) const
{
assert(oper == RSCTL_PV);
assert(oper == RSCTLK_PV);
assert(bdd != nullptr);
return bdd;
}
const BDD *getActionsBDD(void) const
{
assert(RSCTL_COND_ACT(oper));
assert(RSCTLK_COND_ACT(oper));
assert(actions_bdd != nullptr);
return actions_bdd;
}
Oper getOper(void) const
{
assert(RSCTL_IS_VALID(oper));
assert(RSCTLK_IS_VALID(oper));
return oper;
}
FormRSCTL *getLeftSF(void) const
FormRSCTLK *getLeftSF(void) const
{
assert(arg[0] != nullptr);
return arg[0];
}
FormRSCTL *getRightSF(void) const
FormRSCTLK *getRightSF(void) const
{
assert(RSCTL_COND_2ARG(oper));
assert(RSCTLK_COND_2ARG(oper));
assert(arg[1] != nullptr);
return arg[1];
}
std::string getActionsStr(void) const;
bool getTF(void) const
{
assert(oper == RSCTL_TF);
assert(oper == RSCTLK_TF);
return tf;
}
void encodeEntities(const SymRS *srs);
@@ -371,7 +371,7 @@ class FormRSCTL
delete actions_bdd;
}
}
bool isERSCTL(void) const;
bool isERSCTLK(void) const;
};
#endif

6
main.cc
View File

@@ -182,10 +182,10 @@ int main(int argc, char **argv)
if (rstl_model_checking) {
if (bmc) {
cout << "Using BDD-based Bounded Model Checking" << endl;
mc.checkRSCTL(driver.getFormRSCTL());
mc.checkRSCTLK(driver.getFormRSCTLK());
}
else {
mc.checkRSCTLfull(driver.getFormRSCTL());
mc.checkRSCTLKfull(driver.getFormRSCTLK());
}
}
}
@@ -233,7 +233,7 @@ void print_help(std::string path_str)
#endif
<< " Usage: " << path_str << " [options] <inputfile>" << endl << endl
<< " TASKS:" << endl
<< " -c -- perform RSCTL model checking" << endl
<< " -c -- perform RSCTLK model checking" << endl
//<< " -f K -- generate SMT input for the depth K" << endl
<< " -P -- print parsed system" << endl
<< " -r -- print reactions" << endl

128
mc.cc
View File

@@ -233,15 +233,15 @@ bool ModelChecker::checkReach(const Entities testState)
return false;
}
BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
{
assert(reach != nullptr);
Oper oper = form->getOper();
if (oper == RSCTL_PV) {
if (oper == RSCTLK_PV) {
return *form->getBDD() * *reach;
}
else if (oper == RSCTL_TF) {
else if (oper == RSCTLK_TF) {
if (form->getTF() == true) {
return *reach;
}
@@ -249,47 +249,47 @@ BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
return cuddMgr->bddZero();
}
}
else if (oper == RSCTL_AND) {
return getStatesRSCTL(form->getLeftSF()) * getStatesRSCTL(form->getRightSF());
else if (oper == RSCTLK_AND) {
return getStatesRSCTLK(form->getLeftSF()) * getStatesRSCTLK(form->getRightSF());
}
else if (oper == RSCTL_OR) {
return getStatesRSCTL(form->getLeftSF()) + getStatesRSCTL(form->getRightSF());
else if (oper == RSCTLK_OR) {
return getStatesRSCTLK(form->getLeftSF()) + getStatesRSCTLK(form->getRightSF());
}
else if (oper == RSCTL_XOR) {
return getStatesRSCTL(form->getLeftSF()) ^ getStatesRSCTL(form->getRightSF());
else if (oper == RSCTLK_XOR) {
return getStatesRSCTLK(form->getLeftSF()) ^ getStatesRSCTLK(form->getRightSF());
}
else if (oper == RSCTL_IMPL) {
return (!getStatesRSCTL(form->getLeftSF()) * *reach) + getStatesRSCTL(
else if (oper == RSCTLK_IMPL) {
return (!getStatesRSCTLK(form->getLeftSF()) * *reach) + getStatesRSCTLK(
form->getRightSF());
}
else if (oper == RSCTL_NOT) {
return !getStatesRSCTL(form->getLeftSF()) * *reach;
else if (oper == RSCTLK_NOT) {
return !getStatesRSCTLK(form->getLeftSF()) * *reach;
}
else if (oper == RSCTL_EX) {
return getPreE(getStatesRSCTL(form->getLeftSF())) * *reach;
else if (oper == RSCTLK_EX) {
return getPreE(getStatesRSCTLK(form->getLeftSF())) * *reach;
}
else if (oper == RSCTL_EG) {
return statesEG(getStatesRSCTL(form->getLeftSF()));
else if (oper == RSCTLK_EG) {
return statesEG(getStatesRSCTLK(form->getLeftSF()));
}
else if (oper == RSCTL_EU) {
else if (oper == RSCTLK_EU) {
return statesEU(
getStatesRSCTL(form->getLeftSF()),
getStatesRSCTL(form->getRightSF())
getStatesRSCTLK(form->getLeftSF()),
getStatesRSCTLK(form->getRightSF())
);
}
else if (oper == RSCTL_EF) {
return statesEF(getStatesRSCTL(form->getLeftSF()));
else if (oper == RSCTLK_EF) {
return statesEF(getStatesRSCTLK(form->getLeftSF()));
}
else if (oper == RSCTL_AX) {
return !getPreE(!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
else if (oper == RSCTLK_AX) {
return !getPreE(!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
}
else if (oper == RSCTL_AG) {
else if (oper == RSCTLK_AG) {
return !statesEF(
!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
}
else if (oper == RSCTL_AU) {
BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach;
BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach;
else if (oper == RSCTLK_AU) {
BDD ng = !getStatesRSCTLK(form->getRightSF()) * *reach;
BDD nf = !getStatesRSCTLK(form->getLeftSF()) * *reach;
BDD x = !statesEU(ng, ng * nf) * *reach;
@@ -299,40 +299,40 @@ BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
return x;
}
else if (oper == RSCTL_AF) {
else if (oper == RSCTLK_AF) {
return !statesEG(
!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
}
/***** CONTEXT RESTRICTIONS: ******/
else if (oper == RSCTL_EX_ACT) {
return getPreEctx(getStatesRSCTL(form->getLeftSF()),
else if (oper == RSCTLK_EX_ACT) {
return getPreEctx(getStatesRSCTLK(form->getLeftSF()),
form->getActionsBDD()) * *reach;
}
else if (oper == RSCTL_EG_ACT) {
else if (oper == RSCTLK_EG_ACT) {
return statesEGctx(form->getActionsBDD(),
getStatesRSCTL(form->getLeftSF())); /***** EG? *****/
getStatesRSCTLK(form->getLeftSF())); /***** EG? *****/
}
else if (oper == RSCTL_EU_ACT) {
else if (oper == RSCTLK_EU_ACT) {
return statesEUctx(
form->getActionsBDD(),
getStatesRSCTL(form->getLeftSF()),
getStatesRSCTL(form->getRightSF())
getStatesRSCTLK(form->getLeftSF()),
getStatesRSCTLK(form->getRightSF())
);
}
else if (oper == RSCTL_EF_ACT) {
return statesEFctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF()));
else if (oper == RSCTLK_EF_ACT) {
return statesEFctx(form->getActionsBDD(), getStatesRSCTLK(form->getLeftSF()));
}
else if (oper == RSCTL_AX_ACT) {
return !getPreEctx(!getStatesRSCTL(form->getLeftSF()) * *reach,
else if (oper == RSCTLK_AX_ACT) {
return !getPreEctx(!getStatesRSCTLK(form->getLeftSF()) * *reach,
form->getActionsBDD()) * *reach;
}
else if (oper == RSCTL_AG_ACT) {
else if (oper == RSCTLK_AG_ACT) {
return !statesEFctx(form->getActionsBDD(),
!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
}
else if (oper == RSCTL_AU_ACT) {
BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach;
BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach;
else if (oper == RSCTLK_AU_ACT) {
BDD ng = !getStatesRSCTLK(form->getRightSF()) * *reach;
BDD nf = !getStatesRSCTLK(form->getLeftSF()) * *reach;
BDD x = !statesEUctx(form->getActionsBDD(), ng, ng * nf) * *reach;
@@ -342,9 +342,9 @@ BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
return x;
}
else if (oper == RSCTL_AF_ACT) {
else if (oper == RSCTLK_AF_ACT) {
return !statesEGctx(form->getActionsBDD(),
!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
}
assert(0); // Should never happen
@@ -454,17 +454,17 @@ BDD ModelChecker::getIthOnly(Process proc_id)
return bdd;
}
bool ModelChecker::checkRSCTL(FormRSCTL *form)
bool ModelChecker::checkRSCTLK(FormRSCTLK *form)
{
if (form->isERSCTL()) {
return checkRSCTLbmc(form);
if (form->isERSCTLK()) {
return checkRSCTLKbmc(form);
}
else {
return checkRSCTLfull(form);
return checkRSCTLKfull(form);
}
}
bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form)
{
if (opts->measure) {
opts->ver_time = cpuTime();
@@ -474,7 +474,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
bool result = false;
VERB("Model checking for RSCTL formula: " << form->toStr());
VERB("Model checking for RSCTLK formula: " << form->toStr());
VERB("Processing the formula: encoding entities");
form->encodeEntities(srs);
@@ -514,8 +514,8 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
VERB("Checking the formula");
//if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero())
if (*initStates * getStatesRSCTL(form) == *initStates) {
//if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
if (*initStates * getStatesRSCTLK(form) == *initStates) {
result = true;
}
else {
@@ -535,7 +535,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
return result;
}
bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
{
if (opts->measure) {
opts->ver_time = cpuTime();
@@ -543,14 +543,14 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
assert(form != nullptr);
if (!form->isERSCTL()) {
if (!form->isERSCTLK()) {
FERROR("Formula " << form->toStr() <<
" is not syntactically an ERSCTL formula");
" is not syntactically an ERSCTLK formula");
}
bool result = false;
VERB("Bounded model checking for RSCTL formula: " << form->toStr());
VERB("Bounded model checking for RSCTLK formula: " << form->toStr());
VERB("Processing the formula: encoding entities");
form->encodeEntities(srs);
@@ -572,8 +572,8 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
cout << "\rIteration " << ++k << flush;
}
//if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero())
if (*initStates * getStatesRSCTL(form) == *initStates) {
//if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
if (*initStates * getStatesRSCTLK(form) == *initStates) {
result = true;
break;
}
@@ -605,4 +605,4 @@ void ModelChecker::cleanup(void)
reach = nullptr;
}
/** EOF **/
/** EOF **/

10
mc.hh
View File

@@ -4,7 +4,7 @@
#include "cudd.hh"
#include "rs.hh"
#include "symrs.hh"
#include "formrsctl.hh"
#include "formrsctlk.hh"
#include "macro.hh"
#include "bdd_macro.hh"
#include "options.hh"
@@ -53,7 +53,7 @@ class ModelChecker
BDD getSucc(const BDD &states);
BDD getPreE(const BDD &states);
BDD getPreEctx(const BDD &states, const BDD *contexts);
BDD getStatesRSCTL(const FormRSCTL *form);
BDD getStatesRSCTLK(const FormRSCTLK *form);
BDD statesEG(const BDD &states);
BDD statesEU(const BDD &statesA, const BDD &statesB);
BDD statesEF(const BDD &states);
@@ -71,9 +71,9 @@ class ModelChecker
void printReach(void);
void printReachWithSucc(void);
bool checkReach(const Entities testState);
bool checkRSCTL(FormRSCTL *form);
bool checkRSCTLfull(FormRSCTL *form);
bool checkRSCTLbmc(FormRSCTL *form);
bool checkRSCTLK(FormRSCTLK *form);
bool checkRSCTLKfull(FormRSCTLK *form);
bool checkRSCTLKbmc(FormRSCTLK *form);
};
#endif

2
rs.hh
View File

@@ -137,4 +137,4 @@ class RctSys
#endif
/** EOF **/
/** EOF **/

10
rsin_driver.cc
View File

@@ -17,7 +17,7 @@ rsin_driver::rsin_driver(RctSys *rs)
void rsin_driver::initialise(void)
{
rs = nullptr;
rsctlform = nullptr;
rsctlkform = nullptr;
opts = nullptr;
use_ctx_aut = false;
use_concentrations = false;
@@ -49,13 +49,13 @@ void rsin_driver::error(const std::string &m)
std::cerr << m << std::endl;
}
FormRSCTL *rsin_driver::getFormRSCTL(void)
FormRSCTLK *rsin_driver::getFormRSCTLK(void)
{
if (rsctlform == nullptr) {
FERROR("RSCTL formula was not supplied!");
if (rsctlkform == nullptr) {
FERROR("RSCTLK formula was not supplied!");
}
return rsctlform;
return rsctlkform;
}
//

10
rsin_driver.hh
View File

@@ -4,7 +4,7 @@
#include <map>
#include "rsin_parser.hh"
#include "rs.hh"
#include "formrsctl.hh"
#include "formrsctlk.hh"
#include "options.hh"
// Tell Flex the lexer's prototype ...
@@ -25,7 +25,7 @@ class rsin_driver
virtual ~rsin_driver();
//std::map<std::string, int> variables;
FormRSCTL *rsctlform;
FormRSCTLK *rsctlkform;
Options *opts;
// options in configuration file:
@@ -45,11 +45,11 @@ class rsin_driver
{
this->opts = opts;
};
void addFormRSCTL(FormRSCTL *f)
void addFormRSCTLK(FormRSCTLK *f)
{
rsctlform = f;
rsctlkform = f;
};
FormRSCTL *getFormRSCTL(void);
FormRSCTLK *getFormRSCTLK(void);
void ensureOptionsAllowed(void);
void useContextAutomaton(void);

2
rsin_parser.ll
View File

@@ -48,7 +48,7 @@ blank [ \t]
"transitions" return token::TRANSITIONS;
"states" return token::STATES;
"init-state" return token::INITSTATE;
"rsctl-property" return token::RSCTLFORM;
"rsctlk-property" return token::RSCTLKFORM;
"{" return token::LCB;
"}" return token::RCB;
"(" return token::LRB;

138
rsin_parser.yy
View File

@@ -6,7 +6,7 @@
%code requires {
#include <string>
#include <set>
#include "formrsctl.hh"
#include "formrsctlk.hh"
using std::set;
using std::string;
@@ -33,7 +33,7 @@ class rsin_driver;
{
int ival;
std::string *sval;
FormRSCTL *frsctl;
FormRSCTLK *frsctlk;
// Entity_f *ent;
// Action_f *act;
// ActionsVec_f *actionsVec;
@@ -45,7 +45,7 @@ class rsin_driver;
}
%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS
%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM
%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLKFORM
%token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
%token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL DOT COMMA RARR
%token AND OR XOR IMPLIES NOT
@@ -60,7 +60,7 @@ class rsin_driver;
//%right SRB
%type <frsctl> rsctl_form
%type <frsctlk> rsctlk_form
// %type <ent> f_entity
// %type <act> action
// %type <actionsVec> actions
@@ -81,8 +81,8 @@ system:
| INITIALCONTEXTS LCB initstates RCB system
| CONTEXTENTITIES LCB actionentities RCB system
| CONTEXTAUTOMATON LCB ctxaut RCB system
| RSCTLFORM LCB rsctl_form RCB system {
driver.addFormRSCTL($3);
| RSCTLKFORM LCB rsctlk_form RCB system {
driver.addFormRSCTLK($3);
}
;
@@ -316,110 +316,110 @@ bool_contexts: IDENTIFIER DOT IDENTIFIER {
// }
// ;
rsctl_form:
rsctlk_form:
IDENTIFIER DOT IDENTIFIER {
$$ = new FormRSCTL(*$1, *$3);
$$ = new FormRSCTLK(*$1, *$3);
free($1);
free($3);
}
| NOT rsctl_form {
$$ = new FormRSCTL(RSCTL_NOT, $2);
| NOT rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_NOT, $2);
}
| LRB rsctl_form RRB {
| LRB rsctlk_form RRB {
$$ = $2;
}
| rsctl_form AND rsctl_form {
$$ = new FormRSCTL(RSCTL_AND, $1, $3);
| rsctlk_form AND rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AND, $1, $3);
}
| rsctl_form OR rsctl_form {
$$ = new FormRSCTL(RSCTL_OR, $1, $3);
| rsctlk_form OR rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_OR, $1, $3);
}
| rsctl_form XOR rsctl_form {
$$ = new FormRSCTL(RSCTL_XOR, $1, $3);
| rsctlk_form XOR rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_XOR, $1, $3);
}
| rsctl_form IMPLIES rsctl_form {
$$ = new FormRSCTL(RSCTL_IMPL, $1, $3);
| rsctlk_form IMPLIES rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_IMPL, $1, $3);
}
| EX rsctl_form {
$$ = new FormRSCTL(RSCTL_EX, $2);
| EX rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_EX, $2);
}
| EU LRB rsctl_form COMMA rsctl_form RRB {
$$ = new FormRSCTL(RSCTL_EU, $3, $5);
| EU LRB rsctlk_form COMMA rsctlk_form RRB {
$$ = new FormRSCTLK(RSCTLK_EU, $3, $5);
}
| EF rsctl_form {
$$ = new FormRSCTL(RSCTL_EF, $2);
| EF rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_EF, $2);
}
| EG rsctl_form {
$$ = new FormRSCTL(RSCTL_EG, $2);
| EG rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_EG, $2);
}
| AX rsctl_form {
$$ = new FormRSCTL(RSCTL_AX, $2);
| AX rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AX, $2);
}
| AU LRB rsctl_form COMMA rsctl_form RRB {
$$ = new FormRSCTL(RSCTL_AU, $3, $5);
| AU LRB rsctlk_form COMMA rsctlk_form RRB {
$$ = new FormRSCTLK(RSCTLK_AU, $3, $5);
}
| AF rsctl_form {
$$ = new FormRSCTL(RSCTL_AF, $2);
| AF rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AF, $2);
}
| AG rsctl_form {
$$ = new FormRSCTL(RSCTL_AG, $2);
| AG rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AG, $2);
}
| UK LSB IDENTIFIER RSB LRB rsctl_form RRB {
| UK LSB IDENTIFIER RSB LRB rsctlk_form RRB {
Agents_f agents;
agents.insert(*$3);
$$ = new FormRSCTL(RSCTL_UK, agents, $6);
$$ = new FormRSCTLK(RSCTLK_UK, agents, $6);
free($3);
}
// | E LSB actions RSB X rsctl_form {
// $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
// | E LSB actions RSB X rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
// }
// | E LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
// $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
// | E LSB actions RSB U LRB rsctlk_form COMMA rsctlk_form RRB {
// $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
// }
// | E LSB actions RSB F rsctl_form {
// $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
// | E LSB actions RSB F rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
// }
// | E LSB actions RSB G rsctl_form {
// $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
// | E LSB actions RSB G rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
// }
// | A LSB actions RSB X rsctl_form {
// $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
// | A LSB actions RSB X rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
// }
// | A LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
// $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
// | A LSB actions RSB U LRB rsctlk_form COMMA rsctlk_form RRB {
// $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
// }
// | A LSB actions RSB F rsctl_form {
// $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
// | A LSB actions RSB F rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
// }
// | A LSB actions RSB G rsctl_form {
// $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
// | A LSB actions RSB G rsctlk_form {
// $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
// }
/* contexts as boolean formulae */
| E LAB bool_contexts RAB X rsctl_form {
$$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
| E LAB bool_contexts RAB X rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
}
| E LAB bool_contexts RAB U LRB rsctl_form COMMA rsctl_form RRB {
$$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
| E LAB bool_contexts RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
$$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
}
| E LAB bool_contexts RAB F rsctl_form {
$$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
| E LAB bool_contexts RAB F rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
}
| E LAB bool_contexts RAB G rsctl_form {
$$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
| E LAB bool_contexts RAB G rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
}
| A LAB bool_contexts RAB X rsctl_form {
$$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
| A LAB bool_contexts RAB X rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
}
| A LAB bool_contexts RAB U LRB rsctl_form COMMA rsctl_form RRB {
$$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
| A LAB bool_contexts RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
$$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
}
| A LAB bool_contexts RAB F rsctl_form {
$$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
| A LAB bool_contexts RAB F rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
}
| A LAB bool_contexts RAB G rsctl_form {
$$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
| A LAB bool_contexts RAB G rsctlk_form {
$$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
}
;
%%

2
symrs.hh
View File

@@ -30,7 +30,7 @@ using std::map;
class SymRS
{
friend class ModelChecker;
friend class FormRSCTL;
friend class FormRSCTLK;
public:
SymRS(RctSys *rs, Options *opts);