changeset 918:26e3d0226cc6

add McDPP.cbc
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Fri, 29 Jan 2021 12:17:43 +0900
parents 0111b0f68c4d
children 765871c90c74 31ea8f75e9e6
files src/parallel_execution/MCTaskManagerImpl.h src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/examples/DPPMC/McDPP.cbc src/parallel_execution/examples/DPPMC/meta.pm
diffstat 4 files changed, 23 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/MCTaskManagerImpl.h	Fri Jan 29 11:55:16 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.h	Fri Jan 29 12:17:43 2021 +0900
@@ -9,6 +9,7 @@
   struct Element* taskList;
   MemoryPtr mem; // modelchecking memorylenge
   StateDB state_db;
+  StateNode st;
   int loopCounter;
   int cpu;
   int gpu;
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Fri Jan 29 11:55:16 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Fri Jan 29 12:17:43 2021 +0900
@@ -93,14 +93,13 @@
     StateDB out = NULL;
     struct Element* list = NULL;
     struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager;
-    StateNode st;
-    st.memory = mcti->mem;
-    st.hash = get_memory_hash(mcti->mem,0);
+    mcti->st.memory = mcti->mem;
+    mcti->st.hash = get_memory_hash(mcti->mem,0);
     if (dump) {
         dump_memory(mcti->mem);printf("\n");
     }
-    if (visit_StateDB(&st, &mcti->state_db, &out,mcti->visit)) {
-    // found in the state database
+    if (visit_StateDB(&mcti->st, &mcti->state_db, &out,mcti->visit)) {
+      // found in the state database
       // printf("found %d\n",count);
       while(!(list = takeNextIterator(mcworker->task_iter))) {
           // no more branch, go back to the previous one
@@ -123,6 +122,7 @@
       //    here we assume task list is fixed, we don't have to
       //    recover task list itself
       restore_memory(mcworker->task_iter->state->memory);
+      mcti->st = *out;
       context = (Context *)list->data;
       // printf("restore list %x next %x\n",(int)list,(int)(list->next));
     } else {
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/McDPP.cbc	Fri Jan 29 12:17:43 2021 +0900
@@ -0,0 +1,14 @@
+__ncode mcDPP(struct Context* context, enum Code next) {
+  struct MCWorker* mcworker =  (struct MCWorker*) context->worker->worker;
+  struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager;
+
+  if (mcti->prev == C_eatingPhisImpl) {
+    mcti->st->flag |= P_eating;
+  }
+
+  if (current_st & p_F_eating) {
+    mcti->st->flag |= P_F_eating;
+  }
+
+  goto mcMeta(context, next);
+}
--- a/src/parallel_execution/examples/DPPMC/meta.pm	Fri Jan 29 11:55:16 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/meta.pm	Fri Jan 29 12:17:43 2021 +0900
@@ -10,14 +10,14 @@
 
 #my ($currentCodeGearName, $context, $next) = @_;
 
-sub generateRondomMeta {
+sub generateRandomMeta {
   my ($context, $next) = @_;
-  return "goto rondom($context, $next);";
+  return "goto random($context, $next);";
 }
 
 sub generateMcMeta {
   my ($context, $next) = @_;
-  return "goto mcMeta($context, $next);";
+  return "goto mcDPP($context, $next);";
 }
 
 1;