diff options
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph')
2 files changed, 12 insertions, 0 deletions
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml index 7bf4a20b..d4ab204e 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml | |||
@@ -8,6 +8,7 @@ | |||
8 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.entryInRegion"/> | 8 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.entryInRegion"/> |
9 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noEntryInRegion"/> | 9 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noEntryInRegion"/> |
10 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleEntryInRegion"/> | 10 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleEntryInRegion"/> |
11 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.unsat_multipleEntryInRegion"/> | ||
11 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transition"/> | 12 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transition"/> |
12 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transitionFrom"/> | 13 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transitionFrom"/> |
13 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transitionTo"/> | 14 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transitionTo"/> |
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql index 98a10cde..49fb5b2f 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | |||
@@ -22,6 +22,12 @@ pattern multipleEntryInRegion(r : Region) { | |||
22 | e1 != e2; | 22 | e1 != e2; |
23 | } | 23 | } |
24 | 24 | ||
25 | @Constraint(severity="error", message="error", key = {sct}) | ||
26 | pattern unsat_multipleEntryInRegion(sct : Statechart) { | ||
27 | Statechart(sct); | ||
28 | neg find multipleEntryInRegion(_); | ||
29 | } | ||
30 | |||
25 | pattern transition(t : Transition, src : Vertex, trg : Vertex) { | 31 | pattern transition(t : Transition, src : Vertex, trg : Vertex) { |
26 | Transition.source(t, src); | 32 | Transition.source(t, src); |
27 | Transition.target(t, trg); | 33 | Transition.target(t, trg); |
@@ -197,6 +203,11 @@ pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Ve | |||
197 | neg find hasMultipleRegions(c); | 203 | neg find hasMultipleRegions(c); |
198 | } | 204 | } |
199 | 205 | ||
206 | //@Constraint(severity="error", message="error", key = {sct}) | ||
207 | //pattern unsat_SynchronizedRegionDoesNotHaveMultipleRegions(sct : Statechart) { | ||
208 | // Statechart(sct); | ||
209 | // neg find SynchronizedRegionDoesNotHaveMultipleRegions(_, _); | ||
210 | //} | ||
200 | 211 | ||
201 | pattern hasMultipleRegions(composite: CompositeElement) { | 212 | pattern hasMultipleRegions(composite: CompositeElement) { |
202 | CompositeElement.regions(composite,region1); | 213 | CompositeElement.regions(composite,region1); |