package hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu

import epackage "hu.bme.mit.inf.yakindumm"

/////////
// Entry
/////////

pattern entryInRegion(r1 : Region, e1 : Entry) {
	Region.vertices(r1, e1);
}

@Constraint(severity="error", message="error", key = {r1})
pattern noEntryInRegion(r1 : Region) {
	neg find entryInRegion(r1, _);
}

@Constraint(severity="error", message="error", key = {r})
pattern multipleEntryInRegion(r : Region) {
	find entryInRegion(r, e1);
	find entryInRegion(r, e2);
	e1 != e2;
}

@Constraint(severity="error", message="error", key = {sct})
pattern unsat_multipleEntryInRegion(sct : Statechart) {
	Statechart(sct);
	neg find multipleEntryInRegion(_);
}

pattern transition(t : Transition, src : Vertex, trg : Vertex) {
	Transition.source(t, src);
	Transition.target(t, trg);
}

pattern transitionFrom(t : Transition, src : Vertex) {
	Transition.source(t, src);
}

pattern transitionTo(t : Transition, trg : Vertex) {
	Transition.target(t, trg);
}

@Constraint(severity="error", message="error", key = {e})
pattern incomingToEntry(t : Transition, e : Entry) {
	find transitionTo(t, e);
}

@Constraint(severity="error", message="error", key = {e})
pattern noOutgoingTransitionFromEntry(e : Entry) {
	neg find transitionFrom(_, e);
}

@Constraint(severity="error", message="error", key = {e})
pattern multipleTransitionFromEntry(e : Entry, t1 : Transition, t2: Transition) {
	Entry.outgoingTransitions(e,t1);
	Entry.outgoingTransitions(e,t2);
	t1!=t2;
}

/////////
// Exit
/////////

@Constraint(severity="error", message="error", key = {e})
pattern outgoingFromExit(t : Transition, e : Exit) {
	Exit.outgoingTransitions(e,t);
}

/////////
// Final
/////////

@Constraint(severity="error", message="error", key = {f})
pattern outgoingFromFinal(t : Transition, f : FinalState) {
	FinalState.outgoingTransitions(f,t);
}

/////////
// State vs Region
/////////

@Constraint(severity="error", message="error", key = {region})
pattern noStateInRegion(region: Region) {
	neg find StateInRegion(region,_);
}
pattern StateInRegion(region: Region, state: State) {
	Region.vertices(region,state);
}

/////////
// Choice
/////////

@Constraint(severity="error", message="error", key = {c})
pattern choiceHasNoOutgoing(c : Choice) {
	neg find transitionFrom(_, c);
}

@Constraint(severity="error", message="error", key = {c})
pattern choiceHasNoIncoming(c: Choice) {
	neg find transitionTo(_, c);
}

/////////
// Synchronization
/////////

@Constraint(severity="error", message="error", key = {s})
pattern synchHasNoOutgoing(s : Synchronization) {
	neg find transitionFrom(_, s);
}

@Constraint(severity="error", message="error", key = {s})
pattern synchHasNoIncoming(s : Synchronization) {
	neg find transitionTo(_, s);
}

@Constraint(severity="error", message="error", key = {s})
pattern SynchronizedIncomingInSameRegion(s : Synchronization, t1 : Transition, t2 : Transition) {
	find SynchronizedIncomingInSameRegionHelper1(r, s, t1);
	find SynchronizedIncomingInSameRegionHelper1(r, s, t2);
	t1!=t2;
} or {
	find SynchronizedIncomingInSameRegionHelper2(r, s, t1);
	find SynchronizedIncomingInSameRegionHelper2(r, s, t2);
	t1!=t2;
}

pattern SynchronizedIncomingInSameRegionHelper1(r : Region, s : Synchronization, t1 : Transition) {
	find transition(t1, v1, s);
	Region.vertices(r, v1);
}

pattern SynchronizedIncomingInSameRegionHelper2(r : Region, s : Synchronization, t1 : Transition) {
	find transition(t1, s, v1);
	Region.vertices(r, v1);
}

@Constraint(severity="error", message="error", key = {s})
pattern notSynchronizingStates(s : Synchronization) {
	neg find hasMultipleOutgoingTrainsition(s);
	neg find hasMultipleIncomingTrainsition(s);
}

pattern hasMultipleOutgoingTrainsition(v : Synchronization) {
	find transition(_, v, trg1);
	find transition(_, v, trg2);
	trg1 != trg2;
}

pattern hasMultipleIncomingTrainsition(v : Synchronization) {
	find transition(_, src1, v);
	find transition(_, src2, v);
	src1 != src2;
}

@Constraint(severity="error", message="error", key = {s})
pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, r1 : CompositeElement, r2 : CompositeElement) {
	find SynchronizedRegionsAreNotSiblingsHelper1(s, r1);
	find SynchronizedRegionsAreNotSiblingsHelper1(s, r2);
	r1 != r2;
} or {
	find SynchronizedRegionsAreNotSiblingsHelper2(s, r1);
	find SynchronizedRegionsAreNotSiblingsHelper2(s, r2);
	r1 != r2;
}

pattern SynchronizedRegionsAreNotSiblingsHelper1(s : Synchronization, r1 : CompositeElement) {
	find transition(_, s, v1);
	CompositeElement.regions.vertices(r1, v1);
}

pattern SynchronizedRegionsAreNotSiblingsHelper2(s : Synchronization, r1 : CompositeElement) {
	find transition(_, v1, s);
	CompositeElement.regions.vertices(r1, v1);
}

///////////////////////////////
// Extra
//
//@Constraint(severity="error", message="error", key = {s})
//pattern SynchronizedRegionDoesNotHaveParent(s : Synchronization, v : Vertex) {
//	find transition(_, v, s);
//	neg find child(_,v);
//} or {
//	find transition(_, s, v);
//	neg find child(_,v);
//}

pattern child(parent: CompositeElement, child: Vertex) {
	CompositeElement.regions.vertices(parent, child);
}

@Constraint(severity="error", message="error", key = {s})
pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Vertex) {
	find transition(_, v, s);
	find child(c,v);
	neg find hasMultipleRegions(c);
} or {
	find transition(_, s, v);
	find child(c,v);
	neg find hasMultipleRegions(c);
}

//@Constraint(severity="error", message="error", key = {sct})
//pattern unsat_SynchronizedRegionDoesNotHaveMultipleRegions(sct : Statechart) {
//	Statechart(sct);
//	neg find SynchronizedRegionDoesNotHaveMultipleRegions(_, _);
//}

pattern hasMultipleRegions(composite: CompositeElement) {
	CompositeElement.regions(composite,region1);
	CompositeElement.regions(composite,region2);
	region1 != region2;
}

/**
 * Simplifying model generation
 */
@Constraint(severity="error", message="error", key = {s})
pattern synchThree(s: Synchronization) {
	Transition.target(t1,s);
	Transition.target(t2,s);
	Transition.target(t3,s);
	t1!=t2;
	t2!=t3;
	t1!=t3;
} or {
	Transition.source(t1,s);
	Transition.source(t2,s);
	Transition.source(t3,s);
	t1!=t2;
	t2!=t3;
	t1!=t3;
}

/**
 * Simplifying model generation
 */
@Constraint(severity="error", message="error", key = {s1,s2})
pattern twoSynch(s1 : Synchronization, s2 : Synchronization) {
	Synchronization(s1);
	Synchronization(s2);
	s1 != s2;
}

/**
 * Model generation task: at least one synch
 */
//@Constraint(severity="error", message="error", key = {s})
//pattern noSynch(s:Statechart) {
//	Statechart(s);
//	neg find synch(_);
//}
//pattern synch(s:Synchronization) {
//	Synchronization(s);
//}