getOneArbitraryMatch(final hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir pD) {
+ return rawGetOneArbitraryMatch(new Object[]{pD});
+ }
+
+ /**
+ * Indicates whether the given combination of specified pattern parameters constitute a valid pattern match,
+ * under any possible substitution of the unspecified parameters (if any).
+ * @param pD the fixed value of pattern parameter d, or null if not bound.
+ * @return true if the input is a valid (partial) match of the pattern.
+ *
+ */
+ public boolean hasMatch(final hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir pD) {
+ return rawHasMatch(new Object[]{pD});
+ }
+
+ /**
+ * Returns the number of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pD the fixed value of pattern parameter d, or null if not bound.
+ * @return the number of pattern matches found.
+ *
+ */
+ public int countMatches(final hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir pD) {
+ return rawCountMatches(new Object[]{pD});
+ }
+
+ /**
+ * Executes the given processor on an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pD the fixed value of pattern parameter d, or null if not bound.
+ * @param processor the action that will process the selected match.
+ * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked
+ *
+ */
+ public boolean forOneArbitraryMatch(final hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir pD, final Consumer super Dir.Match> processor) {
+ return rawForOneArbitraryMatch(new Object[]{pD}, processor);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pD the fixed value of pattern parameter d, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public Dir.Match newMatch(final hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir pD) {
+ return Dir.Match.newMatch(pD);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for d.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ protected Stream rawStreamAllValuesOfd(final Object[] parameters) {
+ return rawStreamAllValues(POSITION_D, parameters).map(hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir.class::cast);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for d.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfd() {
+ return rawStreamAllValuesOfd(emptyArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for d.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfd() {
+ return rawStreamAllValuesOfd(emptyArray());
+ }
+
+ @Override
+ protected Dir.Match tupleToMatch(final Tuple t) {
+ try {
+ return Dir.Match.newMatch((hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir) t.get(POSITION_D));
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in tuple not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected Dir.Match arrayToMatch(final Object[] match) {
+ try {
+ return Dir.Match.newMatch((hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir) match[POSITION_D]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected Dir.Match arrayToMatchMutable(final Object[] match) {
+ try {
+ return Dir.Match.newMutableMatch((hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir) match[POSITION_D]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ /**
+ * @return the singleton instance of the query specification of this pattern
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static IQuerySpecification querySpecification() {
+ return Dir.instance();
+ }
+ }
+
+ private Dir() {
+ super(GeneratedPQuery.INSTANCE);
+ }
+
+ /**
+ * @return the singleton instance of the query specification
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static Dir instance() {
+ try{
+ return LazyHolder.INSTANCE;
+ } catch (ExceptionInInitializerError err) {
+ throw processInitializerError(err);
+ }
+ }
+
+ @Override
+ protected Dir.Matcher instantiate(final ViatraQueryEngine engine) {
+ return Dir.Matcher.on(engine);
+ }
+
+ @Override
+ public Dir.Matcher instantiate() {
+ return Dir.Matcher.create();
+ }
+
+ @Override
+ public Dir.Match newEmptyMatch() {
+ return Dir.Match.newEmptyMatch();
+ }
+
+ @Override
+ public Dir.Match newMatch(final Object... parameters) {
+ return Dir.Match.newMatch((hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir) parameters[0]);
+ }
+
+ /**
+ * Inner class allowing the singleton instance of {@link JvmGenericType: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Dir (visibility: PUBLIC, simpleName: Dir, identifier: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Dir, deprecated: ) (abstract: false, static: false, final: true, packageName: hu.bme.mit.inf.dslreasoner.domains.alloyexamples) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created
+ * not at the class load time of the outer class,
+ * but rather at the first call to {@link JvmGenericType: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Dir (visibility: PUBLIC, simpleName: Dir, identifier: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Dir, deprecated: ) (abstract: false, static: false, final: true, packageName: hu.bme.mit.inf.dslreasoner.domains.alloyexamples) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}.
+ *
+ * This workaround is required e.g. to support recursion.
+ *
+ */
+ private static class LazyHolder {
+ private static final Dir INSTANCE = new Dir();
+
+ /**
+ * Statically initializes the query specification after the field {@link #INSTANCE} is assigned.
+ * This initialization order is required to support indirect recursion.
+ *
+ *
The static initializer is defined using a helper field to work around limitations of the code generator.
+ *
+ */
+ private static final Object STATIC_INITIALIZER = ensureInitialized();
+
+ public static Object ensureInitialized() {
+ INSTANCE.ensureInitializedInternal();
+ return null;
+ }
+ }
+
+ private static class GeneratedPQuery extends BaseGeneratedEMFPQuery {
+ private static final Dir.GeneratedPQuery INSTANCE = new GeneratedPQuery();
+
+ private final PParameter parameter_d = new PParameter("d", "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("FS", "Dir")), PParameterDirection.INOUT);
+
+ private final List parameters = Arrays.asList(parameter_d);
+
+ private GeneratedPQuery() {
+ super(PVisibility.PUBLIC);
+ }
+
+ @Override
+ public String getFullyQualifiedName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.dir";
+ }
+
+ @Override
+ public List getParameterNames() {
+ return Arrays.asList("d");
+ }
+
+ @Override
+ public List getParameters() {
+ return parameters;
+ }
+
+ @Override
+ public Set doGetContainedBodies() {
+ setEvaluationHints(new QueryEvaluationHint(null, QueryEvaluationHint.BackendRequirement.UNSPECIFIED));
+ Set bodies = new LinkedHashSet<>();
+ {
+ PBody body = new PBody(this);
+ PVariable var_d = body.getOrCreateVariableByName("d");
+ new TypeConstraint(body, Tuples.flatTupleOf(var_d), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "Dir")));
+ body.setSymbolicParameters(Arrays.asList(
+ new ExportedParameter(body, var_d, parameter_d)
+ ));
+ // Dir(d)
+ new TypeConstraint(body, Tuples.flatTupleOf(var_d), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "Dir")));
+ bodies.add(body);
+ }
+ return bodies;
+ }
+ }
+}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Live.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Live.java
index ae0f0c58..14a4c5c0 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Live.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Live.java
@@ -695,7 +695,7 @@ public final class Live extends BaseGeneratedEMFQuerySpecification
new TypeConstraint(body, Tuples.flatTupleOf(var_this), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FileSystem")));
PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}");
new TypeConstraint(body, Tuples.flatTupleOf(var_this, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FS", "FileSystem", "root")));
- new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "Dir")));
+ new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FSObject")));
new Equality(body, var__virtual_0_, var_l);
bodies.add(body);
}
@@ -714,7 +714,7 @@ public final class Live extends BaseGeneratedEMFQuerySpecification
new TypeConstraint(body, Tuples.flatTupleOf(var_this), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FileSystem")));
PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}");
new TypeConstraint(body, Tuples.flatTupleOf(var_this, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FS", "FileSystem", "root")));
- new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "Dir")));
+ new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FSObject")));
new Equality(body, var__virtual_0_, var_root);
// find patternContent+(root,l)
new BinaryTransitiveClosure(body, Tuples.flatTupleOf(var_root, var_l), PatternContent.instance().getInternalQueryRepresentation());
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/PatternContent.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/PatternContent.java
index 690d3e27..5410b693 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/PatternContent.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/PatternContent.java
@@ -3,6 +3,7 @@
*/
package hu.bme.mit.inf.dslreasoner.domains.alloyexamples;
+import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir;
import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FSObject;
import java.util.Arrays;
import java.util.Collection;
@@ -43,7 +44,7 @@ import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil;
*
* Original source:
*
- * pattern patternContent(o1: FSObject, o2: FSObject) {
+ * pattern patternContent(o1: Dir, o2: FSObject) {
* Dir.contents(o1,o2);
* }
*
@@ -67,13 +68,13 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification parameterNames = makeImmutableList("o1", "o2");
- private Match(final FSObject pO1, final FSObject pO2) {
+ private Match(final Dir pO1, final FSObject pO2) {
this.fO1 = pO1;
this.fO2 = pO2;
}
@@ -85,7 +86,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecificationOriginal source:
*
- * pattern patternContent(o1: FSObject, o2: FSObject) {
+ * pattern patternContent(o1: Dir, o2: FSObject) {
* Dir.contents(o1,o2);
* }
*
@@ -308,7 +309,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification getAllMatches(final FSObject pO1, final FSObject pO2) {
+ public Collection getAllMatches(final Dir pO1, final FSObject pO2) {
return rawStreamAllMatches(new Object[]{pO1, pO2}).collect(Collectors.toSet());
}
@@ -323,7 +324,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification streamAllMatches(final FSObject pO1, final FSObject pO2) {
+ public Stream streamAllMatches(final Dir pO1, final FSObject pO2) {
return rawStreamAllMatches(new Object[]{pO1, pO2});
}
@@ -335,7 +336,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification getOneArbitraryMatch(final FSObject pO1, final FSObject pO2) {
+ public Optional getOneArbitraryMatch(final Dir pO1, final FSObject pO2) {
return rawGetOneArbitraryMatch(new Object[]{pO1, pO2});
}
@@ -347,7 +348,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification processor) {
+ public boolean forOneArbitraryMatch(final Dir pO1, final FSObject pO2, final Consumer super PatternContent.Match> processor) {
return rawForOneArbitraryMatch(new Object[]{pO1, pO2}, processor);
}
@@ -384,7 +385,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification rawStreamAllValuesOfo1(final Object[] parameters) {
- return rawStreamAllValues(POSITION_O1, parameters).map(FSObject.class::cast);
+ protected Stream rawStreamAllValuesOfo1(final Object[] parameters) {
+ return rawStreamAllValues(POSITION_O1, parameters).map(Dir.class::cast);
}
/**
@@ -402,7 +403,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification getAllValuesOfo1() {
+ public Set getAllValuesOfo1() {
return rawStreamAllValuesOfo1(emptyArray()).collect(Collectors.toSet());
}
@@ -411,7 +412,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification streamAllValuesOfo1() {
+ public Stream streamAllValuesOfo1() {
return rawStreamAllValuesOfo1(emptyArray());
}
@@ -425,7 +426,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification streamAllValuesOfo1(final PatternContent.Match partialMatch) {
+ public Stream streamAllValuesOfo1(final PatternContent.Match partialMatch) {
return rawStreamAllValuesOfo1(partialMatch.toArray());
}
@@ -439,7 +440,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification streamAllValuesOfo1(final FSObject pO2) {
+ public Stream streamAllValuesOfo1(final FSObject pO2) {
return rawStreamAllValuesOfo1(new Object[]{null, pO2});
}
@@ -448,7 +449,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification getAllValuesOfo1(final PatternContent.Match partialMatch) {
+ public Set getAllValuesOfo1(final PatternContent.Match partialMatch) {
return rawStreamAllValuesOfo1(partialMatch.toArray()).collect(Collectors.toSet());
}
@@ -457,7 +458,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification getAllValuesOfo1(final FSObject pO2) {
+ public Set getAllValuesOfo1(final FSObject pO2) {
return rawStreamAllValuesOfo1(new Object[]{null, pO2}).collect(Collectors.toSet());
}
@@ -512,7 +513,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification streamAllValuesOfo2(final FSObject pO1) {
+ public Stream streamAllValuesOfo2(final Dir pO1) {
return rawStreamAllValuesOfo2(new Object[]{pO1, null});
}
@@ -530,14 +531,14 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecification getAllValuesOfo2(final FSObject pO1) {
+ public Set getAllValuesOfo2(final Dir pO1) {
return rawStreamAllValuesOfo2(new Object[]{pO1, null}).collect(Collectors.toSet());
}
@Override
protected PatternContent.Match tupleToMatch(final Tuple t) {
try {
- return PatternContent.Match.newMatch((FSObject) t.get(POSITION_O1), (FSObject) t.get(POSITION_O2));
+ return PatternContent.Match.newMatch((Dir) t.get(POSITION_O1), (FSObject) t.get(POSITION_O2));
} catch(ClassCastException e) {
LOGGER.error("Element(s) in tuple not properly typed!",e);
return null;
@@ -547,7 +548,7 @@ public final class PatternContent extends BaseGeneratedEMFQuerySpecificationasList(
new ExportedParameter(body, var_o1, parameter_o1),
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/RootIsNotDir.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/RootIsNotDir.java
new file mode 100644
index 00000000..22c31158
--- /dev/null
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/RootIsNotDir.java
@@ -0,0 +1,560 @@
+/**
+ * Generated from platform:/resource/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/FileSystem.vql
+ */
+package hu.bme.mit.inf.dslreasoner.domains.alloyexamples;
+
+import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Dir;
+import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FileSystem;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Objects;
+import java.util.Optional;
+import java.util.Set;
+import java.util.function.Consumer;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+import org.apache.log4j.Logger;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFPQuery;
+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.impl.BaseMatcher;
+import org.eclipse.viatra.query.runtime.api.impl.BasePatternMatch;
+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey;
+import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey;
+import org.eclipse.viatra.query.runtime.matchers.backend.QueryEvaluationHint;
+import org.eclipse.viatra.query.runtime.matchers.psystem.PBody;
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable;
+import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
+import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.ParameterReference;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;
+import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil;
+
+/**
+ * A pattern-specific query specification that can instantiate Matcher in a type-safe way.
+ *
+ * Original source:
+ *
+ * {@literal @}Constraint(key={fs}, severity="error", message="error")
+ * pattern rootIsNotDir(fs: FileSystem) {
+ * FileSystem.root(fs, root);
+ * neg find dir(root);
+ * }
+ *
+ *
+ * @see Matcher
+ * @see Match
+ *
+ */
+@SuppressWarnings("all")
+public final class RootIsNotDir extends BaseGeneratedEMFQuerySpecification {
+ /**
+ * Pattern-specific match representation of the hu.bme.mit.inf.dslreasoner.domains.alloyexamples.rootIsNotDir pattern,
+ * to be used in conjunction with {@link Matcher}.
+ *
+ * Class fields correspond to parameters of the pattern. Fields with value null are considered unassigned.
+ * Each instance is a (possibly partial) substitution of pattern parameters,
+ * usable to represent a match of the pattern in the result of a query,
+ * or to specify the bound (fixed) input parameters when issuing a query.
+ *
+ * @see Matcher
+ *
+ */
+ public static abstract class Match extends BasePatternMatch {
+ private FileSystem fFs;
+
+ private static List parameterNames = makeImmutableList("fs");
+
+ private Match(final FileSystem pFs) {
+ this.fFs = pFs;
+ }
+
+ @Override
+ public Object get(final String parameterName) {
+ if ("fs".equals(parameterName)) return this.fFs;
+ return null;
+ }
+
+ public FileSystem getFs() {
+ return this.fFs;
+ }
+
+ @Override
+ public boolean set(final String parameterName, final Object newValue) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ if ("fs".equals(parameterName) ) {
+ this.fFs = (FileSystem) newValue;
+ return true;
+ }
+ return false;
+ }
+
+ public void setFs(final FileSystem pFs) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ this.fFs = pFs;
+ }
+
+ @Override
+ public String patternName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.rootIsNotDir";
+ }
+
+ @Override
+ public List parameterNames() {
+ return RootIsNotDir.Match.parameterNames;
+ }
+
+ @Override
+ public Object[] toArray() {
+ return new Object[]{fFs};
+ }
+
+ @Override
+ public RootIsNotDir.Match toImmutable() {
+ return isMutable() ? newMatch(fFs) : this;
+ }
+
+ @Override
+ public String prettyPrint() {
+ StringBuilder result = new StringBuilder();
+ result.append("\"fs\"=" + prettyPrintValue(fFs));
+ return result.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(fFs);
+ }
+
+ @Override
+ public boolean equals(final Object obj) {
+ if (this == obj)
+ return true;
+ if (obj == null) {
+ return false;
+ }
+ if ((obj instanceof RootIsNotDir.Match)) {
+ RootIsNotDir.Match other = (RootIsNotDir.Match) obj;
+ return Objects.equals(fFs, other.fFs);
+ } else {
+ // this should be infrequent
+ if (!(obj instanceof IPatternMatch)) {
+ return false;
+ }
+ IPatternMatch otherSig = (IPatternMatch) obj;
+ return Objects.equals(specification(), otherSig.specification()) && Arrays.deepEquals(toArray(), otherSig.toArray());
+ }
+ }
+
+ @Override
+ public RootIsNotDir specification() {
+ return RootIsNotDir.instance();
+ }
+
+ /**
+ * Returns an empty, mutable match.
+ * Fields of the mutable match can be filled to create a partial match, usable as matcher input.
+ *
+ * @return the empty match.
+ *
+ */
+ public static RootIsNotDir.Match newEmptyMatch() {
+ return new Mutable(null);
+ }
+
+ /**
+ * Returns a mutable (partial) match.
+ * Fields of the mutable match can be filled to create a partial match, usable as matcher input.
+ *
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return the new, mutable (partial) match object.
+ *
+ */
+ public static RootIsNotDir.Match newMutableMatch(final FileSystem pFs) {
+ return new Mutable(pFs);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public static RootIsNotDir.Match newMatch(final FileSystem pFs) {
+ return new Immutable(pFs);
+ }
+
+ private static final class Mutable extends RootIsNotDir.Match {
+ Mutable(final FileSystem pFs) {
+ super(pFs);
+ }
+
+ @Override
+ public boolean isMutable() {
+ return true;
+ }
+ }
+
+ private static final class Immutable extends RootIsNotDir.Match {
+ Immutable(final FileSystem pFs) {
+ super(pFs);
+ }
+
+ @Override
+ public boolean isMutable() {
+ return false;
+ }
+ }
+ }
+
+ /**
+ * Generated pattern matcher API of the hu.bme.mit.inf.dslreasoner.domains.alloyexamples.rootIsNotDir pattern,
+ * providing pattern-specific query methods.
+ *
+ *
Use the pattern matcher on a given model via {@link #on(ViatraQueryEngine)},
+ * e.g. in conjunction with {@link ViatraQueryEngine#on(QueryScope)}.
+ *
+ *
Matches of the pattern will be represented as {@link Match}.
+ *
+ *
Original source:
+ *
+ * {@literal @}Constraint(key={fs}, severity="error", message="error")
+ * pattern rootIsNotDir(fs: FileSystem) {
+ * FileSystem.root(fs, root);
+ * neg find dir(root);
+ * }
+ *
+ *
+ * @see Match
+ * @see RootIsNotDir
+ *
+ */
+ public static class Matcher extends BaseMatcher {
+ /**
+ * Initializes the pattern matcher within an existing VIATRA Query engine.
+ * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.
+ *
+ * @param engine the existing VIATRA Query engine in which this matcher will be created.
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ *
+ */
+ public static RootIsNotDir.Matcher on(final ViatraQueryEngine engine) {
+ // check if matcher already exists
+ Matcher matcher = engine.getExistingMatcher(querySpecification());
+ if (matcher == null) {
+ matcher = (Matcher)engine.getMatcher(querySpecification());
+ }
+ return matcher;
+ }
+
+ /**
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ * @return an initialized matcher
+ * @noreference This method is for internal matcher initialization by the framework, do not call it manually.
+ *
+ */
+ public static RootIsNotDir.Matcher create() {
+ return new Matcher();
+ }
+
+ private static final int POSITION_FS = 0;
+
+ private static final Logger LOGGER = ViatraQueryLoggingUtil.getLogger(RootIsNotDir.Matcher.class);
+
+ /**
+ * Initializes the pattern matcher within an existing VIATRA Query engine.
+ * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.
+ *
+ * @param engine the existing VIATRA Query engine in which this matcher will be created.
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ *
+ */
+ private Matcher() {
+ super(querySpecification());
+ }
+
+ /**
+ * Returns the set of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return matches represented as a Match object.
+ *
+ */
+ public Collection getAllMatches(final FileSystem pFs) {
+ return rawStreamAllMatches(new Object[]{pFs}).collect(Collectors.toSet());
+ }
+
+ /**
+ * Returns a stream of all matches of the pattern that conform to the given fixed values of some parameters.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return a stream of matches represented as a Match object.
+ *
+ */
+ public Stream streamAllMatches(final FileSystem pFs) {
+ return rawStreamAllMatches(new Object[]{pFs});
+ }
+
+ /**
+ * Returns an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return a match represented as a Match object, or null if no match is found.
+ *
+ */
+ public Optional getOneArbitraryMatch(final FileSystem pFs) {
+ return rawGetOneArbitraryMatch(new Object[]{pFs});
+ }
+
+ /**
+ * Indicates whether the given combination of specified pattern parameters constitute a valid pattern match,
+ * under any possible substitution of the unspecified parameters (if any).
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return true if the input is a valid (partial) match of the pattern.
+ *
+ */
+ public boolean hasMatch(final FileSystem pFs) {
+ return rawHasMatch(new Object[]{pFs});
+ }
+
+ /**
+ * Returns the number of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return the number of pattern matches found.
+ *
+ */
+ public int countMatches(final FileSystem pFs) {
+ return rawCountMatches(new Object[]{pFs});
+ }
+
+ /**
+ * Executes the given processor on an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @param processor the action that will process the selected match.
+ * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked
+ *
+ */
+ public boolean forOneArbitraryMatch(final FileSystem pFs, final Consumer super RootIsNotDir.Match> processor) {
+ return rawForOneArbitraryMatch(new Object[]{pFs}, processor);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pFs the fixed value of pattern parameter fs, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public RootIsNotDir.Match newMatch(final FileSystem pFs) {
+ return RootIsNotDir.Match.newMatch(pFs);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for fs.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ protected Stream rawStreamAllValuesOffs(final Object[] parameters) {
+ return rawStreamAllValues(POSITION_FS, parameters).map(FileSystem.class::cast);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for fs.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOffs() {
+ return rawStreamAllValuesOffs(emptyArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for fs.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOffs() {
+ return rawStreamAllValuesOffs(emptyArray());
+ }
+
+ @Override
+ protected RootIsNotDir.Match tupleToMatch(final Tuple t) {
+ try {
+ return RootIsNotDir.Match.newMatch((FileSystem) t.get(POSITION_FS));
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in tuple not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected RootIsNotDir.Match arrayToMatch(final Object[] match) {
+ try {
+ return RootIsNotDir.Match.newMatch((FileSystem) match[POSITION_FS]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected RootIsNotDir.Match arrayToMatchMutable(final Object[] match) {
+ try {
+ return RootIsNotDir.Match.newMutableMatch((FileSystem) match[POSITION_FS]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ /**
+ * @return the singleton instance of the query specification of this pattern
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static IQuerySpecification querySpecification() {
+ return RootIsNotDir.instance();
+ }
+ }
+
+ private RootIsNotDir() {
+ super(GeneratedPQuery.INSTANCE);
+ }
+
+ /**
+ * @return the singleton instance of the query specification
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static RootIsNotDir instance() {
+ try{
+ return LazyHolder.INSTANCE;
+ } catch (ExceptionInInitializerError err) {
+ throw processInitializerError(err);
+ }
+ }
+
+ @Override
+ protected RootIsNotDir.Matcher instantiate(final ViatraQueryEngine engine) {
+ return RootIsNotDir.Matcher.on(engine);
+ }
+
+ @Override
+ public RootIsNotDir.Matcher instantiate() {
+ return RootIsNotDir.Matcher.create();
+ }
+
+ @Override
+ public RootIsNotDir.Match newEmptyMatch() {
+ return RootIsNotDir.Match.newEmptyMatch();
+ }
+
+ @Override
+ public RootIsNotDir.Match newMatch(final Object... parameters) {
+ return RootIsNotDir.Match.newMatch((hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FileSystem) parameters[0]);
+ }
+
+ /**
+ * Inner class allowing the singleton instance of {@link JvmGenericType: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.RootIsNotDir (visibility: PUBLIC, simpleName: RootIsNotDir, identifier: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.RootIsNotDir, deprecated: ) (abstract: false, static: false, final: true, packageName: hu.bme.mit.inf.dslreasoner.domains.alloyexamples) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created
+ * not at the class load time of the outer class,
+ * but rather at the first call to {@link JvmGenericType: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.RootIsNotDir (visibility: PUBLIC, simpleName: RootIsNotDir, identifier: hu.bme.mit.inf.dslreasoner.domains.alloyexamples.RootIsNotDir, deprecated: ) (abstract: false, static: false, final: true, packageName: hu.bme.mit.inf.dslreasoner.domains.alloyexamples) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}.
+ *
+ * This workaround is required e.g. to support recursion.
+ *
+ */
+ private static class LazyHolder {
+ private static final RootIsNotDir INSTANCE = new RootIsNotDir();
+
+ /**
+ * Statically initializes the query specification after the field {@link #INSTANCE} is assigned.
+ * This initialization order is required to support indirect recursion.
+ *
+ *
The static initializer is defined using a helper field to work around limitations of the code generator.
+ *
+ */
+ private static final Object STATIC_INITIALIZER = ensureInitialized();
+
+ public static Object ensureInitialized() {
+ INSTANCE.ensureInitializedInternal();
+ return null;
+ }
+ }
+
+ private static class GeneratedPQuery extends BaseGeneratedEMFPQuery {
+ private static final RootIsNotDir.GeneratedPQuery INSTANCE = new GeneratedPQuery();
+
+ private final PParameter parameter_fs = new PParameter("fs", "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FileSystem", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("FS", "FileSystem")), PParameterDirection.INOUT);
+
+ private final List parameters = Arrays.asList(parameter_fs);
+
+ private GeneratedPQuery() {
+ super(PVisibility.PUBLIC);
+ }
+
+ @Override
+ public String getFullyQualifiedName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.rootIsNotDir";
+ }
+
+ @Override
+ public List getParameterNames() {
+ return Arrays.asList("fs");
+ }
+
+ @Override
+ public List getParameters() {
+ return parameters;
+ }
+
+ @Override
+ public Set doGetContainedBodies() {
+ setEvaluationHints(new QueryEvaluationHint(null, QueryEvaluationHint.BackendRequirement.UNSPECIFIED));
+ Set bodies = new LinkedHashSet<>();
+ {
+ PBody body = new PBody(this);
+ PVariable var_fs = body.getOrCreateVariableByName("fs");
+ PVariable var_root = body.getOrCreateVariableByName("root");
+ new TypeConstraint(body, Tuples.flatTupleOf(var_fs), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FileSystem")));
+ body.setSymbolicParameters(Arrays.asList(
+ new ExportedParameter(body, var_fs, parameter_fs)
+ ));
+ // FileSystem.root(fs, root)
+ new TypeConstraint(body, Tuples.flatTupleOf(var_fs), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FileSystem")));
+ PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}");
+ new TypeConstraint(body, Tuples.flatTupleOf(var_fs, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FS", "FileSystem", "root")));
+ new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FS", "FSObject")));
+ new Equality(body, var__virtual_0_, var_root);
+ // neg find dir(root)
+ new NegativePatternCall(body, Tuples.flatTupleOf(var_root), Dir.instance().getInternalQueryRepresentation());
+ bodies.add(body);
+ }
+ {
+ PAnnotation annotation = new PAnnotation("Constraint");
+ annotation.addAttribute("key", Arrays.asList(new Object[] {
+ new ParameterReference("fs")
+ }));
+ annotation.addAttribute("severity", "error");
+ annotation.addAttribute("message", "error");
+ addAnnotation(annotation);
+ }
+ return bodies;
+ }
+ }
+}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/FileSystem.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/FileSystem.java
index 1896e31e..f0066955 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/FileSystem.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/FileSystem.java
@@ -33,12 +33,12 @@ public interface FileSystem extends EObject {
*
*
* @return the value of the 'Root' containment reference.
- * @see #setRoot(Dir)
+ * @see #setRoot(FSObject)
* @see hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage#getFileSystem_Root()
* @model containment="true" required="true"
* @generated
*/
- Dir getRoot();
+ FSObject getRoot();
/**
* Sets the value of the '{@link hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FileSystem#getRoot Root}' containment reference.
@@ -48,7 +48,7 @@ public interface FileSystem extends EObject {
* @see #getRoot()
* @generated
*/
- void setRoot(Dir value);
+ void setRoot(FSObject value);
/**
* Returns the value of the 'Live' reference list.
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/DirImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/DirImpl.java
index 62df04af..c2d417d2 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/DirImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/DirImpl.java
@@ -66,6 +66,7 @@ public class DirImpl extends FSObjectImpl implements Dir {
*
* @generated
*/
+ @Override
public EList getContents() {
if (contents == null) {
contents = new EObjectContainmentWithInverseEList(FSObject.class, this, FilesystemPackage.DIR__CONTENTS, FilesystemPackage.FS_OBJECT__PARENT);
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FSObjectImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FSObjectImpl.java
index c8e73b4e..d87935d6 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FSObjectImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FSObjectImpl.java
@@ -53,6 +53,7 @@ public abstract class FSObjectImpl extends MinimalEObjectImpl.Container implemen
*
* @generated
*/
+ @Override
public Dir getParent() {
if (eContainerFeatureID() != FilesystemPackage.FS_OBJECT__PARENT) return null;
return (Dir)eInternalContainer();
@@ -73,6 +74,7 @@ public abstract class FSObjectImpl extends MinimalEObjectImpl.Container implemen
*
* @generated
*/
+ @Override
public void setParent(Dir newParent) {
if (newParent != eInternalContainer() || (eContainerFeatureID() != FilesystemPackage.FS_OBJECT__PARENT && newParent != null)) {
if (EcoreUtil.isAncestor(this, newParent))
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FileSystemImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FileSystemImpl.java
index adf30f3a..e6859cab 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FileSystemImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FileSystemImpl.java
@@ -2,7 +2,6 @@
*/
package hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.impl;
-import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Dir;
import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FSObject;
import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FileSystem;
import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage;
@@ -42,7 +41,7 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
* @generated
* @ordered
*/
- protected Dir root;
+ protected FSObject root;
/**
* The cached setting delegate for the '{@link #getLive() Live}' reference list.
@@ -78,7 +77,8 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
*
* @generated
*/
- public Dir getRoot() {
+ @Override
+ public FSObject getRoot() {
return root;
}
@@ -87,8 +87,8 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
*
* @generated
*/
- public NotificationChain basicSetRoot(Dir newRoot, NotificationChain msgs) {
- Dir oldRoot = root;
+ public NotificationChain basicSetRoot(FSObject newRoot, NotificationChain msgs) {
+ FSObject oldRoot = root;
root = newRoot;
if (eNotificationRequired()) {
ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, FilesystemPackage.FILE_SYSTEM__ROOT, oldRoot, newRoot);
@@ -102,7 +102,8 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
*
* @generated
*/
- public void setRoot(Dir newRoot) {
+ @Override
+ public void setRoot(FSObject newRoot) {
if (newRoot != root) {
NotificationChain msgs = null;
if (root != null)
@@ -122,6 +123,7 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
* @generated
*/
@SuppressWarnings("unchecked")
+ @Override
public EList getLive() {
return (EList)LIVE__ESETTING_DELEGATE.dynamicGet(this, null, 0, true, false);
}
@@ -165,7 +167,7 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
public void eSet(int featureID, Object newValue) {
switch (featureID) {
case FilesystemPackage.FILE_SYSTEM__ROOT:
- setRoot((Dir)newValue);
+ setRoot((FSObject)newValue);
return;
}
super.eSet(featureID, newValue);
@@ -180,7 +182,7 @@ public class FileSystemImpl extends MinimalEObjectImpl.Container implements File
public void eUnset(int featureID) {
switch (featureID) {
case FilesystemPackage.FILE_SYSTEM__ROOT:
- setRoot((Dir)null);
+ setRoot((FSObject)null);
return;
}
super.eUnset(featureID);
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemFactoryImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemFactoryImpl.java
index e40b0bd1..b4b09e15 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemFactoryImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemFactoryImpl.java
@@ -70,6 +70,7 @@ public class FilesystemFactoryImpl extends EFactoryImpl implements FilesystemFac
*
* @generated
*/
+ @Override
public FileSystem createFileSystem() {
FileSystemImpl fileSystem = new FileSystemImpl();
return fileSystem;
@@ -80,6 +81,7 @@ public class FilesystemFactoryImpl extends EFactoryImpl implements FilesystemFac
*
* @generated
*/
+ @Override
public Dir createDir() {
DirImpl dir = new DirImpl();
return dir;
@@ -90,6 +92,7 @@ public class FilesystemFactoryImpl extends EFactoryImpl implements FilesystemFac
*
* @generated
*/
+ @Override
public File createFile() {
FileImpl file = new FileImpl();
return file;
@@ -100,6 +103,7 @@ public class FilesystemFactoryImpl extends EFactoryImpl implements FilesystemFac
*
* @generated
*/
+ @Override
public Model createModel() {
ModelImpl model = new ModelImpl();
return model;
@@ -110,6 +114,7 @@ public class FilesystemFactoryImpl extends EFactoryImpl implements FilesystemFac
*
* @generated
*/
+ @Override
public FilesystemPackage getFilesystemPackage() {
return (FilesystemPackage)getEPackage();
}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemPackageImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemPackageImpl.java
index 87390fee..4c0ca4c5 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemPackageImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/FilesystemPackageImpl.java
@@ -86,7 +86,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
/**
* Creates, registers, and initializes the Package for this model, and for any others upon which it depends.
- *
+ *
* This method is used to initialize {@link FilesystemPackage#eINSTANCE} when that field is accessed.
* Clients should not invoke it directly. Instead, they should simply access that field to obtain the package.
*
@@ -100,7 +100,8 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
if (isInited) return (FilesystemPackage)EPackage.Registry.INSTANCE.getEPackage(FilesystemPackage.eNS_URI);
// Obtain or create and register package
- FilesystemPackageImpl theFilesystemPackage = (FilesystemPackageImpl)(EPackage.Registry.INSTANCE.get(eNS_URI) instanceof FilesystemPackageImpl ? EPackage.Registry.INSTANCE.get(eNS_URI) : new FilesystemPackageImpl());
+ Object registeredFilesystemPackage = EPackage.Registry.INSTANCE.get(eNS_URI);
+ FilesystemPackageImpl theFilesystemPackage = registeredFilesystemPackage instanceof FilesystemPackageImpl ? (FilesystemPackageImpl)registeredFilesystemPackage : new FilesystemPackageImpl();
isInited = true;
@@ -113,7 +114,6 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
// Mark meta-data to indicate it can't be changed
theFilesystemPackage.freeze();
-
// Update the registry and return the package
EPackage.Registry.INSTANCE.put(FilesystemPackage.eNS_URI, theFilesystemPackage);
return theFilesystemPackage;
@@ -124,6 +124,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EClass getFileSystem() {
return fileSystemEClass;
}
@@ -133,6 +134,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EReference getFileSystem_Root() {
return (EReference)fileSystemEClass.getEStructuralFeatures().get(0);
}
@@ -142,6 +144,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EReference getFileSystem_Live() {
return (EReference)fileSystemEClass.getEStructuralFeatures().get(1);
}
@@ -151,6 +154,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EClass getFSObject() {
return fsObjectEClass;
}
@@ -160,6 +164,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EReference getFSObject_Parent() {
return (EReference)fsObjectEClass.getEStructuralFeatures().get(0);
}
@@ -169,6 +174,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EClass getDir() {
return dirEClass;
}
@@ -178,6 +184,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EReference getDir_Contents() {
return (EReference)dirEClass.getEStructuralFeatures().get(0);
}
@@ -187,6 +194,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EClass getFile() {
return fileEClass;
}
@@ -196,6 +204,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EClass getModel() {
return modelEClass;
}
@@ -205,6 +214,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EReference getModel_Filesystems() {
return (EReference)modelEClass.getEStructuralFeatures().get(0);
}
@@ -214,6 +224,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public EReference getModel_OtherFSObjects() {
return (EReference)modelEClass.getEStructuralFeatures().get(1);
}
@@ -223,6 +234,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
*
* @generated
*/
+ @Override
public FilesystemFactory getFilesystemFactory() {
return (FilesystemFactory)getEFactoryInstance();
}
@@ -296,7 +308,7 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
// Initialize classes, features, and operations; add parameters
initEClass(fileSystemEClass, FileSystem.class, "FileSystem", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
- initEReference(getFileSystem_Root(), this.getDir(), null, "root", null, 1, 1, FileSystem.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+ initEReference(getFileSystem_Root(), this.getFSObject(), null, "root", null, 1, 1, FileSystem.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
initEReference(getFileSystem_Live(), this.getFSObject(), null, "live", null, 0, -1, FileSystem.class, IS_TRANSIENT, IS_VOLATILE, !IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, IS_DERIVED, IS_ORDERED);
initEClass(fsObjectEClass, FSObject.class, "FSObject", IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
@@ -328,12 +340,12 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
* @generated
*/
protected void createEcoreAnnotations() {
- String source = "http://www.eclipse.org/emf/2002/Ecore";
+ String source = "http://www.eclipse.org/emf/2002/Ecore";
addAnnotation
- (this,
- source,
+ (this,
+ source,
new String[] {
- "settingDelegates", "org.eclipse.viatra.query.querybasedfeature"
+ "settingDelegates", "org.eclipse.viatra.query.querybasedfeature"
});
}
@@ -344,12 +356,12 @@ public class FilesystemPackageImpl extends EPackageImpl implements FilesystemPac
* @generated
*/
protected void createOrgAnnotations() {
- String source = "org.eclipse.viatra.query.querybasedfeature";
+ String source = "org.eclipse.viatra.query.querybasedfeature";
addAnnotation
- (getFileSystem_Live(),
- source,
+ (getFileSystem_Live(),
+ source,
new String[] {
- "patternFQN", "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.live"
+ "patternFQN", "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.live"
});
}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/ModelImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/ModelImpl.java
index 4c236e8e..093b9972 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/ModelImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Filesystem/impl/ModelImpl.java
@@ -82,6 +82,7 @@ public class ModelImpl extends MinimalEObjectImpl.Container implements Model {
*
* @generated
*/
+ @Override
public FileSystem getFilesystems() {
return filesystems;
}
@@ -106,6 +107,7 @@ public class ModelImpl extends MinimalEObjectImpl.Container implements Model {
*
* @generated
*/
+ @Override
public void setFilesystems(FileSystem newFilesystems) {
if (newFilesystems != filesystems) {
NotificationChain msgs = null;
@@ -125,6 +127,7 @@ public class ModelImpl extends MinimalEObjectImpl.Container implements Model {
*
* @generated
*/
+ @Override
public EList getOtherFSObjects() {
if (otherFSObjects == null) {
otherFSObjects = new EObjectContainmentEList(FSObject.class, this, FilesystemPackage.MODEL__OTHER_FS_OBJECTS);
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
index d7955ddd..a7e29a22 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
@@ -6,10 +6,11 @@
"warmupIterations": 1,
"iterations": 1,
"domain": "fs",
- "scope": "useful",
+ "scope": "none",
"sizes": [50, 100, 150, 200, 250, 300, 350, 400, 450, 500],
"solver": "ViatraSolver",
"scopePropagator": "polyhedral",
- "propagatedConstraints": "relations",
- "polyhedronSolver": "Clp"
+ "propagatedConstraints": "hints",
+ "polyhedronSolver": "Clp",
+ "scopeHeuristic": "polyhedral"
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend
new file mode 100644
index 00000000..8d6523b1
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend
@@ -0,0 +1,32 @@
+package hu.bme.mit.inf.dslreasoner.run
+
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
+
+class FileSystemHint extends Ecore2LogicTraceBasedHint {
+ static val REMAINING_CONTENTS_ROOT = "hint_root"
+
+ new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
+ super(ecore2Logic, trace)
+ }
+
+ override getAdditionalPatterns(PatternGenerator it) '''
+ pattern «REMAINING_CONTENTS_ROOT»(problem:LogicProblem, interpretation:PartialInterpretation, remainingContents:java Integer) {
+ find interpretation(problem, interpretation);
+ remainingContents == sum find remainingContents_root_reference_Dir_helper(problem, interpretation, _, #_)
+ }
+ '''
+
+ override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) {
+ val dirCount = createBuilder.add(1, "Dir".type).build
+
+ val remainingContentsRootMatcher = createMatcher(REMAINING_CONTENTS_ROOT)
+
+ return [ p |
+ dirCount.tightenLowerBound(remainingContentsRootMatcher.getCount(p))
+ ]
+ }
+
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend
index e79a6261..f4f36951 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend
@@ -35,11 +35,11 @@ class FileSystemInconsistencyDetector extends ModelGenerationMethodBasedGlobalCo
override checkGlobalConstraint(ThreadContext context) {
var requiredNewObjects =
- filesystem.countMatches*2 +
- root.countMatches
+ root.countMatches*2 +
+ filesystem.countMatches
val availableNewObjects = partialInterpretation.maxNewElements
val res = availableNewObjects >= requiredNewObjects
- //println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''')
+ println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''')
return res
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
index 54724226..4b0791d4 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
@@ -195,8 +195,9 @@ class YakinduLoader extends MetamodelLoader {
this.workspace.readModel(EObject, "Yakindu.xmi").eResource.allContents.toList
}
- override additionalConstraints() { // #[]
- #[[method|new SGraphInconsistencyDetector(method)]]
+ override additionalConstraints() {
+ //#[[method|new SGraphInconsistencyDetector(method)]]
+ emptyList
}
override getTypeQuantiles() {
@@ -260,9 +261,17 @@ class FileSystemLoader extends MetamodelLoader {
}
override additionalConstraints() {
- #[[method|new FileSystemInconsistencyDetector(method)]]
+ //#[[method|new FileSystemInconsistencyDetector(method)]]
+ emptyList
}
+ override getTypeQuantiles() {
+ #{
+ "Filesystem" -> new TypeQuantiles(0, 0.05),
+ "Dir" -> new TypeQuantiles(0.15, 0.3),
+ "File" -> new TypeQuantiles(0.25, 0.85)
+ }
+ }
}
class EcoreLoader extends MetamodelLoader {
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend
index e95c0c64..ef5b779e 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend
@@ -9,8 +9,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGene
class SatelliteHint extends Ecore2LogicTraceBasedHint {
static val INTERFEROMETY_PAYLOAD = "hint_interferometryPayload"
static val REMAINING_CONTENTS_KA_COMM_SUBSYSTEM = "hint_kaCommSubsystem"
- static val HINT_SPACECRAFT_UHF_POSSIBLE_LINK = "hint_spacecraftWithUhfPossibleLink"
- static val HINT_SPACECRAFT_UHF_ONLY_NO_LINK = "hint_spacecraftUhfOnlyNoLink"
new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
super(ecore2Logic, trace)
@@ -32,54 +30,19 @@ class SatelliteHint extends Ecore2LogicTraceBasedHint {
find interpretation(problem, interpretation);
remainingContents == sum find «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»_helper(problem, interpretation, _, #_);
}
-
- private pattern hint_spacecraftNotUhfOnly(problem:LogicProblem, interpretation:PartialInterpretation, spacecraft:DefinedElement) {
- find interpretation(problem, interpretation);
- find mustExist(problem, interpretation, spacecraft);
- «typeIndexer.referInstanceOf("Spacecraft".type, Modality.MUST, "spacecraft")»
- «relationDeclarationIndexer.referRelation("CommunicatingElement".relation("commSubsystem"), "spacecraft", "comm", Modality.MAY)»
- neg «typeIndexer.referInstanceOf("UHFCommSubsystem".type, Modality.MUST, "comm")»
- }
-
- private pattern hint_spacecraftWithUhf(problem:LogicProblem, interpretation:PartialInterpretation, spacecraft:DefinedElement) {
- find interpretation(problem, interpretation);
- find mustExist(problem, interpretation, spacecraft);
- «typeIndexer.referInstanceOf("Spacecraft".type, Modality.MUST, "spacecraft")»
- «relationDeclarationIndexer.referRelation("CommunicatingElement".relation("commSubsystem"), "spacecraft", "comm", Modality.MUST)»
- «typeIndexer.referInstanceOf("UHFCommSubsystem".type, Modality.MUST, "comm")»
- }
-
- pattern «HINT_SPACECRAFT_UHF_POSSIBLE_LINK»(problem:LogicProblem, interpretation:PartialInterpretation) {
- find hint_spacecraftWithUhf(problem, interpretation, spacecraft);
- find hint_spacecraftNotUhfOnly(problem, interpretation, spacecraft);
- }
-
- pattern «HINT_SPACECRAFT_UHF_ONLY_NO_LINK»(problem:LogicProblem, interpretation:PartialInterpretation) {
- find interpretation(problem, interpretation);
- find mustExist(problem, interpretation, spacecraft);
- «typeIndexer.referInstanceOf("Spacecraft".type, Modality.MUST, "spacecraft")»
- neg find hint_spacecraftNotUhfOnly(problem, interpretation, spacecraft);
- find currentInRelation_pattern_hu_bme_mit_inf_dslreasoner_domains_satellite_queries_noLinkToGroundStation(problem, interpretation, spacecraft);
- }
'''
override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) {
val interferometryPayloadCount = createBuilder.add(1, "InterferometryPayload".type).build
val kaCommSubsystemWithoutSmallSatCount = createBuilder.add(1, "KaCommSubsystem".type).add(-2, "SmallSat".type).
build
- val uhfCommSubsystemCount = createBuilder.add(1, "UHFCommSubsystem".type).build
val interferometryPayloadMatcher = createMatcher(INTERFEROMETY_PAYLOAD)
val kaCommSubsystemRemainingContentsMatcher = createMatcher(REMAINING_CONTENTS_KA_COMM_SUBSYSTEM)
- val uhfPossibleLinkMatcher = createMatcher(HINT_SPACECRAFT_UHF_POSSIBLE_LINK)
- val uhfNoLinkMatcher = createMatcher(HINT_SPACECRAFT_UHF_ONLY_NO_LINK)
return [ p |
interferometryPayloadCount.tightenLowerBound(2 - interferometryPayloadMatcher.countMatches(p))
kaCommSubsystemWithoutSmallSatCount.tightenUpperBound(kaCommSubsystemRemainingContentsMatcher.getCount(p))
- if (uhfPossibleLinkMatcher.countMatches(p) == 0 && uhfNoLinkMatcher.countMatches(p) >= 1) {
- uhfCommSubsystemCount.tightenLowerBound(1)
- }
]
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
index 5abff962..56a65091 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
@@ -22,7 +22,7 @@ class MeasurementScript {
ScopeHeuristic scopeHeuristic
def toCsvHeader() {
- '''«domain»,«scope»,«solver»,«scopePropagator ?: "NULL"»,«propagatedConstraints ?: "NULL"»,«polyhedronSolver ?: "NULL"»'''
+ '''«domain»,«scope»,«solver»,«scopePropagator ?: "NULL"»,«propagatedConstraints ?: "NULL"»,«polyhedronSolver ?: "NULL"»,«scopeHeuristic ?: "NULL"»'''
}
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
index 48e750cb..bfbbf329 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
@@ -68,7 +68,7 @@ class MeasurementScriptRunner {
this.script = script
inputWorkspace = new FileSystemWorkspace(script.inputPath + "/", "")
outputWorkspace = new FileSystemWorkspace(script.outputPath +
- "/", '''«script.domain»_«script.solver»_«script.scope»_«script.scopePropagator ?: "na"»_«script.propagatedConstraints ?: "na"»_«script.polyhedronSolver ?: "na"»_''')
+ "/", '''«script.domain»_«script.solver»_«script.scope»_«script.scopePropagator ?: "na"»_«script.propagatedConstraints ?: "na"»_«script.polyhedronSolver ?: "na"»_«script.scopeHeuristic ?: "na"»_''')
metamodelLoader = switch (script.domain) {
case fs: new FileSystemLoader(inputWorkspace)
case ecore: new EcoreLoader(inputWorkspace)
--
cgit v1.2.3-54-g00ecf
From be4fbe4fb10a27dd07d4139c1962af7c0de436ea Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Thu, 22 Aug 2019 20:43:03 +0200
Subject: Measurements WIP
---
.../ide/.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes
.../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2570 -> 2570 bytes
...licationConfigurationStandaloneRuntimeModule.xtend | 2 +-
.../execution/EclipseBasedProgressMonitor.xtend | 2 +-
.../execution/GenerationTaskExecutor.xtend | 4 ++--
.../application/execution/MetamodelLoader.xtend | 2 +-
.../application/execution/NullWorkspace.xtend | 2 +-
.../execution/PatternLanguageWithRSModule.xtend | 2 +-
.../execution/PatternLanguageWithRSSetup.xtend | 2 +-
.../application/execution/QueryLoader.xtend | 2 +-
.../application/execution/ScopeLoader.xtend | 2 +-
.../application/execution/ScriptConsole.xtend | 8 ++++----
.../application/execution/ScriptExecutor.xtend | 2 +-
.../execution/StandaloneScriptExecutor.xtend | 12 ++++++------
.../util/ApplicationConfigurationParser.xtend | 2 +-
.../application/validation/MetamodelValidator.xtend | 2 +-
.../validation/QueryAndMetamodelValidator.xtend | 2 +-
...pplicationConfigurationValueConverterService.xtend | 2 +-
.../.project | 1 -
.../representations.aird | 2 --
.../cardinality/RelationConstraintCalculator.xtend | 2 +-
.../dse/PartialModelAsLogicInterpretation.xtend | 2 +-
.../viatrasolver/reasoner/dse/ScopeObjective.xtend | 2 +-
...ful_ViatraSolver_polyhedral_typeHierarchy_Clp.json | 5 +++--
24 files changed, 31 insertions(+), 33 deletions(-)
delete mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/representations.aird
(limited to 'Tests/hu.bme.mit.inf.dslreasoner.run')
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
index 22db4093..47676d41 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
index 3ad5d167..e477a075 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfigurationStandaloneRuntimeModule.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfigurationStandaloneRuntimeModule.xtend
index 2738dfff..55e01a4f 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfigurationStandaloneRuntimeModule.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/ApplicationConfigurationStandaloneRuntimeModule.xtend
@@ -50,4 +50,4 @@ class ApplicationConfigurationStandaloneRuntimeModule extends AbstractApplicatio
// def Class extends ITargetPlatformMetamodelLoader> bindITargetPlatformMetamodelLoader() {
// TargetPlatformMetamodelsIndex
// }
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend
index be35b64a..df25151c 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/EclipseBasedProgressMonitor.xtend
@@ -24,4 +24,4 @@ class EclipseBasedProgressMonitor extends SolverProgressMonitor{
super.isCancelled() || internalMonitor.isCanceled
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
index 807d217a..1ee69827 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend
@@ -304,7 +304,7 @@ class GenerationTaskExecutor {
console.flushStatistics
console.writeMessage("Model generation finished")
} catch(Exception e) {
- console.writeError('''
+ console.writeError('''
Error occured («e.class.simpleName»): «e.message»
«FOR s : e.stackTrace SEPARATOR "\n"» «s»«ENDFOR»''')
}
@@ -350,4 +350,4 @@ class GenerationTaskExecutor {
return false
}
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/MetamodelLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/MetamodelLoader.xtend
index 5e7f84f0..626329dc 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/MetamodelLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/MetamodelLoader.xtend
@@ -120,4 +120,4 @@ class MetamodelLoader {
// }
// return res
// }
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend
index 05081581..5e656e8f 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/NullWorkspace.xtend
@@ -59,4 +59,4 @@ class NullWorkspace extends ReasonerWorkspace{
throw new UnsupportedOperationException(message)
}
override refreshFile(String name) { }
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSModule.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSModule.xtend
index 1269ec1f..3e598dd6 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSModule.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSModule.xtend
@@ -43,4 +43,4 @@ class PatternLanguageWithRSModule extends EMFPatternLanguageRuntimeModule{
override Class extends ITypeInferrer> bindITypeInferrer() {
return EMFTypeInferrer;
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSSetup.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSSetup.xtend
index dd5af673..c209cde5 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSSetup.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/PatternLanguageWithRSSetup.xtend
@@ -12,4 +12,4 @@ class PatternLanguageWithRSSetup extends EMFPatternLanguageStandaloneSetup{
override Injector createInjector() {
return Guice::createInjector(new PatternLanguageWithRSModule());
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/QueryLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/QueryLoader.xtend
index cfc91143..5a73845d 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/QueryLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/QueryLoader.xtend
@@ -144,4 +144,4 @@ class QueryLoader {
}
return res
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
index dcaf74cd..6d6ad85e 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScopeLoader.xtend
@@ -220,4 +220,4 @@ class ScopeLoader {
else return specification.exactNumber
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend
index 0f89ba1e..2ce86a78 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptConsole.xtend
@@ -88,7 +88,7 @@ abstract class ScriptConsole {
def writeStatistics(LinkedHashMap statistics) {
if (statisticsWorkspace !== null) {
- val message = '''
+ val message = '''
«FOR key : statistics.keySet SEPARATOR delimier»«key»«ENDFOR»
«FOR value : statistics.values SEPARATOR delimier»«value»«ENDFOR»'''
statisticsWorkspace.writeText(statisticsFileName, message);
@@ -104,11 +104,11 @@ abstract class ScriptConsole {
def flushStatistics() {
if (statisticsWorkspace !== null) {
- val message = '''
+ val message = '''
«FOR key : statisticsHeaderBuffer SEPARATOR delimier»«key»«ENDFOR»
- «FOR line : statisticsDataBuffer»
+ «FOR line : statisticsDataBuffer»
«FOR key : statisticsHeaderBuffer SEPARATOR delimier»«IF line.containsKey(key)»«line.get(key)»«ELSE»«empty»«ENDIF»«ENDFOR»
- «ENDFOR»
+ «ENDFOR»
'''
statisticsWorkspace.writeText(statisticsFileName, message);
statisticsHeaderBuffer.clear
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
index 25036df6..3941179a 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend
@@ -250,4 +250,4 @@ class ScriptExecutor {
}
}
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/StandaloneScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/StandaloneScriptExecutor.xtend
index 4ed57903..42be3ed7 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/StandaloneScriptExecutor.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/StandaloneScriptExecutor.xtend
@@ -71,11 +71,11 @@ class StandaloneScriptExecutor {
throw new IllegalArgumentException(message)
}
} else {
- val message = '''
- The Configuration Script contains «errors.size» error«IF errors.size>1»s«ENDIF»:
- «FOR error : errors»
- «"\t"»«error.message»
- «ENDFOR»
+ val message = '''
+ The Configuration Script contains «errors.size» error«IF errors.size>1»s«ENDIF»:
+ «FOR error : errors»
+ «"\t"»«error.message»
+ «ENDFOR»
'''
throw new IllegalArgumentException(message)
}
@@ -98,4 +98,4 @@ class StandaloneScriptExecutor {
return e.message
}
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend
index ea738c5a..0d11bd31 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/util/ApplicationConfigurationParser.xtend
@@ -15,4 +15,4 @@ class ApplicationConfigurationParser {
throw new IllegalArgumentException('''Content is not an ConfigurationScript! (got: «content.class.simpleName»)''')
}
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.xtend
index fccc433a..f736f6ba 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.xtend
@@ -73,4 +73,4 @@ class MetamodelValidator {
}
}
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.xtend
index e5488e50..7d79bbbb 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.xtend
@@ -49,4 +49,4 @@ class QueryAndMetamodelValidator {
].flatten.filter(ENamedElement)
].flatten
}
-}
\ No newline at end of file
+}
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.xtend
index 433f7148..840ffb09 100644
--- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.xtend
+++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.xtend
@@ -11,4 +11,4 @@ class ApplicationConfigurationValueConverterService extends DefaultTerminalConve
def IValueConverter QualifiedName() {
converter2
}
-}
\ No newline at end of file
+}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/.project b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/.project
index e594a173..16db5fc5 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/.project
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/.project
@@ -32,7 +32,6 @@
- org.eclipse.sirius.nature.modelingproject
org.eclipse.jdt.core.javanature
org.eclipse.pde.PluginNature
org.eclipse.viatra.query.projectnature
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/representations.aird b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/representations.aird
deleted file mode 100644
index efa8e366..00000000
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/representations.aird
+++ /dev/null
@@ -1,2 +0,0 @@
-
-
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
index 013e53e1..c92260ea 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
@@ -44,7 +44,7 @@ class RelationMultiplicityConstraint {
}
def constrainsUnrepairable() {
- constrainsUnfinished && canHaveMultipleSourcesPerTarget
+ constrainsUnfinished && canHaveMultipleSourcesPerTarget && false
}
def constrainsRemainingInverse() {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
index f61c7333..b63bfe8b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -163,4 +163,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
override getAllStringsInStructure() {
new TreeSet(this.stringForwardTrace.keySet)
}
-}
\ No newline at end of file
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
index e7967b00..69a734f8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -41,4 +41,4 @@ class ScopeObjective implements IObjective{
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getLevel() { 2 }
-}
\ No newline at end of file
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
index 5f8a01b1..b4d51684 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
@@ -3,14 +3,15 @@
"outputPath": "outputModels",
"timeout": 1200,
"saveModels": false,
+ "saveTemporaryFiles": true,
"warmupIterations": 0,
"iterations": 5,
"domain": "Yakindu",
- "scope": "quantiles",
+ "scope": "none",
"sizes": [100],
"solver": "ViatraSolver",
"scopePropagator": "polyhedral",
"propagatedConstraints": "hints",
"polyhedronSolver": "Clp",
- "scopeHeuristic": "basic"
+ "scopeHeuristic": "polyhedral"
}
--
cgit v1.2.3-54-g00ecf
From 1f5cab77334817776618092501628ed70368dd6e Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Fri, 30 Aug 2019 15:52:45 +0200
Subject: FAM metamodel loader experiments
---
.../ide/.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes
.../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2570 -> 2570 bytes
...ful_ViatraSolver_polyhedral_typeHierarchy_Clp.json | 7 +++++--
.../bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend | 15 ++++++++-------
4 files changed, 13 insertions(+), 9 deletions(-)
(limited to 'Tests/hu.bme.mit.inf.dslreasoner.run')
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
index 47676d41..8925abcb 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
index e477a075..2b883b66 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
index 26df3c74..1e2d4dd4 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
@@ -4,10 +4,13 @@
"timeout": 1200,
"saveModels": true,
"warmupIterations": 0,
- "iterations": 1,
+ "iterations": 5,
"domain": "FAM",
"scope": "none",
"sizes": [500],
"solver": "ViatraSolver",
- "scopePropagator": "basic"
+ "scopePropagator": "polyhedral",
+ "propagatedConstraints": "hints",
+ "polyhedronSolver": "Clp",
+ "scopeHeuristics": "polyhedral"
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
index 4b0791d4..1be03eed 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
@@ -85,8 +85,9 @@ class FAMLoader extends MetamodelLoader {
val List classes = package.EClassifiers.filter(EClass).toList
val List enums = package.EClassifiers.filter(EEnum).toList
val List literals = enums.map[ELiterals].flatten.toList
- val List references = classes.map[EReferences].flatten.filter[name != "type" && name != "model"].
- toList
+ val List references = classes.map[EReferences].flatten.filter [ reference |
+ !#{"model", "type"}.contains(reference.name)
+ ].toList
val List attributes = classes.map[EAttributes].flatten.toList
return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)
}
@@ -196,7 +197,7 @@ class YakinduLoader extends MetamodelLoader {
}
override additionalConstraints() {
- //#[[method|new SGraphInconsistencyDetector(method)]]
+ // #[[method|new SGraphInconsistencyDetector(method)]]
emptyList
}
@@ -261,7 +262,7 @@ class FileSystemLoader extends MetamodelLoader {
}
override additionalConstraints() {
- //#[[method|new FileSystemInconsistencyDetector(method)]]
+ // #[[method|new FileSystemInconsistencyDetector(method)]]
emptyList
}
@@ -386,11 +387,11 @@ class SatelliteLoader extends MetamodelLoader {
}
override additionalConstraints() { #[] }
-
+
override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
#[new SatelliteHint(ecore2Logic, trace)]
}
-
+
override getTypeQuantiles() {
#{
"CubeSat3U" -> new TypeQuantiles(0.1, 0.25),
@@ -402,5 +403,5 @@ class SatelliteLoader extends MetamodelLoader {
"InterferometryPayload" -> new TypeQuantiles(0.15, 0.25)
}
}
-
+
}
--
cgit v1.2.3-54-g00ecf
From 78b145df05795a71bef18c73526b0c8ff6a53e7e Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Tue, 29 Oct 2019 17:33:59 +0100
Subject: MeasurementScriptRunner fix
---
.../.classpath | 7 +++-
.../build.properties | 3 +-
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 7 ++--
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 6 +--
.../run/script/MeasurementScriptRunner.xtend | 47 ++++++++++++++++------
5 files changed, 48 insertions(+), 22 deletions(-)
(limited to 'Tests/hu.bme.mit.inf.dslreasoner.run')
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/.classpath b/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/.classpath
index 4a3597ed..e7847821 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/.classpath
+++ b/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/.classpath
@@ -1,9 +1,12 @@
-
+
+
+
+
+
-
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/build.properties b/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/build.properties
index ce900fd9..e1651110 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/build.properties
+++ b/Tests/hu.bme.mit.inf.dslreasoner.application.FAMTest/build.properties
@@ -3,6 +3,5 @@ bin.includes = META-INF/,\
additional.bundles = org.apache.log4j,\
org.junit
source.. = src/,\
- xtend-gen/,\
- src-gen/
+ xtend-gen/
output.. = bin/
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
index 42073422..72e97957 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
@@ -7,9 +7,10 @@
"iterations": 5,
"domain": "ecore",
"scope": "quantiles",
- "sizes": [100],
+ "sizes": [50],
"solver": "ViatraSolver",
"scopePropagator": "polyhedral",
- "propagatedConstraints": "relations",
- "polyhedronSolver": "Clp"
+ "propagatedConstraints": "hints",
+ "polyhedronSolver": "Clp",
+ "scopeHeuristic": "polyhedral"
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
index 474962e7..d5469948 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
@@ -1,14 +1,14 @@
{
"inputPath": "initialModels",
"outputPath": "outputModels",
- "timeout": 1200,
+ "timeout": 120,
"saveModels": true,
"saveTemporaryFiles": true,
"warmupIterations": 0,
"iterations": 1,
- "domain": "satellite",
+ "domain": "Yakindu",
"scope": "quantiles",
- "sizes": [50],
+ "sizes": [10, 20, 30, 40, 50, 60, 70, 80, 90, 100],
"solver": "ViatraSolver",
"scopePropagator": "polyhedral",
"propagatedConstraints": "hints",
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
index bfbbf329..1127f01a 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
@@ -1,11 +1,14 @@
package hu.bme.mit.inf.dslreasoner.run.script
import com.google.gson.Gson
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
import hu.bme.mit.inf.dslreasoner.ecore2logic.EClassMapper
import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
@@ -138,12 +141,10 @@ class MeasurementScriptRunner {
Thread.sleep(800)
}
- private def runExperiment(int modelSize) {
- if (script.solver != Solver.ViatraSolver) {
- throw new IllegalArgumentException("Only VIATRA-Generator is supported")
- }
+ private def createViatraConfig() {
val config = new ViatraReasonerConfiguration
- config.solutionScope.numberOfRequiredSolutions = 1
+ config.debugConfiguration.partialInterpretatioVisualiser = null
+ config.searchSpaceConstraints.additionalGlobalConstraints += metamodelLoader.additionalConstraints
config.scopePropagatorStrategy = switch (script.scopePropagator) {
case none:
ScopePropagatorStrategy.None
@@ -187,11 +188,28 @@ class MeasurementScriptRunner {
default:
throw new IllegalArgumentException("Unknown scope propagator: " + script.scopePropagator)
}
+ config
+ }
+
+ private def createAlloyConfig() {
+ val config = new AlloySolverConfiguration
+ config
+ }
+
+ private def createConfig(int modelSize) {
+ val config = switch (solver : script.solver) {
+ case ViatraSolver: createViatraConfig()
+ case AlloySolver: createAlloyConfig()
+ default: throw new IllegalArgumentException("Unknown solver: " + solver)
+ }
+ config.solutionScope.numberOfRequiredSolutions = 1
config.runtimeLimit = script.timeout
config.documentationLevel = if(script.saveTemporaryFiles) DocumentationLevel.NORMAL else DocumentationLevel.NONE
- config.debugConfiguration.partialInterpretatioVisualiser = null
- config.searchSpaceConstraints.additionalGlobalConstraints += metamodelLoader.additionalConstraints
+ config
+ }
+ private def runExperiment(int modelSize) {
+ val config = createConfig(modelSize)
val modelLoadingStart = System.nanoTime
val metamodelDescriptor = metamodelLoader.loadMetamodel
val partialModelDescriptor = metamodelLoader.loadPartialModel
@@ -214,8 +232,8 @@ class MeasurementScriptRunner {
new Viatra2LogicConfiguration
).output
initializeScope(config, modelSize, problem, ecore2Logic, modelGeneration.trace)
- if (script.propagatedConstraints == ScopeConstraints.hints) {
- config.hints = metamodelLoader.getHints(ecore2Logic, modelGeneration.trace)
+ if (config instanceof ViatraReasonerConfiguration && script.propagatedConstraints == ScopeConstraints.hints) {
+ (config as ViatraReasonerConfiguration).hints = metamodelLoader.getHints(ecore2Logic, modelGeneration.trace)
}
val domain2LogicTransformationTime = System.nanoTime - domain2LogicTransformationStart
@@ -223,7 +241,11 @@ class MeasurementScriptRunner {
outputWorkspace.writeModel(problem, "initial.logicproblem")
}
- val solver = new ViatraReasoner
+ val solver = switch (solver : script.solver) {
+ case ViatraSolver: new ViatraReasoner
+ case AlloySolver: new AlloySolver
+ default: throw new IllegalArgumentException("Unknown solver: " + solver)
+ }
val result = solver.solve(problem, config, outputWorkspace)
val statistics = result.statistics
statistics.entries += createIntStatisticEntry => [
@@ -253,7 +275,7 @@ class MeasurementScriptRunner {
new ExperimentResult(result.class.simpleName, statistics, modelResult)
}
- private def initializeScope(ViatraReasonerConfiguration config, int modelSize, LogicProblem problem,
+ private def initializeScope(LogicSolverConfiguration config, int modelSize, LogicProblem problem,
EClassMapper eClassMapper, Ecore2Logic_Trace trace) {
val knownElements = initializeKnownElements(problem, config.typeScopes)
if (modelSize < 0) {
@@ -278,7 +300,8 @@ class MeasurementScriptRunner {
val currentCount = if(knownInstances === null) 0 else knownInstances.size
val lowCount = Math.floor(modelSize * quantile.low) as int
val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int
- config.typeScopes.minNewElementsByType.put(type, lowCount - currentCount)
+// println('''«type.name» «lowCount» «highCount»''')
+ config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0))
config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount)
}
}
--
cgit v1.2.3-54-g00ecf
From 6a3ff9bb588bf47242a56b91e35479dbba38eb19 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Thu, 7 May 2020 17:26:07 +0200
Subject: Scope unsat benchmarks
---
.../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes
.../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2570 -> 2526 bytes
.../Examples/ModelGenExampleFAM_plugin/.project | 6 +
.../Examples/ModelGenExampleFAM_plugin/plugin.xml | 18 +-
.../dslreasoner/domains/alloyexamples/Ecore.vql | 10 +
.../plugin.xml | 2 +
.../dslreasoner/domains/alloyexamples/.gitignore | 5 +
.../alloyexamples/Unsat_loopInInheritance.java | 566 +++++++++++++++++
.../domains/alloyexamples/Unsat_subpackage.java | 704 +++++++++++++++++++++
.../domains/alloyexamples/internal/.gitignore | 4 +
.../plugin.xml | 12 +-
.../domains/satellite/queries/SatelliteQueries.vql | 13 +
.../plugin.xml | 1 +
.../partialsnapshot_mavo/yakindu/patterns.vql | 11 +
.../.classpath | 26 +-
.../META-INF/MANIFEST.MF | 7 +-
.../NeighbourhoodBasedStateCoderFactory.xtend | 9 +-
.../reasoner/ViatraReasonerConfiguration.xtend | 2 +-
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 16 -
.../configs/Yakindu.json | 13 +
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 17 -
.../configs/ecore.json | 17 +
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 16 -
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 16 -
.../configs/satellite.json | 17 +
..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 17 -
.../mit/inf/dslreasoner/run/MetamodelLoader.xtend | 63 +-
.../dslreasoner/run/script/MeasurementScript.xtend | 13 +-
.../run/script/MeasurementScriptRunner.xtend | 46 +-
29 files changed, 1511 insertions(+), 136 deletions(-)
create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_loopInInheritance.java
create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_subpackage.java
create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/internal/.gitignore
delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json
delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json
delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json
delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
(limited to 'Tests/hu.bme.mit.inf.dslreasoner.run')
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
index 83195553..c8086733 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
index f5085470..1a907776 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ
diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/.project b/Domains/Examples/ModelGenExampleFAM_plugin/.project
index 6e1b3a06..570f8a60 100644
--- a/Domains/Examples/ModelGenExampleFAM_plugin/.project
+++ b/Domains/Examples/ModelGenExampleFAM_plugin/.project
@@ -5,6 +5,11 @@
+
+ org.eclipse.xtext.ui.shared.xtextBuilder
+
+
+
org.eclipse.viatra.query.tooling.ui.projectbuilder
@@ -30,5 +35,6 @@
org.eclipse.jdt.core.javanature
org.eclipse.viatra.query.projectnature
org.eclipse.pde.PluginNature
+ org.eclipse.xtext.ui.shared.xtextNature
diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml b/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml
index c117a28e..8d99d401 100644
--- a/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml
+++ b/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml
@@ -5,23 +5,13 @@
-
-
-
-
+
+
+
+
-
-
-
-
-
-
-
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Ecore.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Ecore.vql
index 78525a35..16c24d05 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Ecore.vql
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Ecore.vql
@@ -11,6 +11,16 @@ pattern loopInInheritence(a: EClass) {
find directSupertype+(a,a);
}
+pattern unsat_subpackage(a: EPackage, b: EPackage) {
+ EPackage.eSubpackages(a, b);
+}
+
+@Constraint(key={p}, severity="error", message="error")
+pattern unsat_loopInInheritance(p: EPackage) {
+ neg find unsat_subpackage(_, p);
+ neg find loopInInheritence(_);
+}
+
pattern opposite(a:EReference, b: EReference) {
EReference.eOpposite(a,b);
}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/plugin.xml
index 6eae8535..eddd482c 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/plugin.xml
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/plugin.xml
@@ -11,6 +11,8 @@
+
+
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/.gitignore b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/.gitignore
index 0f8c77a1..70eab455 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/.gitignore
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/.gitignore
@@ -54,3 +54,8 @@
/.RootIsNotDir.java._trace
/Dir.java
/RootIsNotDir.java
+/.Unsat_loopInInheritance.java._trace
+/.Subpackage.java._trace
+/.Unsat_subpackage.java._trace
+/.Unsat_subpackageOrSelf.java._trace
+/.Unsat_topLevelPackageWithLoop.java._trace
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_loopInInheritance.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_loopInInheritance.java
new file mode 100644
index 00000000..83bd0f66
--- /dev/null
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_loopInInheritance.java
@@ -0,0 +1,566 @@
+/**
+ * Generated from platform:/resource/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Ecore.vql
+ */
+package hu.bme.mit.inf.dslreasoner.domains.alloyexamples;
+
+import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.LoopInInheritence;
+import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Unsat_subpackage;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Objects;
+import java.util.Optional;
+import java.util.Set;
+import java.util.function.Consumer;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+import org.apache.log4j.Logger;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EPackage;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFPQuery;
+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.impl.BaseMatcher;
+import org.eclipse.viatra.query.runtime.api.impl.BasePatternMatch;
+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey;
+import org.eclipse.viatra.query.runtime.matchers.backend.QueryEvaluationHint;
+import org.eclipse.viatra.query.runtime.matchers.psystem.PBody;
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable;
+import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
+import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.ParameterReference;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;
+import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil;
+
+/**
+ * A pattern-specific query specification that can instantiate Matcher in a type-safe way.
+ *
+ * Original source:
+ *
+ * {@literal @}Constraint(key={p}, severity="error", message="error")
+ * pattern unsat_loopInInheritance(p: EPackage) {
+ * neg find unsat_subpackage(_, p);
+ * neg find loopInInheritence(_);
+ * }
+ *
+ *
+ * @see Matcher
+ * @see Match
+ *
+ */
+@SuppressWarnings("all")
+public final class Unsat_loopInInheritance extends BaseGeneratedEMFQuerySpecification {
+ /**
+ * Pattern-specific match representation of the hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_loopInInheritance pattern,
+ * to be used in conjunction with {@link Matcher}.
+ *
+ * Class fields correspond to parameters of the pattern. Fields with value null are considered unassigned.
+ * Each instance is a (possibly partial) substitution of pattern parameters,
+ * usable to represent a match of the pattern in the result of a query,
+ * or to specify the bound (fixed) input parameters when issuing a query.
+ *
+ * @see Matcher
+ *
+ */
+ public static abstract class Match extends BasePatternMatch {
+ private EPackage fP;
+
+ private static List parameterNames = makeImmutableList("p");
+
+ private Match(final EPackage pP) {
+ this.fP = pP;
+ }
+
+ @Override
+ public Object get(final String parameterName) {
+ switch(parameterName) {
+ case "p": return this.fP;
+ default: return null;
+ }
+ }
+
+ @Override
+ public Object get(final int index) {
+ switch(index) {
+ case 0: return this.fP;
+ default: return null;
+ }
+ }
+
+ public EPackage getP() {
+ return this.fP;
+ }
+
+ @Override
+ public boolean set(final String parameterName, final Object newValue) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ if ("p".equals(parameterName) ) {
+ this.fP = (EPackage) newValue;
+ return true;
+ }
+ return false;
+ }
+
+ public void setP(final EPackage pP) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ this.fP = pP;
+ }
+
+ @Override
+ public String patternName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_loopInInheritance";
+ }
+
+ @Override
+ public List parameterNames() {
+ return Unsat_loopInInheritance.Match.parameterNames;
+ }
+
+ @Override
+ public Object[] toArray() {
+ return new Object[]{fP};
+ }
+
+ @Override
+ public Unsat_loopInInheritance.Match toImmutable() {
+ return isMutable() ? newMatch(fP) : this;
+ }
+
+ @Override
+ public String prettyPrint() {
+ StringBuilder result = new StringBuilder();
+ result.append("\"p\"=" + prettyPrintValue(fP));
+ return result.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(fP);
+ }
+
+ @Override
+ public boolean equals(final Object obj) {
+ if (this == obj)
+ return true;
+ if (obj == null) {
+ return false;
+ }
+ if ((obj instanceof Unsat_loopInInheritance.Match)) {
+ Unsat_loopInInheritance.Match other = (Unsat_loopInInheritance.Match) obj;
+ return Objects.equals(fP, other.fP);
+ } else {
+ // this should be infrequent
+ if (!(obj instanceof IPatternMatch)) {
+ return false;
+ }
+ IPatternMatch otherSig = (IPatternMatch) obj;
+ return Objects.equals(specification(), otherSig.specification()) && Arrays.deepEquals(toArray(), otherSig.toArray());
+ }
+ }
+
+ @Override
+ public Unsat_loopInInheritance specification() {
+ return Unsat_loopInInheritance.instance();
+ }
+
+ /**
+ * Returns an empty, mutable match.
+ * Fields of the mutable match can be filled to create a partial match, usable as matcher input.
+ *
+ * @return the empty match.
+ *
+ */
+ public static Unsat_loopInInheritance.Match newEmptyMatch() {
+ return new Mutable(null);
+ }
+
+ /**
+ * Returns a mutable (partial) match.
+ * Fields of the mutable match can be filled to create a partial match, usable as matcher input.
+ *
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return the new, mutable (partial) match object.
+ *
+ */
+ public static Unsat_loopInInheritance.Match newMutableMatch(final EPackage pP) {
+ return new Mutable(pP);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public static Unsat_loopInInheritance.Match newMatch(final EPackage pP) {
+ return new Immutable(pP);
+ }
+
+ private static final class Mutable extends Unsat_loopInInheritance.Match {
+ Mutable(final EPackage pP) {
+ super(pP);
+ }
+
+ @Override
+ public boolean isMutable() {
+ return true;
+ }
+ }
+
+ private static final class Immutable extends Unsat_loopInInheritance.Match {
+ Immutable(final EPackage pP) {
+ super(pP);
+ }
+
+ @Override
+ public boolean isMutable() {
+ return false;
+ }
+ }
+ }
+
+ /**
+ * Generated pattern matcher API of the hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_loopInInheritance pattern,
+ * providing pattern-specific query methods.
+ *
+ *
Use the pattern matcher on a given model via {@link #on(ViatraQueryEngine)},
+ * e.g. in conjunction with {@link ViatraQueryEngine#on(QueryScope)}.
+ *
+ *
Matches of the pattern will be represented as {@link Match}.
+ *
+ *
Original source:
+ *
+ * {@literal @}Constraint(key={p}, severity="error", message="error")
+ * pattern unsat_loopInInheritance(p: EPackage) {
+ * neg find unsat_subpackage(_, p);
+ * neg find loopInInheritence(_);
+ * }
+ *
+ *
+ * @see Match
+ * @see Unsat_loopInInheritance
+ *
+ */
+ public static class Matcher extends BaseMatcher {
+ /**
+ * Initializes the pattern matcher within an existing VIATRA Query engine.
+ * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.
+ *
+ * @param engine the existing VIATRA Query engine in which this matcher will be created.
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ *
+ */
+ public static Unsat_loopInInheritance.Matcher on(final ViatraQueryEngine engine) {
+ // check if matcher already exists
+ Matcher matcher = engine.getExistingMatcher(querySpecification());
+ if (matcher == null) {
+ matcher = (Matcher)engine.getMatcher(querySpecification());
+ }
+ return matcher;
+ }
+
+ /**
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ * @return an initialized matcher
+ * @noreference This method is for internal matcher initialization by the framework, do not call it manually.
+ *
+ */
+ public static Unsat_loopInInheritance.Matcher create() {
+ return new Matcher();
+ }
+
+ private static final int POSITION_P = 0;
+
+ private static final Logger LOGGER = ViatraQueryLoggingUtil.getLogger(Unsat_loopInInheritance.Matcher.class);
+
+ /**
+ * Initializes the pattern matcher within an existing VIATRA Query engine.
+ * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.
+ *
+ * @param engine the existing VIATRA Query engine in which this matcher will be created.
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ *
+ */
+ private Matcher() {
+ super(querySpecification());
+ }
+
+ /**
+ * Returns the set of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return matches represented as a Match object.
+ *
+ */
+ public Collection getAllMatches(final EPackage pP) {
+ return rawStreamAllMatches(new Object[]{pP}).collect(Collectors.toSet());
+ }
+
+ /**
+ * Returns a stream of all matches of the pattern that conform to the given fixed values of some parameters.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return a stream of matches represented as a Match object.
+ *
+ */
+ public Stream streamAllMatches(final EPackage pP) {
+ return rawStreamAllMatches(new Object[]{pP});
+ }
+
+ /**
+ * Returns an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return a match represented as a Match object, or null if no match is found.
+ *
+ */
+ public Optional getOneArbitraryMatch(final EPackage pP) {
+ return rawGetOneArbitraryMatch(new Object[]{pP});
+ }
+
+ /**
+ * Indicates whether the given combination of specified pattern parameters constitute a valid pattern match,
+ * under any possible substitution of the unspecified parameters (if any).
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return true if the input is a valid (partial) match of the pattern.
+ *
+ */
+ public boolean hasMatch(final EPackage pP) {
+ return rawHasMatch(new Object[]{pP});
+ }
+
+ /**
+ * Returns the number of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return the number of pattern matches found.
+ *
+ */
+ public int countMatches(final EPackage pP) {
+ return rawCountMatches(new Object[]{pP});
+ }
+
+ /**
+ * Executes the given processor on an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @param processor the action that will process the selected match.
+ * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked
+ *
+ */
+ public boolean forOneArbitraryMatch(final EPackage pP, final Consumer super Unsat_loopInInheritance.Match> processor) {
+ return rawForOneArbitraryMatch(new Object[]{pP}, processor);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pP the fixed value of pattern parameter p, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public Unsat_loopInInheritance.Match newMatch(final EPackage pP) {
+ return Unsat_loopInInheritance.Match.newMatch(pP);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for p.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ protected Stream rawStreamAllValuesOfp(final Object[] parameters) {
+ return rawStreamAllValues(POSITION_P, parameters).map(EPackage.class::cast);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for p.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfp() {
+ return rawStreamAllValuesOfp(emptyArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for p.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfp() {
+ return rawStreamAllValuesOfp(emptyArray());
+ }
+
+ @Override
+ protected Unsat_loopInInheritance.Match tupleToMatch(final Tuple t) {
+ try {
+ return Unsat_loopInInheritance.Match.newMatch((EPackage) t.get(POSITION_P));
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in tuple not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected Unsat_loopInInheritance.Match arrayToMatch(final Object[] match) {
+ try {
+ return Unsat_loopInInheritance.Match.newMatch((EPackage) match[POSITION_P]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected Unsat_loopInInheritance.Match arrayToMatchMutable(final Object[] match) {
+ try {
+ return Unsat_loopInInheritance.Match.newMutableMatch((EPackage) match[POSITION_P]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ /**
+ * @return the singleton instance of the query specification of this pattern
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static IQuerySpecification querySpecification() {
+ return Unsat_loopInInheritance.instance();
+ }
+ }
+
+ private Unsat_loopInInheritance() {
+ super(GeneratedPQuery.INSTANCE);
+ }
+
+ /**
+ * @return the singleton instance of the query specification
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static Unsat_loopInInheritance instance() {
+ try{
+ return LazyHolder.INSTANCE;
+ } catch (ExceptionInInitializerError err) {
+ throw processInitializerError(err);
+ }
+ }
+
+ @Override
+ protected Unsat_loopInInheritance.Matcher instantiate(final ViatraQueryEngine engine) {
+ return Unsat_loopInInheritance.Matcher.on(engine);
+ }
+
+ @Override
+ public Unsat_loopInInheritance.Matcher instantiate() {
+ return Unsat_loopInInheritance.Matcher.create();
+ }
+
+ @Override
+ public Unsat_loopInInheritance.Match newEmptyMatch() {
+ return Unsat_loopInInheritance.Match.newEmptyMatch();
+ }
+
+ @Override
+ public Unsat_loopInInheritance.Match newMatch(final Object... parameters) {
+ return Unsat_loopInInheritance.Match.newMatch((org.eclipse.emf.ecore.EPackage) parameters[0]);
+ }
+
+ /**
+ * Inner class allowing the singleton instance of {@link Unsat_loopInInheritance} to be created
+ * not at the class load time of the outer class,
+ * but rather at the first call to {@link Unsat_loopInInheritance#instance()}.
+ *
+ * This workaround is required e.g. to support recursion.
+ *
+ */
+ private static class LazyHolder {
+ private static final Unsat_loopInInheritance INSTANCE = new Unsat_loopInInheritance();
+
+ /**
+ * Statically initializes the query specification after the field {@link #INSTANCE} is assigned.
+ * This initialization order is required to support indirect recursion.
+ *
+ *
The static initializer is defined using a helper field to work around limitations of the code generator.
+ *
+ */
+ private static final Object STATIC_INITIALIZER = ensureInitialized();
+
+ public static Object ensureInitialized() {
+ INSTANCE.ensureInitializedInternal();
+ return null;
+ }
+ }
+
+ private static class GeneratedPQuery extends BaseGeneratedEMFPQuery {
+ private static final Unsat_loopInInheritance.GeneratedPQuery INSTANCE = new GeneratedPQuery();
+
+ private final PParameter parameter_p = new PParameter("p", "org.eclipse.emf.ecore.EPackage", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.eclipse.org/emf/2002/Ecore", "EPackage")), PParameterDirection.INOUT);
+
+ private final List parameters = Arrays.asList(parameter_p);
+
+ private GeneratedPQuery() {
+ super(PVisibility.PUBLIC);
+ }
+
+ @Override
+ public String getFullyQualifiedName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_loopInInheritance";
+ }
+
+ @Override
+ public List getParameterNames() {
+ return Arrays.asList("p");
+ }
+
+ @Override
+ public List getParameters() {
+ return parameters;
+ }
+
+ @Override
+ public Set doGetContainedBodies() {
+ setEvaluationHints(new QueryEvaluationHint(null, QueryEvaluationHint.BackendRequirement.UNSPECIFIED));
+ Set bodies = new LinkedHashSet<>();
+ {
+ PBody body = new PBody(this);
+ PVariable var_p = body.getOrCreateVariableByName("p");
+ PVariable var___0_ = body.getOrCreateVariableByName("_<0>");
+ PVariable var___1_ = body.getOrCreateVariableByName("_<1>");
+ new TypeConstraint(body, Tuples.flatTupleOf(var_p), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.eclipse.org/emf/2002/Ecore", "EPackage")));
+ body.setSymbolicParameters(Arrays.asList(
+ new ExportedParameter(body, var_p, parameter_p)
+ ));
+ // neg find unsat_subpackage(_, p)
+ new NegativePatternCall(body, Tuples.flatTupleOf(var___0_, var_p), Unsat_subpackage.instance().getInternalQueryRepresentation());
+ // neg find loopInInheritence(_)
+ new NegativePatternCall(body, Tuples.flatTupleOf(var___1_), LoopInInheritence.instance().getInternalQueryRepresentation());
+ bodies.add(body);
+ }
+ {
+ PAnnotation annotation = new PAnnotation("Constraint");
+ annotation.addAttribute("key", Arrays.asList(new Object[] {
+ new ParameterReference("p")
+ }));
+ annotation.addAttribute("severity", "error");
+ annotation.addAttribute("message", "error");
+ addAnnotation(annotation);
+ }
+ return bodies;
+ }
+ }
+}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_subpackage.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_subpackage.java
new file mode 100644
index 00000000..a9c8aed8
--- /dev/null
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Unsat_subpackage.java
@@ -0,0 +1,704 @@
+/**
+ * Generated from platform:/resource/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/Ecore.vql
+ */
+package hu.bme.mit.inf.dslreasoner.domains.alloyexamples;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Objects;
+import java.util.Optional;
+import java.util.Set;
+import java.util.function.Consumer;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+import org.apache.log4j.Logger;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EPackage;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFPQuery;
+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.impl.BaseMatcher;
+import org.eclipse.viatra.query.runtime.api.impl.BasePatternMatch;
+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey;
+import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey;
+import org.eclipse.viatra.query.runtime.matchers.backend.QueryEvaluationHint;
+import org.eclipse.viatra.query.runtime.matchers.psystem.PBody;
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;
+import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil;
+
+/**
+ * A pattern-specific query specification that can instantiate Matcher in a type-safe way.
+ *
+ * Original source:
+ *
+ * pattern unsat_subpackage(a: EPackage, b: EPackage) {
+ * EPackage.eSubpackages(a, b);
+ * }
+ *
+ *
+ * @see Matcher
+ * @see Match
+ *
+ */
+@SuppressWarnings("all")
+public final class Unsat_subpackage extends BaseGeneratedEMFQuerySpecification {
+ /**
+ * Pattern-specific match representation of the hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_subpackage pattern,
+ * to be used in conjunction with {@link Matcher}.
+ *
+ * Class fields correspond to parameters of the pattern. Fields with value null are considered unassigned.
+ * Each instance is a (possibly partial) substitution of pattern parameters,
+ * usable to represent a match of the pattern in the result of a query,
+ * or to specify the bound (fixed) input parameters when issuing a query.
+ *
+ * @see Matcher
+ *
+ */
+ public static abstract class Match extends BasePatternMatch {
+ private EPackage fA;
+
+ private EPackage fB;
+
+ private static List parameterNames = makeImmutableList("a", "b");
+
+ private Match(final EPackage pA, final EPackage pB) {
+ this.fA = pA;
+ this.fB = pB;
+ }
+
+ @Override
+ public Object get(final String parameterName) {
+ switch(parameterName) {
+ case "a": return this.fA;
+ case "b": return this.fB;
+ default: return null;
+ }
+ }
+
+ @Override
+ public Object get(final int index) {
+ switch(index) {
+ case 0: return this.fA;
+ case 1: return this.fB;
+ default: return null;
+ }
+ }
+
+ public EPackage getA() {
+ return this.fA;
+ }
+
+ public EPackage getB() {
+ return this.fB;
+ }
+
+ @Override
+ public boolean set(final String parameterName, final Object newValue) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ if ("a".equals(parameterName) ) {
+ this.fA = (EPackage) newValue;
+ return true;
+ }
+ if ("b".equals(parameterName) ) {
+ this.fB = (EPackage) newValue;
+ return true;
+ }
+ return false;
+ }
+
+ public void setA(final EPackage pA) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ this.fA = pA;
+ }
+
+ public void setB(final EPackage pB) {
+ if (!isMutable()) throw new java.lang.UnsupportedOperationException();
+ this.fB = pB;
+ }
+
+ @Override
+ public String patternName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_subpackage";
+ }
+
+ @Override
+ public List parameterNames() {
+ return Unsat_subpackage.Match.parameterNames;
+ }
+
+ @Override
+ public Object[] toArray() {
+ return new Object[]{fA, fB};
+ }
+
+ @Override
+ public Unsat_subpackage.Match toImmutable() {
+ return isMutable() ? newMatch(fA, fB) : this;
+ }
+
+ @Override
+ public String prettyPrint() {
+ StringBuilder result = new StringBuilder();
+ result.append("\"a\"=" + prettyPrintValue(fA) + ", ");
+ result.append("\"b\"=" + prettyPrintValue(fB));
+ return result.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(fA, fB);
+ }
+
+ @Override
+ public boolean equals(final Object obj) {
+ if (this == obj)
+ return true;
+ if (obj == null) {
+ return false;
+ }
+ if ((obj instanceof Unsat_subpackage.Match)) {
+ Unsat_subpackage.Match other = (Unsat_subpackage.Match) obj;
+ return Objects.equals(fA, other.fA) && Objects.equals(fB, other.fB);
+ } else {
+ // this should be infrequent
+ if (!(obj instanceof IPatternMatch)) {
+ return false;
+ }
+ IPatternMatch otherSig = (IPatternMatch) obj;
+ return Objects.equals(specification(), otherSig.specification()) && Arrays.deepEquals(toArray(), otherSig.toArray());
+ }
+ }
+
+ @Override
+ public Unsat_subpackage specification() {
+ return Unsat_subpackage.instance();
+ }
+
+ /**
+ * Returns an empty, mutable match.
+ * Fields of the mutable match can be filled to create a partial match, usable as matcher input.
+ *
+ * @return the empty match.
+ *
+ */
+ public static Unsat_subpackage.Match newEmptyMatch() {
+ return new Mutable(null, null);
+ }
+
+ /**
+ * Returns a mutable (partial) match.
+ * Fields of the mutable match can be filled to create a partial match, usable as matcher input.
+ *
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return the new, mutable (partial) match object.
+ *
+ */
+ public static Unsat_subpackage.Match newMutableMatch(final EPackage pA, final EPackage pB) {
+ return new Mutable(pA, pB);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public static Unsat_subpackage.Match newMatch(final EPackage pA, final EPackage pB) {
+ return new Immutable(pA, pB);
+ }
+
+ private static final class Mutable extends Unsat_subpackage.Match {
+ Mutable(final EPackage pA, final EPackage pB) {
+ super(pA, pB);
+ }
+
+ @Override
+ public boolean isMutable() {
+ return true;
+ }
+ }
+
+ private static final class Immutable extends Unsat_subpackage.Match {
+ Immutable(final EPackage pA, final EPackage pB) {
+ super(pA, pB);
+ }
+
+ @Override
+ public boolean isMutable() {
+ return false;
+ }
+ }
+ }
+
+ /**
+ * Generated pattern matcher API of the hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_subpackage pattern,
+ * providing pattern-specific query methods.
+ *
+ *
Use the pattern matcher on a given model via {@link #on(ViatraQueryEngine)},
+ * e.g. in conjunction with {@link ViatraQueryEngine#on(QueryScope)}.
+ *
+ *
Matches of the pattern will be represented as {@link Match}.
+ *
+ *
Original source:
+ *
+ * pattern unsat_subpackage(a: EPackage, b: EPackage) {
+ * EPackage.eSubpackages(a, b);
+ * }
+ *
+ *
+ * @see Match
+ * @see Unsat_subpackage
+ *
+ */
+ public static class Matcher extends BaseMatcher {
+ /**
+ * Initializes the pattern matcher within an existing VIATRA Query engine.
+ * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.
+ *
+ * @param engine the existing VIATRA Query engine in which this matcher will be created.
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ *
+ */
+ public static Unsat_subpackage.Matcher on(final ViatraQueryEngine engine) {
+ // check if matcher already exists
+ Matcher matcher = engine.getExistingMatcher(querySpecification());
+ if (matcher == null) {
+ matcher = (Matcher)engine.getMatcher(querySpecification());
+ }
+ return matcher;
+ }
+
+ /**
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ * @return an initialized matcher
+ * @noreference This method is for internal matcher initialization by the framework, do not call it manually.
+ *
+ */
+ public static Unsat_subpackage.Matcher create() {
+ return new Matcher();
+ }
+
+ private static final int POSITION_A = 0;
+
+ private static final int POSITION_B = 1;
+
+ private static final Logger LOGGER = ViatraQueryLoggingUtil.getLogger(Unsat_subpackage.Matcher.class);
+
+ /**
+ * Initializes the pattern matcher within an existing VIATRA Query engine.
+ * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.
+ *
+ * @param engine the existing VIATRA Query engine in which this matcher will be created.
+ * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation
+ *
+ */
+ private Matcher() {
+ super(querySpecification());
+ }
+
+ /**
+ * Returns the set of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return matches represented as a Match object.
+ *
+ */
+ public Collection getAllMatches(final EPackage pA, final EPackage pB) {
+ return rawStreamAllMatches(new Object[]{pA, pB}).collect(Collectors.toSet());
+ }
+
+ /**
+ * Returns a stream of all matches of the pattern that conform to the given fixed values of some parameters.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return a stream of matches represented as a Match object.
+ *
+ */
+ public Stream streamAllMatches(final EPackage pA, final EPackage pB) {
+ return rawStreamAllMatches(new Object[]{pA, pB});
+ }
+
+ /**
+ * Returns an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return a match represented as a Match object, or null if no match is found.
+ *
+ */
+ public Optional getOneArbitraryMatch(final EPackage pA, final EPackage pB) {
+ return rawGetOneArbitraryMatch(new Object[]{pA, pB});
+ }
+
+ /**
+ * Indicates whether the given combination of specified pattern parameters constitute a valid pattern match,
+ * under any possible substitution of the unspecified parameters (if any).
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return true if the input is a valid (partial) match of the pattern.
+ *
+ */
+ public boolean hasMatch(final EPackage pA, final EPackage pB) {
+ return rawHasMatch(new Object[]{pA, pB});
+ }
+
+ /**
+ * Returns the number of all matches of the pattern that conform to the given fixed values of some parameters.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return the number of pattern matches found.
+ *
+ */
+ public int countMatches(final EPackage pA, final EPackage pB) {
+ return rawCountMatches(new Object[]{pA, pB});
+ }
+
+ /**
+ * Executes the given processor on an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.
+ * Neither determinism nor randomness of selection is guaranteed.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @param processor the action that will process the selected match.
+ * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked
+ *
+ */
+ public boolean forOneArbitraryMatch(final EPackage pA, final EPackage pB, final Consumer super Unsat_subpackage.Match> processor) {
+ return rawForOneArbitraryMatch(new Object[]{pA, pB}, processor);
+ }
+
+ /**
+ * Returns a new (partial) match.
+ * This can be used e.g. to call the matcher with a partial match.
+ * The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.
+ * @param pA the fixed value of pattern parameter a, or null if not bound.
+ * @param pB the fixed value of pattern parameter b, or null if not bound.
+ * @return the (partial) match object.
+ *
+ */
+ public Unsat_subpackage.Match newMatch(final EPackage pA, final EPackage pB) {
+ return Unsat_subpackage.Match.newMatch(pA, pB);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ protected Stream rawStreamAllValuesOfa(final Object[] parameters) {
+ return rawStreamAllValues(POSITION_A, parameters).map(EPackage.class::cast);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfa() {
+ return rawStreamAllValuesOfa(emptyArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfa() {
+ return rawStreamAllValuesOfa(emptyArray());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ *
+ * @return the Stream of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfa(final Unsat_subpackage.Match partialMatch) {
+ return rawStreamAllValuesOfa(partialMatch.toArray());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ *
+ * @return the Stream of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfa(final EPackage pB) {
+ return rawStreamAllValuesOfa(new Object[]{null, pB});
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfa(final Unsat_subpackage.Match partialMatch) {
+ return rawStreamAllValuesOfa(partialMatch.toArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for a.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfa(final EPackage pB) {
+ return rawStreamAllValuesOfa(new Object[]{null, pB}).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ protected Stream rawStreamAllValuesOfb(final Object[] parameters) {
+ return rawStreamAllValues(POSITION_B, parameters).map(EPackage.class::cast);
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfb() {
+ return rawStreamAllValuesOfb(emptyArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfb() {
+ return rawStreamAllValuesOfb(emptyArray());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ *
+ * @return the Stream of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfb(final Unsat_subpackage.Match partialMatch) {
+ return rawStreamAllValuesOfb(partialMatch.toArray());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ *
+ * NOTE: It is important not to modify the source model while the stream is being processed.
+ * If the match set of the pattern changes during processing, the contents of the stream is undefined.
+ * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.
+ *
+ * @return the Stream of all values or empty set if there are no matches
+ *
+ */
+ public Stream streamAllValuesOfb(final EPackage pA) {
+ return rawStreamAllValuesOfb(new Object[]{pA, null});
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfb(final Unsat_subpackage.Match partialMatch) {
+ return rawStreamAllValuesOfb(partialMatch.toArray()).collect(Collectors.toSet());
+ }
+
+ /**
+ * Retrieve the set of values that occur in matches for b.
+ * @return the Set of all values or empty set if there are no matches
+ *
+ */
+ public Set getAllValuesOfb(final EPackage pA) {
+ return rawStreamAllValuesOfb(new Object[]{pA, null}).collect(Collectors.toSet());
+ }
+
+ @Override
+ protected Unsat_subpackage.Match tupleToMatch(final Tuple t) {
+ try {
+ return Unsat_subpackage.Match.newMatch((EPackage) t.get(POSITION_A), (EPackage) t.get(POSITION_B));
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in tuple not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected Unsat_subpackage.Match arrayToMatch(final Object[] match) {
+ try {
+ return Unsat_subpackage.Match.newMatch((EPackage) match[POSITION_A], (EPackage) match[POSITION_B]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ @Override
+ protected Unsat_subpackage.Match arrayToMatchMutable(final Object[] match) {
+ try {
+ return Unsat_subpackage.Match.newMutableMatch((EPackage) match[POSITION_A], (EPackage) match[POSITION_B]);
+ } catch(ClassCastException e) {
+ LOGGER.error("Element(s) in array not properly typed!",e);
+ return null;
+ }
+ }
+
+ /**
+ * @return the singleton instance of the query specification of this pattern
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static IQuerySpecification querySpecification() {
+ return Unsat_subpackage.instance();
+ }
+ }
+
+ private Unsat_subpackage() {
+ super(GeneratedPQuery.INSTANCE);
+ }
+
+ /**
+ * @return the singleton instance of the query specification
+ * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded
+ *
+ */
+ public static Unsat_subpackage instance() {
+ try{
+ return LazyHolder.INSTANCE;
+ } catch (ExceptionInInitializerError err) {
+ throw processInitializerError(err);
+ }
+ }
+
+ @Override
+ protected Unsat_subpackage.Matcher instantiate(final ViatraQueryEngine engine) {
+ return Unsat_subpackage.Matcher.on(engine);
+ }
+
+ @Override
+ public Unsat_subpackage.Matcher instantiate() {
+ return Unsat_subpackage.Matcher.create();
+ }
+
+ @Override
+ public Unsat_subpackage.Match newEmptyMatch() {
+ return Unsat_subpackage.Match.newEmptyMatch();
+ }
+
+ @Override
+ public Unsat_subpackage.Match newMatch(final Object... parameters) {
+ return Unsat_subpackage.Match.newMatch((org.eclipse.emf.ecore.EPackage) parameters[0], (org.eclipse.emf.ecore.EPackage) parameters[1]);
+ }
+
+ /**
+ * Inner class allowing the singleton instance of {@link Unsat_subpackage} to be created
+ * not at the class load time of the outer class,
+ * but rather at the first call to {@link Unsat_subpackage#instance()}.
+ *
+ * This workaround is required e.g. to support recursion.
+ *
+ */
+ private static class LazyHolder {
+ private static final Unsat_subpackage INSTANCE = new Unsat_subpackage();
+
+ /**
+ * Statically initializes the query specification after the field {@link #INSTANCE} is assigned.
+ * This initialization order is required to support indirect recursion.
+ *
+ *
The static initializer is defined using a helper field to work around limitations of the code generator.
+ *
+ */
+ private static final Object STATIC_INITIALIZER = ensureInitialized();
+
+ public static Object ensureInitialized() {
+ INSTANCE.ensureInitializedInternal();
+ return null;
+ }
+ }
+
+ private static class GeneratedPQuery extends BaseGeneratedEMFPQuery {
+ private static final Unsat_subpackage.GeneratedPQuery INSTANCE = new GeneratedPQuery();
+
+ private final PParameter parameter_a = new PParameter("a", "org.eclipse.emf.ecore.EPackage", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.eclipse.org/emf/2002/Ecore", "EPackage")), PParameterDirection.INOUT);
+
+ private final PParameter parameter_b = new PParameter("b", "org.eclipse.emf.ecore.EPackage", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.eclipse.org/emf/2002/Ecore", "EPackage")), PParameterDirection.INOUT);
+
+ private final List parameters = Arrays.asList(parameter_a, parameter_b);
+
+ private GeneratedPQuery() {
+ super(PVisibility.PUBLIC);
+ }
+
+ @Override
+ public String getFullyQualifiedName() {
+ return "hu.bme.mit.inf.dslreasoner.domains.alloyexamples.unsat_subpackage";
+ }
+
+ @Override
+ public List getParameterNames() {
+ return Arrays.asList("a","b");
+ }
+
+ @Override
+ public List getParameters() {
+ return parameters;
+ }
+
+ @Override
+ public Set doGetContainedBodies() {
+ setEvaluationHints(new QueryEvaluationHint(null, QueryEvaluationHint.BackendRequirement.UNSPECIFIED));
+ Set bodies = new LinkedHashSet<>();
+ {
+ PBody body = new PBody(this);
+ PVariable var_a = body.getOrCreateVariableByName("a");
+ PVariable var_b = body.getOrCreateVariableByName("b");
+ new TypeConstraint(body, Tuples.flatTupleOf(var_a), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.eclipse.org/emf/2002/Ecore", "EPackage")));
+ new TypeConstraint(body, Tuples.flatTupleOf(var_b), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.eclipse.org/emf/2002/Ecore", "EPackage")));
+ body.setSymbolicParameters(Arrays.asList(
+ new ExportedParameter(body, var_a, parameter_a),
+ new ExportedParameter(body, var_b, parameter_b)
+ ));
+ // EPackage.eSubpackages(a, b)
+ new TypeConstraint(body, Tuples.flatTupleOf(var_a), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.eclipse.org/emf/2002/Ecore", "EPackage")));
+ PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}");
+ new TypeConstraint(body, Tuples.flatTupleOf(var_a, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.eclipse.org/emf/2002/Ecore", "EPackage", "eSubpackages")));
+ new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.eclipse.org/emf/2002/Ecore", "EPackage")));
+ new Equality(body, var__virtual_0_, var_b);
+ bodies.add(body);
+ }
+ return bodies;
+ }
+ }
+}
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/internal/.gitignore b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/internal/.gitignore
new file mode 100644
index 00000000..995169ff
--- /dev/null
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/src-gen/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/internal/.gitignore
@@ -0,0 +1,4 @@
+/.EcoreAll.java._trace
+/.SubpackageOrSelf.java._trace
+/.Subpackage.java._trace
+/.TopLevelPackageWithLoop.java._trace
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml
index b0b77996..fe1af62e 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/plugin.xml
@@ -1,9 +1,12 @@
-
-
-
-
+
+
+
+
@@ -11,6 +14,7 @@
+
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql
index 1f83a3b0..ba12bbda 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql
@@ -59,6 +59,19 @@ pattern noLinkToGroundStation(Spacecraft : Spacecraft) {
neg find indirectCommunicationLink(Spacecraft, GroundStation);
}
+//@Constraint(severity = "error", key = {Spacecraft}, message = "UNSAT")
+//pattern unsat_linkToGroundStation(Spacecraft : Spacecraft) {
+// ConstellationMission.groundStationNetwork(Mission, GroundStation);
+// ConstellationMission.spacecraft(Mission, Spacecraft);
+// find indirectCommunicationLink(Spacecraft, GroundStation);
+//}
+
+@Constraint(severity = "error", key = {Mission}, message = "UNSAT")
+pattern unsat_linkToGroundStation(Mission : InterferometryMission) {
+ InterferometryMission(Mission);
+ neg find noLinkToGroundStation(_);
+}
+
@Constraint(severity = "error", key = {Spacecraft},
message = "Spacecraft has no potential communication path to the ground station.")
pattern noPotentialLinkToGroundStation(Spacecraft : Spacecraft) {
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 @@
+
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);
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
index de68b5f7..25b7f16f 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
@@ -1,11 +1,15 @@
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
index b944302b..75581def 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
@@ -20,7 +20,8 @@ Require-Bundle: com.google.guava,
org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0",
hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
org.eclipse.viatra.query.runtime;bundle-version="2.0.0"
-Import-Package: org.apache.log4j;version="1.2.15"
-Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
-Bundle-ActivationPolicy: lazy
Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Bundle-ActivationPolicy: lazy
+Bundle-NativeCode: libminisat.so;osname=Linux;processor=x86_64
+Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+Import-Package: org.apache.log4j;version="1.2.15"
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
index 5e442ca7..f19ac30f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
@@ -59,15 +59,14 @@ class NeighbourhoodBasedPartialInterpretationStateCoder exten
override doCreateActivationCode(IPatternMatch match) {
val size = match.specification.parameters.size
val res = new ArrayList(size)
- var int index = 0
var int equivalenceHash = 0
val prime = 31
- while (index < size) {
- res.add(getCode(match.get(index)))
- index++
+ for (var int index = 0; index < size; index++) {
+ val matchArgument = match.get(index)
+ res.add(getCode(matchArgument))
for (var i = 0; i < index; i++) {
- val number = if (match.get(index) === match.get(i)) {
+ val number = if (matchArgument === match.get(i)) {
1
} else {
0
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index 6f38d261..c0a71c85 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -55,7 +55,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
*/
public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
- public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
+ public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.Polyhedral(
PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
public var List hints = newArrayList
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index 1e2d4dd4..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,16 +0,0 @@
-{
- "inputPath": "initialModels",
- "outputPath": "outputModels",
- "timeout": 1200,
- "saveModels": true,
- "warmupIterations": 0,
- "iterations": 5,
- "domain": "FAM",
- "scope": "none",
- "sizes": [500],
- "solver": "ViatraSolver",
- "scopePropagator": "polyhedral",
- "propagatedConstraints": "hints",
- "polyhedronSolver": "Clp",
- "scopeHeuristics": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json
new file mode 100644
index 00000000..b602f2fe
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json
@@ -0,0 +1,13 @@
+{
+ "inputPath": "initialModels",
+ "outputPath": "outputModels",
+ "timeout": 300,
+ "saveModels": true,
+ "saveTemporaryFiles": false,
+ "warmupIterations": 0,
+ "iterations": 30,
+ "domain": "Yakindu",
+ "scope": "unsat",
+ "sizes": [20],
+ "solver": "AlloySolver"
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index b4d51684..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,17 +0,0 @@
-{
- "inputPath": "initialModels",
- "outputPath": "outputModels",
- "timeout": 1200,
- "saveModels": false,
- "saveTemporaryFiles": true,
- "warmupIterations": 0,
- "iterations": 5,
- "domain": "Yakindu",
- "scope": "none",
- "sizes": [100],
- "solver": "ViatraSolver",
- "scopePropagator": "polyhedral",
- "propagatedConstraints": "hints",
- "polyhedronSolver": "Clp",
- "scopeHeuristic": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json
new file mode 100644
index 00000000..36fb0ea2
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json
@@ -0,0 +1,17 @@
+{
+ "inputPath": "initialModels",
+ "outputPath": "outputModels",
+ "timeout": 300,
+ "saveModels": true,
+ "saveTemporaryFiles": false,
+ "warmupIterations": 0,
+ "iterations": 1,
+ "domain": "ecoreUnsat",
+ "scope": "none",
+ "sizes": [5, 10, 20, 30, 40, 50],
+ "solver": "ViatraSolver",
+ "scopePropagator": "polyhedral",
+ "propagatedConstraints": "hints",
+ "polyhedronSolver": "Clp",
+ "scopeHeuristic": "polyhedral"
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index 72e97957..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,16 +0,0 @@
-{
- "inputPath": "initialModels",
- "outputPath": "outputModels",
- "timeout": 1200,
- "saveModels": true,
- "warmupIterations": 0,
- "iterations": 5,
- "domain": "ecore",
- "scope": "quantiles",
- "sizes": [50],
- "solver": "ViatraSolver",
- "scopePropagator": "polyhedral",
- "propagatedConstraints": "hints",
- "polyhedronSolver": "Clp",
- "scopeHeuristic": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index a7e29a22..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,16 +0,0 @@
-{
- "inputPath": "initialModels",
- "outputPath": "outputModels",
- "timeout": 1200,
- "saveModels": true,
- "warmupIterations": 1,
- "iterations": 1,
- "domain": "fs",
- "scope": "none",
- "sizes": [50, 100, 150, 200, 250, 300, 350, 400, 450, 500],
- "solver": "ViatraSolver",
- "scopePropagator": "polyhedral",
- "propagatedConstraints": "hints",
- "polyhedronSolver": "Clp",
- "scopeHeuristic": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json
new file mode 100644
index 00000000..16abb5d0
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json
@@ -0,0 +1,17 @@
+{
+ "inputPath": "initialModels",
+ "outputPath": "outputModels",
+ "timeout": 300,
+ "saveModels": true,
+ "saveTemporaryFiles": false,
+ "warmupIterations": 0,
+ "iterations": 30,
+ "domain": "satelliteUnsat",
+ "scope": "none",
+ "sizes": [10],
+ "solver": "ViatraSolver",
+ "scopePropagator": "polyhedral",
+ "propagatedConstraints": "hints",
+ "polyhedronSolver": "Clp",
+ "scopeHeuristic": "polyhedral"
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index d5469948..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,17 +0,0 @@
-{
- "inputPath": "initialModels",
- "outputPath": "outputModels",
- "timeout": 120,
- "saveModels": true,
- "saveTemporaryFiles": true,
- "warmupIterations": 0,
- "iterations": 1,
- "domain": "Yakindu",
- "scope": "quantiles",
- "sizes": [10, 20, 30, 40, 50, 60, 70, 80, 90, 100],
- "solver": "ViatraSolver",
- "scopePropagator": "polyhedral",
- "propagatedConstraints": "hints",
- "polyhedronSolver": "Clp",
- "scopeHeuristic": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
index 1be03eed..bf9ca274 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
@@ -40,6 +40,8 @@ class TypeQuantiles {
}
abstract class MetamodelLoader {
+ public static val UNSAT_PREFIX = "unsat_"
+
protected val ReasonerWorkspace workspace
new(ReasonerWorkspace workspace) {
@@ -61,6 +63,10 @@ abstract class MetamodelLoader {
def Map getTypeQuantiles() {
emptyMap
}
+
+ def Map getUnsatTypeQuantiles() {
+ throw new UnsupportedOperationException("This domain has no type quantiles for unsatisfiable problems")
+ }
def List getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
emptyList
@@ -136,9 +142,15 @@ class YakinduLoader extends MetamodelLoader {
public static val patternsWithComplexStates = #["outgoingFromExit", "outgoingFromFinal", "choiceHasNoOutgoing",
"choiceHasNoIncoming"]
+ val boolean satisfiable
+
new(ReasonerWorkspace workspace) {
+ this(workspace, true)
+ }
+
+ new(ReasonerWorkspace workspace, boolean satisfiable) {
super(workspace)
- YakindummPackage.eINSTANCE.eClass
+ this.satisfiable = satisfiable
}
def setUseSynchronization(boolean useSynchronization) {
@@ -173,6 +185,8 @@ class YakinduLoader extends MetamodelLoader {
useSynchInThisLoad || !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)]
].filter [ spec |
useComplexStates || !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)]
+ ].filter [
+ !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX)
].toList
val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
val derivedFeatures = new LinkedHashMap
@@ -213,6 +227,19 @@ class YakinduLoader extends MetamodelLoader {
"Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581)
}
}
+
+ override getUnsatTypeQuantiles() {
+ #{
+ "Choice" -> new TypeQuantiles(0.118279569892473, 0.154020979020979),
+ "Entry" -> new TypeQuantiles(0.2, 0.4),
+ "Exit" -> new TypeQuantiles(0, 0),
+ "FinalState" -> new TypeQuantiles(0, 0),
+ "Region" -> new TypeQuantiles(0.0294117647058824, 0.0633258678611422),
+ "State" -> new TypeQuantiles(0.132023636740618, 0.175925925925926),
+// "Statechart" -> new TypeQuantiles(0.00961538461538462, 0.010752688172043),
+ "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581)
+ }
+ }
override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
#[new SGraphHint(ecore2Logic, trace)]
@@ -276,9 +303,15 @@ class FileSystemLoader extends MetamodelLoader {
}
class EcoreLoader extends MetamodelLoader {
+ val boolean satisfiable
new(ReasonerWorkspace workspace) {
+ this(workspace, true)
+ }
+
+ new(ReasonerWorkspace workspace, boolean satisfiable) {
super(workspace)
+ this.satisfiable = satisfiable
}
override loadMetamodel() {
@@ -307,7 +340,12 @@ class EcoreLoader extends MetamodelLoader {
override loadQueries(EcoreMetamodelDescriptor metamodel) {
val patternGroup = Ecore.instance
val patterns = patternGroup.specifications.toList
- val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
+ val allWfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
+ val wfPatterns = if (satisfiable) {
+ allWfPatterns.filter[!it.simpleName.startsWith(UNSAT_PREFIX)].toSet
+ } else {
+ allWfPatterns
+ }
val derivedFeatures = new HashMap
return new ViatraQuerySetDescriptor(
patterns,
@@ -346,9 +384,15 @@ class EcoreLoader extends MetamodelLoader {
}
class SatelliteLoader extends MetamodelLoader {
+ val boolean satisfiable
new(ReasonerWorkspace workspace) {
+ this(workspace, true)
+ }
+
+ new(ReasonerWorkspace workspace, boolean satisfiable) {
super(workspace)
+ this.satisfiable = satisfiable
}
override loadMetamodel() {
@@ -371,7 +415,9 @@ class SatelliteLoader extends MetamodelLoader {
override loadQueries(EcoreMetamodelDescriptor metamodel) {
val i = SatelliteQueriesAll.instance
- val patterns = i.specifications.toList
+ val patterns = i.specifications.filter [
+ !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX)
+ ].toList
val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
val derivedFeatures = new LinkedHashMap
val res = new ViatraQuerySetDescriptor(
@@ -404,4 +450,15 @@ class SatelliteLoader extends MetamodelLoader {
}
}
+ override getUnsatTypeQuantiles() {
+ #{
+ "CubeSat3U" -> new TypeQuantiles(0.1, 0.25),
+ "CubeSat6U" -> new TypeQuantiles(0.1, 0.25),
+ "SmallSat" -> new TypeQuantiles(0.1, 0.25),
+ "UHFCommSubsystem" -> new TypeQuantiles(0.08, 0.1),
+ "XCommSubsystem" -> new TypeQuantiles(0, 0.1),
+ "KaCommSubsystem" -> new TypeQuantiles(0, 0.05),
+ "InterferometryPayload" -> new TypeQuantiles(0.15, 0.25)
+ }
+ }
}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
index 56a65091..f842afb5 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
@@ -29,19 +29,26 @@ class MeasurementScript {
enum Domain {
fs,
ecore,
+ ecoreUnsat,
Yakindu,
+ YakinduUnsat,
FAM,
- satellite
+ satellite,
+ satelliteUnsat
}
enum Scope {
none,
- quantiles
+ quantiles,
+ upperOnly,
+ unsat,
+ exactly
}
enum Solver {
ViatraSolver,
- AlloySolver
+ AlloySolver,
+ AlloyMiniSat
}
enum ScopePropagator {
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
index 1127f01a..973c3d13 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
@@ -54,6 +54,7 @@ import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandalone
import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions
import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory
import org.eclipse.xtend.lib.annotations.Data
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
class MeasurementScriptRunner {
static val MODEL_SIZE_GAP = 0
@@ -75,9 +76,12 @@ class MeasurementScriptRunner {
metamodelLoader = switch (script.domain) {
case fs: new FileSystemLoader(inputWorkspace)
case ecore: new EcoreLoader(inputWorkspace)
+ case ecoreUnsat: new EcoreLoader(inputWorkspace, false)
case Yakindu: new YakinduLoader(inputWorkspace) => [useSynchronization = false; useComplexStates = true]
+ case YakinduUnsat: new YakinduLoader(inputWorkspace, false) => [useSynchronization = false; useComplexStates = true]
case FAM: new FAMLoader(inputWorkspace)
case satellite: new SatelliteLoader(inputWorkspace)
+ case satelliteUnsat: new SatelliteLoader(inputWorkspace, false)
default: throw new IllegalArgumentException("Unsupported domain: " + script.domain)
}
}
@@ -191,15 +195,17 @@ class MeasurementScriptRunner {
config
}
- private def createAlloyConfig() {
+ private def createAlloyConfig(AlloyBackendSolver backendSolver) {
val config = new AlloySolverConfiguration
+ config.solver = backendSolver
config
}
private def createConfig(int modelSize) {
val config = switch (solver : script.solver) {
case ViatraSolver: createViatraConfig()
- case AlloySolver: createAlloyConfig()
+ case AlloySolver: createAlloyConfig(AlloyBackendSolver.SAT4J)
+ case AlloyMiniSat: createAlloyConfig(AlloyBackendSolver.MiniSatJNI)
default: throw new IllegalArgumentException("Unknown solver: " + solver)
}
config.solutionScope.numberOfRequiredSolutions = 1
@@ -243,7 +249,8 @@ class MeasurementScriptRunner {
val solver = switch (solver : script.solver) {
case ViatraSolver: new ViatraReasoner
- case AlloySolver: new AlloySolver
+ case AlloySolver,
+ case AlloyMiniSat: new AlloySolver
default: throw new IllegalArgumentException("Unknown solver: " + solver)
}
val result = solver.solve(problem, config, outputWorkspace)
@@ -284,14 +291,31 @@ class MeasurementScriptRunner {
} else {
val numberOfKnownElements = knownElements.values.flatten.toSet.size
val newElementCount = modelSize - numberOfKnownElements
- config.typeScopes.minNewElements = newElementCount
- config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
+ switch (script.scope) {
+ case upperOnly:
+ config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
+ case exactly: {
+ config.typeScopes.minNewElements = newElementCount
+ config.typeScopes.maxNewElements = newElementCount
+ }
+ default: {
+ config.typeScopes.minNewElements = newElementCount
+ config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
+ }
+ }
}
- switch (script.scope) {
- case none:
+ switch (scope : script.scope) {
+ case none,
+ case exactly:
return
- case quantiles: {
- val quantiles = metamodelLoader.typeQuantiles
+ case quantiles,
+ case unsat,
+ case upperOnly: {
+ val quantiles = if (scope == Scope.unsat) {
+ metamodelLoader.unsatTypeQuantiles
+ } else {
+ metamodelLoader.typeQuantiles
+ }
for (eClassInScope : eClassMapper.allClassesInScope(trace)) {
val quantile = quantiles.get(eClassInScope.name)
if (quantile !== null) {
@@ -301,7 +325,9 @@ class MeasurementScriptRunner {
val lowCount = Math.floor(modelSize * quantile.low) as int
val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int
// println('''«type.name» «lowCount» «highCount»''')
- config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0))
+ if (script.scope != Scope.upperOnly) {
+ config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0))
+ }
config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount)
}
}
--
cgit v1.2.3-54-g00ecf