Advertisement
Guest User

Untitled

a guest
Dec 19th, 2014
162
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
C 1.78 KB | None | 0 0
  1. static void
  2. test_relprod()
  3. {
  4.     sylvan_gc_disable();
  5.  
  6.     BDDVAR vars[] = {0,2,4};
  7.     BDDVAR all_vars[] = {0,1,2,3,4,5};
  8.  
  9.     BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6);
  10.  
  11.     BDD s, t, next, prev;
  12.     BDD zeroes, ones;
  13.  
  14.     // transition relation: 000 --> 111 and !000 --> 000
  15.     t = sylvan_false;
  16.     t = sylvan_or(t, sylvan_cube(all_vars, 6, (char[]){0,1,0,1,0,1}));
  17.     t = sylvan_or(t, sylvan_cube(all_vars, 6, (char[]){1,0,2,0,2,0}));
  18.     t = sylvan_or(t, sylvan_cube(all_vars, 6, (char[]){2,0,1,0,2,0}));
  19.     t = sylvan_or(t, sylvan_cube(all_vars, 6, (char[]){2,0,2,0,1,0}));
  20.  
  21.     s = sylvan_cube(vars, 3, (char[]){0,0,1});
  22.     zeroes = sylvan_cube(vars, 3, (char[]){0,0,0});
  23.     ones = sylvan_cube(vars, 3, (char[]){1,1,1});
  24.  
  25.     next = sylvan_relprod_paired(s, t, all_vars_set);
  26.     prev = sylvan_relprod_paired_prev(next, t, all_vars_set);
  27.     assert(next == zeroes);
  28.     assert(prev == sylvan_not(zeroes));
  29.  
  30.     next = sylvan_relprod_paired(next, t, all_vars_set);
  31.     prev = sylvan_relprod_paired_prev(next, t, all_vars_set);
  32.     assert(next == ones);
  33.     assert(prev == zeroes);
  34.  
  35.     t = sylvan_cube(all_vars, 6, (char[]){0,0,0,0,0,1});
  36.     assert(sylvan_relprod_paired_prev(s, t, all_vars_set) == zeroes);
  37.     assert(sylvan_relprod_paired_prev(sylvan_not(s), t, all_vars_set) == sylvan_false);
  38.     assert(sylvan_relprod_paired(s, t, all_vars_set) == sylvan_false);
  39.     assert(sylvan_relprod_paired(zeroes, t, all_vars_set) == s);
  40.  
  41.     t = sylvan_cube(all_vars, 6, (char[]){0,0,0,0,0,2});
  42.     assert(sylvan_relprod_paired_prev(s, t, all_vars_set) == zeroes);
  43.     assert(sylvan_relprod_paired_prev(zeroes, t, all_vars_set) == zeroes);
  44.     assert(sylvan_relprod_paired(sylvan_not(zeroes), t, all_vars_set) == sylvan_false);
  45.  
  46.     sylvan_gc_enable();
  47. }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement