Mercurial > hg > Gears > Gears

changeset 935:40735db036d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
flag checking
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Feb 2021 16:01:25 +0900
parents 296be5d6d524
children 55ae765ffcdd
files src/parallel_execution/MCTaskManagerImpl.cbc src/parallel_execution/MCTaskManagerImpl.h src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/ModelChecking/MCWorker.h src/parallel_execution/examples/DPPMC/McDPP.cbc src/parallel_execution/examples/DPPMC/McDPP.h
diffstat 6 files changed, 23 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/MCTaskManagerImpl.cbc	Mon Feb 01 15:46:05 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.cbc	Mon Feb 01 16:01:25 2021 +0900
@@ -7,7 +7,7 @@
 #include <stdio.h>
 #include <unistd.h>
 
-static void defultStatefunc(MCTaskManagerImpl* mcti, struct MCWorker* mcworker , StateDB now,StateDB next) {
+static void defultStatefunc(MCTaskManagerImpl* mcti, struct MCWorker* mcworker , StateDB now,StateDB next,int flag) {
 }
 
 void createWorkers(struct Context* context, MCTaskManagerImpl* taskManager);
--- a/src/parallel_execution/MCTaskManagerImpl.h	Mon Feb 01 15:46:05 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.h	Mon Feb 01 16:01:25 2021 +0900
@@ -14,6 +14,6 @@
   int gpu;
   int io;
   int maxCPU;
-  void (*statefunc)(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next);
+  void (*statefunc)(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next, int flag);
   __code next(...);
 } MCTaskManagerImpl;
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Feb 01 15:46:05 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Feb 01 16:01:25 2021 +0900
@@ -110,7 +110,7 @@
         dump_memory(mcti->mem);printf("\n");
     }
     int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit);
-    mcti->statefunc(mcti, mcWorker, mcWorker->parent, out);
+    mcti->statefunc(mcti, mcWorker, mcWorker->parent, out, mcWorker->checking);
     if (found) {
       // found in the state database
       // printf("found %d\n",count);
@@ -120,16 +120,17 @@
           if (!prev_iter) {
             printf("All done count %d repeat %d\n",mcWorker->count,mcWorker->visit);
             memory_usage();
-            if (! mcWorker->change) {
+            if (! mcWorker->change && mcWorker->checking) {
               exit(0);
-            } else {
-                mcWorker->change = 0;
-		mcWorker->visit++;
-                // start from root state and iterator
-                mcWorker->depth = 0;
-                struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcWorker->mcQueue->queue;
-                mcWorker->task_iter = createQueueIterator(mcSingleQueue->top->next,mcWorker->root,NULL);
-            }
+            } else if (! mcWorker->change ) {
+                mcWorker->checking = 1;
+            } 
+            mcWorker->change = 0;
+            mcWorker->visit++;
+            // start from root state and iterator
+            mcWorker->depth = 0;
+            struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcWorker->mcQueue->queue;
+            mcWorker->task_iter = createQueueIterator(mcSingleQueue->top->next,mcWorker->root,NULL);
           } else {
             //printf("no more branch %d\n",count);
             mcWorker->depth--;
--- a/src/parallel_execution/ModelChecking/MCWorker.h	Mon Feb 01 15:46:05 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.h	Mon Feb 01 16:01:25 2021 +0900
@@ -18,5 +18,6 @@
   int depth;
   int visit;
   int count;
-  int change;  // state db flag is changed
+  int change;    // state db flag is changed
+  int checking;  // state checking phase
 } MCWorker;
--- a/src/parallel_execution/examples/DPPMC/McDPP.cbc	Mon Feb 01 15:46:05 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/McDPP.cbc	Mon Feb 01 16:01:25 2021 +0900
@@ -1,6 +1,7 @@
 #include "McDPP.h"
+#include <stdio.h>
 
-void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcWorker, StateDB now,StateDB next) {
+void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcWorker, StateDB now,StateDB next, int check) {
   PhilsImpl* phils = (PhilsImpl*)GearImpl(mcWorker->mcContext, Phils, phils);
   int prev_now = now->flag; 
   int prev_next = next->flag; 
@@ -14,4 +15,9 @@
   }
   if ( prev_now != now->flag || prev_next != next->flag )
      mcWorker->change = 1;
+  if (check) {
+     if (!(now->flag & t_F_eating)) {
+         printf("not <> eating\n");
+     }
+  }
 }
--- a/src/parallel_execution/examples/DPPMC/McDPP.h	Mon Feb 01 15:46:05 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/McDPP.h	Mon Feb 01 16:01:25 2021 +0900
@@ -19,6 +19,6 @@
    f_GF_eating  = 0x30,     // ¬[] <> eating
 };
 
-extern void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next) ;
+extern void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next, int checking) ;
 
 #endif