//namespace DSM.machine.PetriNet;

import DSM.metamodel.PetriNet.PetriNetEditor;
 
@incremental
// All transformation for Petri Net simulation
machine 'PetriNetGenerator'
{
	// 'Transition' is a transition of the petri net 'PN'.
	pattern petriTransition(PN, Transition) =
	{
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X, PN, Transition);
	}
	
	rule test() = seq{
		let C = 1/*, PN = DSM.model.PetriNet.Sparse_0*/ in iterate choose P,PN with find petriPlace(PN,P) do seq{
			println("found: " + P);
			update C = C + 1;
			if (C > 5) fail;
		}
	}
	
	@Random
	pattern petriPlace(PN,Place) =
	{	 
		'PetriNet'(PN);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X2, PN, Place);
	}
	
	// 'Place' is a source place for transition 'Transition'.
	pattern sourcePlace(Transition, Place, OutArc) =
	{
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X1, PN, Transition);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X2, PN, Place);
		'PetriNet'.'Place'.'OutArc'(OutArc, Place, Transition);
	}
	
	// 'Place' is a target place for transition 'Transition'.
	@Random
	pattern targetPlace(Transition, Place, InArc) =
	{
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X1, PN, Transition);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X2, PN, Place);
		'PetriNet'.'Transition'.'InArc'(InArc, Transition, Place);
	}

	// 'Place' contains a token 'Token' linked to it
	pattern placeWithToken(Place, Token) =
	{
		'PetriNet'.'Place'(Place);
		'PetriNet'.'Place'.'Token'(Token) in Place;
		'PetriNet'.'Place'.'tokens'(X, Place, Token);
	}
	
	pattern token(Token) =
	{
		'PetriNet'.'Place'.'Token'(Token); 
	}
	
	pattern placeWithToken2(Place) =
	{
		'PetriNet'.'Place'(Place);
		'PetriNet'.'Place'.'Token'(Token) in Place;
		'PetriNet'.'Place'.'tokens'(X, Place, Token);
	}
	
	
	asmfunction counter/1;



	rule generatePlaceRestriction(in PN) = 
	let Temp = undef in seq
	{
	forall Place below PN with find petriPlace(PN,Place) do 
		let NewPlace = undef, NewToken = undef in
		seq
		{
			update counter("Places") = counter("Places")+1;
			new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
			new('PetriNet'.'places'(Temp, PN, NewPlace));
			
			update counter("Token") = counter("Token") + 1;
			new('PetriNet'.'Place'.'Token'(NewToken) in Place); rename(NewToken,"Tk"+counter("Token"));
			new('PetriNet'.'Place'.'tokens'(Temp,NewPlace,NewToken));
			
		forall Transition below PN, OutArc below PN with find sourcePlace(Transition, Place, OutArc) do seq
			{
				new('PetriNet'.'Transition'.'InArc'(Temp,Transition,NewPlace));
			}
		
		forall Transition below PN, InArc below PN with find targetPlace(Transition, Place, InArc) do seq
			{
				new('PetriNet'.'Place'.'OutArc'(Temp,NewPlace,Transition));
			}
	//	move(NewPlace,Place);
		}
	}



	rule inverseSelfPlaceLoop_rule(in Transition, in PN) = 
		let NewPlace = undef, NewOutArc= undef, NewInArc= undef,
		 	Temp = undef, NewToken = undef in
				seq{
				update counter("Places") = counter("Places")+1;
				new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
				new('PetriNet'.'Transition'.'InArc'(NewInArc,Transition,NewPlace));
				new('PetriNet'.'Place'.'OutArc'(NewOutArc,NewPlace,Transition));
				new('PetriNet'.'places'(Temp, PN, NewPlace));
				
				update counter("Token") = counter("Token") + 1;
				new('PetriNet'.'Place'.'Token'(NewToken) in NewPlace); rename(NewToken,"Tk"+counter("Token"));
				new('PetriNet'.'Place'.'tokens'(Temp,NewPlace,NewToken));
				}
	

	gtrule inverseSelfPlaceLoop(out Transition, in PN) = {
	precondition find petriTransition(PN, Transition)
	
	action{
		let NewPlace = undef, NewOutArc= undef, NewInArc= undef,
		 Temp = undef, NewToken = undef in
		seq{
			update counter("Places") = counter("Places")+1;
			new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,Transition,NewPlace));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,NewPlace,Transition));
			new('PetriNet'.'places'(Temp, PN, NewPlace));
			
			update counter("Token") = counter("Token") + 1;
			new('PetriNet'.'Place'.'Token'(NewToken) in NewPlace); rename(NewToken,"Tk"+counter("Token"));
			new('PetriNet'.'Place'.'tokens'(Temp,NewPlace,NewToken));
			}
		}
	}
	
	rule inverseSelfTransitionLoop_rule(in Place, in PN) = 
	let NewTransition = undef, NewOutArc= undef, NewInArc= undef,
		 Temp = undef in
		seq{
			update counter("Transitions") = counter("Transitions")+1;
			new('PetriNet'.'Transition'(NewTransition) in PN); rename(NewTransition,"T"+counter("Transitions"));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,Place,NewTransition));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,NewTransition,Place));
			new('PetriNet'.'transitions'(Temp, PN, NewTransition));
			}
		
	
	gtrule inverseSelfTransitionLoop(out Place, in PN) = {
	precondition find petriPlace(PN, Place)
	
	action{
		let NewTransition = undef, NewOutArc= undef, NewInArc= undef,
		 Temp = undef in
		seq{
			update counter("Transitions") = counter("Transitions")+1;
			new('PetriNet'.'Transition'(NewTransition) in PN); rename(NewTransition,"T"+counter("Transitions"));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,Place,NewTransition));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,NewTransition,Place));
			new('PetriNet'.'transitions'(Temp, PN, NewTransition));
			}
		}
	}
	
	rule inverseParallelTransitionRedaction_rule(in Place, in PN, in NextPlace) = 
		let NewTransition = undef, NewOutArc= undef, NewInArc= undef, X1 = undef in
		seq{
			update counter("Transitions") = counter("Transitions")+1;
			new('PetriNet'.'Transition'(NewTransition) in PN); rename(NewTransition,"T"+counter("Transitions"));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,Place,NewTransition));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,NewTransition,NextPlace));
			new('PetriNet'.'transitions'(X1, PN, NewTransition));
			}
		
	pattern getPlace(Place, NextPlace, PN) = {
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X1, PN, Transition);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X2, PN, Place);
		'PetriNet'.'Place'(NextPlace);
		'PetriNet'.'places'(X3, PN, NextPlace);
		'PetriNet'.'Place'.'OutArc'(OutArc, Place, Transition);
		'PetriNet'.'Transition'.'InArc'(InArc, Transition, NextPlace);
	}

	gtrule inverseParallelTransitionRedaction(out Place) = {
	precondition pattern getPlace(Place, NextPlace, PN) = {
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X1, PN, Transition);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X2, PN, Place);
		'PetriNet'.'Place'(NextPlace);
		'PetriNet'.'places'(X3, PN, NextPlace);
		'PetriNet'.'Place'.'OutArc'(OutArc, Place, Transition);
		'PetriNet'.'Transition'.'InArc'(InArc, Transition, NextPlace);
	}
	
	action{
		let NewTransition = undef, NewOutArc= undef, NewInArc= undef, X1 = undef in
		seq{
			update counter("Transitions") = counter("Transitions")+1;
			new('PetriNet'.'Transition'(NewTransition) in PN); rename(NewTransition,"T"+counter("Transitions"));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,Place,NewTransition));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,NewTransition,NextPlace));
			new('PetriNet'.'transitions'(X1, PN, NewTransition));
			}
		}
	}
	
	rule inverseParallelPlaceRedaction_rule(in Transition, in PN, in NextTransition) = 
		let NewPlace = undef, NewOutArc= undef, NewInArc= undef, X1 = undef in
		seq{
			update counter("Places") = counter("Places")+1;
			new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,Transition,NewPlace));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,NewPlace,NextTransition));
			new('PetriNet'.'places'(X1, PN, NewPlace));
			}
	
	@Random
	pattern getTransition(Transition, NextTransition, PN) = {
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X1, PN, Transition);
		'PetriNet'.'Transition'(NextTransition);
		'PetriNet'.'transitions'(X2, PN, NextTransition);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X3, PN, Place);
		'PetriNet'.'Transition'.'InArc'(InArc, Transition, Place);
		'PetriNet'.'Place'.'OutArc'(OutArc, Place, NextTransition);
	}
	
	gtrule inverseParallelPlaceRedaction(out Transition) = {
	
	precondition pattern getTransition(Transition, NextTransition, PN) = {
		'PetriNet'(PN);
		'PetriNet'.'Transition'(Transition);
		'PetriNet'.'transitions'(X1, PN, Transition);
		'PetriNet'.'Transition'(NextTransition);
		'PetriNet'.'transitions'(X2, PN, NextTransition);
		'PetriNet'.'Place'(Place);
		'PetriNet'.'places'(X3, PN, Place);
		'PetriNet'.'Transition'.'InArc'(InArc, Transition, Place);
		'PetriNet'.'Place'.'OutArc'(OutArc, Place, NextTransition);
	}
	
	action{
		let NewPlace = undef, NewOutArc= undef, NewInArc= undef, X1 = undef in
		seq{
			update counter("Places") = counter("Places")+1;
			new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
			new('PetriNet'.'Transition'.'InArc'(NewInArc,Transition,NewPlace));
			new('PetriNet'.'Place'.'OutArc'(NewOutArc,NewPlace,NextTransition));
			new('PetriNet'.'places'(X1, PN, NewPlace));
			}
		}
	}
	
	gtrule addToken(out Place, in PN) = {
		precondition find petriPlace(PN,Place)
		action {call addToken_Rule(Place);}
	}
	rule addToken_Rule(in Place) = 
		let NewToken = undef, Temp = undef in seq{
			update counter("Token") = counter("Token") + 1;
			new('PetriNet'.'Place'.'Token'(NewToken) in Place); rename(NewToken,"Tk"+counter("Token"));
			new('PetriNet'.'Place'.'tokens'(Temp,Place,NewToken));
		}
	
rule inverseSerialPlaceRedaction(in Place, in PN) = 
		let NewPlace = undef, NewTransition = undef,
		Temp = undef in seq
		{update counter("InArcs") = 0;
		 update counter("OutArcs") = 0;
		
		update counter("Places") = counter("Places")+1;
		new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
		new('PetriNet'.'places'(Temp,PN,NewPlace));
		 
		//sets all target ARCs to the newNode 
		forall Tr, OutArc with find sourcePlace(Tr, Place, OutArc) do seq{
		//	  println("1_invSerialPlace: "+fqn(OutArc)+" setTo "+fqn(NewPlace)); 
		  	  setFrom(OutArc,NewPlace);
		 } 
		//sets all odd source ARCs to the new Place
		forall Tr, InArc with find targetPlace(Tr, Place, InArc) do seq{
		  update counter("InArcs") = counter("InArcs")+1;
		  if(toInteger(counter("InArcs")) % 2 == 0 ) 
		  	 seq{ setTo(InArc,NewPlace); 
		//  	 	  println("2_invSerialPlace: "+fqn(InArc)+" setTo "+fqn(NewPlace));
		  	 	}
		 }
		
		//creates the additional transition 
		update counter("Transitions") = counter("Transitions")+1;
		new('PetriNet'.'Transition'(NewTransition) in PN); rename(NewTransition,"T"+counter("Transitions"));	
		new('PetriNet'.'transitions'(Temp, PN, NewTransition));
	 
		new('PetriNet'.'Place'.'OutArc'(Temp,Place,NewTransition));
		new('PetriNet'.'Transition'.'InArc'(Temp,NewTransition,NewPlace)); 
		}

rule inverseSerialTransitionRedaction(in Transition, in PN) = 
	let NewPlace = undef, NewTransition = undef,
	Temp = undef in seq
	{update counter("InArcs") = 0;
	 
	update counter("Transitions") = counter("Transitions")+1;
	new('PetriNet'.'Transition'(NewTransition) in PN); rename(NewTransition,"T"+counter("Transitions"));
	new('PetriNet'.'transitions'(Temp,PN,NewTransition));
	 
	forall Place, InArc with find targetPlace(Transition, Place, InArc) do seq{
	  update counter("InArcs") = counter("InArcs")+1;
	  if( toInteger(counter("InArcs")) % 2 == 1 ) 
	  	 seq{ setFrom(InArc,NewTransition); 
	  	// 	  println("2_invSerialTrans: "+fqn(InArc)+" setFrom "+fqn(NewTransition));
	  	 	}
	 }
	
	//creates the additional transition 
	update counter("Places") = counter("Places")+1;
	new('PetriNet'.'Place'(NewPlace) in PN); rename(NewPlace,"P"+counter("Places"));
	new('PetriNet'.'places'(Temp, PN, NewPlace));
 
	new('PetriNet'.'Transition'.'InArc'(Temp,Transition,NewPlace));
	new('PetriNet'.'Place'.'OutArc'(Temp,NewPlace,NewTransition)); 
	}
 
//Its input parameter is the root container of the newly generated Petri-net 
rule main(in Where, in Iterations) = 
	let PN = undef, P1= undef, P2 = undef, T1 = undef, T2= undef,
	Temp = undef , Tk1= undef, Tk2 = undef in
	seq
	{	//creates the 2 place 2 transition petri net
		//places h
		
		new('PetriNet'(PN) in ref(Where)); 
		
		new('PetriNet'.'Place'(P1) in PN); rename(P1,"P1");
		new('PetriNet'.'Place'(P2) in PN); rename(P2,"P2");
		new('PetriNet'.'places'(Temp,PN,P1));
		new('PetriNet'.'places'(Temp,PN,P2));
		//transition
		new('PetriNet'.'Transition'(T1) in P1); rename(T1,"T1");
		new('PetriNet'.'transitions'(Temp, PN, T1));
		new('PetriNet'.'Transition'(T2) in P2); rename(T2,"T2");
		new('PetriNet'.'transitions'(Temp, PN, T2));
		
		//Arcs
		new('PetriNet'.'Place'.'OutArc'(Temp,P1,T1));
		new('PetriNet'.'Transition'.'InArc'(Temp,T1,P2));
		
		new('PetriNet'.'Place'.'OutArc'(Temp,P2,T2));
		new('PetriNet'.'Transition'.'InArc'(Temp,T2,P1));
		
		//tokens
		new('PetriNet'.'Place'.'Token'(Tk1) in P1); rename(Tk1,"Tk1");
		new('PetriNet'.'Place'.'tokens'(Temp,P1,Tk1));
		
		new('PetriNet'.'Place'.'Token'(Tk2) in P2); rename(Tk2,"Tk2");
		new('PetriNet'.'Place'.'tokens'(Temp,P2,Tk2));

	//initializes the counters	
	update counter("ParPlace") = 0;
	update counter("ParTrans") = 0;
	update counter("SerPlace") = 0;
	update counter("SerTrans") = 0;
	update counter("LoopPlace") = 0;
	update counter("LoopTrans") = 0;
	update counter("Random") = 0;
	update counter("Token") = 2;
	update counter("Places") = 2;
	update counter("Transitions") = 2; 

	//random  generation   
	//name of the PetriNet itself
	rename(PN,"Sparse_"+Iterations);	
	iterate let Iter = toInteger(Iterations) in seq
		{
			update counter("Random") = counter("Random") + 1;
			if (counter("Random") > Iter) fail; //****The number of iteration 
		 	random
		 	{
		 		choose Place below PN, NextPlace below PN with find getPlace(Place, NextPlace, PN)
		 		 do call inverseParallelTransitionRedaction_rule(Place,PN,NextPlace);
		 		choose P below PN with find petriPlace(PN,P) do call inverseSerialPlaceRedaction(P, PN);

		 		choose NextTransition below PN, Transition below PN with find getTransition(Transition, NextTransition, PN)
		 	 	 do call inverseParallelPlaceRedaction_rule(Transition,PN, NextTransition);
		 		choose T below PN with find petriTransition(PN,T) do call inverseSerialTransitionRedaction(T, PN);
		 		choose P below PN with find petriPlace(PN,P) do call inverseSelfTransitionLoop_rule(P,PN);
			}
		}
	//Token	
	iterate seq 
		{
			if (counter("Token") > 8) fail; //The number of Tokens generated into the Petri-net
			 
			choose  P with find petriPlace(PN, P) do seq { call addToken_Rule(P); println("Token added to: "+ fqn(P)); }
		}
	
	//to generate the extra places for the capacity constraint
	//call generatePlaceRestriction(PN); 
	
	//Counts the size of the generated Petri-net 
	//update counter("Tokens") = 0;	  
	//forall Tok below PN with find token(Tok) do update counter("Tokens") = counter("Tokens")+1;	
		 
	//forall P below PN with find petriPlace(PN,P) do update counter("Places") = counter("Places")+1;
		 	
	//forall T below PN with find petriTransition(PN,T) do update counter("Transitions") = counter("Transitions")+1;
	 	 
	println("\nNumber of iterations: "+(counter("Random")-1)); 	
	println("*** The generated Petri net contains "+ counter("Places")+" places and "+ counter("Transitions")+" Transitions and " +counter("Token")+" Tokens");	
	} 	
}