From 6a3ff9bb588bf47242a56b91e35479dbba38eb19 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <marussy@mit.bme.hu>
Date: Thu, 7 May 2020 17:26:07 +0200
Subject: Scope unsat benchmarks

---
 .../plugin.xml                                                |  1 +
 .../inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | 11 +++++++++++
 2 files changed, 12 insertions(+)

(limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph')

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 @@
       <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.entryInRegion"/>
       <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noEntryInRegion"/>
       <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleEntryInRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.unsat_multipleEntryInRegion"/>
       <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transition"/>
       <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transitionFrom"/>
       <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) {
 	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);
@@ -197,6 +203,11 @@ pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Ve
 	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);
-- 
cgit v1.2.3-54-g00ecf