+
+
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-70-g09d2
From 09c0f7bd18e6cec7f8e37bd2bcac9849636d33d1 Mon Sep 17 00:00:00 2001
From: Oszkar Semerath
Date: Mon, 11 May 2020 22:03:54 +0200
Subject: Bigliteral serialization in xmi transformation fixed
---
.../bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend | 14 +++++++++++++-
.../visualisation/PartialInterpretation2Gml.xtend | 2 +-
2 files changed, 14 insertions(+), 2 deletions(-)
(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner')
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend
index 92deeae6..08c6b7b7 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic2ecore/src/hu/bme/mit/inf/dslreasoner/logic2ecore/Logic2Ecore.xtend
@@ -20,6 +20,8 @@ import org.eclipse.emf.ecore.EcorePackage
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
import java.util.Map
+import org.eclipse.emf.ecore.EAttribute
+import java.math.BigDecimal
class Logic2Ecore {
val extension LogicStructureBuilder structureBuilder = new LogicStructureBuilder
@@ -92,7 +94,7 @@ class Logic2Ecore {
list += l.key
} else {
try {
- sourceObject.eSet(attributeType,l.key)
+ sourceObject.eSet(attributeType,translateType(attributeType.EAttributeType,l.key))
} catch(Exception e) {
e.printStackTrace
}
@@ -107,6 +109,16 @@ class Logic2Ecore {
return element2Object.values.root
}
+ def translateType(EDataType type, Object value) {
+ if(type == EcorePackage.eINSTANCE.EFloat) {
+ val bd = value as BigDecimal
+ return bd.floatValue
+ } else if( type == EcorePackage.eINSTANCE.EDouble ) {
+ val bd = value as BigDecimal
+ return bd.doubleValue
+ } else return value
+ }
+
// if(attributeType.EAttributeType.isSuperTypeOf(targetObject.eClass)) {
// val expression = ecore2Logic.IsAttributeValue(forwardTrace,sourceElement,targetElement,attributeType)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
index 2b42a8b1..190b5c94 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
@@ -107,7 +107,7 @@ class PartialInterpretation2Gml {
}
def protected transormTitle(DefinedElement object) {
- if(object.name!= null)object.name
+ if(object.name!= null)object.name.replace("\"", "")
else "null"
}
--
cgit v1.2.3-70-g09d2
From 746bb0ba666286b9586ff8c2724ba21e1490c906 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Tue, 19 May 2020 23:55:46 +0200
Subject: Add new state coder
---
.../neighbourhood/Descriptor.xtend | 196 ++++++----
.../neighbourhood/NeighbourhoodOptions.xtend | 22 ++
.../neighbourhood/PartialInterpretation2Hash.xtend | 2 +-
...nterpretation2NeighbourhoodRepresentation.xtend | 423 +++++++++++----------
...ation2PairwiseNeighbourhoodRepresentation.xtend | 68 ++++
...bstractNeighborhoodBasedStateCoderFactory.xtend | 137 +++++++
.../IdentifierBasedStateCoderFactory.xtend | 4 +-
.../NeighbourhoodBasedStateCoderFactory.xtend | 289 ++++----------
...irwiseNeighbourhoodBasedStateCoderFactory.xtend | 75 ++++
9 files changed, 730 insertions(+), 486 deletions(-)
create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodOptions.xtend
create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2PairwiseNeighbourhoodRepresentation.xtend
create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/AbstractNeighborhoodBasedStateCoderFactory.xtend
create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/PairwiseNeighbourhoodBasedStateCoderFactory.xtend
(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner')
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend
index 41482b28..e4bdb086 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend
@@ -4,10 +4,21 @@ import java.util.HashMap
import java.util.Map
import java.util.Set
import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend2.lib.StringConcatenationClient
@Data abstract class AbstractNodeDescriptor {
long dataHash
-
+
+ protected def StringConcatenationClient prettyPrint() {
+ '''(«dataHash»)[«class.simpleName»]'''
+ }
+
+ override toString() {
+ '''
+ «prettyPrint»
+ '''
+ }
+
// @Pure
// @Override
// override public boolean equals(Object obj) {
@@ -24,34 +35,45 @@ import org.eclipse.xtend.lib.annotations.Data
// }
}
-@Data class LocalNodeDescriptor extends AbstractNodeDescriptor{
+@Data class LocalNodeDescriptor extends AbstractNodeDescriptor {
Set types
String id;
+
new(String id, Set types) {
- super(calcualteDataHash(id,types))
+ super(calcualteDataHash(id, types))
this.types = types
this.id = id
}
-
+
def private static calcualteDataHash(String id, Set types) {
val int prime = 31;
var result = 0
- if(id !== null)
- result = id.hashCode();
- if(types !== null) {
- result = prime * result + types.hashCode
- }
- return result
+ if (id !== null)
+ result = id.hashCode();
+ if (types !== null) {
+ result = prime * result + types.hashCode
+ }
+ return result
}
-
+
override hashCode() {
return this.dataHash.hashCode
}
-
+
+ override equals(Object other) {
+ other.class == LocalNodeDescriptor && (other as AbstractNodeDescriptor).hashCode == hashCode
+ }
+
+ override protected prettyPrint() {
+ '''(«dataHash»)[«IF id !== null»id = "«id»"«IF types === null || !types.empty», «ENDIF»«ENDIF»«IF types === null»TYPES = null«ELSE»«FOR type : types SEPARATOR ", "»«type»«ENDFOR»«ENDIF»]'''
+ }
+
override toString() {
- return class.name + this.dataHash
+ '''
+ «prettyPrint»
+ '''
}
-
+
// @Pure
// @Override
// override public boolean equals(Object obj) {
@@ -66,7 +88,6 @@ import org.eclipse.xtend.lib.annotations.Data
// return false;
// return true;
// }
-
// @Pure
// override public boolean equals(Object obj) {
// if (this === obj)
@@ -97,49 +118,74 @@ import org.eclipse.xtend.lib.annotations.Data
String type
}
-@Data class FurtherNodeDescriptor extends AbstractNodeDescriptor{
-
- NodeRep previousRepresentation
- Map,Integer> incomingEdges
- Map,Integer> outgoingEdges
-
- new(
- NodeRep previousRepresentation,
- Map,Integer> incomingEdges,
- Map,Integer> outgoingEdges)
- {
- super(calculateDataHash(previousRepresentation,incomingEdges,outgoingEdges))
- this.previousRepresentation = previousRepresentation
- this.incomingEdges = new HashMap(incomingEdges)
- this.outgoingEdges = new HashMap(outgoingEdges)
- }
-
- static def private int calculateDataHash(
- NodeRep previousRepresentation,
- Map,Integer> incomingEdges,
- Map,Integer> outgoingEdges)
- {
- val int prime = 31;
- var int result = previousRepresentation.hashCode;
- if(incomingEdges !== null)
- result = prime * result + incomingEdges.hashCode();
- if(outgoingEdges !== null)
- result = prime * result + outgoingEdges.hashCode();
- return result;
- }
-
- override hashCode() {
- return this.dataHash.hashCode
+@Data class FurtherNodeDescriptor extends AbstractNodeDescriptor {
+
+ NodeRep previousRepresentation
+ Map, Integer> incomingEdges
+ Map, Integer> outgoingEdges
+
+ new(NodeRep previousRepresentation, Map, Integer> incomingEdges,
+ Map, Integer> outgoingEdges) {
+ super(calculateDataHash(previousRepresentation, incomingEdges, outgoingEdges))
+ this.previousRepresentation = previousRepresentation
+ this.incomingEdges = new HashMap(incomingEdges)
+ this.outgoingEdges = new HashMap(outgoingEdges)
}
-
+
+ static def private int calculateDataHash(NodeRep previousRepresentation,
+ Map, Integer> incomingEdges, Map, Integer> outgoingEdges) {
+ val int prime = 31;
+ var int result = previousRepresentation.hashCode;
+ if (incomingEdges !== null)
+ result = prime * result + incomingEdges.hashCode();
+ if (outgoingEdges !== null)
+ result = prime * result + outgoingEdges.hashCode();
+ return result;
+ }
+
+ override hashCode() {
+ return this.dataHash.hashCode
+ }
+
+ override equals(Object other) {
+ other.class == FurtherNodeDescriptor && (other as AbstractNodeDescriptor).hashCode == hashCode
+ }
+
+ override prettyPrint() {
+ '''
+ («dataHash»)[
+ PREV = «previousRepresentation?.prettyPrint»
+ «IF incomingEdges === null»
+ IN null
+ «ELSE»
+ «FOR edge : incomingEdges.entrySet»
+ IN «edge.value» «edge.key.type» = «edge.key.from.prettyPrint»
+ «ENDFOR»
+ «ENDIF»
+ «IF outgoingEdges === null»
+ OUT null
+ «ELSE»
+ «FOR edge : outgoingEdges.entrySet»
+ OUT «edge.value» «edge.key.type» = «edge.key.to.prettyPrint»
+ «ENDFOR»
+ «ENDIF»
+ ]'''
+ }
+
+ private def StringConcatenationClient prettyPrint(NodeRep rep) {
+ if (rep instanceof AbstractNodeDescriptor) {
+ rep.prettyPrint
+ } else {
+ '''«rep»'''
+ }
+ }
+
override toString() {
- return class.name + dataHash
-// return '''[«previousRepresentation»,(«FOR
-// in: incomingEdges.entrySet»(«in.key.type.name»=«in.key.from»,«in.value»)«ENDFOR»),(«FOR
-// out: outgoingEdges.entrySet»(«out.key.type.name»=«out.key.to»,«out.value»)«ENDFOR»),«FOR
-// att: attributeValues»(«att.type.name»=«att.value»)«ENDFOR»]'''
+ '''
+ «prettyPrint»
+ '''
}
-
+
// @Pure
// @Override
// override public boolean equals(Object obj) {
@@ -154,7 +200,6 @@ import org.eclipse.xtend.lib.annotations.Data
// return false;
// return true;
// }
-
// @Pure
// override public boolean equals(Object obj) {
// if (this === obj)
@@ -191,24 +236,23 @@ import org.eclipse.xtend.lib.annotations.Data
// return true;
// }
}
-
/*
-@Data
-class ModelDescriptor {
- int dataHash
- int unknownElements
- Map extends AbstractNodeDescriptor,Integer> knownElements
-
- public new(Map extends AbstractNodeDescriptor,Integer> knownElements, int unknownElements) {
- this.dataHash = calculateDataHash(knownElements,unknownElements)
- this.unknownElements = unknownElements
- this.knownElements = knownElements
- }
-
- def private static calculateDataHash(Map extends AbstractNodeDescriptor,Integer> knownElements, int unknownElements)
- {
- val int prime = 31;
- return knownElements.hashCode * prime + unknownElements.hashCode
- }
-}
-*/
\ No newline at end of file
+ * @Data
+ * class ModelDescriptor {
+ * int dataHash
+ * int unknownElements
+ * Map extends AbstractNodeDescriptor,Integer> knownElements
+ *
+ * public new(Map extends AbstractNodeDescriptor,Integer> knownElements, int unknownElements) {
+ * this.dataHash = calculateDataHash(knownElements,unknownElements)
+ * this.unknownElements = unknownElements
+ * this.knownElements = knownElements
+ * }
+ *
+ * def private static calculateDataHash(Map extends AbstractNodeDescriptor,Integer> knownElements, int unknownElements)
+ * {
+ * val int prime = 31;
+ * return knownElements.hashCode * prime + unknownElements.hashCode
+ * }
+ * }
+ */
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodOptions.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodOptions.xtend
new file mode 100644
index 00000000..c6e03f75
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodOptions.xtend
@@ -0,0 +1,22 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
+
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import java.util.Set
+import org.eclipse.xtend.lib.annotations.Data
+
+@Data
+class NeighbourhoodOptions {
+ public static val FixPointRange = -1
+ public static val GraphWidthRange = -2
+ public static val FullParallels = Integer.MAX_VALUE
+ public static val MaxNumbers = Integer.MAX_VALUE
+
+ public static val DEFAULT = new NeighbourhoodOptions(FixPointRange, FullParallels, MaxNumbers, null, null)
+
+ val int range
+ val int parallels
+ val int maxNumber
+ val Set relevantTypes
+ val Set relevantRelations
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend
index d474877d..ddf7d712 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend
@@ -5,7 +5,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
class PartialInterpretation2Hash extends PartialInterpretation2NeighbourhoodRepresentation{
- protected new() {
+ new() {
super(false, true)
}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend
index d1bf0348..3048167e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend
@@ -4,32 +4,34 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation
+import java.util.ArrayList
import java.util.HashMap
import java.util.HashSet
-import java.util.LinkedList
import java.util.List
import java.util.Map
import java.util.Set
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation
-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
-abstract class PartialInterpretation2NeighbourhoodRepresentation {
- private val boolean deepRepresentation
- private val boolean mergeSimilarNeighbourhood
+abstract class PartialInterpretation2NeighbourhoodRepresentation {
+ val boolean deepRepresentation
+ val boolean mergeSimilarNeighbourhood
protected new(boolean deeprepresentation, boolean mergeSimilarNeighbourhood) {
this.deepRepresentation = deeprepresentation
this.mergeSimilarNeighbourhood = mergeSimilarNeighbourhood
}
-
- public static val FixPointRage = -1
- public static val GraphWidthRange = -2
- public static val FullParallels = Integer.MAX_VALUE
- public static val MaxNumbers = Integer.MAX_VALUE
-
+
+ public static val FixPointRange = NeighbourhoodOptions.FixPointRange
+ public static val GraphWidthRange = NeighbourhoodOptions.GraphWidthRange
+ public static val FullParallels = NeighbourhoodOptions.FullParallels
+ public static val MaxNumbers = NeighbourhoodOptions.MaxNumbers
+
+ static val FOCUSED_ELEMENT_NAME = "<>"
+
/**
* Creates a neighbourhood representation with traces
* @param model The model to be represented.
@@ -37,10 +39,15 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation relevantTypes, Set relevantRelations)
- {
+ def createRepresentation(PartialInterpretation model, int range, int parallels, int maxNumber,
+ Set relevantTypes, Set relevantRelations) {
+ createRepresentationWithFocus(model, range, parallels, maxNumber, relevantTypes, relevantRelations, null)
+ }
+
+ def createRepresentationWithFocus(PartialInterpretation model, NeighbourhoodOptions options,
+ DefinedElement focusedElement) {
+ createRepresentationWithFocus(model, options.range, options.parallels, options.maxNumber, options.relevantTypes,
+ options.relevantRelations, focusedElement)
+ }
+
+ def createRepresentationWithFocus(PartialInterpretation model, int range, int parallels, int maxNumber,
+ Set relevantTypes, Set relevantRelations, DefinedElement focusedElement) {
val Map> types = new HashMap
- fillTypes(model,types,relevantTypes)
+ fillTypes(model, types, relevantTypes)
val Map>> IncomingRelations = new HashMap;
val Map>> OutgoingRelations = new HashMap;
- fillReferences(model,IncomingRelations,OutgoingRelations,relevantRelations)
-
- val res = doRecursiveNeighbourCalculation(model,types,IncomingRelations,OutgoingRelations,range,parallels,maxNumber);
-
+ fillReferences(model, IncomingRelations, OutgoingRelations, relevantRelations)
+
+ val res = doRecursiveNeighbourCalculation(model, types, IncomingRelations, OutgoingRelations, range, parallels,
+ maxNumber, focusedElement);
+
return res;
}
-
+
def private isRelevant(TypeDeclaration t, Set relevantTypes) {
- if(relevantTypes === null) {
+ if (relevantTypes === null) {
return true
} else {
return relevantTypes.contains(t)
}
}
+
def private isRelevant(RelationDeclaration r, Set relevantRelations) {
- if(relevantRelations === null) {
+ if (relevantRelations === null) {
return true
} else {
return relevantRelations.contains(r)
}
}
- /**
- * Gets the largest
- */
-/**
+ /**
* Gets the minimal neighbourhood size such that every reachable node appears in the shape of every other at least once.
-
*/
-
def private getWidth(Map> types,
Map>> IncomingRelations,
Map>> OutgoingRelations) {
@@ -99,6 +111,7 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation doRecursiveNeighbourCalculation(
- PartialInterpretation model,
- Map> types,
+ def private NeighbourhoodWithTraces doRecursiveNeighbourCalculation(
+ PartialInterpretation model, Map> types,
Map>> IncomingRelations,
- Map>> OutgoingRelations,
- int range, int parallels, int maxNumber)
- {
- if(range == 0){
- val r = calculateLocalNodeDescriptors(model,types,maxNumber)
- val res = this.createLocalRepresentation(r.value,r.key)
- if(res.modelRepresentation === null) {
+ Map>> OutgoingRelations, int range, int parallels,
+ int maxNumber, DefinedElement focusedElement) {
+ if (range == 0) {
+ val r = calculateLocalNodeDescriptors(model, types, maxNumber, focusedElement)
+ val res = this.createLocalRepresentation(r.value, r.key)
+ if (res.modelRepresentation === null) {
throw new IllegalArgumentException('''Model representation is null''')
- } else if(res.nodeRepresentations === null || res.nodeRepresentations.empty) {
+ } else if (res.nodeRepresentations === null || res.nodeRepresentations.empty) {
throw new IllegalArgumentException('''No node representation''')
- } else if(res.previousRepresentation !== null) {
+ } else if (res.previousRepresentation !== null) {
throw new IllegalArgumentException('''The previous representation of the first neighbourhood have to be null''')
- } else return res
- } else if(range > 0) {
- val previous = doRecursiveNeighbourCalculation(model,types,IncomingRelations,OutgoingRelations,range-1,parallels,maxNumber)
- val r = calculateFurtherNodeDescriptors(model,previous,IncomingRelations,OutgoingRelations,parallels,maxNumber)
- //println('''Level «range» finished.''')
- val res = createFurtherRepresentation(r.key,r.value,previous,deepRepresentation)
- if(res.modelRepresentation === null) {
+ } else
+ return res
+ } else if (range > 0) {
+ val previous = doRecursiveNeighbourCalculation(model, types, IncomingRelations, OutgoingRelations,
+ range - 1, parallels, maxNumber, focusedElement)
+ val r = calculateFurtherNodeDescriptors(model, previous, IncomingRelations, OutgoingRelations, parallels,
+ maxNumber)
+ // println('''Level «range» finished.''')
+ val res = createFurtherRepresentation(r.key, r.value, previous, deepRepresentation)
+ if (res.modelRepresentation === null) {
throw new IllegalArgumentException('''Model representation is null''')
- } else if(res.nodeRepresentations === null || res.nodeRepresentations.empty) {
+ } else if (res.nodeRepresentations === null || res.nodeRepresentations.empty) {
throw new IllegalArgumentException('''No node representation''')
- } else if(res.previousRepresentation === null && deepRepresentation) {
+ } else if (res.previousRepresentation === null && deepRepresentation) {
throw new IllegalArgumentException('''Need previous representations''')
- } else return res
- } else if (range == FixPointRage) {
- return refineUntilFixpoint(model,types,IncomingRelations,OutgoingRelations,parallels,maxNumber)
+ } else
+ return res
+ } else if (range == FixPointRange) {
+ return refineUntilFixpoint(model, types, IncomingRelations, OutgoingRelations, parallels, maxNumber,
+ focusedElement)
} else if (range == GraphWidthRange) {
- val width = this.getWidth(types,IncomingRelations,OutgoingRelations)
- //println(width)
- return doRecursiveNeighbourCalculation(model,types,IncomingRelations,OutgoingRelations,width,parallels,maxNumber)
+ val width = this.getWidth(types, IncomingRelations, OutgoingRelations)
+ // println(width)
+ return doRecursiveNeighbourCalculation(model, types, IncomingRelations, OutgoingRelations, width, parallels,
+ maxNumber, focusedElement)
}
}
-
- def private refineUntilFixpoint(
- PartialInterpretation model,
- Map> types,
+
+ def private refineUntilFixpoint(PartialInterpretation model, Map> types,
Map>> IncomingRelations,
- Map>> OutgoingRelations,
- int parallels, int maxNumbers)
- {
+ Map>> OutgoingRelations, int parallels, int maxNumbers,
+ DefinedElement focusedElement) {
var lastRange = 0
- val last = calculateLocalNodeDescriptors(model,types,maxNumbers)
- var lastRepresentation = this.createLocalRepresentation(last.value,last.key)
- //println('''Level 0 finished.''')
+ val last = calculateLocalNodeDescriptors(model, types, maxNumbers, focusedElement)
+ var lastRepresentation = this.createLocalRepresentation(last.value, last.key)
+ // println('''Level 0 finished.''')
var boolean hasRefined
do {
- val nextRange = lastRange+1
- val next = calculateFurtherNodeDescriptors(model,lastRepresentation,IncomingRelations,OutgoingRelations,parallels,maxNumbers)
- val nextRepresentation = createFurtherRepresentation(next.key,next.value,lastRepresentation,deepRepresentation)
-
- val previousNumberOfTypes =lastRepresentation.nodeRepresentations.values.toSet.size
+ val nextRange = lastRange + 1
+ val next = calculateFurtherNodeDescriptors(model, lastRepresentation, IncomingRelations, OutgoingRelations,
+ parallels, maxNumbers)
+ val nextRepresentation = createFurtherRepresentation(next.key, next.value, lastRepresentation,
+ deepRepresentation)
+
+ val previousNumberOfTypes = lastRepresentation.nodeRepresentations.values.toSet.size
val nextNumberOfTypes = nextRepresentation.nodeRepresentations.values.toSet.size
- hasRefined = nextNumberOfTypes > previousNumberOfTypes
-
+ hasRefined = nextNumberOfTypes > previousNumberOfTypes
+
lastRange = nextRange
lastRepresentation = nextRepresentation
-
+
// if(hasRefined) {
// println('''Level «nextRange» is calculated, number of types is refined: «previousNumberOfTypes» -> «nextNumberOfTypes»''')
// } else {
@@ -201,211 +216,219 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation> node2Type, Set relevantTypes) {
- for(element : model.elements) {
+
+ def private fillTypes(PartialInterpretation model, Map> node2Type,
+ Set relevantTypes) {
+ for (element : model.elements) {
node2Type.put(element, new HashSet)
}
-
+
// for(typeDefinition : model.problem.types.filter(TypeDefinition)) {
// // Dont need
// }
- for(typeInterpretation : model.partialtypeinterpratation) {
- if(typeInterpretation instanceof PartialPrimitiveInterpretation) {
-
- } else if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
+ for (typeInterpretation : model.partialtypeinterpratation) {
+ if (typeInterpretation instanceof PartialPrimitiveInterpretation) {
+ } else if (typeInterpretation instanceof PartialComplexTypeInterpretation) {
val type = typeInterpretation.interpretationOf
- if(type.isRelevant(relevantTypes)) {
- for(element : typeInterpretation.elements) {
+ if (type.isRelevant(relevantTypes)) {
+ for (element : typeInterpretation.elements) {
element.lookup(node2Type).add(type.name)
}
}
}
}
}
-
+
/**
* Indexes the references
*/
def private fillReferences(PartialInterpretation model,
Map>> IncomingRelations,
Map>> OutgoingRelations,
- Set relevantRelations)
- {
- for(object : model.elements) {
- IncomingRelations.put(object,new LinkedList)
- OutgoingRelations.put(object,new LinkedList)
+ Set relevantRelations) {
+ for (object : model.elements) {
+ IncomingRelations.put(object, new ArrayList)
+ OutgoingRelations.put(object, new ArrayList)
}
- for(relationInterpretation : model.partialrelationinterpretation) {
+ for (relationInterpretation : model.partialrelationinterpretation) {
val type = relationInterpretation.interpretationOf
- if(type.isRelevant(relevantRelations)) {
- for(link : relationInterpretation.relationlinks) {
- if(link instanceof BinaryElementRelationLink) {
- OutgoingRelations.get(link.param1) += new OutgoingRelation(link.param2,type.name)
- IncomingRelations.get(link.param2) += new IncomingRelation(link.param1,type.name)
- } else throw new UnsupportedOperationException
+ if (type.isRelevant(relevantRelations)) {
+ for (link : relationInterpretation.relationlinks) {
+ if (link instanceof BinaryElementRelationLink) {
+ OutgoingRelations.get(link.param1) += new OutgoingRelation(link.param2, type.name)
+ IncomingRelations.get(link.param2) += new IncomingRelation(link.param1, type.name)
+ } else
+ throw new UnsupportedOperationException
}
}
}
}
-
+
/**
* Creates a local representation of the objects (aka zero range neighbourhood)
*/
- def abstract protected NeighbourhoodWithTraces createLocalRepresentation(
+ def abstract protected NeighbourhoodWithTraces createLocalRepresentation(
Map node2Representation,
Map representation2Amount
)
-
+
/**
* Creates a
*/
- def abstract protected NeighbourhoodWithTraces createFurtherRepresentation(
+ def abstract protected NeighbourhoodWithTraces createFurtherRepresentation(
Map