Mercurial > hg > Gears > Gears
view src/parallel_execution/ModelChecking/state_db.c @ 916:c8d83e38d87c
add visit_StateDB
author | ikkun <ikkun@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 28 Jan 2021 18:11:53 +0900 |
parents | 187d7172c951 |
children | 0111b0f68c4d |
line wrap: on
line source
#include <stdlib.h> #include "state_db.h" #include "memory.h" StateDB create_stateDB() { StateDB s = (StateDB)malloc(sizeof(StateNode)); if (!s) die_exit("Cann't alloc state db node."); return s; } static MemoryPtr mem_db; static int state_count0; void reset_state_count() { state_count0 = 0; } int state_count() { return state_count0; } /* lookup_StateDB(struct state *s, StateDB *parent, StatePtr *out) s->memory points the real memory if s is new, it is copied in the database (parent). if s is in the database, existing state is returned. if return value is 0, it returns new state. if out is null, no copy_state is created. (lookup mode) Founded state or newly created state is returned in out. */ int lookup_StateDB(StateDB s, StateDB *parent, StateDB *out) { StateDB db; int r; while(1) { db = *parent; if (!db) { /* not found */ if (out) { db = create_stateDB(); db->left = db->right = 0; db->memory = copy_memory(s->memory,&mem_db); db->hash = s->hash; state_count0 ++; *parent = db; *out = db; } return 0; } if (s->hash == db->hash) { r = cmp_memory(s->memory,db->memory); } else r = (s->hash > db->hash)? 1 : -1; if(!r) { /* bingo */ if (out) *out = db; return 1; } else if (r>0) { parent = &db->left; } else if (r<0) { parent = &db->right; } } } 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 */