Mercurial > hg > Gears > Gears

changeset 916:c8d83e38d87c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add visit_StateDB
author ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
date Thu, 28 Jan 2021 18:11:53 +0900
parents 675eb6b5b69d
children 0111b0f68c4d
files src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/ModelChecking/state_db.c src/parallel_execution/ModelChecking/state_db.h
diffstat 3 files changed, 15 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Thu Jan 28 11:15:48 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Thu Jan 28 18:11:53 2021 +0900
@@ -14,7 +14,7 @@
 extern int lengthSingleLinkedQueue(struct SingleLinkedQueue* queue);
 extern Element* getElementByIdx(struct SingleLinkedQueue* queue, int idx);
 
-static int dump = 0;
+static int dump = 1;
 
 Worker* createMCWorker(struct Context* context, int id, Queue* queue) {
     struct Worker* worker = new Worker();
--- a/src/parallel_execution/ModelChecking/state_db.c	Thu Jan 28 11:15:48 2021 +0900
+++ b/src/parallel_execution/ModelChecking/state_db.c	Thu Jan 28 18:11:53 2021 +0900
@@ -48,7 +48,7 @@
 {
     StateDB db;
     int r;
-
+    
     while(1) {
       db = *parent;
       if (!db) {
@@ -80,4 +80,15 @@
     }
 }
 
+int
+visit_StateDB(StateDB s, StateDB *parent, int visit)
+{
+  StateDB out;
+  lookup__StateDB(s,parent,&out);
+  if (out->visit == visit) {
+    return 1;
+  }
+  out->visit = visit;
+  return 0;
+ }
 /* end */
--- a/src/parallel_execution/ModelChecking/state_db.h	Thu Jan 28 11:15:48 2021 +0900
+++ b/src/parallel_execution/ModelChecking/state_db.h	Thu Jan 28 18:11:53 2021 +0900
@@ -4,6 +4,8 @@
 typedef struct state_db {
     struct memory *memory;
     int hash;
+    int visit; // visiting count for repeating search
+    int flag;
     struct state_db *left;
     struct state_db *right;
 } StateNode, *StateDB;