Skip to content

Evaluating Well Formedness Constraints on Partial Models

Jump to bottom
Oszkár Semeráth edited this page Sep 29, 2016 · 12 revisions

This page is dedicated to present the results of the paper "Evaluating Well-Formedness Constraints on Partial Models".

Under construction

We illustrated our approach on a partial metamodel of Yakindu statechart modeling tool developed by Itemis. The partial metamodel we used is illustrated below:

The previous metamodel is extended with an additional annotations in oreder to represent partial models. The metamodel for partial modeling is visible below:

This partial model representation has three important characteristics:

  • Reference elements represents the objects of the partial model. Our technique incorporates objects only if they are referred by the partial model with this reference. Thus it is easy to temporarily exclude elements from an existing model to create experimental variations of the model without modifying it.
  • A partial model contains additional symbolic (newly created) elements along the newElements reference. A new element in a may-match represents a new object that needs to be created (in a proper context) in order to satisfy the condition of the match. Typically, a partial model contains a new element for each concrete (non-abstract) object of the metamodel. However, the analysis can be restricted by removing objects, thus forbidding the creation of this kind of object.
  • The semantic interpretation of the partial model can be changed between open-world and close-world by setting sa boolean attribute openWorld.

We generated both a may- and a must-approximation from the graph pattern of the designated constraint, and we evaluated those patterns on sample prototypical instance models. The correctness of the generation was established by manually inspecting the retrieved result set of the may and must patterns.

The construction of the over- and under-approximated patterns is separated into two layers: (1) first a uncertain property indexer collects the possible variations of model properties (like objects and references), and (2) an uncertain pattern layer that combines those uncertain properties into over- and under-approximated patterns. This section presents the uncertain property indexer.

Base Type Indexers

First, base indexing patterns are generated to collect the basic properties of an instance model (types, references and equivalence) with must and may modalities.

Generated type indexers

// Must type indexers
pattern mustType_Pseudostate(p,e) {
	Pseudostate(e); PartialModel.elements(p,e);
}
pattern mustType_Vertex(p,e) {
	Vertex(e); PartialModel.elements(p,e);
}
pattern mustType_Region(p,e) {
	Region(e); PartialModel.elements(p,e);
}
pattern mustType_Transition(p,e) {
	Transition(e); PartialModel.elements(p,e);
}
pattern mustType_Statechart(p,e) {
	Statechart(e); PartialModel.elements(p,e);
}
pattern mustType_Entry(p,e) {
	Entry(e); PartialModel.elements(p,e);
}
pattern mustType_Synchronization(p,e) {
	Synchronization(e); PartialModel.elements(p,e);
}
pattern mustType_State(p,e) {
	State(e); PartialModel.elements(p,e);
}
pattern mustType_RegularState(p,e) {
	RegularState(e); PartialModel.elements(p,e);
}
pattern mustType_CompositeElement(p,e) {
	CompositeElement(e); PartialModel.elements(p,e);
}

// May type indexers
pattern mayType_Pseudostate(p,e) {
	Pseudostate(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Pseudostate(p,e);
}
pattern mayType_Vertex(p,e) {
	Vertex(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Vertex(p,e);
}
pattern mayType_Region(p,e) {
	Region(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Region(p,e);
}
pattern mayType_Transition(p,e) {
	Transition(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Transition(p,e);
}
pattern mayType_Statechart(p,e) {
	Statechart(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Statechart(p,e);
}
pattern mayType_Entry(p,e) {
	Entry(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Entry(p,e);
}
pattern mayType_Synchronization(p,e) {
	Synchronization(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_Synchronization(p,e);
}
pattern mayType_State(p,e) {
	State(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_State(p,e);
}
pattern mayType_RegularState(p,e) {
	RegularState(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_RegularState(p,e);
}
pattern mayType_CompositeElement(p,e) {
	CompositeElement(e); PartialModel.newElements(p,e); PartialModel.openWorld(p,true);
} or { 
	find mustType_CompositeElement(p,e);
}

Generated Reference Indexers

// Must reference indexers
pattern mustReference_incomingTransitions(p, s, t) {
	PartialModel.elements(p, s); PartialModel.elements(p, t); Vertex.incomingTransitions(s, t);
}
pattern mustReference_outgoingTransitions(p, s, t) {
	PartialModel.elements(p, s); PartialModel.elements(p, t); Vertex.outgoingTransitions(s, t);
}
pattern mustReference_vertices(p, s, t) {
	PartialModel.elements(p, s); PartialModel.elements(p, t); Region.vertices(s, t);
}
pattern mustReference_target(p, s, t) {
	PartialModel.elements(p, s); PartialModel.elements(p, t); Transition.target(s, t);
}
pattern mustReference_source(p, s, t) {
	PartialModel.elements(p, s); PartialModel.elements(p, t); Transition.source(s, t);
}
pattern mustReference_regions(p, s, t) {
	PartialModel.elements(p, s); PartialModel.elements(p, t); CompositeElement.regions(s, t);
}

// May reference indexers
pattern mayReference_incomingTransitions(p, s, t) {
	// If the model is openworld, any two object with the correct types can be connected with the reference
	PartialModel.openWorld(p,true);find mayType_Vertex(p,s);
	find mayType_Transition(p,t);
	// There are "numberOfExistingReferences" currently existing instances of the reference to the target,
	// the upper bound of the opposite reference multiplicity should be considered.
	numberOfExistingOppositeReferences == count find mustReference_incomingTransitions(p, _, t);
	check(numberOfExistingOppositeReferences < 1);
} or {
	find mustReference_incomingTransitions(p, s, t);
}
pattern mayReference_outgoingTransitions(p, s, t) {
	// If the model is openworld, any two object with the correct types can be connected with the reference
	PartialModel.openWorld(p,true);find mayType_Vertex(p,s);
	find mayType_Transition(p,t);
	// There are "numberOfExistingReferences" currently existing instances of the reference to the target,
	// the upper bound of the opposite reference multiplicity should be considered.
	numberOfExistingOppositeReferences == count find mustReference_outgoingTransitions(p, _, t);
	check(numberOfExistingOppositeReferences < 1);
	// The reference is containment, then a new reference cannot be create if:
	// 1. Multiple parents
	neg find mustContains3(p,_,t);
	// 2. Circle in the containment hierarchy
	neg find mustTransitiveContains(t,s);
} or {
	find mustReference_outgoingTransitions(p, s, t);
}
pattern mayReference_vertices(p, s, t) {
	// If the model is openworld, any two object with the correct types can be connected with the reference
	PartialModel.openWorld(p,true);find mayType_Region(p,s);
	find mayType_Vertex(p,t);
	// The reference is containment, then a new reference cannot be create if:
	// 1. Multiple parents
	neg find mustContains3(p,_,t);
	// 2. Circle in the containment hierarchy
	neg find mustTransitiveContains(t,s);
} or {
	find mustReference_vertices(p, s, t);
}
pattern mayReference_target(p, s, t) {
	// If the model is openworld, any two object with the correct types can be connected with the reference
	PartialModel.openWorld(p,true);find mayType_Transition(p,s);
	find mayType_Vertex(p,t);
	// There are "numberOfExistingReferences" currently existing instances of the reference from the source,
	// the upper bound of the multiplicity should be considered.
	numberOfExistingReferences == count find mustReference_target(p, s, _);
	check(numberOfExistingReferences < 1);
} or {
	find mustReference_target(p, s, t);
}
pattern mayReference_source(p, s, t) {
	// If the model is openworld, any two object with the correct types can be connected with the reference
	PartialModel.openWorld(p,true);find mayType_Transition(p,s);
	find mayType_Vertex(p,t);
	// There are "numberOfExistingReferences" currently existing instances of the reference from the source,
	// the upper bound of the multiplicity should be considered.
	numberOfExistingReferences == count find mustReference_source(p, s, _);
	check(numberOfExistingReferences < 1);
	// The eOpposite of the reference is containment, then a referebce cannot be created if
	// 1. Multiple parents
	neg find mustContains3(p,s,_);
	// 2. Circle in the containment hierarchy
	neg find mustTransitiveContains(s,t);
} or {
	find mustReference_source(p, s, t);
}
pattern mayReference_regions(p, s, t) {
	// If the model is openworld, any two object with the correct types can be connected with the reference
	PartialModel.openWorld(p,true);find mayType_CompositeElement(p,s);
	find mayType_Region(p,t);
	// The reference is containment, then a new reference cannot be create if:
	// 1. Multiple parents
	neg find mustContains3(p,_,t);
	// 2. Circle in the containment hierarchy
	neg find mustTransitiveContains(t,s);
} or {
	find mustReference_regions(p, s, t);
}

Containment Inxexers

pattern mustContains2(s,t)
{ find mustReference_outgoingTransitions(_,s,t);
}or
{ find mustReference_vertices(_,s,t);
}or
{ find mustReference_regions(_,s,t);
}
pattern mustContains3(p,s,t)
{ find mustReference_outgoingTransitions(p,s,t);
}or
{ find mustReference_vertices(p,s,t);
}or
{ find mustReference_regions(p,s,t);
 }
pattern mustTransitiveContains(s,t) {
	find mustContains2+(s,t);
}

Equivalence Indexers

pattern mustEqual(p,e1,e2) {
	PartialModel.elements(p,e1);
	e1 == e2;
}
pattern mayEqual(p,e1,e2) {
	PartialModel.openWorld(p,true);
	PartialModel.newElements(p,e2);
	e1 == e2;
} or {
	find mustEqual(p,e1,e2);
}

Pattern transformation

Pattern transformation

Original pattern:

pattern entryInRegion(r : Region, e : Entry) {
	Region.vertices(r, e);
}

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.entryInRegion
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,e)
{
	find mustType_Region(pm___,r);
	find mustType_Entry(pm___,e);
	// r is exported
	// e is exported
	find mustType_Region(pm___,r);
	find mustReference_vertices(pm___,r,virtual0);
	find mustEqual(pm___,virtual0,e);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,e)
{
	find mayType_Region(pm___,r);
	find mayType_Entry(pm___,e);
	// r is exported
	// e is exported
	find mayType_Region(pm___,r);
	find mayReference_vertices(pm___,r,virtual0);
	find mayEqual(pm___,virtual0,e);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noEntryInRegion
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion(pm___,r)
{
	find mustType_Region(pm___,r);
	// r is exported
	neg find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,_0);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion(pm___,r)
{
	find mayType_Region(pm___,r);
	// r is exported
	neg find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,_0);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleEntryInRegion
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleEntryInRegion(pm___,r)
{
	// r is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,e1);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,e2);
	neg find mayEqual(pm___,e1,e2);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleEntryInRegion(pm___,r)
{
	// r is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,e1);
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_entryInRegion(pm___,r,e2);
	neg find mustEqual(pm___,e1,e2);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transition
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,src,trg)
{
	// t is exported
	// src is exported
	// trg is exported
	find mustType_Transition(pm___,t);
	find mustReference_source(pm___,t,virtual0);
	find mustEqual(pm___,virtual0,src);
	find mustType_Transition(pm___,t);
	find mustReference_target(pm___,t,virtual1);
	find mustEqual(pm___,virtual1,trg);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,src,trg)
{
	// t is exported
	// src is exported
	// trg is exported
	find mayType_Transition(pm___,t);
	find mayReference_source(pm___,t,virtual0);
	find mayEqual(pm___,virtual0,src);
	find mayType_Transition(pm___,t);
	find mayReference_target(pm___,t,virtual1);
	find mayEqual(pm___,virtual1,trg);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.incomingToEntry
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_incomingToEntry(pm___,t,e)
{
	find mustType_Entry(pm___,e);
	// t is exported
	// e is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,_0,e);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_incomingToEntry(pm___,t,e)
{
	find mayType_Entry(pm___,e);
	// t is exported
	// e is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,_0,e);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noOutgoingTransitionFromEntry
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry(pm___,e)
{
	find mustType_Entry(pm___,e);
	// e is exported
	neg find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,e,_1);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry(pm___,e)
{
	find mayType_Entry(pm___,e);
	// e is exported
	neg find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,e,_1);
}

Original pattern:

@Constraint(severity="error", message="error", key = {e})
pattern multipleTransitionFromEntry(e : Entry, t1, t2) {
	find transition(t1, e, _);
	find transition(t2, e, _);
	t1 != t2;
}

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleTransitionFromEntry
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleTransitionFromEntry(pm___,e,t1,t2)
{
	find mustType_Entry(pm___,e);
	// e is exported
	// t1 is exported
	// t2 is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t1,e,_0);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t2,e,_1);
	neg find mayEqual(pm___,t1,t2);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_multipleTransitionFromEntry(pm___,e,t1,t2)
{
	find mayType_Entry(pm___,e);
	// e is exported
	// t1 is exported
	// t2 is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t1,e,_0);
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t2,e,_1);
	neg find mustEqual(pm___,t1,t2);
}

Original pattern:

@Constraint(severity="error", message="error", key = {e})
pattern outgoingTrainsitionToDifferentRegion(e : Entry, trg) {
	find transition(_, e, trg);
	Region.vertices(r1, e);
	Region.vertices(r2, trg);
	r1 != r2;
}

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.outgoingTrainsitionToDifferentRegion
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_outgoingTrainsitionToDifferentRegion(pm___,e,trg)
{
	find mustType_Entry(pm___,e);
	// e is exported
	// trg is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,e,trg);
	find mustType_Region(pm___,r1);
	find mustReference_vertices(pm___,r1,virtual0);
	find mustEqual(pm___,virtual0,e);
	find mustType_Region(pm___,r2);
	find mustReference_vertices(pm___,r2,virtual1);
	find mustEqual(pm___,virtual1,trg);
	neg find mayEqual(pm___,r1,r2);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_outgoingTrainsitionToDifferentRegion(pm___,e,trg)
{
	find mayType_Entry(pm___,e);
	// e is exported
	// trg is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,e,trg);
	find mayType_Region(pm___,r1);
	find mayReference_vertices(pm___,r1,virtual0);
	find mayEqual(pm___,virtual0,e);
	find mayType_Region(pm___,r2);
	find mayReference_vertices(pm___,r2,virtual1);
	find mayEqual(pm___,virtual1,trg);
	neg find mustEqual(pm___,r1,r2);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasNoIncomingOrOutgoing
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoIncomingOrOutgoing(pm___,s)
{
	find mustType_Synchronization(pm___,s);
	// s is exported
	neg find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,_1,s);
}or{
	find mustType_Synchronization(pm___,s);
	// s is exported
	neg find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,s,_1);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoIncomingOrOutgoing(pm___,s)
{
	find mayType_Synchronization(pm___,s);
	// s is exported
	neg find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,_1,s);
}or{
	find mayType_Synchronization(pm___,s);
	// s is exported
	neg find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,s,_1);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleOutgoingTrainsition
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleOutgoingTrainsition(pm___,v)
{
	// v is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,v,trg1);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_1,v,trg2);
	neg find mayEqual(pm___,trg1,trg2);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleOutgoingTrainsition(pm___,v)
{
	// v is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,v,trg1);
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_1,v,trg2);
	neg find mustEqual(pm___,trg1,trg2);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleIncomingTrainsition
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleIncomingTrainsition(pm___,v)
{
	// v is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,src1,v);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_1,src2,v);
	neg find mayEqual(pm___,src1,src2);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleIncomingTrainsition(pm___,v)
{
	// v is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_0,src1,v);
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,_1,src2,v);
	neg find mustEqual(pm___,src1,src2);
}

Original pattern:

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

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.notSynchronizingStates
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_notSynchronizingStates(pm___,s)
{
	find mustType_Synchronization(pm___,s);
	// s is exported
	neg find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleOutgoingTrainsition(pm___,s);
	neg find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleIncomingTrainsition(pm___,s);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_notSynchronizingStates(pm___,s)
{
	find mayType_Synchronization(pm___,s);
	// s is exported
	neg find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleOutgoingTrainsition(pm___,s);
	neg find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasMultipleIncomingTrainsition(pm___,s);
}

Original patter:

@Constraint(severity="error", message="error", key = {s})
pattern SynchronizedVerticesInSameRegion(s : Synchronization, v1, v2) {
	find transition(t, v1, s);
	find transition(t, v2, s);
	Region.vertices(r, v1);
	Region.vertices(r, v2);
} or {
	find transition(t, s, v1);
	find transition(t, s, v2);
	Region.vertices(r, v1);
	Region.vertices(r, v2);
}

Approximated patterns

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedVerticesInSameRegion
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedVerticesInSameRegion(pm___,s,v1,v2)
{
	find mustType_Synchronization(pm___,s);
	// s is exported
	// v1 is exported
	// v2 is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,v1,s);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,v2,s);
	find mustType_Region(pm___,r);
	find mustReference_vertices(pm___,r,virtual0);
	find mustEqual(pm___,virtual0,v1);
	find mustType_Region(pm___,r);
	find mustReference_vertices(pm___,r,virtual1);
	find mustEqual(pm___,virtual1,v2);
}or{
	find mustType_Synchronization(pm___,s);
	// s is exported
	// v1 is exported
	// v2 is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,s,v1);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,s,v2);
	find mustType_Region(pm___,r);
	find mustReference_vertices(pm___,r,virtual0);
	find mustEqual(pm___,virtual0,v1);
	find mustType_Region(pm___,r);
	find mustReference_vertices(pm___,r,virtual1);
	find mustEqual(pm___,virtual1,v2);
}

Original pattern:

@Constraint(severity="error", message="error", key = {s})
pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1, v2) {
	find transition(t, v1, s);
	find transition(t, v2, s);
	CompositeElement.regions.vertices(r1, v1);
	CompositeElement.regions.vertices(r2, v2);
	r1 != r2;
} or {
	find transition(t, s, v1);
	find transition(t, s, v2);
	CompositeElement.regions.vertices(r1, v1);
	CompositeElement.regions.vertices(r2, v2);
	r1 != r2;
}

Approximated pattern:

// Must and May queries for hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedRegionsAreNotSiblings
pattern mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionsAreNotSiblings(pm___,s,v1,v2)
{
	find mustType_Synchronization(pm___,s);
	// s is exported
	// v1 is exported
	// v2 is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,v1,s);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,v2,s);
	find mustType_CompositeElement(pm___,r1);
	find mustReference_regions(pm___,r1,virtual0);
	find mustReference_vertices(pm___,virtual0,virtual1);
	find mustEqual(pm___,virtual1,v1);
	find mustType_CompositeElement(pm___,r2);
	find mustReference_regions(pm___,r2,virtual2);
	find mustReference_vertices(pm___,virtual2,virtual3);
	find mustEqual(pm___,virtual3,v2);
	neg find mayEqual(pm___,r1,r2);
}or{
	find mustType_Synchronization(pm___,s);
	// s is exported
	// v1 is exported
	// v2 is exported
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,s,v1);
	find mustPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,s,v2);
	find mustType_CompositeElement(pm___,r1);
	find mustReference_regions(pm___,r1,virtual0);
	find mustReference_vertices(pm___,virtual0,virtual1);
	find mustEqual(pm___,virtual1,v1);
	find mustType_CompositeElement(pm___,r2);
	find mustReference_regions(pm___,r2,virtual2);
	find mustReference_vertices(pm___,virtual2,virtual3);
	find mustEqual(pm___,virtual3,v2);
	neg find mayEqual(pm___,r1,r2);
}
pattern mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionsAreNotSiblings(pm___,s,v1,v2)
{
	find mayType_Synchronization(pm___,s);
	// s is exported
	// v1 is exported
	// v2 is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,v1,s);
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,v2,s);
	find mayType_CompositeElement(pm___,r1);
	find mayReference_regions(pm___,r1,virtual0);
	find mayReference_vertices(pm___,virtual0,virtual1);
	find mayEqual(pm___,virtual1,v1);
	find mayType_CompositeElement(pm___,r2);
	find mayReference_regions(pm___,r2,virtual2);
	find mayReference_vertices(pm___,virtual2,virtual3);
	find mayEqual(pm___,virtual3,v2);
	neg find mustEqual(pm___,r1,r2);
}or{
	find mayType_Synchronization(pm___,s);
	// s is exported
	// v1 is exported
	// v2 is exported
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,s,v1);
	find mayPattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_transition(pm___,t,s,v2);
	find mayType_CompositeElement(pm___,r1);
	find mayReference_regions(pm___,r1,virtual0);
	find mayReference_vertices(pm___,virtual0,virtual1);
	find mayEqual(pm___,virtual1,v1);
	find mayType_CompositeElement(pm___,r2);
	find mayReference_regions(pm___,r2,virtual2);
	find mayReference_vertices(pm___,virtual2,virtual3);
	find mayEqual(pm___,virtual3,v2);
	neg find mustEqual(pm___,r1,r2);
}
Clone this wiki locally