+
+
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 957082776dbb7efed53a783c5e5be6b443a9bb86 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Sat, 27 Jun 2020 17:56:46 +0200
Subject: Fix scope + numerical propagation WIP
---
.../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes
.../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes
.../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes
.../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes
.../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes
....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes
...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes
.../hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | 6 +-
.../.settings/org.eclipse.jdt.core.prefs | 8 ++
.../lib/libviatracbc.so | Bin 33944 -> 46416 bytes
.../MultiplicityGoalConstraintCalculator.xtend | 15 +--
.../cardinality/PolyhedronScopePropagator.xtend | 8 +-
.../logic2viatra/cardinality/ScopePropagator.xtend | 14 +-
.../rules/GoalConstraintProvider.xtend | 3 +-
.../rules/RefinementRuleProvider.xtend | 150 ++++++++++++---------
.../PartialInterpretationInitialiser.xtend | 29 ++--
.../reasoner/ViatraReasonerConfiguration.xtend | 5 +-
.../dse/BestFirstStrategyForModelGeneration.java | 22 +--
.../dse/ModelGenerationCompositeObjective.xtend | 2 +-
.../viatrasolver/reasoner/dse/ScopeObjective.xtend | 2 +-
.../case.study.familyTree.run/bin/.gitignore | 1 -
.../inputs/SatelliteInstance.xmi | 2 +-
.../src/run/RunGeneratorConfig.xtend | 6 +-
23 files changed, 136 insertions(+), 137 deletions(-)
create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs
delete mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore
(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage')
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
index b5a7c99c..94c786eb 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
index 9274eee0..46ab9b95 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin
index 8e8e8c70..27dc1dd4 100644
Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin
index 741776d1..d71f4f21 100644
Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin
index 73356e7f..801783da 100644
Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin
index 24f61d80..30c2ff9e 100644
Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin
index eae3bd77..261f466c 100644
Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath
index e19039ae..93829d26 100644
--- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath
+++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath
@@ -1,10 +1,6 @@
-
-
-
-
-
+
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 00000000..9f6ece88
--- /dev/null
+++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,8 @@
+eclipse.preferences.version=1
+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.compliance=1.8
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
+org.eclipse.jdt.core.compiler.release=disabled
+org.eclipse.jdt.core.compiler.source=1.8
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so
index 96289216..ba3cdc06 100755
Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so differ
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
index 034420d6..b28cd584 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
@@ -10,15 +10,13 @@ class MultiplicityGoalConstraintCalculator {
val String targetRelationName
val IQuerySpecification> querySpecification
var ViatraQueryMatcher> matcher
- val int minValue
val boolean containment
val int cost
- public new(String targetRelationName, IQuerySpecification> querySpecification, int minValue, boolean containment, int cost) {
+ public new(String targetRelationName, IQuerySpecification> querySpecification, boolean containment, int cost) {
this.targetRelationName = targetRelationName
this.querySpecification = querySpecification
this.matcher = null
- this.minValue = minValue
this.containment = containment
this.cost = cost
}
@@ -27,7 +25,6 @@ class MultiplicityGoalConstraintCalculator {
this.targetRelationName = other.targetRelationName
this.querySpecification = other.querySpecification
this.matcher = null
- this.minValue = other.minValue
this.containment = other.containment
this.cost = other.cost
}
@@ -49,14 +46,8 @@ class MultiplicityGoalConstraintCalculator {
var res = 0
val allMatches = this.matcher.allMatches
for(match : allMatches) {
- val existingMultiplicity = match.get(4) as Integer
- if(existingMultiplicity < this.minValue) {
- val missingMultiplicity = this.minValue-existingMultiplicity
- res += missingMultiplicity
- }
-// if(missingMultiplicity!=0) {
-// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity)
-// }
+ val missingMultiplicity = match.get(2) as Integer
+ res += missingMultiplicity
}
// if(res>0)
// println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
index 120fb18a..9b4dff0f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -88,6 +88,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
val result = operator.saturate()
if (result == PolyhedronSaturationResult.EMPTY) {
cache.put(signature, PolyhedronSignature.EMPTY)
+// println("INVALID")
setScopesInvalid()
} else {
val resultSignature = polyhedron.createSignature
@@ -110,11 +111,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
}
}
- override propagateAdditionToRelation(Relation r) {
- super.propagateAdditionToRelation(r)
- if (relevantRelations.contains(r)) {
- propagateAllScopeConstraints()
- }
+ override isPropagationNeededAfterAdditionToRelation(Relation r) {
+ relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r)
}
def resetBounds() {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
index 8f3a5bb0..8350c7f4 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -114,21 +114,21 @@ class ScopePropagator {
}
}
- def void propagateAdditionToRelation(Relation r) {
- // Nothing to propagate.
+ def isPropagationNeededAfterAdditionToRelation(Relation r) {
+ false
}
private def removeOne(Scope scope) {
- if (scope.maxNewElements === 0) {
- throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')
- } else if (scope.maxNewElements > 0) {
- scope.maxNewElements = scope.maxNewElements - 1
- }
if (scope.minNewElements > 0) {
scope.minNewElements = scope.minNewElements - 1
}
if (scope.minNewElementsHeuristic > 0) {
scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1
}
+ if (scope.maxNewElements > 0) {
+ scope.maxNewElements = scope.maxNewElements - 1
+ } else if (scope.maxNewElements === 0) {
+ setScopesInvalid()
+ }
}
}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
index 238ade5b..d2ee80dc 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
@@ -15,9 +15,8 @@ class GoalConstraintProvider {
val queries = entry.value
val targetRelationName = constraint.relation.name
val query = queries.unfinishedMultiplicityQuery
- val minValue = constraint.lowerBound
val containment = constraint.containment
- res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, minValue, containment, 1)
+ res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1)
}
}
return res
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
index 0b8a9019..863ee18b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
@@ -32,9 +32,12 @@ import java.util.LinkedHashMap
import java.util.LinkedList
import java.util.List
import java.util.Map
+import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine
import org.eclipse.viatra.query.runtime.api.GenericPatternMatch
import org.eclipse.viatra.query.runtime.api.IQuerySpecification
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+import org.eclipse.viatra.query.runtime.emf.EMFScope
import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory
import org.eclipse.xtend.lib.annotations.Data
@@ -45,6 +48,8 @@ class RefinementRuleProvider {
val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE
val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE
+ var AdvancedViatraQueryEngine queryEngine
+
def canonizeName(String name) {
return name.replace(' ','_')
}
@@ -60,6 +65,7 @@ class RefinementRuleProvider {
{
val res = new LinkedHashMap
val recursiveObjectCreation = recursiveObjectCreation(p,i)
+ queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine
for(LHSEntry: patterns.refineObjectQueries.entrySet) {
val containmentRelation = LHSEntry.key.containmentRelation
val inverseRelation = LHSEntry.key.inverseContainment
@@ -90,8 +96,7 @@ class RefinementRuleProvider {
if(inverseRelation!== null) {
ruleBuilder.action[match |
statistics.incrementTransformationCount
-// println(name)
- val startTime = System.nanoTime
+// println(name)
//val problem = match.get(0) as LogicProblem
val interpretation = match.get(1) as PartialInterpretation
val relationInterpretation = match.get(2) as PartialRelationInterpretation
@@ -99,79 +104,89 @@ class RefinementRuleProvider {
val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation
val container = match.get(5) as DefinedElement
- createObjectActionWithContainmentAndInverse(
- nameNewElement,
- interpretation,
- typeInterpretation,
- container,
- relationInterpretation,
- inverseRelationInterpretation,
- [createDefinedElement],
- recursiceObjectCreations,
- scopePropagator
- )
-
- val propagatorStartTime = System.nanoTime
- statistics.addExecutionTime(propagatorStartTime-startTime)
+ queryEngine.delayUpdatePropagation [
+ val startTime = System.nanoTime
+ createObjectActionWithContainmentAndInverse(
+ nameNewElement,
+ interpretation,
+ typeInterpretation,
+ container,
+ relationInterpretation,
+ inverseRelationInterpretation,
+ [createDefinedElement],
+ recursiceObjectCreations,
+ scopePropagator
+ )
+ statistics.addExecutionTime(System.nanoTime-startTime)
+ ]
// Scope propagation
- scopePropagator.propagateAllScopeConstraints()
- statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ queryEngine.delayUpdatePropagation [
+ val propagatorStartTime = System.nanoTime
+ scopePropagator.propagateAllScopeConstraints()
+ statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ ]
]
} else {
ruleBuilder.action[match |
statistics.incrementTransformationCount
// println(name)
- val startTime = System.nanoTime
//val problem = match.get(0) as LogicProblem
val interpretation = match.get(1) as PartialInterpretation
val relationInterpretation = match.get(2) as PartialRelationInterpretation
val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation
val container = match.get(4) as DefinedElement
- createObjectActionWithContainment(
- nameNewElement,
- interpretation,
- typeInterpretation,
- container,
- relationInterpretation,
- [createDefinedElement],
- recursiceObjectCreations,
- scopePropagator
- )
-
- val propagatorStartTime = System.nanoTime
- statistics.addExecutionTime(propagatorStartTime-startTime)
+ queryEngine.delayUpdatePropagation [
+ val startTime = System.nanoTime
+ createObjectActionWithContainment(
+ nameNewElement,
+ interpretation,
+ typeInterpretation,
+ container,
+ relationInterpretation,
+ [createDefinedElement],
+ recursiceObjectCreations,
+ scopePropagator
+ )
+ statistics.addExecutionTime(System.nanoTime-startTime)
+ ]
// Scope propagation
- scopePropagator.propagateAllScopeConstraints()
- statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ queryEngine.delayUpdatePropagation [
+ val propagatorStartTime = System.nanoTime
+ scopePropagator.propagateAllScopeConstraints()
+ statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ ]
]
}
} else {
ruleBuilder.action[match |
statistics.incrementTransformationCount
// println(name)
- val startTime = System.nanoTime
//val problem = match.get(0) as LogicProblem
val interpretation = match.get(1) as PartialInterpretation
val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation
- createObjectAction(
- nameNewElement,
- interpretation,
- typeInterpretation,
- [createDefinedElement],
- recursiceObjectCreations,
- scopePropagator
- )
-
- val propagatorStartTime = System.nanoTime
- statistics.addExecutionTime(propagatorStartTime-startTime)
+ queryEngine.delayUpdatePropagation [
+ val startTime = System.nanoTime
+ createObjectAction(
+ nameNewElement,
+ interpretation,
+ typeInterpretation,
+ [createDefinedElement],
+ recursiceObjectCreations,
+ scopePropagator
+ )
+ statistics.addExecutionTime(System.nanoTime-startTime)
+ ]
// Scope propagation
- scopePropagator.propagateAllScopeConstraints()
- statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ queryEngine.delayUpdatePropagation [
+ val propagatorStartTime = System.nanoTime
+ scopePropagator.propagateAllScopeConstraints()
+ statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ ]
]
}
return ruleBuilder.build
@@ -342,7 +357,7 @@ class RefinementRuleProvider {
if (inverseRelation === null) {
ruleBuilder.action [ match |
statistics.incrementTransformationCount
- val startTime = System.nanoTime
+
// println(name)
// val problem = match.get(0) as LogicProblem
// val interpretation = match.get(1) as PartialInterpretation
@@ -350,19 +365,24 @@ class RefinementRuleProvider {
val src = match.get(3) as DefinedElement
val trg = match.get(4) as DefinedElement
- createRelationLinkAction(src, trg, relationInterpretation)
-
- val propagatorStartTime = System.nanoTime
- statistics.addExecutionTime(propagatorStartTime-startTime)
+ queryEngine.delayUpdatePropagation [
+ val startTime = System.nanoTime
+ createRelationLinkAction(src, trg, relationInterpretation)
+ statistics.addExecutionTime(System.nanoTime-startTime)
+ ]
// Scope propagation
- scopePropagator.propagateAdditionToRelation(declaration)
- statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) {
+ queryEngine.delayUpdatePropagation [
+ val propagatorStartTime = System.nanoTime
+ scopePropagator.propagateAllScopeConstraints()
+ statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ ]
+ }
]
} else {
ruleBuilder.action [ match |
statistics.incrementTransformationCount
- val startTime = System.nanoTime
// println(name)
// val problem = match.get(0) as LogicProblem
// val interpretation = match.get(1) as PartialInterpretation
@@ -371,14 +391,20 @@ class RefinementRuleProvider {
val src = match.get(4) as DefinedElement
val trg = match.get(5) as DefinedElement
- createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation)
-
- val propagatorStartTime = System.nanoTime
- statistics.addExecutionTime(propagatorStartTime-startTime)
+ queryEngine.delayUpdatePropagation [
+ val startTime = System.nanoTime
+ createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation)
+ statistics.addExecutionTime(System.nanoTime-startTime)
+ ]
// Scope propagation
- scopePropagator.propagateAdditionToRelation(declaration)
- statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) {
+ queryEngine.delayUpdatePropagation [
+ val propagatorStartTime = System.nanoTime
+ scopePropagator.propagateAllScopeConstraints()
+ statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
+ ]
+ }
]
}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
index d37acb6d..20ff58f2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
@@ -2,19 +2,24 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStar
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion
-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.NaryRelationLink
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation
@@ -22,10 +27,10 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.UnaryElementRelationLink
import java.math.BigDecimal
import java.util.HashMap
import java.util.Map
@@ -35,14 +40,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
import org.eclipse.xtend.lib.annotations.Data
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
@Data class Problem2PartialInterpretationTrace {
Map type2Interpretation
@@ -194,7 +191,7 @@ class PartialInterpretationInitialiser {
interpretation.minNewElements = minNewElements
interpretation.maxNewElements = maxNewElements
// elements from problem are included
- if(maxNewElements>0) {
+ if(maxNewElements != 0) {
val newElements = createDefinedElement => [it.name = "New Objects"]
interpretation.openWorldElements += newElements
}
@@ -213,12 +210,8 @@ class PartialInterpretationInitialiser {
def private initialiseTypeScope(PartialTypeInterpratation interpretation, Integer min, Integer max) {
val res = createScope
res.targetTypeInterpretation = interpretation
- if(min !== null) {
- res.minNewElements = min
- }
- if(max !== null) {
- res.maxNewElements = max
- }
+ res.minNewElements = min ?: 0
+ res.maxNewElements = max ?: -1
return res
}
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 ddd25aac..e33a2590 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
@@ -58,13 +58,14 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
public var runIntermediateNumericalConsistencyChecks = true
public var punishSize = true
- public var scopeWeight = 1
- public var conaintmentWeight = 2
+ public var scopeWeight = 2
+ public var conaintmentWeight = 1
public var nonContainmentWeight = 1
public var unfinishedWFWeight = 1
public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
+// public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy
public var List hints = newArrayList
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index e529892c..09575384 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -18,6 +18,7 @@ import java.util.List;
import java.util.PriorityQueue;
import java.util.Random;
+import org.apache.log4j.Level;
import org.apache.log4j.Logger;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
@@ -76,7 +77,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
private volatile boolean isInterrupted = false;
private ModelResult modelResultByInternalSolver = null;
private Random random = new Random();
- //private Collection> matchers;
+// private Collection> matchers;
public ActivationSelector activationSelector = new EvenActivationSelector(random);
public ViatraReasonerSolutionSaver solutionSaver;
public NumericSolver numericSolver;
@@ -100,7 +101,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
this.method = method;
this.solutionSaver = solutionSaver;
this.numericSolver = numericSolver;
- //logger.setLevel(Level.DEBUG);
+// logger.setLevel(Level.DEBUG);
}
public int getNumberOfStatecoderFail() {
@@ -136,7 +137,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
// ViatraQueryEngine engine = context.getQueryEngine();
// matchers = new LinkedList>();
// for(IQuerySpecification extends ViatraQueryMatcher extends IPatternMatch>> p : this.method.getAllPatterns()) {
-// //System.out.println(p.getSimpleName());
// ViatraQueryMatcher extends IPatternMatch> matcher = p.getMatcher(engine);
// matchers.add(matcher);
// }
@@ -154,13 +154,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
@Override
public void explore() {
-// System.out.println("press enter");
-// try {
-// new BufferedReader(new InputStreamReader(System.in)).readLine();
-// } catch (IOException e) {
-// // TODO Auto-generated catch block
-// e.printStackTrace();
-// }
this.explorationStarted=System.nanoTime();
if (!checkGlobalConstraints()) {
logger.info("Global contraint is not satisifed in the first state. Terminate.");
@@ -219,10 +212,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) {
final Object nextActivation = iterator.next();
-// if (!iterator.hasNext()) {
-// logger.debug("Last untraversed activation of the state.");
-// trajectoiresToExplore.remove(currentTrajectoryWithfitness);
-// }
logger.debug("Executing new activation: " + nextActivation);
context.executeAcitvationId(nextActivation);
method.getStatistics().incrementDecisionCount();
@@ -230,10 +219,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
visualiseCurrentState();
// for(ViatraQueryMatcher extends IPatternMatch> matcher : matchers) {
// int c = matcher.countMatches();
-// if(c>=100) {
+// if(c>=1) {
// System.out.println(c+ " " +matcher.getPatternName());
-// }
-//
+// }
// }
boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness);
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
index d2faaa65..481f4ce1 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -112,7 +112,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective {
override isHardObjective() { true }
- override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
+ override satisifiesHardObjective(Double fitness) { fitness <= 0.9 }
override setComparator(Comparator comparator) {
throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
index 69a734f8..7abc5cb8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -25,7 +25,7 @@ class ScopeObjective implements IObjective{
val interpretation = context.model as PartialInterpretation
var res = interpretation.minNewElementsHeuristic.doubleValue
for(scope : interpretation.scopes) {
- res += scope.minNewElementsHeuristic*2
+ res += scope.minNewElementsHeuristic
}
return res
}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore
deleted file mode 100644
index 7050a7e3..00000000
--- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/queries/
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi
index 3d07a199..66512878 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi
@@ -4,4 +4,4 @@
xmlns:xmi="http://www.omg.org/XMI"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xmlns:satellite="http://www.example.org/satellite"
- xsi:schemaLocation="http://www.example.org/satellite ../model/satellite.ecore"/>
+ xsi:schemaLocation="http://www.example.org/satellite ../../hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"/>
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
index 20eed2e2..e4d6fe9f 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
@@ -12,7 +12,9 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.RuntimeEn
import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ScopeSpecification
import hu.bme.mit.inf.dslreasoner.application.execution.ScriptExecutor
import hu.bme.mit.inf.dslreasoner.application.execution.StandaloneScriptExecutor
+import hu.bme.mit.inf.dslreasoner.application.execution.StandardOutputBasedScriptConsole
import java.io.File
+import java.io.PrintWriter
import java.text.SimpleDateFormat
import java.util.Date
import org.apache.commons.cli.BasicParser
@@ -23,8 +25,6 @@ import org.apache.commons.cli.Option
import org.apache.commons.cli.Options
import org.apache.commons.cli.ParseException
import org.eclipse.core.runtime.NullProgressMonitor
-import com.google.common.io.Files
-import java.io.PrintWriter
class RunGeneratorConfig {
static var SIZE_LB = 20
@@ -102,7 +102,7 @@ class RunGeneratorConfig {
val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm")
val formattedDate = format.format(date)
- val executor = new ScriptExecutor
+ val executor = new ScriptExecutor(StandardOutputBasedScriptConsole.FACTORY)
val path = "config//generic" + DOMAIN + ".vsconfig"
var ConfigurationScript config = StandaloneScriptExecutor.loadScript(path)
--
cgit v1.2.3-70-g09d2
From 329ac27dfa84e9a07760bea75b36476dddcf29a7 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy
Date: Tue, 14 Jul 2020 10:45:03 +0200
Subject: Optimizations
---
.../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes
.../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes
.../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes
.../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes
.../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes
....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes
...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes
.../ModelGenerationMethodProvider.xtend | 22 +++--
.../cardinality/PolyhedronScopePropagator.xtend | 4 +
.../logic2viatra/cardinality/ScopePropagator.xtend | 4 +
.../logic2viatra/patterns/PatternProvider.xtend | 12 +++
.../rules/RefinementRuleProvider.xtend | 12 +--
.../META-INF/MANIFEST.MF | 3 +-
.../neighbourhood/Descriptor.xtend | 106 ++++++---------------
.../neighbourhood/PartialInterpretation2Hash.xtend | 14 ++-
...nterpretation2NeighbourhoodRepresentation.xtend | 63 ++++++------
.../NeighbourhoodBasedStateCoderFactory.xtend | 21 +++-
.../viatrasolver/reasoner/ViatraReasoner.xtend | 2 +-
.../config/genericSatellite.vsconfig | 6 +-
.../config/genericTaxation.vsconfig | 6 +-
.../case.study.pledge.run/inputs/Resource50hh.xmi | 59 ++++++++++++
21 files changed, 196 insertions(+), 138 deletions(-)
create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/Resource50hh.xmi
(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage')
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin
index bd1eabaf..35e3fe34 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin
index f4956ec0..b597e715 100644
Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin
index 0ee6ab93..5d90d470 100644
Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin
index 1fbc1b5a..f054d52c 100644
Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin
index 6dfd9bdd..faaea19c 100644
Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin
index 9e4a0e33..704006b4 100644
Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ
diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin
index 2a1c8746..76be2b25 100644
Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index b79039cb..56beacfa 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -1,6 +1,7 @@
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
import com.google.common.collect.ImmutableMap
+import com.google.common.collect.ImmutableSet
import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
@@ -57,7 +58,7 @@ class ModelGenerationStatistics {
}
public var int transformationInvocations
-
+
synchronized def incrementTransformationCount() {
transformationInvocations++
}
@@ -67,7 +68,7 @@ class ModelGenerationStatistics {
synchronized def incrementScopePropagationCount() {
scopePropagatorInvocations++
}
-
+
public var int scopePropagatorSolverInvocations
synchronized def incrementScopePropagationSolverCount() {
@@ -126,9 +127,7 @@ class ModelGenerationMethodProvider {
val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)
val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,
workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles)
- val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution))
- GenericQueryGroup.of(queries.allQueries).prepare(queryEngine)
-
+
val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics)
scopePropagator.propagateAllScopeConstraints
val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,
@@ -136,7 +135,8 @@ class ModelGenerationMethodProvider {
val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator,
statistics)
- val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries,calculateObjectCreationCosts)
+ val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries,
+ calculateObjectCreationCosts)
val unfinishedWF = queries.getUnfinishedWFQueries.values
@@ -150,10 +150,18 @@ class ModelGenerationMethodProvider {
val modalRelationQueries = modalRelationQueriesBuilder.build
val invalidWF = queries.getInvalidWFQueries.values
-
+
val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
+ val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll(
+ queries.refineTypeQueries.values).addAll(queries.refinerelationQueries.values).addAll(queries.
+ multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll(
+ queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll(
+ queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build
+ val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution))
+ GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine)
+
return new ModelGenerationMethod(
statistics,
objectRefinementRules.values,
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
index db22b95c..c28d4caa 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -114,6 +114,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
override isPropagationNeededAfterAdditionToRelation(Relation r) {
relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r)
}
+
+ override isQueryEngineFlushRequiredBeforePropagation() {
+ true
+ }
def resetBounds() {
for (dimension : polyhedron.dimensions) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
index 3e95b2cc..93b83577 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -130,6 +130,10 @@ class ScopePropagator {
def isPropagationNeededAfterAdditionToRelation(Relation r) {
false
}
+
+ def isQueryEngineFlushRequiredBeforePropagation() {
+ false
+ }
private def removeOne(Scope scope) {
if (scope.minNewElements > 0) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index 2f7c9e2d..d57705ce 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -1,5 +1,6 @@
package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
+import com.google.common.collect.ImmutableSet
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
@@ -55,6 +56,17 @@ class ModalPatternQueries {
class UnifinishedMultiplicityQueries {
val IQuerySpecification extends ViatraQueryMatcher extends IPatternMatch>> existingMultiplicityQuery
val IQuerySpecification extends ViatraQueryMatcher extends IPatternMatch>> existingInverseMultiplicityQuery
+
+ def Set>> getAllQueries() {
+ val builder = ImmutableSet.builder
+ if (existingMultiplicityQuery !== null) {
+ builder.add(existingMultiplicityQuery)
+ }
+ if (existingInverseMultiplicityQuery !== null) {
+ builder.add(existingInverseMultiplicityQuery)
+ }
+ builder.build
+ }
}
class PatternProvider {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
index 1d976e14..f7fe97a3 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
@@ -114,7 +114,7 @@ class RefinementRuleProvider {
)
statistics.addExecutionTime(System.nanoTime - startTime)
- flushQueryEngine
+ flushQueryEngine(scopePropagator)
// Scope propagation
val propagatorStartTime = System.nanoTime
@@ -144,7 +144,7 @@ class RefinementRuleProvider {
)
statistics.addExecutionTime(System.nanoTime - startTime)
- flushQueryEngine
+ flushQueryEngine(scopePropagator)
// Scope propagation
val propagatorStartTime = System.nanoTime
@@ -171,7 +171,7 @@ class RefinementRuleProvider {
)
statistics.addExecutionTime(System.nanoTime - startTime)
- flushQueryEngine
+ flushQueryEngine(scopePropagator)
// Scope propagation
val propagatorStartTime = System.nanoTime
@@ -404,7 +404,7 @@ class RefinementRuleProvider {
// Scope propagation
if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) {
- flushQueryEngine
+ flushQueryEngine(scopePropagator)
val propagatorStartTime = System.nanoTime
scopePropagator.propagateAllScopeConstraints()
@@ -581,8 +581,8 @@ class RefinementRuleProvider {
inverseInterpretation.relationlinks += inverseLink
}
- protected def flushQueryEngine() {
- if (queryEngine.updatePropagationDelayed) {
+ protected def flushQueryEngine(ScopePropagator scopePropagator) {
+ if (scopePropagator.queryEngineFlushRequiredBeforePropagation && queryEngine.updatePropagationDelayed) {
delayMessageDelivery.setBoolean(queryEngine, false)
queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates
delayMessageDelivery.setBoolean(queryEngine, true)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/META-INF/MANIFEST.MF
index 83c90829..639a8a9c 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/META-INF/MANIFEST.MF
@@ -28,7 +28,8 @@ Require-Bundle: org.eclipse.core.runtime,
org.eclipse.xtend.lib.macro,
org.eclipse.viatra.query.runtime;bundle-version="1.5.0",
org.eclipse.viatra.dse;bundle-version="0.15.0",
- hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0"
+ hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
+ org.eclipse.collections;bundle-version="10.1.0"
Bundle-ActivationPolicy: lazy
Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage
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 e4bdb086..685a1f5a 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
@@ -7,7 +7,7 @@ import org.eclipse.xtend.lib.annotations.Data
import org.eclipse.xtend2.lib.StringConcatenationClient
@Data abstract class AbstractNodeDescriptor {
- long dataHash
+ int dataHash
protected def StringConcatenationClient prettyPrint() {
'''(«dataHash»)[«class.simpleName»]'''
@@ -57,7 +57,7 @@ import org.eclipse.xtend2.lib.StringConcatenationClient
}
override hashCode() {
- return this.dataHash.hashCode
+ return this.dataHash
}
override equals(Object other) {
@@ -119,7 +119,6 @@ import org.eclipse.xtend2.lib.StringConcatenationClient
}
@Data class FurtherNodeDescriptor extends AbstractNodeDescriptor {
-
NodeRep previousRepresentation
Map, Integer> incomingEdges
Map, Integer> outgoingEdges
@@ -128,8 +127,8 @@ import org.eclipse.xtend2.lib.StringConcatenationClient
Map, Integer> outgoingEdges) {
super(calculateDataHash(previousRepresentation, incomingEdges, outgoingEdges))
this.previousRepresentation = previousRepresentation
- this.incomingEdges = new HashMap(incomingEdges)
- this.outgoingEdges = new HashMap(outgoingEdges)
+ this.incomingEdges = incomingEdges
+ this.outgoingEdges = outgoingEdges
}
static def private int calculateDataHash(NodeRep previousRepresentation,
@@ -137,14 +136,14 @@ import org.eclipse.xtend2.lib.StringConcatenationClient
val int prime = 31;
var int result = previousRepresentation.hashCode;
if (incomingEdges !== null)
- result = prime * result + incomingEdges.hashCode();
+ result = prime * result + hashIncomingNeighborhood(incomingEdges)
if (outgoingEdges !== null)
- result = prime * result + outgoingEdges.hashCode();
+ result = prime * result + hashOutgoingNeighborhood(outgoingEdges)
return result;
}
override hashCode() {
- return this.dataHash.hashCode
+ return this.dataHash
}
override equals(Object other) {
@@ -179,80 +178,31 @@ import org.eclipse.xtend2.lib.StringConcatenationClient
'''«rep»'''
}
}
+
+ private static def hashIncomingNeighborhood(Map, Integer> neighborhood) {
+ val int prime = 31
+ var int hash = 0
+ for (entry : neighborhood.entrySet) {
+ val relation = entry.key
+ hash += (prime * relation.from.hashCode + relation.type.hashCode).bitwiseXor(entry.value.hashCode)
+ }
+ hash
+ }
+
+ private static def hashOutgoingNeighborhood(Map, Integer> neighborhood) {
+ val int prime = 31
+ var int hash = 0
+ for (entry : neighborhood.entrySet) {
+ val relation = entry.key
+ hash += (prime * relation.to.hashCode + relation.type.hashCode).bitwiseXor(entry.value.hashCode)
+ }
+ hash
+ }
override toString() {
'''
«prettyPrint»
'''
}
-
-// @Pure
-// @Override
-// override public boolean equals(Object obj) {
-// if (this === obj)
-// return true;
-// if (obj === null)
-// return false;
-// if (getClass() != obj.getClass())
-// return false;
-// val AbstractNodeDescriptor other = obj as AbstractNodeDescriptor;
-// if (other.dataHash != this.dataHash)
-// return false;
-// return true;
-// }
-// @Pure
-// override public boolean equals(Object obj) {
-// if (this === obj)
-// return true;
-// if (obj === null)
-// return false;
-// if (getClass() != obj.getClass())
-// return false;
-// if (!super.equals(obj))
-// return false;
-// val FurtherNodeDescriptor> other = obj as FurtherNodeDescriptor>;
-// if (this.previousRepresentation === null) {
-// if (other.previousRepresentation != null)
-// return false;
-//
-// }
-//// } else if (!this.previousRepresentation.equals(other.previousRepresentation))
-//// return false;
-// if (this.incomingEdges === null) {
-// if (other.incomingEdges != null)
-// return false;
-// } else if (!this.incomingEdges.equals(other.incomingEdges))
-// return false;
-// if (this.outgoingEdges === null) {
-// if (other.outgoingEdges != null)
-// return false;
-// } else if (!this.outgoingEdges.equals(other.outgoingEdges))
-// return false;
-// if (this.attributeValues === null) {
-// if (other.attributeValues != null)
-// return false;
-// } else if (!this.attributeValues.equals(other.attributeValues))
-// return false;
-// 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
- * }
- * }
- */
+
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 ddf7d712..5da202eb 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
@@ -1,7 +1,8 @@
package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
-import java.util.Map
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import java.util.Map
+import org.eclipse.collections.api.factory.Maps
class PartialInterpretation2Hash extends PartialInterpretation2NeighbourhoodRepresentation{
@@ -11,15 +12,22 @@ class PartialInterpretation2Hash extends PartialInterpretation2NeighbourhoodRepr
override protected createLocalRepresentation(Map node2Representation, Map representation2Amount) {
return new NeighbourhoodWithTraces(
- representation2Amount.hashCode,node2Representation.mapValues[it.hashCode],
+ representation2Amount.hashCode,node2Representation.hashValues,
null)
}
override protected createFurtherRepresentation(Map, Integer> nodeDescriptors, Map> node2Representation, NeighbourhoodWithTraces previous, boolean deepRepresentation) {
return new NeighbourhoodWithTraces(
nodeDescriptors.hashCode,
- node2Representation.mapValues[it.hashCode],
+ node2Representation.hashValues,
if(deepRepresentation) {previous} else {null})
}
+ private def hashValues(Map map) {
+ val hashedMap = Maps.mutable.ofInitialCapacity(map.size)
+ for (entry : map.entrySet) {
+ hashedMap.put(entry.key, entry.value.hashCode)
+ }
+ hashedMap
+ }
}
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 3048167e..93eab816 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
@@ -8,11 +8,11 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
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.List
import java.util.Map
import java.util.Set
+import org.eclipse.collections.api.factory.Maps
+import org.eclipse.collections.impl.factory.Sets
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
@@ -68,10 +68,11 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation relevantTypes, Set relevantRelations, DefinedElement focusedElement) {
- val Map> types = new HashMap
+ val initialSize = model.elements.size
+ val Map> types = Maps.mutable.ofInitialCapacity(initialSize)
fillTypes(model, types, relevantTypes)
- val Map>> IncomingRelations = new HashMap;
- val Map>> OutgoingRelations = new HashMap;
+ val Map>> IncomingRelations = Maps.mutable.ofInitialCapacity(initialSize);
+ val Map>> OutgoingRelations = Maps.mutable.ofInitialCapacity(initialSize);
fillReferences(model, IncomingRelations, OutgoingRelations, relevantRelations)
val res = doRecursiveNeighbourCalculation(model, types, IncomingRelations, OutgoingRelations, range, parallels,
@@ -103,12 +104,12 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation>> IncomingRelations,
Map>> OutgoingRelations) {
val elements = types.keySet
- var Map> reachable = new HashMap
- var Map> newReachable = new HashMap
+ var Map> reachable = Maps.mutable.ofInitialCapacity(elements.size)
+ var Map> newReachable = Maps.mutable.ofInitialCapacity(elements.size)
for (element : elements) {
- val set = new HashSet
+ val set = Sets.mutable.of
set.add(element)
- reachable.put(element, new HashSet)
+ reachable.put(element, Sets.mutable.of)
newReachable.put(element, set)
}
@@ -201,8 +202,8 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation previousNumberOfTypes
lastRange = nextRange
@@ -224,7 +225,7 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation> node2Type,
Set relevantTypes) {
for (element : model.elements) {
- node2Type.put(element, new HashSet)
+ node2Type.put(element, Sets.mutable.of)
}
// for(typeDefinition : model.problem.types.filter(TypeDefinition)) {
@@ -286,7 +287,11 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation max) return Integer.MAX_VALUE else return original + 1
}
@@ -294,15 +299,11 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation>> IncomingRelations,
DefinedElement object, Map previousNodeRepresentations,
int parallel) {
- val Map, Integer> res = new HashMap
+ val Map, Integer> res = Maps.mutable.of
for (incomingConcreteEdge : IncomingRelations.get(object)) {
val IncomingRelation e = new IncomingRelation(
previousNodeRepresentations.get(incomingConcreteEdge.from), incomingConcreteEdge.type)
- if (res.containsKey(e)) {
- res.put(e, addOne(res.get(e), parallel))
- } else {
- res.put(e, 1)
- }
+ res.compute(e, [key, value | addOne(value, parallel)])
}
return res
}
@@ -310,17 +311,13 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation>> OutgoingRelations,
DefinedElement object, Map previousNodeRepresentations,
int parallel) {
- val Map, Integer> res = new HashMap
+ val Map, Integer> res = Maps.mutable.of
for (outgoingConcreteEdge : OutgoingRelations.get(object)) {
val OutgoingRelation e = new OutgoingRelation(
previousNodeRepresentations.get(outgoingConcreteEdge.to), outgoingConcreteEdge.type)
- if (res.containsKey(e)) {
- res.put(e, addOne(res.get(e), parallel))
- } else {
- res.put(e, 1)
- }
+ res.compute(e, [key, value | addOne(value, parallel)])
}
- return res;
+ return res
}
/*def private void addOrCreate_Set(Map> map, KEY key, VALUE value) {
@@ -338,16 +335,17 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation>> IncomingRelations,
Map>> OutgoingRelations, int parallels, int maxNumber) {
val previousNodeRepresentations = previous.nodeRepresentations
- val node2Representation = new HashMap>
+ val size = previousNodeRepresentations.size
+ val node2Representation = Maps.mutable.>ofInitialCapacity(size)
val Map, Integer> descriptor2Number = if (this.
mergeSimilarNeighbourhood) {
- new HashMap
+ Maps.mutable.ofInitialCapacity(size)
} else {
null
}
val Map, FurtherNodeDescriptor> uniqueDescription = if (this.
mergeSimilarNeighbourhood) {
- new HashMap
+ Maps.mutable.ofInitialCapacity(size)
} else {
null
}
@@ -392,14 +390,15 @@ abstract class PartialInterpretation2NeighbourhoodRepresentation> types,
int maxNumber, DefinedElement focusedElement) {
- val Map node2Representation = new HashMap
+ val size = types.size
+ val Map node2Representation = Maps.mutable.ofInitialCapacity(size)
val Map representation2Amount = if (mergeSimilarNeighbourhood) {
- new HashMap
+ Maps.mutable.ofInitialCapacity(size)
} else {
null
}
val Map uniqueRepresentation = if (this.mergeSimilarNeighbourhood) {
- new HashMap
+ Maps.mutable.ofInitialCapacity(size)
} else {
null
}
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 f19ac30f..04c49506 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
@@ -9,6 +9,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
import java.util.ArrayList
import java.util.Map
import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification
class NeighbourhoodBasedStateCoderFactory extends AbstractNeighbourhoodBasedStateCoderFactory {
new() {
@@ -38,6 +39,7 @@ class NeighbourhoodBasedHashStateCoderFactory extends AbstractNeighbourhoodBased
class NeighbourhoodBasedPartialInterpretationStateCoder extends AbstractNeighbourhoodBasedPartialInterpretationStateCoder {
val PartialInterpretation2NeighbourhoodRepresentation calculator
+ val Map, String> fullyQualifiedNames = newHashMap
var Map nodeRepresentations = null
var ModelRep modelRepresentation = null
@@ -55,27 +57,36 @@ class NeighbourhoodBasedPartialInterpretationStateCoder exten
modelRepresentation = code.modelRepresentation
nodeRepresentations = code.nodeRepresentations
}
+
+ private def getFullyQualifiedNameCached(IQuerySpecification> specification) {
+ fullyQualifiedNames.computeIfAbsent(specification, [fullyQualifiedName])
+ }
override doCreateActivationCode(IPatternMatch match) {
val size = match.specification.parameters.size
- val res = new ArrayList(size)
- var int equivalenceHash = 0
+ var int hash = 0
val prime = 31
for (var int index = 0; index < size; index++) {
val matchArgument = match.get(index)
- res.add(getCode(matchArgument))
+ val code = getCode(matchArgument)
+ val codeNumber = if (code === null) {
+ 0
+ } else {
+ code.hashCode
+ }
+ hash = prime * hash + codeNumber
for (var i = 0; i < index; i++) {
val number = if (matchArgument === match.get(i)) {
1
} else {
0
}
- equivalenceHash = prime * equivalenceHash + number
+ hash = prime * hash + number
}
}
- match.specification.fullyQualifiedName -> (res -> equivalenceHash).hashCode
+ match.specification.fullyQualifiedNameCached -> hash
}
def private getCode(Object o) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index fd871615..c333feca 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -206,7 +206,7 @@ class ViatraReasoner extends LogicReasoner {
it.transformationTime = (transformationTime / 1000000) as int
for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {
it.entries += createIntStatisticEntry => [
- it.name = '''_Solution«pair.key»FoundAt'''
+ it.name = '''Solution«pair.key»FoundAt'''
it.value = (pair.value / 1000000) as int
]
}
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
index 57eaf326..192dac7b 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
@@ -33,10 +33,8 @@ generate {
runtime = 10000,
log-level = normal,
"fitness-scope" = "3",
- "fitness-punishSize" = "inverse",
- "fitness-objectCreationCosts" = "true",
- "scopePropagator" = "typeHierarchy",
- "fitness-missing-containment" = "2"
+ "fitness-punishSize" = "true",
+ "scopePropagator" = "polyhedral"
}
runs = 1
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
index 7d742202..ee3c3631 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
@@ -35,7 +35,11 @@ generate {
config = {
runtime = 10000,
log-level = normal,
- "fitness-objectCreationCosts" = "true"
+ "fitness-scope" = "1",
+ "fitness-punishSize" = "inverse",
+ "fitness-objectCreationCosts" = "true",
+ "scopePropagator" = "typeHierarchy",
+ "fitness-missing-containment" = "2"
}
runs = 1
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/Resource50hh.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/Resource50hh.xmi
new file mode 100644
index 00000000..5b110b76
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/Resource50hh.xmi
@@ -0,0 +1,59 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--
cgit v1.2.3-70-g09d2