+ ModelAction *act = tlt->front();
+ ClockVector *cv = act->get_cv();
+
+ /* Find the earliest in SC ordering */
+ for (int i = 0; i <= maxthreads; i++) {
+ if ( i == t )
+ continue;
+ action_list_t *threadlist = &threadlists[i];
+ if (threadlist->empty())
+ continue;
+ ModelAction *first = threadlist->front();
+ if (cv->synchronized_since(first)) {
+ act = NULL;
+ break;
+ }
+ }
+ if (act != NULL) {
+ array[count++]=act;
+ }
+ }
+
+ ASSERT(count==0 || cyclic);
+
+ return count;
+}
+
+ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) {
+ /* No choice */
+ if (count == 1)
+ return array[0];
+
+ /* Choose first non-write action */
+ ModelAction *nonwrite=NULL;
+ for(int i=0;i<count;i++) {
+ if (!array[i]->is_write())
+ if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number())
+ nonwrite = array[i];
+ }
+ if (nonwrite != NULL)
+ return nonwrite;
+
+ /* Look for non-conflicting action */
+ ModelAction *nonconflict=NULL;
+ for(int a=0;a<count;a++) {
+ ModelAction *act=array[a];
+ for (int i = 0; i <= maxthreads && act != NULL; i++) {
+ thread_id_t tid = int_to_id(i);
+ if (tid == act->get_tid())
+ continue;
+
+ action_list_t *list = &threadlists[id_to_int(tid)];
+ for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
+ ModelAction *write = *rit;
+ if (!write->is_write())
+ continue;
+ ClockVector *writecv = cvmap.get(write);
+ if (writecv->synchronized_since(act))
+ break;
+ if (write->get_location() == act->get_location()) {
+ //write is sc after act
+ act = NULL;
+ break;
+ }
+ }