Scope unsat benchmarks

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 @@
       <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);