import datatypes;
import DSM.coremetamodel.Editor;
import DSM.metamodel.PetriNet.PetriNetEditor.PetriNet;

@incremental
machine petriNetSMorMG{
	
	asmfunction temp/1; 
	asmfunction model/0; 
	asmfunction violations/0; 
	
	/**
	* SMorMG: "SM" for state machine, "MG" for marked graph
	*/
	rule main(in PetriNetModel, in SMorMG) = seq{
		
		println("Petri Net Corruption Sequence Starting...");
		if(PetriNetModel != undef && find petriNetModel(ref(PetriNetModel))) seq{
			println(" >> Target: " + PetriNetModel);
			update model() = ref(PetriNetModel);
		} else seq{
			println("Model not found or not a PetriNet");
			fail;
		}
		
		if(SMorMG != undef && SMorMG == "SM") let Rt = undef, C = 0 in seq{
			println(" >> Transforming PN to SM");
			
			iterate choose T in model() with find stateMachineViolatingTransition(T) do seq{
				if(C > 100) fail;
				update C = C + 1;
				if (find MoreThanOneOutPlace(T)) seq{
					println(" >>> MoreThanOneOutPlace");
					try choose P in model(),R  with find connectedNodesRel(T,P,R) do seq{
						println(" >>>> delete " + R);
						delete(R);
					}
				} else if (find MoreThanOneInPlace(T)) seq{
					println(" >> MoreThanOneInPlace");
					try choose P in model(),R with find connectedNodesRel(P,T,R) do seq{
						println(" >>>> delete " + R);
						delete(R);
					}
				} else if (find LessThanOneOutPlace(T)) seq{
					println(" >> LessThanOneOutPlace");
					try choose P in model() with find notConnectedNodes(T,P) do seq{
						if(find place(P)) seq{
							new(Transition.InArc(Rt,T,P));
							println(" >>>> create " + Rt);
						}
					}
				} else if (find LessThanOneInPlace(T)) seq{
					println(" >> LessThanOneInPlace");
					try choose P in model() with find notConnectedNodes(P,T) do seq{
						if(find place(P)) seq{
							new(Place.OutArc(Rt,P,T));
							println(" >>>> create " + Rt);
						}
					}
				}
			}
		
		} else if(SMorMG != undef && SMorMG == "MG") let Rt = undef, C = 0 in seq{
			println(" >> Transforming PN to MG");
			iterate choose P in model() with find markedGraphViolatingPlace(P) do seq{
				if(C > 100) fail;
				update C = C + 1;
				if (find MoreThanOneOutTransition(P)) seq{
					println(" >> MoreThanOneOutTransition");
					try choose T in model(),R with find connectedNodesRel(P,T,R) do  seq{
						println(" >>>> delete " + R);
						delete(R);
					}
				} else if (find MoreThanOneInTransition(P)) seq{
					println(" >> MoreThanOneInTransition");
					try choose T in model(),R with find connectedNodesRel(T,P,R) do  seq{
						println(" >>>> delete " + R);
						delete(R);
					}
				} else if (find LessThanOneOutTransition(P)) seq{
					println(" >> LessThanOneOutTransition");
					try choose T in model() with find notConnectedNodes(P,T) do  seq{
						if(find transition(T)) seq{
							new(Place.OutArc(Rt,P,T));
							println(" >>>> create " + Rt);
						}
					}
				} else if (find LessThanOneInTransition(P)) seq{
					println(" >> LessThanOneInTransition");
					try choose T in model() with find notConnectedNodes(T,P) do seq{
						if(find transition(T)) seq{
							new(Transition.InArc(Rt,T,P));
							println(" >>>> create " + Rt);
						}
					}
				}
			}
		}
	}
	
	pattern petriNetModel(Model) = {
		DSM.metamodel.PetriNet.PetriNetEditor.PetriNet(Model);
	}
	
	@Random pattern place(P) = {Place(P);}
	@Random pattern transition(T) = {Transition(T);}
	
	@Random
	pattern notConnectedToPlace(T,P) = {
		Place(P);
		Transition(T);
		find notConnectedNodes(T,P);
		
	}
	
	@Random
	pattern notConnectedToTrans(P,T) = {
		Place(P);
		Transition(T);
		find notConnectedNodes(P,T);
		
	}
	
	@Random
	pattern notConnectedNodes(N1, N2) = {
		Node(N1);
		Node(N2);
		neg pattern arcbetween(N1,N2) = {
			Node(N1);
			Node(N2);
			Node.Edge(Arc,N1,N2);
		}
	}
	
	@Random
	pattern connectedNodes(N1, N2) = {
		Node(N1);
		Node(N2);
		Node.Edge(Arc,N1,N2);
	}
	
	@Random
	pattern connectedNodesRel(N1, N2, Arc) = {
		Node(N1);
		Node(N2);
		Node.Edge(Arc,N1,N2);
	}
	
	@Random
	pattern notConnectedSameTypeNodes(N1,N2) = {
		Node(N1);
		Node(N2);
		find notConnectedNodes(N1,N2);
		find sameType(N1,N2);	
	} 
	
	
	pattern selfArc(Arc) = {
		Node(N);
		Node.Edge(Arc,N,N);
	}
	
	pattern invalidArc(Arc) = {
		Node(N1);
		Node(N2);
		Node.Edge(Arc,N1,N2);
		
		find sameType(N1,N2);
	}
	
	pattern sameType(N1,N2) = {	
		Place(N1);
		Place(N2);
	} or {
		Transition(N1);
		Transition(N2);
	}

	pattern lonelyToken(Token) = {
		Place.Token(Token);
		
		neg pattern place(Token,P) = {
			Place.Token(Token);
			Place(P);
			Place.tokens(R,P,Token); }
	}
	
	pattern lonelyPlace(Place) = {
		Place(Place);
		
		neg pattern toTransition(Place,Transition) = {
			Place(Place);
			Transition(Transition);
			Node.Edge(R,Place,Transition); }
		neg pattern fromTransition(Place,Transition) = {
			Place(Place);
			Transition(Transition);
			Node.Edge(R,Transition,Place); }
	}
	
	pattern lonelyTransition(Transition) = {
		Transition(Transition);
		
		neg pattern fromPlace(Place,Transition) = {
			Place(Place);
			Transition(Transition);
			Node.Edge(R,Place,Transition); }
		neg pattern toPlace(Place,Transition) = {
			Place(Place);
			Transition(Transition);
			Node.Edge(R,Transition,Place); }
	}
	
	pattern stateMachineViolatingTransition(T) = {
		Transition(T);
		find MoreThanOneOutPlace(T);
	} or {
		Transition(T);
		find MoreThanOneInPlace(T);
	} or {
		Transition(T);
		find LessThanOneInPlace(T);
	} or {
		Transition(T);
		find LessThanOneOutPlace(T);
	}
	
	pattern MoreThanOneOutPlace(T) = {
		Place(P1);
		Place(P2);
		Transition(T);
		Transition.InArc(R1,T,P1);
		Transition.InArc(R2,T,P2);
	}
	
	pattern MoreThanOneInPlace(T) = {
		Place(P1);
		Place(P2);
		Transition(T);
		Place.OutArc(R1,P1,T);
		Place.OutArc(R2,P2,T);
	}
	
	pattern LessThanOneOutPlace(T) = {
		Transition(T);
		neg pattern noOutPlace(T) = {
			Transition(T);
			Place(P1);
			Transition.InArc(R1,T,P1);
		}
	}
	
	pattern LessThanOneInPlace(T) = {
		Transition(T);
		neg pattern noInPlace(T) = {
			Transition(T);
			Place(P1);
			Place.OutArc(R1,P1,T);
		}
	}
	
	pattern markedGraphViolatingPlace(P) = {
		Place(P);
		find MoreThanOneInTransition(P);
	} or {
		Place(P);
		find MoreThanOneOutTransition(P);
	} or {
		Place(P);
		find LessThanOneInTransition(P);
	} or {
		Place(P);
		find LessThanOneOutTransition(P);
	}
	
	pattern MoreThanOneInTransition(P) = {
		Transition(T1);
		Transition(T2);
		Place(P);
		Transition.InArc(R1,T1,P);
		Transition.InArc(R2,T2,P);
	}
		
	pattern MoreThanOneOutTransition(P) = {
		Transition(T1);
		Transition(T2);
		Place(P);
		Place.OutArc(R1,P,T1);
		Place.OutArc(R2,P,T2);
	}
	
	pattern LessThanOneInTransition(P) = {
		Place(P);
		neg pattern noInTransition(P) = {
			Transition(T);
			Place(P);
			Transition.InArc(R,T,P);
		}
	}
	
	pattern LessThanOneOutTransition(P) = {
		Place(P);
		neg pattern noOutTransition(P) = {
			Transition(T);
			Place(P);
			Place.OutArc(R,P,T);
		}
	}
	
	//@goal
	//pattern freeChoiceViolatingPlace(Place)
	
	//@goal
	//pattern assimetricChoiceViolatingPlaces(Place1, Place2)
	
}