This document  describes the MCI file format for storing
Petri net unfolding prefixes. 

Below, CHAR is a 1-byte char, and UINT4 is a little-endian
(i.e. the least significant byte is at the lowest address,
and the other bytes follow in increasing order of
significance.) 4-byte unsigned int (Intel is little-endian).

- the total number of conditions (UINT4)

- the total number of events (UINT4)

- for each event (from first to last):
	-- the number of the original transition (UINT4)

- for each condition (from first to last):
	--  the number of the original place (UINT4)
	--  the number of the preset event (UINT4); 
	    it's 0 if the condition is initial
	--  0(UINT4)-terminated list of postset events numbers (UINT4)

- for each cut-off event
	--  the number of cut-off event (UINT4)
	--  the number of corresponding event (UINT4); 
	    it's 0(UINT4) if the corresponding event is the 
	    virtual initial event; it's 0xFFFFFFFF (i.e ~0U) if the
	    corresponding event is unspecified for some reason,
	    e.g. the corresponding configuration is non-local 

- separating 0(UINT4)

- for each configuration:
	-- 0(UINT4)-terminated list of events numbers. 
	   (This is used by some ancient model checker; 
	   PUNF doesn't create it and just outputs the 
	   terminating 0(UINT4).)

- separating 0(UINT4)

- the total number of places in the original net (UINT4)

- the total number of transitions the in original net (UINT4)

- the maximal string length for place/transition names (UINT4) 
  (useful for memory allocation in the parser)

- for each place in original net:
	-- the name (0(CHAR)-terminated string)

- separating 0(CHAR)

- for each transition in original net:
	-- the name (0(CHAR)-terminated string)

- terminating 0(CHAR)


The following C++ code implements an MCI parser, and might
hopefully be useful as a reference:

void LLMCIProcess::readMCI(const char* filename){
	FILE* f=fopen(filename,"rb");
	if(!f){
		Error(cannot_open_file_inp,filename);
		exit(error_level());
	}

	unsigned num_cond=Read4bytesNum(f,filename);
	unsigned num_ev=Read4bytesNum(f,filename);

	// the sanity check: if the provided file is not little-endian 
	// or not an mci-file at all, fail gracefully rather than 
	// exhaust the memory;
	// if any of the file access functions fail during this check,
	// we simply skip the sanity check;
	// 1. try to determine the length of the file
	if(fseek(f,0,SEEK_END)==0){
		long file_len=ftell(f);
		if(file_len>=0){
			// the sanity check: the file should be least 4*num_ev+12*num_cond+30 bytes long
			if((VLONGUINT)file_len<4*(VLONGUINT)num_ev+12*(VLONGUINT)num_cond+30){
				Error(wrong_mci_file,filename);
				exit(error_level());
			}
		}
	}
	// rewind the file and skip the already read info 
	rewind(f);
	Read4bytesNum(f,filename);
	Read4bytesNum(f,filename);


	this->arr_pl.destroy_all();
	this->arr_pl.provide(num_cond);
	for(unsigned i=0;i<num_cond;i++){
		this->arr_pl.add(new CONDITION(i+1));
	}
	this->arr_tr.destroy_all();
	this->arr_tr.provide(num_ev);
	for(unsigned i=0;i<num_ev;i++){
		this->arr_tr.add(new EVENT(i+1,0));
	}
	
	unsigned buf;
	for(unsigned i=0;i<this->arr_tr.numit;i++){
		buf=Read4bytesNum(f,filename);
		this->arr_tr[i]->orig_node=(typename ORIGINAL_NET::TRANSITION*)buf;
	}
	
	for(unsigned i=0;i<this->arr_pl.numit;i++){
		buf=Read4bytesNum(f,filename);
		this->arr_pl[i]->orig_node=(typename ORIGINAL_NET::PLACE*)buf;
		buf=Read4bytesNum(f,filename);
		if(buf){
			this->arr_pl[i]->preset=this->arr_tr[buf-1];
			this->arr_tr[buf-1]->postset.add(this->arr_pl[i]);
		}
		buf=Read4bytesNum(f,filename);
		while(buf!=0){
			this->arr_pl[i]->postset.add(this->arr_tr[buf-1]);
			this->arr_tr[buf-1]->preset.add(this->arr_pl[i]);
			buf=Read4bytesNum(f,filename);
		}
	}
	
	// sort conditions postsets
	for(unsigned i=0;i<this->arr_pl.numit;i++){
		this->arr_pl[i]->sort_postset(cmp_numbers);
	}
	// sort events' presets and postsets
	for(unsigned i=0;i<this->arr_tr.numit;i++){
		this->arr_tr[i]->sort_preset(cmp_numbers);
		this->arr_tr[i]->sort_postset(cmp_numbers);
	}
	
	buf=Read4bytesNum(f,filename);
	while(buf!=0){
		EVENT* ev=this->arr_tr[buf-1];
		buf=Read4bytesNum(f,filename);
		if(buf==EVENT::CorrespondingConfiguration::get_unspecified_configuration_number()){
			ev->cutoff_corr.assign_unspecified();
		}
		else if(buf==0){
			ev->cutoff_corr.assign_empty();
		}
		else{
			ev->cutoff_corr.assign(this->arr_tr[buf-1]);
		}
		buf=Read4bytesNum(f,filename);
	}
	
	buf=Read4bytesNum(f,filename);
	while(buf!=0){
		while(buf!=0){
			buf=Read4bytesNum(f,filename);
		}
		buf=Read4bytesNum(f,filename);
	}
	
	if(!this->net) this->net = new ORIGINAL_NET();
	
	buf=Read4bytesNum(f,filename);
	this->net->arr_pl.destroy_all();
	this->net->arr_pl.provide(buf);
	for(unsigned i=0;i<buf;i++){
		this->net->arr_pl.add(new typename ORIGINAL_NET::PLACE(0,i+1));
	}
	
	buf=Read4bytesNum(f,filename);
	this->net->arr_tr.destroy_all();
	this->net->arr_tr.provide(buf);
	for(unsigned i=0;i<buf;i++){
		this->net->arr_tr.add(new typename ORIGINAL_NET::TRANSITION(0,i+1));
	}
	
	unsigned len=Read4bytesNum(f,filename);
	char* str=new char[len+1];
	for(unsigned i=0;i<this->net->arr_pl.numit;i++){
		ReadStr(str,f,filename);
		this->net->arr_pl[i]->name=_strdup(str);
	}
	
	ReadChar(f,filename);
	
	for(unsigned i=0;i<this->net->arr_tr.numit;i++){
		ReadStr(str,f,filename);
		this->net->arr_tr[i]->name=_strdup(str);
	}
	
	delete[] str;
	
	// fix the orig_node field of all mp-conditions and mp-events
	for(unsigned i=0;i<this->arr_pl.numit;i++){
		CONDITION* cond=this->arr_pl[i];
		cond->orig_node=this->net->arr_pl[(unsigned)cond->orig_node-1];
	}
	for(unsigned i=0;i<this->arr_tr.numit;i++){
		EVENT* ev=this->arr_tr[i];
		ev->orig_node=this->net->arr_tr[(unsigned)ev->orig_node-1];
	}

	for(unsigned i=0;i<this->arr_tr.numit;i++){
		EVENT* ev=this->arr_tr[i];
		typename ORIGINAL_NET::TRANSITION* tr=ev->orig_node;
		if(tr->preset.numit || tr->postset.numit) continue;
		for(unsigned j=0;j<ev->preset.numit;j++){
			typename ORIGINAL_NET::PLACE* pl=ev->preset[j]->orig_node;
			tr->preset.add(pl);
			pl->postset.add(tr);
		}
		for(unsigned j=0;j<ev->postset.numit;j++){
			typename ORIGINAL_NET::PLACE* pl=ev->postset[j]->orig_node;
			tr->postset.add(pl);
			pl->preset.add(tr);
		}
		
	}

	this->net->sort_nodes();
	
	// calculate the initial marking
	for(unsigned i=0;i<this->arr_pl.numit;i++){
		CONDITION* cond=this->arr_pl[i];
		if(!cond->preset){
			cond->orig_node->init_marking.add(new PNToken(PNToken::t_dot));
		}
	}
	
	fclose(f);
}