- case EQUALITY:
- model_print("equality predicate, under construction\n");
- break;
- case NULLITY:
- model_print("nullity predicate, under construction\n");
- break;
- default:
- model_print("unknown predicate token\n");
+
+ switch(expression->token) {
+ case EQUALITY:
+ FuncInst * to_be_compared;
+ ModelAction * last_act;
+
+ to_be_compared = expression->func_inst;
+ last_act = inst_act_map->get(to_be_compared);
+
+ last_read = last_act->get_reads_from_value();
+ write_val = write_act->get_write_value();
+
+ equality = (last_read == write_val);
+ if (equality != expression->value)
+ satisfy_predicate = false;
+
+ model_print("equality predicate\n");
+ break;
+ case NULLITY:
+ model_print("nullity predicate, under construction\n");
+ break;
+ default:
+ model_print("unknown predicate token\n");
+ break;
+ }
+
+ if (!satisfy_predicate)