From 03cbf26afabfdcaf5e46891335f345350bb9f008 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Mon, 26 Mar 2018 22:05:23 +0100
Subject: [PATCH] Bugfixes

---
 main.cc  |  8 ++++++--
 mc.cc    | 13 +++++++++----
 symrs.cc | 52 ++++++++++++++++++++++++++++++----------------------
 symrs.hh |  1 -
 4 files changed, 45 insertions(+), 29 deletions(-)

diff --git a/main.cc b/main.cc
index 2f8e3f1..3464b6c 100644
--- a/main.cc
+++ b/main.cc
@@ -186,9 +186,13 @@ int main(int argc, char **argv)
         ModelChecker mc(&srs, opts);
 
         if (reach_states)
-            mc.printReach();
+		{
+			mc.printReach();
+		}
         if (reach_states_succ)
-            mc.printReachWithSucc();
+		{
+			mc.printReachWithSucc();	
+		}
 
         if (rstl_model_checking)
         {
diff --git a/mc.cc b/mc.cc
index 51d5817..bcf74b0 100644
--- a/mc.cc
+++ b/mc.cc
@@ -7,7 +7,7 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
     
 	cuddMgr = srs->getCuddMgr();
 	
-	if (srs->usingContextAutomaton())
+	if (!srs->usingContextAutomaton())
 	    initStates = srs->getEncInitStates();
 	
     totalStateVars = srs->getTotalStateVars();
@@ -107,11 +107,15 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
 
 void ModelChecker::printReach(void)
 {
+	VERB_LN(2, "Printing/generating reachable states");
+	
     if (opts->measure)
         opts->ver_time = cpuTime();
 
+	assert(initStates != nullptr);
+	
     BDD *reach = new BDD(*initStates);
-    BDD reach_p = cuddMgr->bddZero();
+    BDD reach_p = BDD_FALSE;
 
     unsigned int k = 0;
 
@@ -138,12 +142,13 @@ void ModelChecker::printReach(void)
 
 void ModelChecker::printReachWithSucc(void)
 {
+	VERB_LN(2, "Printing/generating reachable states (with successors)");
+	
     BDD *reach = new BDD(*initStates);
     BDD reach_p = cuddMgr->bddZero();
 
     while (*reach != reach_p)
     {
-        //cout << "==[ " << ++k << " ]===========================" << endl;
         reach_p = *reach;
         BDD newStates = getSucc(*reach) - *reach;
         *reach += newStates;
@@ -530,7 +535,7 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
 
     cleanup(); 
 
-    cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold") << endl;
+    cout << "Formula " << form->toStr() << " " << (result ? "holds" : "does not hold") << endl;
 
     if (opts->measure)
     {
diff --git a/symrs.cc b/symrs.cc
index 6a9f502..268d2c6 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -13,15 +13,16 @@ SymRS::SymRS(RctSys *rs, Options *opts)
     totalStateVars = rs->getEntitiesSize();
     totalReactions = rs->getReactionsSize();
     totalActions = rs->getActionsSize();
+	
 	totalCtxAutStateVars = getCtxAutStateEncodingSize();
-
+	
     partTrans = nullptr;
     monoTrans = nullptr;
 	
 	pv_ca = nullptr;
 	pv_ca_succ = nullptr;
 
-    encode();
+    encode();	
 }
 
 BDD SymRS::encEntity_raw(Entity entity, bool succ) const
@@ -200,28 +201,31 @@ void SymRS::initBDDvars(void)
         *pv_act_E *= (*pv_act)[i];
     }
 
-	offset += totalActions;
-
-	VERB("Context automaton variables");
-
-	pv_ca = new vector<BDD>(totalCtxAutStateVars);
-	pv_ca_succ = new vector<BDD>(totalCtxAutStateVars);
-	pv_ca_E = new BDD(BDD_TRUE);
-	pv_ca_succ_E = new BDD(BDD_TRUE);
-	
-	//
-	// BDD variables for encoding local states of context automaton
-	//
-	unsigned int base_index = offset;
-	for (unsigned int i = 0; i < totalCtxAutStateVars; ++i)
+	if (usingContextAutomaton())
 	{
-		(*pv_ca)[i] = cuddMgr->bddVar(base_index);
-		(*pv_ca_succ)[i] = cuddMgr->bddVar(base_index+1);
+		VERB("Context automaton variables");
+
+		offset += totalActions;
+
+		pv_ca = new vector<BDD>(totalCtxAutStateVars);
+		pv_ca_succ = new vector<BDD>(totalCtxAutStateVars);
+		pv_ca_E = new BDD(BDD_TRUE);
+		pv_ca_succ_E = new BDD(BDD_TRUE);
 		
-		*pv_ca_E *= (*pv_ca)[i];
-		*pv_ca_succ_E *= (*pv_ca_succ)[i];
-	
-		base_index += 2;
+		//
+		// BDD variables for encoding local states of context automaton
+		//
+		unsigned int base_index = offset;
+		for (unsigned int i = 0; i < totalCtxAutStateVars; ++i)
+		{
+			(*pv_ca)[i] = cuddMgr->bddVar(base_index);
+			(*pv_ca_succ)[i] = cuddMgr->bddVar(base_index+1);
+			
+			*pv_ca_E *= (*pv_ca)[i];
+			*pv_ca_succ_E *= (*pv_ca_succ)[i];
+		
+			base_index += 2;
+		}
 	}
 
     VERB("All BDD variables ready");
@@ -433,6 +437,10 @@ BDD SymRS::encActStrEntity(std::string name) const
 
 size_t SymRS::getCtxAutStateEncodingSize(void)
 {
+	if (!usingContextAutomaton()) return 0;
+	
+	assert(rs->ctx_aut != nullptr);
+	
     size_t bitCount = 0;
     size_t bitCountMaxVal = 1;
     size_t numStates = rs->ctx_aut->statesCount();
diff --git a/symrs.hh b/symrs.hh
index a7e6e57..4f9d5c7 100644
--- a/symrs.hh
+++ b/symrs.hh
@@ -65,7 +65,6 @@ class SymRS
     unsigned int totalActions;
 	unsigned int totalCtxAutStateVars;
 	
-
     BDD encEntity_raw(Entity entity, bool succ) const;
     BDD encEntity(Entity entity) const {
         return encEntity_raw(entity, false);