From fa587e6f2a1532ee04601bd300a2ab5add6ae1ce Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Mon, 26 Mar 2018 13:10:26 +0100
Subject: [PATCH] Started on encoding for CA

---
 mc.cc    | 43 +++++++++++++++++++++++++++++++++++++++++++
 mc.hh    | 26 ++++++++------------------
 rs.hh    |  2 ++
 symrs.cc | 20 ++++++++++++++++++++
 symrs.hh |  9 +++++++++
 5 files changed, 82 insertions(+), 18 deletions(-)

diff --git a/mc.cc b/mc.cc
index 6a2c7c3..6fd8342 100644
--- a/mc.cc
+++ b/mc.cc
@@ -1,5 +1,47 @@
 #include "mc.hh"
 
+ModelChecker::ModelChecker(SymRS *srs, Options *opts)
+{
+    this->srs = srs;
+    this->opts = opts;
+    
+	cuddMgr = srs->getCuddMgr();
+	
+	if (srs->usingContextAutomaton())
+	    initStates = srs->getEncInitStates();
+	
+    totalStateVars = srs->getTotalStateVars();
+    
+	pv = srs->getEncPV();
+    pv_succ = srs->getEncPVsucc();
+    pv_E = srs->getEncPV_E();
+    pv_succ_E = srs->getEncPVsucc_E();
+    pv_act_E = srs->getEncPVact_E();
+
+    //
+	// Transition relations
+	//
+	// If we use trp, then trm is going to be nullptr (same for trm)
+	//
+	trp = srs->getEncPartTrans();
+    if (trp == nullptr) 
+		trp_size = 0;
+    else 
+		trp_size = trp->size();	
+    trm = srs->getEncMonoTrans();
+    
+	if (srs->usingContextAutomaton())
+	{
+		ca_init_state = srs->getEncCA_InitState();
+		pv_ca = srs->getEncCA_PV();
+		pv_ca_succ = srs->getEncCA_PVsucc();
+		ca_tr = srs->getEncCA_Trans();
+	}
+	
+	// Initialise the set of reachable states
+	reach = nullptr;
+}
+
 inline BDD ModelChecker::getSucc(const BDD &states)
 {
     BDD q = BDD_TRUE;
@@ -502,3 +544,4 @@ void ModelChecker::cleanup(void)
     reach = nullptr;
 }
 
+/** EOF **/
\ No newline at end of file
diff --git a/mc.hh b/mc.hh
index e2ddf5f..a09c68e 100644
--- a/mc.hh
+++ b/mc.hh
@@ -29,6 +29,13 @@ class ModelChecker
     BDD *reach;
     vector<BDD> *trp;
     BDD *trm;
+	
+	// Context Automaton
+	BDD *ca_init_state;
+	vector<BDD> *pv_ca;
+	vector<BDD> *pv_ca_succ;
+	BDD *ca_tr;
+	
     unsigned int trp_size;
     unsigned int totalStateVars;
 
@@ -46,24 +53,7 @@ class ModelChecker
     void cleanup(void);
 
 public:
-    ModelChecker(SymRS *srs, Options *opts)
-    {
-        this->srs = srs;
-        this->opts = opts;
-        cuddMgr = srs->getCuddMgr();
-        initStates = srs->getEncInitStates();
-        totalStateVars = srs->getTotalStateVars();
-        pv = srs->getEncPV();
-        pv_succ = srs->getEncPVsucc();
-        pv_E = srs->getEncPV_E();
-        pv_succ_E = srs->getEncPVsucc_E();
-        pv_act_E = srs->getEncPVact_E();
-        trp = srs->getEncPartTrans();
-        if (trp == nullptr) trp_size = 0;
-        else trp_size = trp->size();
-        trm = srs->getEncMonoTrans();
-        reach = nullptr;
-    }
+    ModelChecker(SymRS *srs, Options *opts);
 
     void printReach(void);
     void printReachWithSucc(void);
diff --git a/rs.hh b/rs.hh
index 513a4bf..21df20d 100644
--- a/rs.hh
+++ b/rs.hh
@@ -102,3 +102,5 @@ class RctSys
 };
 
 #endif
+
+/** EOF **/
\ No newline at end of file
diff --git a/symrs.cc b/symrs.cc
index fb6d4e5..a8f6d98 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -408,4 +408,24 @@ BDD SymRS::encActStrEntity(std::string name) const
 	}
 }
 
+BDD *SymRS::getEncCA_InitState(void)
+{
+	return new BDD(BDD_TRUE);
+}
+
+vector<BDD> *SymRS::getEncCA_PV(void)
+{
+	return new vector<BDD>();
+}
+
+vector<BDD> *SymRS::getEncCA_PVsucc(void)
+{
+	return new vector<BDD>();
+}
+
+BDD *SymRS::getEncCA_Trans(void)
+{
+	return new BDD(BDD_TRUE);
+}
+
 /** EOF **/
diff --git a/symrs.hh b/symrs.hh
index 08fd346..9f807ec 100644
--- a/symrs.hh
+++ b/symrs.hh
@@ -137,7 +137,16 @@ public:
     BDD encActStrEntity(std::string name) const;
     BDD getBDDtrue(void) const { return BDD_TRUE; }
     BDD getBDDfalse(void) const { return BDD_FALSE; }
+	
+	bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; }
+	
+	BDD *getEncCA_InitState(void);
+	vector<BDD> *getEncCA_PV(void);
+	vector<BDD> *getEncCA_PVsucc(void);
+	BDD *getEncCA_Trans(void);
+	
 };
 
 #endif
 
+/** EOF **/
\ No newline at end of file