diff --git a/src/main/java/nl/uu/cs/ape/APE.java b/src/main/java/nl/uu/cs/ape/APE.java index 29a5ecb5..35b51647 100644 --- a/src/main/java/nl/uu/cs/ape/APE.java +++ b/src/main/java/nl/uu/cs/ape/APE.java @@ -25,19 +25,19 @@ import nl.uu.cs.ape.configuration.APERunConfig; import nl.uu.cs.ape.configuration.tags.validation.ValidationResults; import nl.uu.cs.ape.constraints.ConstraintTemplate; -import nl.uu.cs.ape.domain.APEDimensionsException; -import nl.uu.cs.ape.domain.APEDomainSetup; -import nl.uu.cs.ape.domain.OWLReader; import nl.uu.cs.ape.models.MappingsException; import nl.uu.cs.ape.models.enums.SynthesisFlag; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.solver.SynthesisEngine; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; import nl.uu.cs.ape.solver.solutionStructure.SolutionWorkflow; import nl.uu.cs.ape.solver.solutionStructure.SolutionsList; import nl.uu.cs.ape.solver.solutionStructure.cwl.DefaultCWLCreator; import nl.uu.cs.ape.utils.APEFiles; import nl.uu.cs.ape.utils.APEUtils; +import nl.uu.cs.ape.utils.OWLReader; /** * The {@code APE} class is the main class of the library and is supposed to be @@ -52,7 +52,7 @@ public class APE implements APEInterface { private final APECoreConfig config; /** Object containing general APE encoding. */ - private APEDomainSetup apeDomainSetup; + private Domain apeDomainSetup; /** * Create instance of the APE solver. @@ -125,7 +125,7 @@ private boolean setupDomain() throws APEDimensionsException, IOException, OWLOnt * Encode the taxonomies as objects - generate the list of all types / modules * occurring in the taxonomies defining their submodules/subtypes */ - apeDomainSetup = new APEDomainSetup(config); + apeDomainSetup = new Domain(config); OWLReader owlReader = new OWLReader(apeDomainSetup, config.getOntologyFile()); boolean ontologyRead = owlReader.readOntology(); @@ -185,7 +185,7 @@ public APECoreConfig getConfig() { * @return The object that contains all crucial information about the domain * (e.g. list of tools, data types, constraint factory, etc.) */ - public APEDomainSetup getDomainSetup() { + public Domain getDomainSetup() { return apeDomainSetup; } @@ -284,7 +284,7 @@ public SolutionsList runSynthesis(APERunConfig runConfig) throws IOException, JS * file. * @throws JSONException Error in configuration object. */ - private SolutionsList runSynthesis(JSONObject runConfigJson, APEDomainSetup apeDomainSetup) + private SolutionsList runSynthesis(JSONObject runConfigJson, Domain apeDomainSetup) throws IOException, JSONException, APEConfigException { apeDomainSetup.clearConstraints(); APERunConfig runConfig = new APERunConfig(runConfigJson, apeDomainSetup); diff --git a/src/main/java/nl/uu/cs/ape/APEInterface.java b/src/main/java/nl/uu/cs/ape/APEInterface.java index 4cc9a999..5abc84f9 100644 --- a/src/main/java/nl/uu/cs/ape/APEInterface.java +++ b/src/main/java/nl/uu/cs/ape/APEInterface.java @@ -11,8 +11,8 @@ import nl.uu.cs.ape.configuration.APECoreConfig; import nl.uu.cs.ape.configuration.APERunConfig; import nl.uu.cs.ape.constraints.ConstraintTemplate; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import nl.uu.cs.ape.solver.solutionStructure.SolutionsList; /** @@ -45,7 +45,7 @@ public interface APEInterface { * @return The object that contains all crucial information about the domain * (e.g. list of tools, data types, constraint factory, etc.) */ - public APEDomainSetup getDomainSetup(); + public Domain getDomainSetup(); /** * Returns all the taxonomy elements that are subclasses of the given element. diff --git a/src/main/java/nl/uu/cs/ape/Main.java b/src/main/java/nl/uu/cs/ape/Main.java index e0b07f7e..80819cad 100644 --- a/src/main/java/nl/uu/cs/ape/Main.java +++ b/src/main/java/nl/uu/cs/ape/Main.java @@ -27,8 +27,15 @@ public class Main { * The entry point of application when the library is used in a Command Line * Interface (CLI). * - * @param args APE expects at most one (1) argument: The absolute or relative - * path to the configuration file. + * @param args APE expects at most two (2) arguments:
+ *
+ * (1) the absolute or relative path to the configuration file.
+ *
+ * (2) the maximum number of solutions to be returned. + * + * Note: If no arguments are provided, the default configuration + * file on location ./config.json is used. + * */ public static void main(String[] args) { String path; diff --git a/src/main/java/nl/uu/cs/ape/automaton/Block.java b/src/main/java/nl/uu/cs/ape/automaton/Block.java index fbcf6719..5864f230 100644 --- a/src/main/java/nl/uu/cs/ape/automaton/Block.java +++ b/src/main/java/nl/uu/cs/ape/automaton/Block.java @@ -14,7 +14,7 @@ public class Block { * States that comprise this block. Number of stater correspond to the max * number of inputs or outputs. */ - private List typeStates; + private final List typeStates; /** * Order number of the block in the solution. @@ -27,7 +27,7 @@ public class Block { * @param blockNumber The block number. */ public Block(int blockNumber) { - typeStates = new ArrayList(); + typeStates = new ArrayList<>(); this.blockNumber = blockNumber; } diff --git a/src/main/java/nl/uu/cs/ape/automaton/ModuleAutomaton.java b/src/main/java/nl/uu/cs/ape/automaton/ModuleAutomaton.java index e5ab3b47..21ffe1e1 100644 --- a/src/main/java/nl/uu/cs/ape/automaton/ModuleAutomaton.java +++ b/src/main/java/nl/uu/cs/ape/automaton/ModuleAutomaton.java @@ -19,7 +19,7 @@ */ public class ModuleAutomaton implements Automaton { - private List moduleStates; + private final List moduleStates = new ArrayList<>(); /** * Generate the Module State automatons based on the defined length. @@ -31,7 +31,6 @@ public class ModuleAutomaton implements Automaton { * modules). */ public ModuleAutomaton(int automataBound, int inputBranching, int outputBranching) { - moduleStates = new ArrayList(); automataBound = Math.max(automataBound, 1); for (int i = 1; i <= automataBound; i++) { diff --git a/src/main/java/nl/uu/cs/ape/automaton/State.java b/src/main/java/nl/uu/cs/ape/automaton/State.java index fc048acb..3eda2229 100644 --- a/src/main/java/nl/uu/cs/ape/automaton/State.java +++ b/src/main/java/nl/uu/cs/ape/automaton/State.java @@ -1,7 +1,7 @@ package nl.uu.cs.ape.automaton; import nl.uu.cs.ape.models.enums.AtomType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; /*** * The {@code State} class is used to represent the states in module and type @@ -15,7 +15,7 @@ * * @author Vedran Kasalica */ -public class State implements PredicateLabel, StateInterface { +public class State implements Predicate, StateInterface { /** Unique name of the state */ private final String stateName; @@ -98,7 +98,7 @@ public boolean equals(Object obj) { * before than, equal to, or after than the specified State. */ @Override - public int compareTo(PredicateLabel other) { + public int compareTo(Predicate other) { if (!(other instanceof State)) { return this.getPredicateID().compareTo(other.getPredicateID()); } diff --git a/src/main/java/nl/uu/cs/ape/automaton/TypeAutomaton.java b/src/main/java/nl/uu/cs/ape/automaton/TypeAutomaton.java index 68fe0806..2037cac1 100644 --- a/src/main/java/nl/uu/cs/ape/automaton/TypeAutomaton.java +++ b/src/main/java/nl/uu/cs/ape/automaton/TypeAutomaton.java @@ -27,13 +27,13 @@ public class TypeAutomaton implements Automaton { * Blocks of data types that are being added to the memory (usually outputs from * the tools, apart from the initial workflow input). */ - private List memoryTypesAutomaton; + private final List memoryTypesAutomaton = new ArrayList<>(); /** * Blocks of data types that are being used by tools from the memory (inputs to * the tools). */ - private List usedTypesAutomaton; + private final List usedTypesAutomaton = new ArrayList<>(); /** * State is used in order to represent no state. @@ -54,8 +54,6 @@ public class TypeAutomaton implements Automaton { * modules) */ public TypeAutomaton(int automataBound, int inputBranching, int outputBranching) { - memoryTypesAutomaton = new ArrayList(); - usedTypesAutomaton = new ArrayList(); nullState = new State(null, null, -1, inputBranching, outputBranching); automataBound = automataBound < 1 ? 1 : automataBound; @@ -224,7 +222,7 @@ public Block getMemoryTypesBlock(int i) { * @return List of memory States. */ public List getMemoryStatesUntilBlockNo(int maxBlockNo) { - List untilStates = new ArrayList(); + List untilStates = new ArrayList<>(); for (int i = 0; i <= maxBlockNo && i < this.usedTypesAutomaton.size(); i++) { Block currBlock = this.getMemoryTypesBlock(i); for (State currState : currBlock.getStates()) { @@ -244,7 +242,7 @@ public List getMemoryStatesUntilBlockNo(int maxBlockNo) { * @return List of Type States. */ public List getAllStatesUntilBlockNo(int maxBlockNo) { - List untilStates = new ArrayList(); + List untilStates = new ArrayList<>(); for (int i = 0; i <= maxBlockNo && i < this.usedTypesAutomaton.size(); i++) { Block currBlock = this.usedTypesAutomaton.get(i); for (State currState : currBlock.getStates()) { @@ -268,7 +266,7 @@ public List getAllStatesUntilBlockNo(int maxBlockNo) { * @return List of Memory Type States. */ public List getAllMemoryStatesUntilBlockNo(int maxBlockNo) { - List untilStates = new ArrayList(); + List untilStates = new ArrayList<>(); for (int i = 0; i <= maxBlockNo && i < this.usedTypesAutomaton.size(); i++) { Block currBlock = this.memoryTypesAutomaton.get(i); for (State currState : currBlock.getStates()) { @@ -287,7 +285,7 @@ public List getAllMemoryStatesUntilBlockNo(int maxBlockNo) { * @return List of memory States. */ public List getMemoryStatesAfterBlockNo(int minBlockNo) { - List afterStates = new ArrayList(); + List afterStates = new ArrayList<>(); for (int i = minBlockNo + 1; i < this.memoryTypesAutomaton.size(); i++) { Block currBlock = this.getMemoryTypesBlock(i); for (State currState : currBlock.getStates()) { @@ -307,7 +305,7 @@ public List getMemoryStatesAfterBlockNo(int minBlockNo) { * @return List of Used States. */ public List getUsedStatesAfterBlockNo(int minBlockNo) { - List afterStates = new ArrayList(); + List afterStates = new ArrayList<>(); for (int i = minBlockNo + 1; i < this.usedTypesAutomaton.size(); i++) { Block currBlock = this.usedTypesAutomaton.get(i); for (State currState : currBlock.getStates()) { @@ -324,7 +322,7 @@ public List getUsedStatesAfterBlockNo(int minBlockNo) { */ @Override public List getAllStates() { - List allStates = new ArrayList(); + List allStates = new ArrayList<>(); for (Block currBlock : getAllBlocks()) { for (State currState : currBlock.getStates()) { allStates.add(currState); @@ -339,7 +337,7 @@ public List getAllStates() { * @return List of memory type states. */ public List getAllMemoryTypesStates() { - List allMemoryStates = new ArrayList(); + List allMemoryStates = new ArrayList<>(); for (Block currBlock : getMemoryTypesBlocks()) { for (State currState : currBlock.getStates()) { allMemoryStates.add(currState); @@ -354,7 +352,7 @@ public List getAllMemoryTypesStates() { * @return List of used type states. */ public List getAllUsedTypesStates() { - List allUsedStates = new ArrayList(); + List allUsedStates = new ArrayList<>(); for (Block currBlock : getUsedTypesBlocks()) { for (State currState : currBlock.getStates()) { allUsedStates.add(currState); diff --git a/src/main/java/nl/uu/cs/ape/configuration/APECoreConfig.java b/src/main/java/nl/uu/cs/ape/configuration/APECoreConfig.java index 14357fb4..1d490c04 100644 --- a/src/main/java/nl/uu/cs/ape/configuration/APECoreConfig.java +++ b/src/main/java/nl/uu/cs/ape/configuration/APECoreConfig.java @@ -11,10 +11,10 @@ import nl.uu.cs.ape.configuration.tags.APEConfigTags; import nl.uu.cs.ape.configuration.tags.APEConfigTagFactory.TAGS.*; import nl.uu.cs.ape.configuration.tags.validation.ValidationResults; -import nl.uu.cs.ape.domain.APEDimensionsException; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; import nl.uu.cs.ape.utils.APEFiles; import nl.uu.cs.ape.utils.APEUtils; -import nl.uu.cs.ape.domain.OWLReader; +import nl.uu.cs.ape.utils.OWLReader; import java.io.File; import java.io.IOException; diff --git a/src/main/java/nl/uu/cs/ape/configuration/APERunConfig.java b/src/main/java/nl/uu/cs/ape/configuration/APERunConfig.java index bfc2cd5a..ba1e1bba 100644 --- a/src/main/java/nl/uu/cs/ape/configuration/APERunConfig.java +++ b/src/main/java/nl/uu/cs/ape/configuration/APERunConfig.java @@ -11,11 +11,11 @@ import nl.uu.cs.ape.configuration.tags.APEConfigTags; import nl.uu.cs.ape.configuration.tags.APEConfigTagFactory.TAGS.*; import nl.uu.cs.ape.configuration.tags.validation.ValidationResults; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.models.Range; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.ConfigEnum; import nl.uu.cs.ape.models.enums.SolverType; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import java.io.IOException; import java.nio.file.Path; @@ -99,12 +99,12 @@ public class APERunConfig { /** * Input types of the workflow. */ - private final APEConfigDependentTag.One, APEDomainSetup> PROGRAM_INPUTS = new APEConfigTagFactory.TAGS.PROGRAM_INPUTS( + private final APEConfigDependentTag.One, Domain> PROGRAM_INPUTS = new APEConfigTagFactory.TAGS.PROGRAM_INPUTS( this::getApeDomainSetup); /** * Output types of the workflow. */ - private final APEConfigDependentTag.One, APEDomainSetup> PROGRAM_OUTPUTS = new APEConfigTagFactory.TAGS.PROGRAM_OUTPUTS( + private final APEConfigDependentTag.One, Domain> PROGRAM_OUTPUTS = new APEConfigTagFactory.TAGS.PROGRAM_OUTPUTS( this::getApeDomainSetup); /** * All the Tags specified in this class. Should be in correct order of @@ -153,10 +153,7 @@ public class APERunConfig { * Object containing domain information needed for the execution. */ @Getter - private APEDomainSetup apeDomainSetup; - - /** Solver type that should be used (SAT). */ - private SolverType solverType = SolverType.SAT; + private Domain apeDomainSetup; /** * Constructor used to implement the Builder Pattern. @@ -189,10 +186,10 @@ private APERunConfig(Builder builder) { /** * Private constructor used by - * {@link APERunConfig#validate(JSONObject config, APEDomainSetup setup)} + * {@link APERunConfig#validate(JSONObject config, Domain setup)} * to create an empty instance. */ - private APERunConfig(APEDomainSetup setup) { + private APERunConfig(Domain setup) { this.apeDomainSetup = setup; } @@ -206,7 +203,7 @@ private APERunConfig(APEDomainSetup setup) { * @param setup the domain setup * @return the validation results */ - public static ValidationResults validate(JSONObject json, APEDomainSetup setup) { + public static ValidationResults validate(JSONObject json, Domain setup) { APERunConfig dummy = new APERunConfig(setup); ValidationResults results = new ValidationResults(); for (APEConfigTag tag : dummy.all_tags) { @@ -229,7 +226,7 @@ public static ValidationResults validate(JSONObject json, APEDomainSetup setup) * @throws JSONException Error in parsing the configuration file. * @throws APEConfigException Error in setting up the the configuration. */ - public APERunConfig(JSONObject runConfiguration, APEDomainSetup apeDomainSetup) + public APERunConfig(JSONObject runConfiguration, Domain apeDomainSetup) throws IOException, JSONException, APEConfigException { /* JSONObject must have been parsed correctly. */ @@ -577,22 +574,6 @@ public void setSolutionLength(int solutionMinLength, int solutionMaxLength) { this.SOLUTION_LENGTH_RANGE.setValue(Range.of(solutionMinLength, solutionMaxLength)); } - /** - * Gets the Solver type that should be used for solving. - * - * @return {@link SolverType} that corresponds to the solver type - */ - public SolverType getSolverType() { - return this.solverType; - } - - /** - * @param solverType the solverType to set - */ - public void setSolverType(SolverType solverType) { - this.solverType = solverType; - } - /** * Creates interface for the min length of {@link APERunConfig}. */ @@ -624,7 +605,7 @@ public interface IMaxNoSolutionsStage { * Creates interface to setup the domain of {@link APERunConfig}. */ public interface IApeDomainSetupStage { - IBuildStage withApeDomainSetup(APEDomainSetup apeDomainSetup); + IBuildStage withApeDomainSetup(Domain apeDomainSetup); } /** @@ -671,7 +652,7 @@ public static final class Builder implements ISolutionMinLengthStage, ISolutionM private int solutionMinLength; private int solutionMaxLength; private int maxNoSolutions; - private APEDomainSetup apeDomainSetup; + private Domain apeDomainSetup; private JSONArray constraintsJSON; private boolean toolSeqRepeat; private String solutionDirPath; @@ -708,7 +689,7 @@ public IApeDomainSetupStage withMaxNoSolutions(int maxNoSolutions) { } @Override - public IBuildStage withApeDomainSetup(APEDomainSetup apeDomainSetup) { + public IBuildStage withApeDomainSetup(Domain apeDomainSetup) { this.apeDomainSetup = apeDomainSetup; return this; } diff --git a/src/main/java/nl/uu/cs/ape/configuration/tags/APEConfigTagFactory.java b/src/main/java/nl/uu/cs/ape/configuration/tags/APEConfigTagFactory.java index 02f49c4a..3f9c6b8d 100644 --- a/src/main/java/nl/uu/cs/ape/configuration/tags/APEConfigTagFactory.java +++ b/src/main/java/nl/uu/cs/ape/configuration/tags/APEConfigTagFactory.java @@ -6,17 +6,15 @@ import nl.uu.cs.ape.configuration.APEConfigException; import nl.uu.cs.ape.configuration.tags.validation.ValidationResults; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEFiles; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.Range; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.ConfigEnum; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import javax.inject.Provider; -import static nl.uu.cs.ape.configuration.tags.APEConfigTag.TagType.*; - import java.io.File; import java.io.IOException; import java.nio.file.Path; @@ -119,9 +117,9 @@ public TagType getType() { /** * Abstract field type. */ - public abstract static class DataInstances extends APEConfigDependentTag.One, APEDomainSetup> { + public abstract static class DataInstances extends APEConfigDependentTag.One, Domain> { - protected DataInstances(Provider provider) { + protected DataInstances(Provider provider) { super(provider); } @@ -131,7 +129,7 @@ public TagType getType() { } @Override - protected ValidationResults validate(List value, APEDomainSetup apeDomainSetup, + protected ValidationResults validate(List value, Domain apeDomainSetup, ValidationResults results) { // TODO: check data instances return results; @@ -485,7 +483,7 @@ public APEConfigDefaultValue> getDefault() { */ public static class PROGRAM_INPUTS extends TYPES.DataInstances { - public PROGRAM_INPUTS(Provider provider) { + public PROGRAM_INPUTS(Provider provider) { super(provider); } @@ -505,7 +503,7 @@ public String getDescription() { } @Override - protected List constructFromJSON(JSONObject obj, APEDomainSetup apeDomainSetup) { + protected List constructFromJSON(JSONObject obj, Domain apeDomainSetup) { final ArrayList instances = new ArrayList<>(); if (apeDomainSetup == null) { @@ -535,7 +533,7 @@ protected List constructFromJSON(JSONObject obj, APEDomainSetup apeDomainS */ public static class PROGRAM_OUTPUTS extends TYPES.DataInstances { - public PROGRAM_OUTPUTS(Provider provider) { + public PROGRAM_OUTPUTS(Provider provider) { super(provider); } @@ -555,7 +553,7 @@ public String getDescription() { } @Override - protected List constructFromJSON(JSONObject obj, APEDomainSetup apeDomainSetup) { + protected List constructFromJSON(JSONObject obj, Domain apeDomainSetup) { final ArrayList instances = new ArrayList<>(); if (apeDomainSetup == null) { diff --git a/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java b/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java index c54391a4..ef5952a0 100644 --- a/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java +++ b/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java @@ -2,12 +2,12 @@ import java.util.*; +import lombok.NoArgsConstructor; import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.automaton.ModuleAutomaton; import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.domain.APEDomainSetup; -import nl.uu.cs.ape.models.AllModules; -import nl.uu.cs.ape.models.AllTypes; +import nl.uu.cs.ape.models.DomainModules; +import nl.uu.cs.ape.models.DomainTypes; import nl.uu.cs.ape.models.ConstraintTemplateData; import nl.uu.cs.ape.models.SATAtomMappings; import nl.uu.cs.ape.models.enums.AtomType; @@ -15,6 +15,7 @@ import nl.uu.cs.ape.models.templateFormulas.SLTLxTemplateFormula; import nl.uu.cs.ape.models.templateFormulas.SLTLxTemplateFinally; import nl.uu.cs.ape.models.templateFormulas.SLTLxTemplateGlobally; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; /** * The {@code ConstraintFactory} class represents the Factory Method Pattern for @@ -24,16 +25,10 @@ * @author Vedran Kasalica */ @Slf4j +@NoArgsConstructor public class ConstraintFactory { - private Map constraintTemplates; - - /** - * Instantiates a new Constraint factory. - */ - public ConstraintFactory() { - this.constraintTemplates = new HashMap<>(); - } + private final Map constraintTemplates = new HashMap<>(); /** * Retrieves a list of the constraint templates. @@ -95,7 +90,7 @@ public String printConstraintsCodes() { * @return String description of all the formats (ID, description and number of * parameters for each). */ - public boolean initializeConstraints(AllModules allModules, AllTypes allTypes) { + public boolean initializeConstraints(DomainModules allModules, DomainTypes allTypes) { TaxonomyPredicate rootModule = allModules.getRootModule(); List rootTypes = allTypes.getDataTaxonomyDimensions(); @@ -331,7 +326,7 @@ protected ConstraintDependModule(String id, List pa } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -359,7 +354,7 @@ protected ConstraintGenType(String id, List paramet } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -392,7 +387,7 @@ protected ConstraintIf_genThenNotType(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -422,7 +417,7 @@ protected ConstraintIf_genThenType(String id, List } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -452,7 +447,7 @@ protected ConstraintIfThenModule(String id, List pa } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -481,7 +476,7 @@ protected ConstraintIfThenNotModule(String id, List } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -510,7 +505,7 @@ protected ConstraintIfUseThenNotType(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -540,7 +535,7 @@ protected ConstraintIfUseThenType(String id, List p } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -570,7 +565,7 @@ protected Constraint_lastModule(String id, List par } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -599,7 +594,7 @@ protected Constraint_nextModule(String id, List par } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -628,7 +623,7 @@ protected ConstraintNotGenType(String id, List para } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -660,7 +655,7 @@ protected ConstraintNotUseModule(String id, List pa } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -691,7 +686,7 @@ protected ConstraintNotUseType(String id, List para } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -723,7 +718,7 @@ protected Constraint_prevModule(String id, List par } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -751,7 +746,7 @@ protected ConstraintUseModule(String id, List param } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -781,7 +776,7 @@ protected ConstraintUseType(String id, List paramet } @Override - public String getConstraint(List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -812,7 +807,7 @@ protected ConstraintUseModuleWithInput(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -843,7 +838,7 @@ protected ConstraintUseModuleWithOutput(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -874,7 +869,7 @@ protected Constraint_connectedModules(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -904,7 +899,7 @@ protected ConstraintNot_connectedModules(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); @@ -934,7 +929,7 @@ protected ConstraintNot_repeatModules(String id, List parameters, APEDomainSetup domainSetup, + public String getConstraint(List parameters, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { if (parameters.size() != this.getNoOfParameters()) { super.throwParametersError(parameters.size()); diff --git a/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplate.java b/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplate.java index 4e963603..d04a0c18 100644 --- a/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplate.java +++ b/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplate.java @@ -6,9 +6,9 @@ import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.automaton.ModuleAutomaton; import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.models.SATAtomMappings; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import java.util.List; @@ -118,7 +118,7 @@ public ConstraintTemplateParameter getParameter(int index) { * @return The String CNF representation of the constraint. null in case of * incorrect number of constraint parameters. */ - public abstract String getConstraint(List list, APEDomainSetup domainSetup, + public abstract String getConstraint(List list, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings); diff --git a/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplateParameter.java b/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplateParameter.java index 604d039d..733d821d 100644 --- a/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplateParameter.java +++ b/src/main/java/nl/uu/cs/ape/constraints/ConstraintTemplateParameter.java @@ -7,18 +7,17 @@ import org.json.JSONObject; import lombok.extern.slf4j.Slf4j; -import nl.uu.cs.ape.domain.APEDimensionsException; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.AbstractModule; import nl.uu.cs.ape.models.Module; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; /** * The {@code ConstraintTemplateParameter} class is used to represent a - * parameter of a - * constraint. + * parameter of a constraint. * * @author Vedran Kasalica */ @@ -40,7 +39,7 @@ public ConstraintTemplateParameter(List parameterTypes) { if (parameterTypes != null) { this.parameterTypes = parameterTypes; } else { - this.parameterTypes = new ArrayList(); + this.parameterTypes = new ArrayList<>(); } } @@ -48,7 +47,7 @@ public ConstraintTemplateParameter(List parameterTypes) { * Instantiates a new Constraint parameter. */ public ConstraintTemplateParameter() { - this.parameterTypes = new ArrayList(); + this.parameterTypes = new ArrayList<>(); } /** @@ -108,7 +107,7 @@ public JSONObject toJSON() { * @throws APEDimensionsException if the referenced types/modules are not well * defined */ - public TaxonomyPredicate readConstraintParameterFromJson(JSONObject jsonParam, APEDomainSetup domainSetup) + public TaxonomyPredicate readConstraintParameterFromJson(JSONObject jsonParam, Domain domainSetup) throws JSONException, APEDimensionsException { if (parameterTypes.get(0) instanceof Type) { return Type.taxonomyInstanceFromJson(jsonParam, domainSetup, false); diff --git a/src/main/java/nl/uu/cs/ape/models/AuxModulePredicate.java b/src/main/java/nl/uu/cs/ape/models/AuxModulePredicate.java index 29d404a0..d0f0a7c0 100644 --- a/src/main/java/nl/uu/cs/ape/models/AuxModulePredicate.java +++ b/src/main/java/nl/uu/cs/ape/models/AuxModulePredicate.java @@ -4,11 +4,11 @@ import java.util.SortedSet; import java.util.TreeSet; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.enums.LogicOperation; import nl.uu.cs.ape.models.enums.NodeType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; /** * The {@code AuxModulePredicate} class represents an abstract class used @@ -74,7 +74,7 @@ private AuxModulePredicate(String moduleName, String moduleID, String rootNode, * disjunction/conjunction of the labels. */ public static AbstractModule generateAuxiliaryPredicate(SortedSet relatedPredicates, - LogicOperation logicOp, APEDomainSetup domainSetup) { + LogicOperation logicOp, Domain domainSetup) { if (relatedPredicates.isEmpty()) { return null; } diff --git a/src/main/java/nl/uu/cs/ape/models/AuxTypePredicate.java b/src/main/java/nl/uu/cs/ape/models/AuxTypePredicate.java index ee2758a5..dabbc775 100644 --- a/src/main/java/nl/uu/cs/ape/models/AuxTypePredicate.java +++ b/src/main/java/nl/uu/cs/ape/models/AuxTypePredicate.java @@ -4,11 +4,11 @@ import java.util.SortedSet; import java.util.TreeSet; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.enums.LogicOperation; import nl.uu.cs.ape.models.enums.NodeType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; /** * The {@code AuxTypePredicate} class represents an abstract class used @@ -67,7 +67,7 @@ private AuxTypePredicate(String typeName, String typeID, String rootNode, NodeTy * disjunction/conjunction of the labels. */ public static Type generateAuxiliaryPredicate(SortedSet relatedPredicates, - LogicOperation logicOp, APEDomainSetup domainSetup) { + LogicOperation logicOp, Domain domainSetup) { if (relatedPredicates.isEmpty()) { return null; } diff --git a/src/main/java/nl/uu/cs/ape/models/AuxiliaryPredicate.java b/src/main/java/nl/uu/cs/ape/models/AuxiliaryPredicate.java index 60f29179..6edb8e39 100644 --- a/src/main/java/nl/uu/cs/ape/models/AuxiliaryPredicate.java +++ b/src/main/java/nl/uu/cs/ape/models/AuxiliaryPredicate.java @@ -3,7 +3,7 @@ import java.util.SortedSet; import nl.uu.cs.ape.models.enums.LogicOperation; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; /** @@ -13,7 +13,7 @@ * @author Vedran Kasalica * */ -public interface AuxiliaryPredicate extends PredicateLabel { +public interface AuxiliaryPredicate extends Predicate { /** * Gets logic operator used to group the abstracted predicates. diff --git a/src/main/java/nl/uu/cs/ape/models/AllModules.java b/src/main/java/nl/uu/cs/ape/models/DomainModules.java similarity index 89% rename from src/main/java/nl/uu/cs/ape/models/AllModules.java rename to src/main/java/nl/uu/cs/ape/models/DomainModules.java index 46fb1741..15a8dd2f 100644 --- a/src/main/java/nl/uu/cs/ape/models/AllModules.java +++ b/src/main/java/nl/uu/cs/ape/models/DomainModules.java @@ -7,25 +7,25 @@ import nl.uu.cs.ape.configuration.APECoreConfig; import nl.uu.cs.ape.utils.APEUtils; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; /** - * The {@code AllModules} class represent the set of all modules/tools that can - * be - * part of our program. Each of them is either {@link Module} or + * The {@code DomainModules} class represent the set of all modules/tools that + * are part of the configured domain. They can + * be steps in generated workflows. Each of them is either {@link Module} or * {@link AbstractModule}. * * @author Vedran Kasalica */ -public class AllModules extends AllPredicates { +public class DomainModules extends DomainPredicates { /** * Instantiates a new All modules. * * @param config the config */ - public AllModules(APECoreConfig config) { + public DomainModules(APECoreConfig config) { super(Arrays.asList(config.getToolTaxonomyRoot())); } @@ -34,7 +34,7 @@ public AllModules(APECoreConfig config) { * * @param moduleTaxonomyRoot root module */ - public AllModules(String moduleTaxonomyRoot) { + public DomainModules(String moduleTaxonomyRoot) { super(Arrays.asList(moduleTaxonomyRoot)); } @@ -125,9 +125,9 @@ public AbstractModule get(String moduleID) { * * @return List of pairs of modules. */ - public Set> getSimplePairs() { + public Set> getSimplePairs() { - Set iterator = new HashSet(); + Set iterator = new HashSet(); for (TaxonomyPredicate module : getMappedPredicates().values()) { if (module.isSimplePredicate()) { iterator.add(module); diff --git a/src/main/java/nl/uu/cs/ape/models/AllPredicates.java b/src/main/java/nl/uu/cs/ape/models/DomainPredicates.java similarity index 94% rename from src/main/java/nl/uu/cs/ape/models/AllPredicates.java rename to src/main/java/nl/uu/cs/ape/models/DomainPredicates.java index 0a00e6c6..d11c07d5 100644 --- a/src/main/java/nl/uu/cs/ape/models/AllPredicates.java +++ b/src/main/java/nl/uu/cs/ape/models/DomainPredicates.java @@ -6,17 +6,18 @@ import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; /** - * The {@code AllPredicates} class is used to group all mappedPredicates of the - * same type (such as module, data) into one collection. + * The {@code DomainPredicates} abstract class represents a collection of + * predicates of the + * same type (e.g., module, data) within the configured domain. * * @author Vedran Kasalica */ -public abstract class AllPredicates { +public abstract class DomainPredicates { /** * Map of all predicated mapped to their predicateID. */ - private Map mappedPredicates; + private final Map mappedPredicates = new HashMap<>(); /** * Root of the taxonomy. @@ -28,9 +29,8 @@ public abstract class AllPredicates { * * @param taxonomyRoots the taxonomy roots */ - protected AllPredicates(List taxonomyRoots) { + protected DomainPredicates(List taxonomyRoots) { this.dimensionRoots = taxonomyRoots; - this.mappedPredicates = new HashMap<>(); } /** diff --git a/src/main/java/nl/uu/cs/ape/models/AllTypes.java b/src/main/java/nl/uu/cs/ape/models/DomainTypes.java similarity index 87% rename from src/main/java/nl/uu/cs/ape/models/AllTypes.java rename to src/main/java/nl/uu/cs/ape/models/DomainTypes.java index 07ef4d71..623e909a 100644 --- a/src/main/java/nl/uu/cs/ape/models/AllTypes.java +++ b/src/main/java/nl/uu/cs/ape/models/DomainTypes.java @@ -6,53 +6,51 @@ import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.configuration.APECoreConfig; -import nl.uu.cs.ape.domain.APEDimensionsException; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.enums.NodeType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; /** - * The {@code AllTypes} class represent the set of all the data dimensions that - * can be used in our program. The data - * can be grouped in multiple data dimensions (e.g. types,formats, etc.) and + * The {@code DomainTypes} class represent the collection of all the data types + * within the configured domain. + * The data types are grouped in one or more data dimensions (e.g. + * types,formats, etc.) and * each {@link Type} will belong to one of those dimensions. * * @author Vedran Kasalica */ @Slf4j -public class AllTypes extends AllPredicates { +public class DomainTypes extends DomainPredicates { - private static String empty = "empty"; - private static String apeLabel = "APE_label"; - private static String emptyLabel = "emptyLabel"; + private static final String empty = "empty"; + private static final String apeLabel = "APE_label"; + private static final String emptyLabel = "emptyLabel"; /** * {@link Type} object representing the "empty type". */ - private Type emptyType; + private final Type emptyType = new Type(empty, empty, empty, NodeType.EMPTY); /** * {@link Type} object representing the "empty label root". */ - private Type apeLabelRoot; + private final Type apeLabelRoot = new Type(apeLabel, apeLabel, apeLabel, NodeType.ROOT); /** * {@link Type} object representing the "empty label type". */ - private Type emptyLabelType; + private final Type emptyLabelType = new Type(emptyLabel, emptyLabel, apeLabel, NodeType.EMPTY_LABEL); /** * Instantiates a new AllTypes object. * * @param config the config */ - public AllTypes(APECoreConfig config) { + public DomainTypes(APECoreConfig config) { super(Stream.concat(config.getDataDimensionRoots().stream(), Stream.of(apeLabel)) .collect(Collectors.toList())); - emptyType = new Type(empty, empty, empty, NodeType.EMPTY); - apeLabelRoot = new Type(apeLabel, apeLabel, apeLabel, NodeType.ROOT); - emptyLabelType = new Type(emptyLabel, emptyLabel, apeLabel, NodeType.EMPTY_LABEL); setRelevant(emptyType); setRelevant(apeLabelRoot); setRelevant(emptyLabelType); @@ -65,12 +63,9 @@ public AllTypes(APECoreConfig config) { * * @param typeTaxonomyRoots the list of data dimension roots */ - public AllTypes(List typeTaxonomyRoots) { + public DomainTypes(List typeTaxonomyRoots) { super(Stream.concat(typeTaxonomyRoots.stream(), Stream.of(apeLabel)) .collect(Collectors.toList())); - emptyType = new Type(empty, empty, empty, NodeType.EMPTY); - apeLabelRoot = new Type(apeLabel, apeLabel, apeLabel, NodeType.ROOT); - emptyLabelType = new Type(emptyLabel, emptyLabel, apeLabel, NodeType.EMPTY_LABEL); setRelevant(emptyType); setRelevant(apeLabelRoot); setRelevant(emptyLabelType); @@ -233,8 +228,8 @@ public Class getPredicateClass() { * * @return List of pairs of types. */ - public List> getTypePairsForEachSubTaxonomy() { - List> pairs = new ArrayList>(); + public List> getTypePairsForEachSubTaxonomy() { + List> pairs = new ArrayList>(); /* * Create a list for each subtree of the Data Taxonomy (e.g. TypeSubTaxonomy, @@ -272,7 +267,7 @@ public List> getTypePairsForEachSubTaxonomy() { for (List iterator : subTreesMap.values()) { for (int i = 0; i < iterator.size() - 1; i++) { for (int j = i + 1; j < iterator.size(); j++) { - pairs.add(new Pair(iterator.get(i), iterator.get(j))); + pairs.add(new Pair(iterator.get(i), iterator.get(j))); } } } diff --git a/src/main/java/nl/uu/cs/ape/models/Module.java b/src/main/java/nl/uu/cs/ape/models/Module.java index 4cae6dfd..e94951b7 100644 --- a/src/main/java/nl/uu/cs/ape/models/Module.java +++ b/src/main/java/nl/uu/cs/ape/models/Module.java @@ -3,12 +3,12 @@ import org.json.JSONException; import org.json.JSONObject; -import nl.uu.cs.ape.domain.APEDimensionsException; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.enums.LogicOperation; import nl.uu.cs.ape.models.enums.NodeType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import java.util.*; @@ -24,12 +24,12 @@ public class Module extends AbstractModule { /** * List of input types required by the tool. */ - private List moduleInput; + private final List moduleInput; /** * List of output types generated by the tool. */ - private List moduleOutput; + private final List moduleOutput; /** * Tool execution command. @@ -62,8 +62,8 @@ public class Module extends AbstractModule { public Module(String moduleName, String moduleID, String rootNode, List moduleInput, List moduleOutput, String moduleExecution) { super(moduleName, moduleID, rootNode, NodeType.LEAF); - this.moduleInput = new ArrayList(moduleInput); - this.moduleOutput = new ArrayList(moduleOutput); + this.moduleInput = new ArrayList<>(moduleInput); + this.moduleOutput = new ArrayList<>(moduleOutput); this.executionCommand = moduleExecution; } @@ -79,8 +79,8 @@ public Module(String moduleName, String moduleID, String rootNode, List mo */ public Module(String moduleName, String moduleID, String rootNode, String moduleExecution) { super(moduleName, moduleID, rootNode, NodeType.LEAF); - this.moduleInput = new ArrayList(); - this.moduleOutput = new ArrayList(); + this.moduleInput = new ArrayList<>(); + this.moduleOutput = new ArrayList<>(); this.executionCommand = moduleExecution; } @@ -112,12 +112,15 @@ public List getModuleInput() { } /** - * Sets module input. + * Sets module input to the given list of types. * * @param moduleInputs the module inputs */ public void setModuleInput(List moduleInputs) { - this.moduleInput = moduleInputs; + moduleInput.clear(); + for (Type currModuleInput : moduleInputs) { + addModuleInput(currModuleInput); + } } /** @@ -149,7 +152,10 @@ public List getModuleOutput() { * @param moduleOutput the module output */ public void setModuleOutput(List moduleOutput) { - this.moduleOutput = moduleOutput; + moduleOutput.clear(); + for (Type currModuleOutput : moduleOutput) { + addModuleOutput(currModuleOutput); + } } /** @@ -222,11 +228,11 @@ public void setCwlImplementation(Map cwlImplementation) { * @throws JSONException if the given JSON is not well formatted * @throws APEDimensionsException if the referenced modules are not well defined */ - public static AbstractModule taxonomyInstanceFromJson(JSONObject jsonParam, APEDomainSetup domainSetup) + public static AbstractModule taxonomyInstanceFromJson(JSONObject jsonParam, Domain domainSetup) throws JSONException { /* Set of predicates where each describes a type dimension */ SortedSet parameterDimensions = new TreeSet(); - AllModules allModules = domainSetup.getAllModules(); + DomainModules allModules = domainSetup.getAllModules(); /* Iterate through each of the dimensions */ for (String currRootLabel : jsonParam.keySet()) { String curRootIRI = currRootLabel; diff --git a/src/main/java/nl/uu/cs/ape/models/SATAtomMappings.java b/src/main/java/nl/uu/cs/ape/models/SATAtomMappings.java index 7a70b041..9365383c 100644 --- a/src/main/java/nl/uu/cs/ape/models/SATAtomMappings.java +++ b/src/main/java/nl/uu/cs/ape/models/SATAtomMappings.java @@ -1,11 +1,13 @@ package nl.uu.cs.ape.models; +import java.io.Serializable; import java.util.HashMap; import java.util.Map; +import lombok.NoArgsConstructor; import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.models.enums.AtomType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtomVar; @@ -20,7 +22,8 @@ * * @author Vedran Kasalica */ -public class SATAtomMappings { +@NoArgsConstructor +public class SATAtomMappings implements Serializable { /** * First variable that can be used for auxiliary variables. @@ -28,57 +31,37 @@ public class SATAtomMappings { * {@code false}. */ private static final int auxDefaultInit = 3; + /** + * Last number used to represent auxiliary introduced variables. + * Numbers 1 and 2 are special symbols. 1 is {@code true} and 2 is + * {@code false}. + */ + private int auxiliary = auxDefaultInit; /** Max number of all auxiliary variables. */ private static final int auxMax = 100000; + /** Max number of all expected atoms containing variables. */ private static final int atomVarMaxNo = 100000; + + /** Number of mapped atoms. */ + private int atomNo = auxMax + atomVarMaxNo + 1; + + /** Number of mapped atoms containing variables. */ + private int atomVarNo = auxMax + 1; + /** Mapping of the atoms to integers. */ - private Map mappings; + private final Map mappings = new HashMap<>(); /** Inverse mapping from integers to atoms. */ - private Map reverseMapping; + private final Map reverseMapping = new HashMap<>(); /** Map of all the IDs that were mapped to atoms. */ - private Map mapped; + private final Map mapped = new HashMap<>(); /** Mapping of the atoms over variables to integers. */ - private Map vMappings; + private final Map vMappings = new HashMap<>(); /** Inverse mapping from integers to atoms containing variables. */ - private Map vReverseMapping; + private final Map vReverseMapping = new HashMap<>(); /** Map of all the IDs that were mapped to atoms containing variables. */ - private Map vMapped; - - /** - * Number of mapped atoms. - */ - private int atomNo; - - /** - * Number of mapped atoms containing variables. - */ - private int atomVarNo; - - /** - * Last number used to represent auxiliary introduced variables. - * Numbers 1 and 2 are special symbols. 1 is {@code true} and 2 is - * {@code false}. - */ - private int auxiliary; - - /** - * Instantiates a new SLTLxAtom mappings. - */ - public SATAtomMappings() { - mappings = new HashMap(); - reverseMapping = new HashMap(); - mapped = new HashMap(); - vMappings = new HashMap(); - vReverseMapping = new HashMap(); - vMapped = new HashMap(); - - /* First auxMax variables are reserved for auxiliary variables */ - auxiliary = auxDefaultInit; - atomVarNo = auxMax + 1; - atomNo = auxMax + atomVarMaxNo + 1; - } + private final Map vMapped = new HashMap<>(); /** * Function is returning the mapping number of the @@ -93,7 +76,7 @@ public SATAtomMappings() { * (such as {@link AtomType#MODULE}. * @return Mapping number of the atom (number is always > 0). */ - public synchronized Integer add(PredicateLabel predicate, State usedInState, AtomType elementType) + public synchronized Integer add(Predicate predicate, State usedInState, AtomType elementType) throws MappingsException { SLTLxAtom atom = new SLTLxAtom(elementType, predicate, usedInState); @@ -211,7 +194,7 @@ public int getSize() { } /** - * Get the next auxiliary number and increase the counterErrors by 1. + * Get the next auxiliary number and increase the counter by 1. * * @return Mapping number that can be used for auxiliary variables. */ diff --git a/src/main/java/nl/uu/cs/ape/models/Type.java b/src/main/java/nl/uu/cs/ape/models/Type.java index 71eb621f..5cde4756 100644 --- a/src/main/java/nl/uu/cs/ape/models/Type.java +++ b/src/main/java/nl/uu/cs/ape/models/Type.java @@ -6,12 +6,12 @@ import org.json.JSONException; import org.json.JSONObject; -import nl.uu.cs.ape.domain.APEDimensionsException; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.enums.LogicOperation; import nl.uu.cs.ape.models.enums.NodeType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; /** * The {@code Type} class represents data dimension (e.g. data type, data @@ -97,12 +97,12 @@ public Type getPlainType() { * @throws JSONException if the given JSON is not well formatted * @throws APEDimensionsException if the referenced types are not well defined */ - public static Type taxonomyInstanceFromJson(JSONObject jsonParam, APEDomainSetup domainSetup, boolean isOutputData) + public static Type taxonomyInstanceFromJson(JSONObject jsonParam, Domain domainSetup, boolean isOutputData) throws JSONException, APEDimensionsException { /* Set of predicates where each describes a type dimension */ SortedSet parameterDimensions = new TreeSet<>(); boolean labelDefined = false; - AllTypes allTypes = domainSetup.getAllTypes(); + DomainTypes allTypes = domainSetup.getAllTypes(); /* Iterate through each of the dimensions */ for (String currRootLabel : jsonParam.keySet()) { String curRootIRI = currRootLabel; diff --git a/src/main/java/nl/uu/cs/ape/models/logic/constructs/APEPredicate.java b/src/main/java/nl/uu/cs/ape/models/logic/constructs/APEPredicate.java deleted file mode 100644 index e9771a75..00000000 --- a/src/main/java/nl/uu/cs/ape/models/logic/constructs/APEPredicate.java +++ /dev/null @@ -1,11 +0,0 @@ -package nl.uu.cs.ape.models.logic.constructs; - -/** - * Class provides interface for all APE related predicated used in the encoding. - * - * @author Vedran Kasalica - * - */ -public interface APEPredicate { - -} diff --git a/src/main/java/nl/uu/cs/ape/models/logic/constructs/CustomLabel.java b/src/main/java/nl/uu/cs/ape/models/logic/constructs/CustomPredicate.java similarity index 78% rename from src/main/java/nl/uu/cs/ape/models/logic/constructs/CustomLabel.java rename to src/main/java/nl/uu/cs/ape/models/logic/constructs/CustomPredicate.java index a77ceecb..a4d6df68 100644 --- a/src/main/java/nl/uu/cs/ape/models/logic/constructs/CustomLabel.java +++ b/src/main/java/nl/uu/cs/ape/models/logic/constructs/CustomPredicate.java @@ -1,22 +1,23 @@ package nl.uu.cs.ape.models.logic.constructs; /** - * The {@code CustomLabel} used to represent custom labels (dimension) of the - * data. + * The {@code CustomPredicate} used to represent custom predicates describing + * the data, + * e.g., new data dimensions. * * @author Vedran Kasalica * */ -public class CustomLabel implements PredicateLabel { +public class CustomPredicate implements Predicate { private String label; - public CustomLabel(String label) { + public CustomPredicate(String label) { this.label = label; } @Override - public int compareTo(PredicateLabel arg0) { + public int compareTo(Predicate arg0) { return this.getPredicateID().compareTo(arg0.getPredicateID()); } @@ -61,7 +62,7 @@ public boolean equals(Object obj) { return false; if (getClass() != obj.getClass()) return false; - CustomLabel other = (CustomLabel) obj; + CustomPredicate other = (CustomPredicate) obj; if (label == null) { if (other.label != null) return false; diff --git a/src/main/java/nl/uu/cs/ape/models/logic/constructs/PredicateLabel.java b/src/main/java/nl/uu/cs/ape/models/logic/constructs/Predicate.java similarity index 87% rename from src/main/java/nl/uu/cs/ape/models/logic/constructs/PredicateLabel.java rename to src/main/java/nl/uu/cs/ape/models/logic/constructs/Predicate.java index eaf00573..7548eb80 100644 --- a/src/main/java/nl/uu/cs/ape/models/logic/constructs/PredicateLabel.java +++ b/src/main/java/nl/uu/cs/ape/models/logic/constructs/Predicate.java @@ -1,12 +1,12 @@ package nl.uu.cs.ape.models.logic.constructs; /** - * The {@code PredicateLabel} class is used to represent a label that describes + * The {@code Predicate} class is used to represent a label that describes * predicates, such as data types, operations or states in the system. * * @author Vedran Kasalica */ -public interface PredicateLabel extends Comparable, APEPredicate { +public interface Predicate extends Comparable { /** * Get the unique predicate identifier defined as String. diff --git a/src/main/java/nl/uu/cs/ape/models/logic/constructs/TaxonomyPredicate.java b/src/main/java/nl/uu/cs/ape/models/logic/constructs/TaxonomyPredicate.java index 63f3fae6..ffc401f0 100644 --- a/src/main/java/nl/uu/cs/ape/models/logic/constructs/TaxonomyPredicate.java +++ b/src/main/java/nl/uu/cs/ape/models/logic/constructs/TaxonomyPredicate.java @@ -5,7 +5,7 @@ import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.utils.APEUtils; -import nl.uu.cs.ape.models.AllPredicates; +import nl.uu.cs.ape.models.DomainPredicates; import nl.uu.cs.ape.models.enums.NodeType; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; @@ -19,7 +19,7 @@ * @author Vedran Kasalica */ @Slf4j -public abstract class TaxonomyPredicate implements PredicateLabel { +public abstract class TaxonomyPredicate implements Predicate { /** * Describes the node in from the taxonomy hierarchy. The type can represent a @@ -131,7 +131,7 @@ public boolean equals(Object obj) { return true; } - public int compareTo(PredicateLabel other) { + public int compareTo(Predicate other) { if (!(other instanceof TaxonomyPredicate)) { return this.getPredicateID().compareTo(other.getPredicateID()); } @@ -211,7 +211,7 @@ public Map toMap() { * @param allPredicates Map of all the predicates of the given type. * @return true if the predicates were successfully set to be relevant. */ - public boolean setAsRelevantTaxonomyTerm(AllPredicates allPredicates) { + public boolean setAsRelevantTaxonomyTerm(DomainPredicates allPredicates) { if (this.isRelevant) { return true; } @@ -236,7 +236,7 @@ public boolean setAsRelevantTaxonomyTerm(AllPredicates allPredicates) { * @param allPredicates Map of all the predicates of the given type. * @return true if the predicates were successfully set to be relevant. */ - private boolean setAsRelevantTaxonomyTermTopDown(AllPredicates allPredicates) { + private boolean setAsRelevantTaxonomyTermTopDown(DomainPredicates allPredicates) { if (this.isRelevant) { return true; } @@ -258,7 +258,7 @@ private boolean setAsRelevantTaxonomyTermTopDown(AllPredicates allPredicates) { * @param allPredicates Map of all the predicates of the given type. * @return true if the predicates were successfully set to be relevant. */ - private boolean setAsRelevantTaxonomyTermBottomUp(AllPredicates allPredicates) { + private boolean setAsRelevantTaxonomyTermBottomUp(DomainPredicates allPredicates) { if (this.isRelevant) { return true; } @@ -307,7 +307,7 @@ public String toShortString() { * distinguish between the tree levels. * @param allPredicates Set of all the predicates. */ - public void printTree(String str, AllPredicates allPredicates) { + public void printTree(String str, DomainPredicates allPredicates) { log.debug(str + toShortString() + "[" + getNodeType() + "]"); for (TaxonomyPredicate predicate : APEUtils.safe(this.subPredicates)) { predicate.printTree(str + ". ", allPredicates); diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/CNFClause.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/CNFClause.java index a76aaecc..00864fd4 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/CNFClause.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/CNFClause.java @@ -16,7 +16,7 @@ */ public class CNFClause { - List atoms; + private final List atoms = new ArrayList<>(); /** * Create clause based on the list of elements (integers, bigger that 0) @@ -25,7 +25,6 @@ public class CNFClause { */ public CNFClause(List atoms) { super(); - this.atoms = new ArrayList<>(); atoms.forEach(atom -> this.atoms.add(atom)); } @@ -36,7 +35,6 @@ public CNFClause(List atoms) { */ public CNFClause(Integer atom) { super(); - this.atoms = new ArrayList<>(); this.atoms.add(atom); } @@ -51,7 +49,7 @@ public CNFClause(Integer atom) { */ public static Set conjunctClausesCollection(Set> facts) { Set allClauses = new HashSet<>(); - facts.forEach(col -> allClauses.addAll(col)); + facts.forEach(allClauses::addAll); return allClauses; } diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtom.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtom.java index 4fa7b87f..ae9ea4da 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtom.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtom.java @@ -4,7 +4,7 @@ import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.models.enums.AtomType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; /** @@ -17,7 +17,7 @@ public class SLTLxAtom extends SLTLxFormula implements Comparable { /** * StateInterface that is referred (tool or type). */ - private final PredicateLabel predicate; + private final Predicate predicate; /** * State in which the type/operation was used. @@ -46,7 +46,7 @@ public class SLTLxAtom extends SLTLxFormula implements Comparable { * @param predicate Predicate used. * @param usedInState State in the automaton it was used/created in. */ - public SLTLxAtom(AtomType elementType, PredicateLabel predicate, State usedInState) { + public SLTLxAtom(AtomType elementType, Predicate predicate, State usedInState) { super(); this.predicate = predicate; this.argumentState = usedInState; @@ -71,7 +71,7 @@ private SLTLxAtom(int mapping) { * * @return Field {@link #predicate}. */ - public PredicateLabel getPredicate() { + public Predicate getPredicate() { return predicate; } diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtomVar.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtomVar.java index 03531485..3b5a0175 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtomVar.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxAtomVar.java @@ -6,7 +6,7 @@ import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.enums.AtomType; import nl.uu.cs.ape.models.enums.AtomVarType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; /** @@ -21,7 +21,7 @@ public class SLTLxAtomVar extends SLTLxFormula { * First argument is usually predicate that is referred (tool or type), or a * variable representing a type state. */ - private PredicateLabel firstArg; + private Predicate firstArg; /** * Second argument is a variable representing a typeState. @@ -50,7 +50,7 @@ public class SLTLxAtomVar extends SLTLxFormula { * @param secondArg - Variable representing state in the automaton it was * used/created in. */ - public SLTLxAtomVar(AtomVarType elementType, PredicateLabel firstArg, SLTLxVariable secondArg) { + public SLTLxAtomVar(AtomVarType elementType, Predicate firstArg, SLTLxVariable secondArg) { super(); this.firstArg = firstArg; this.secondArg = secondArg; @@ -62,7 +62,7 @@ public SLTLxAtomVar(AtomVarType elementType, PredicateLabel firstArg, SLTLxVaria * * @return Field {@link #firstArg}. */ - public PredicateLabel getFirstArg() { + public Predicate getFirstArg() { return firstArg; } diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxConjunction.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxConjunction.java index d21632be..06ad3049 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxConjunction.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxConjunction.java @@ -14,11 +14,11 @@ */ public class SLTLxConjunction extends SLTLxFormula { - private Set conjunctedFacts; + /** Set of conjuncted facts. */ + private final Set conjunctedFacts = new HashSet<>(); public SLTLxConjunction(SLTLxFormula arg1, SLTLxFormula arg2) { super(); - this.conjunctedFacts = new HashSet<>(); if (arg1 != null) this.conjunctedFacts.add(arg1); if (arg2 != null) @@ -27,7 +27,6 @@ public SLTLxConjunction(SLTLxFormula arg1, SLTLxFormula arg2) { public SLTLxConjunction(SLTLxFormula arg1, SLTLxFormula arg2, SLTLxFormula arg3) { super(); - this.conjunctedFacts = new HashSet<>(); if (arg1 != null) this.conjunctedFacts.add(arg1); if (arg2 != null) @@ -38,7 +37,6 @@ public SLTLxConjunction(SLTLxFormula arg1, SLTLxFormula arg2, SLTLxFormula arg3) public SLTLxConjunction(Collection conjunctedFacts) { super(); - this.conjunctedFacts = new HashSet<>(); conjunctedFacts.forEach(fact -> { if (fact != null) this.conjunctedFacts.add(fact); diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxDisjunction.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxDisjunction.java index a32de782..ccf41688 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxDisjunction.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxDisjunction.java @@ -14,11 +14,11 @@ */ public class SLTLxDisjunction extends SLTLxFormula { - private Set disjointFacts; + /** Set of disjoint facts. */ + private final Set disjointFacts = new HashSet<>(); public SLTLxDisjunction(SLTLxFormula arg1, SLTLxFormula arg2) { super(); - this.disjointFacts = new HashSet<>(); if (arg1 != null) this.disjointFacts.add(arg1); if (arg2 != null) @@ -27,7 +27,6 @@ public SLTLxDisjunction(SLTLxFormula arg1, SLTLxFormula arg2) { public SLTLxDisjunction(Collection conjunctedFacts) { super(); - this.disjointFacts = new HashSet<>(); conjunctedFacts.forEach(fact -> { if (fact != null) this.disjointFacts.add(fact); diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxExists.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxExists.java index 4e522909..d26306df 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxExists.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxExists.java @@ -22,15 +22,15 @@ public SLTLxExists(SLTLxVariable boundVariable, SLTLxFormula formula) { public Set getCNFEncoding(int stateNo, SLTLxVariableSubstitutionCollection curVarMapping, SATSynthesisEngine synthesisEngine) { Set clauses = new HashSet<>(); - SLTLxVariableSubstitutionCollection newVarMappping = new SLTLxVariableSubstitutionCollection(curVarMapping); - SLTLxVariable flatBindedVariable = newVarMappping.addNewVariable(boundVariable, + SLTLxVariableSubstitutionCollection newVarMapping = new SLTLxVariableSubstitutionCollection(curVarMapping); + SLTLxVariable flatBindedVariable = newVarMapping.addNewVariable(boundVariable, SLTLxVariable.getVariableDomain(stateNo, synthesisEngine)); /** Encode the possible substitutions for the given variable. */ - clauses.addAll(flatBindedVariable.getExistentialCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(flatBindedVariable.getExistentialCNFEncoding(stateNo, newVarMapping, synthesisEngine)); /** Encode the variable substitution and the underlying formula. */ - clauses.addAll(super.getCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(super.getCNFEncoding(stateNo, newVarMapping, synthesisEngine)); return clauses; } @@ -42,17 +42,17 @@ public Set getNegatedCNFEncoding(int stateNo, SLTLxVariableSubstitutionC /** Encode the possible substitutions for the given variable. */ SLTLxVariable.getVariableDomain(stateNo, synthesisEngine).forEach( state -> { - SLTLxVariableSubstitutionCollection newVarMappping = new SLTLxVariableSubstitutionCollection( + SLTLxVariableSubstitutionCollection newVarMapping = new SLTLxVariableSubstitutionCollection( curVarMapping); Set domainState = new HashSet<>(); domainState.add(state); - SLTLxVariable flatBindedVariable = newVarMappping.addNewVariable(boundVariable, domainState); + SLTLxVariable flatBindedVariable = newVarMapping.addNewVariable(boundVariable, domainState); /* Encode the substitution. */ clauses.addAll( - flatBindedVariable.getUniversalCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + flatBindedVariable.getUniversalCNFEncoding(stateNo, newVarMapping, synthesisEngine)); /** Encode the variable substitution and the underlying formula. */ - clauses.addAll(super.getNegatedCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(super.getNegatedCNFEncoding(stateNo, newVarMapping, synthesisEngine)); }); return clauses; diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxForall.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxForall.java index 4d74c6a6..686811f2 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxForall.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxForall.java @@ -26,17 +26,17 @@ public Set getCNFEncoding(int stateNo, SLTLxVariableSubstitutionCollecti /** Encode the possible substitutions for the given variable. */ SLTLxVariable.getVariableDomain(stateNo, synthesisEngine).forEach( state -> { - SLTLxVariableSubstitutionCollection newVarMappping = new SLTLxVariableSubstitutionCollection( + SLTLxVariableSubstitutionCollection newVarMapping = new SLTLxVariableSubstitutionCollection( curVarMapping); Set domainState = new HashSet<>(); domainState.add(state); - SLTLxVariable flatBindedVariable = newVarMappping.addNewVariable(boundVariable, domainState); + SLTLxVariable flatBindedVariable = newVarMapping.addNewVariable(boundVariable, domainState); /* Encode the substitution. */ clauses.addAll( - flatBindedVariable.getUniversalCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + flatBindedVariable.getUniversalCNFEncoding(stateNo, newVarMapping, synthesisEngine)); /** Encode the variable substitution and the underlying formula. */ - clauses.addAll(super.getCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(super.getCNFEncoding(stateNo, newVarMapping, synthesisEngine)); }); return clauses; @@ -45,16 +45,16 @@ public Set getCNFEncoding(int stateNo, SLTLxVariableSubstitutionCollecti @Override public Set getNegatedCNFEncoding(int stateNo, SLTLxVariableSubstitutionCollection curVarMapping, SATSynthesisEngine synthesisEngine) { - Set clauses = new HashSet(); - SLTLxVariableSubstitutionCollection newVarMappping = new SLTLxVariableSubstitutionCollection(curVarMapping); - SLTLxVariable flatBindedVariable = newVarMappping.addNewVariable(boundVariable, + Set clauses = new HashSet<>(); + SLTLxVariableSubstitutionCollection newVarMapping = new SLTLxVariableSubstitutionCollection(curVarMapping); + SLTLxVariable flatBindedVariable = newVarMapping.addNewVariable(boundVariable, SLTLxVariable.getVariableDomain(stateNo, synthesisEngine)); /** Encode the possible substitutions for the given variable. */ - clauses.addAll(flatBindedVariable.getExistentialCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(flatBindedVariable.getExistentialCNFEncoding(stateNo, newVarMapping, synthesisEngine)); /** Encode the variable substitution and the underlying formula. */ - clauses.addAll(super.getNegatedCNFEncoding(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(super.getNegatedCNFEncoding(stateNo, newVarMapping, synthesisEngine)); return clauses; } diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxLiteral.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxLiteral.java index 8fab0086..8ec64e9d 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxLiteral.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxLiteral.java @@ -3,7 +3,7 @@ import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.models.SATAtomMappings; import nl.uu.cs.ape.models.enums.AtomType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; /** * The {@code SLTLxLiteral} class represents literals (atoms that can be @@ -160,7 +160,7 @@ public SLTLxAtom getAtom() { * * @return StateInterface object that is referred by the literal. */ - public PredicateLabel getPredicate() { + public Predicate getPredicate() { return atom.getPredicate(); } diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVarQuantification.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVarQuantification.java index aee5382f..3aabefcd 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVarQuantification.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVarQuantification.java @@ -25,7 +25,7 @@ protected SLTLxVarQuantification(SLTLxVariable boundVariable, SLTLxFormula formu @Override public Set getCNFEncoding(int stateNo, SLTLxVariableSubstitutionCollection newVarMapping, SATSynthesisEngine synthesisEngine) { - Set clauses = new HashSet(); + Set clauses = new HashSet<>(); SLTLxVariable flatBoundVariable = newVarMapping.getVarSabstitute(boundVariable); /** Encode the underlying formula. */ clauses.addAll(formula.getCNFEncoding(stateNo, newVarMapping, synthesisEngine)); diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariable.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariable.java index e1a78e1e..c13c62ff 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariable.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariable.java @@ -9,7 +9,7 @@ import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.enums.AtomType; import nl.uu.cs.ape.models.enums.AtomVarType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; /*** @@ -23,7 +23,7 @@ * * @author Vedran Kasalica */ -public class SLTLxVariable implements StateInterface, PredicateLabel { +public class SLTLxVariable implements StateInterface, Predicate { /** Unique name of the type state variable */ private final String variableID; @@ -75,7 +75,7 @@ public String getPredicateID() { return variableID; } - public int compareTo(PredicateLabel other) { + public int compareTo(Predicate other) { return this.getPredicateID().compareTo(other.getPredicateID()); } @@ -207,7 +207,7 @@ private static Set generateDataPropertySubstitutionRules(SLTLxVari */ for (State varState : variableSubstitutions.getVariableDomain(variable)) { - for (PredicateLabel usedPred : varOccurrences.getDataTypes(variable)) { + for (Predicate usedPred : varOccurrences.getDataTypes(variable)) { /* (VAL(?x,a) => (P(?x) <=> P(a)) */ allFacts.add(new SLTLxImplication( new SLTLxAtomVar( @@ -357,7 +357,7 @@ public Set getVariableMutualExclusion(int stateNo, SLTLxVariableSubstitu * and thus we use the next state to get the domain of the variable. */ int nextStateNo = stateNo + 1; - Set> statePairs = APEUtils + Set> statePairs = APEUtils .getUniquePairs(synthesisEngine.getTypeAutomaton().getAllMemoryStatesUntilBlockNo(nextStateNo)); statePairs.forEach(statePair -> { diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableOccurrenceCollection.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableOccurrenceCollection.java index d2fe26e4..eff7a9a6 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableOccurrenceCollection.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableOccurrenceCollection.java @@ -5,11 +5,12 @@ import java.util.Map; import java.util.Set; +import lombok.NoArgsConstructor; import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.enums.AtomVarType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; /** * Class used to list all usages of the given variables within the formulas. @@ -17,30 +18,20 @@ * @author Vedran Kasalica * */ +@NoArgsConstructor public class SLTLxVariableOccurrenceCollection { /** Mapping variables to their predicate properties. */ - private Map> variableDataTypes; + private final Map> variableDataTypes = new HashMap<>(); /** * Mapping variables (depicting memory states) to tool inputs that reference * them. */ - private Map> variableMemoryReferences; + private final Map> variableMemoryReferences = new HashMap<>(); /** Mapping pairs variables to their usages under binary predicates. */ - private Map, Set> binaryPredicates; + private final Map, Set> binaryPredicates = new HashMap<>(); /** Variable mapping to variables it is combined with under a pair. */ - private Map>> variablePairs; - - /** - * Create the variable usage class. - */ - public SLTLxVariableOccurrenceCollection() { - super(); - this.variableDataTypes = new HashMap<>(); - this.variableMemoryReferences = new HashMap<>(); - this.binaryPredicates = new HashMap<>(); - this.variablePairs = new HashMap<>(); - } + private final Map>> variablePairs = new HashMap<>(); /** * Associate the data type to the corresponding variable. @@ -50,9 +41,9 @@ public SLTLxVariableOccurrenceCollection() { * @return {@code true} if the property was associated with the variable, * {@code false} otherwise. */ - public boolean addDataType(PredicateLabel dataType, SLTLxVariable variableState) { + public boolean addDataType(Predicate dataType, SLTLxVariable variableState) { if (this.variableDataTypes.get(variableState) == null) { - Set preds = new HashSet<>(); + Set preds = new HashSet<>(); boolean tmp = preds.add(dataType); this.variableDataTypes.put(variableState, preds); return tmp; @@ -136,9 +127,9 @@ public void addBinaryPred(Pair varPair, AtomVarType relType) { * @return Set (possibly empty) of memory references that are mentioned in * combination with the given variable. */ - public Set getDataTypes(SLTLxVariable satVariable) { - Set unaryPreds = this.variableDataTypes.get(satVariable); - return ((unaryPreds == null) ? new HashSet() : unaryPreds); + public Set getDataTypes(SLTLxVariable satVariable) { + Set unaryPreds = this.variableDataTypes.get(satVariable); + return ((unaryPreds == null) ? new HashSet() : unaryPreds); } /** diff --git a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableSubstitutionCollection.java b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableSubstitutionCollection.java index 581e09ff..bd7696ba 100644 --- a/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableSubstitutionCollection.java +++ b/src/main/java/nl/uu/cs/ape/models/sltlxStruc/SLTLxVariableSubstitutionCollection.java @@ -4,6 +4,7 @@ import java.util.Map; import java.util.Set; +import lombok.NoArgsConstructor; import nl.uu.cs.ape.automaton.State; /** @@ -13,24 +14,16 @@ * @author Vedran Kasalica * */ +@NoArgsConstructor public class SLTLxVariableSubstitutionCollection { /** Variable mapping to unique IDs. */ - private Map mappedVariables; + private final Map mappedVariables = new HashMap<>(); /** Variable mapping to its domain. */ - private Map> variableDomain; + private final Map> variableDomain = new HashMap<>(); /** Number of variables. */ private static int variableNo = 1; - /** - * Create a new variable mapping class. - */ - public SLTLxVariableSubstitutionCollection() { - super(); - this.mappedVariables = new HashMap<>(); - this.variableDomain = new HashMap<>(); - } - /** * Create a new variable mapping, based on the existing one. * @@ -38,11 +31,9 @@ public SLTLxVariableSubstitutionCollection() { */ public SLTLxVariableSubstitutionCollection(SLTLxVariableSubstitutionCollection existing) { super(); - this.mappedVariables = new HashMap<>(); for (SLTLxVariable key : existing.mappedVariables.keySet()) { this.mappedVariables.put(key, existing.mappedVariables.get(key)); } - this.variableDomain = new HashMap<>(); for (SLTLxVariable key : existing.variableDomain.keySet()) { this.variableDomain.put(key, existing.variableDomain.get(key)); } diff --git a/src/main/java/nl/uu/cs/ape/models/templateFormulas/SLTLxTemplateFormula.java b/src/main/java/nl/uu/cs/ape/models/templateFormulas/SLTLxTemplateFormula.java index 108be1e7..71bd3be0 100644 --- a/src/main/java/nl/uu/cs/ape/models/templateFormulas/SLTLxTemplateFormula.java +++ b/src/main/java/nl/uu/cs/ape/models/templateFormulas/SLTLxTemplateFormula.java @@ -10,7 +10,6 @@ import nl.uu.cs.ape.automaton.ModuleAutomaton; import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.AbstractModule; import nl.uu.cs.ape.models.Module; @@ -19,6 +18,7 @@ import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.AtomType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; /** * The class is used to represent a predefined SLTLx constraints according to a @@ -615,7 +615,7 @@ public static String notConnectedModules(TaxonomyPredicate firstPredicate, Taxon return constraints.toString(); } - public static String notRepeatModules(TaxonomyPredicate predicate, APEDomainSetup domainSetup, + public static String notRepeatModules(TaxonomyPredicate predicate, Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { StringBuilder constraints = new StringBuilder(); diff --git a/src/main/java/nl/uu/cs/ape/parserSLTLx/SLTLxSATVisitor.java b/src/main/java/nl/uu/cs/ape/parserSLTLx/SLTLxSATVisitor.java index 8dc05741..e3f416b2 100644 --- a/src/main/java/nl/uu/cs/ape/parserSLTLx/SLTLxSATVisitor.java +++ b/src/main/java/nl/uu/cs/ape/parserSLTLx/SLTLxSATVisitor.java @@ -12,8 +12,8 @@ import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.AbstractModule; -import nl.uu.cs.ape.models.AllModules; -import nl.uu.cs.ape.models.AllTypes; +import nl.uu.cs.ape.models.DomainModules; +import nl.uu.cs.ape.models.DomainTypes; import nl.uu.cs.ape.models.enums.AtomVarType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; @@ -67,8 +67,8 @@ public class SLTLxSATVisitor extends SLTLxBaseVisitor { static int usedState = 0; int memIndexFactor; - private final AllTypes allTypes; - private final AllModules allModules; + private final DomainTypes allTypes; + private final DomainModules allModules; private String ontologyPrexifIRI; public SLTLxSATVisitor(SATSynthesisEngine synthesisEngine) { diff --git a/src/main/java/nl/uu/cs/ape/solver/EncodingPredicates.java b/src/main/java/nl/uu/cs/ape/solver/EncodingPredicates.java new file mode 100644 index 00000000..429f2af7 --- /dev/null +++ b/src/main/java/nl/uu/cs/ape/solver/EncodingPredicates.java @@ -0,0 +1,32 @@ +package nl.uu.cs.ape.solver; + +import java.util.ArrayList; +import java.util.List; + +import lombok.Getter; +import lombok.NoArgsConstructor; +import nl.uu.cs.ape.models.AuxiliaryPredicate; + +/** + * The {@code EncodingPredicates} class is used to store the helper predicates, + * i.e., predicates that are used to encode complex + * logic expressions. + */ +@NoArgsConstructor +public abstract class EncodingPredicates { + + /** + * Helper predicates defined within the domain model. + */ + @Getter + private final List helperPredicates = new ArrayList<>(); + + /** + * Add predicate to the list of auxiliary predicates that should be encoded. + * + * @param helperPredicate + */ + public void addHelperPredicate(AuxiliaryPredicate helperPredicate) { + helperPredicates.add(helperPredicate); + } +} diff --git a/src/main/java/nl/uu/cs/ape/solver/ModuleUtils.java b/src/main/java/nl/uu/cs/ape/solver/ModuleUtils.java index 514f3cbd..f09b196e 100644 --- a/src/main/java/nl/uu/cs/ape/solver/ModuleUtils.java +++ b/src/main/java/nl/uu/cs/ape/solver/ModuleUtils.java @@ -5,11 +5,11 @@ import nl.uu.cs.ape.automaton.ModuleAutomaton; import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.models.AllModules; +import nl.uu.cs.ape.models.DomainModules; import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.enums.AtomType; import nl.uu.cs.ape.models.SATAtomMappings; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; /** @@ -184,7 +184,7 @@ public abstract String enforceDataDependencyOverDataReferencing(TypeAutomaton ty * @param mappings Mapping function. * @return The String representation of constraints. */ - public abstract String moduleMutualExclusion(AllModules allModules, ModuleAutomaton moduleAutomaton, + public abstract String moduleMutualExclusion(DomainModules allModules, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings); /** @@ -196,7 +196,7 @@ public abstract String moduleMutualExclusion(AllModules allModules, ModuleAutoma * @param mappings Mapping function. * @return String representation of constraints. */ - public abstract String moduleMandatoryUsage(AllModules allModules, ModuleAutomaton moduleAutomaton, + public abstract String moduleMandatoryUsage(DomainModules allModules, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings); /** @@ -211,7 +211,7 @@ public abstract String moduleMandatoryUsage(AllModules allModules, ModuleAutomat * @return String representation of constraints enforcing taxonomy * classifications. */ - public abstract String moduleEnforceTaxonomyStructure(AllModules allModules, TaxonomyPredicate currModule, + public abstract String moduleEnforceTaxonomyStructure(DomainModules allModules, TaxonomyPredicate currModule, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings); /** @@ -222,8 +222,8 @@ public abstract String moduleEnforceTaxonomyStructure(AllModules allModules, Tax * modules are not returned, only the unique pairs of modules that are * representing actual tools. */ - public static List> getPredicatePairs(List predicateList) { - List> pairs = new ArrayList<>(); + public static List> getPredicatePairs(List predicateList) { + List> pairs = new ArrayList<>(); for (int i = 0; i < predicateList.size() - 1; i++) { for (int j = i + 1; j < predicateList.size(); j++) { diff --git a/src/main/java/nl/uu/cs/ape/solver/SolutionInterpreter.java b/src/main/java/nl/uu/cs/ape/solver/SolutionInterpreter.java index 312641c9..7da9b965 100644 --- a/src/main/java/nl/uu/cs/ape/solver/SolutionInterpreter.java +++ b/src/main/java/nl/uu/cs/ape/solver/SolutionInterpreter.java @@ -2,7 +2,7 @@ import java.util.List; -import nl.uu.cs.ape.models.AllModules; +import nl.uu.cs.ape.models.DomainModules; import nl.uu.cs.ape.models.Module; /** @@ -48,7 +48,7 @@ public abstract class SolutionInterpreter { * @param allModules the all modules * @return the relevant solution modules */ - public abstract List getRelevantSolutionModules(AllModules allModules); + public abstract List getRelevantSolutionModules(DomainModules allModules); /** * Is sat boolean. diff --git a/src/main/java/nl/uu/cs/ape/solver/SynthesisEngine.java b/src/main/java/nl/uu/cs/ape/solver/SynthesisEngine.java index ffb6283e..0f1d5f20 100644 --- a/src/main/java/nl/uu/cs/ape/solver/SynthesisEngine.java +++ b/src/main/java/nl/uu/cs/ape/solver/SynthesisEngine.java @@ -5,8 +5,8 @@ import java.util.List; import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.models.SATAtomMappings; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import nl.uu.cs.ape.solver.solutionStructure.SolutionWorkflow; /** @@ -46,7 +46,7 @@ public interface SynthesisEngine { * * @return Object that contains the domain model annotations, params, etc. */ - public APEDomainSetup getDomainSetup(); + public Domain getDomainSetup(); /** * Get atom mappings diff --git a/src/main/java/nl/uu/cs/ape/domain/APEDimensionsException.java b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/APEDimensionsException.java similarity index 97% rename from src/main/java/nl/uu/cs/ape/domain/APEDimensionsException.java rename to src/main/java/nl/uu/cs/ape/solver/domainconfiguration/APEDimensionsException.java index 673d6b07..2edb1f9a 100644 --- a/src/main/java/nl/uu/cs/ape/domain/APEDimensionsException.java +++ b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/APEDimensionsException.java @@ -1,7 +1,7 @@ /** * */ -package nl.uu.cs.ape.domain; +package nl.uu.cs.ape.solver.domainconfiguration; /** * The {@code APEDataDimensionsOverlapException} exception will be thrown if the diff --git a/src/main/java/nl/uu/cs/ape/domain/APEDomainSetup.java b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/Domain.java similarity index 55% rename from src/main/java/nl/uu/cs/ape/domain/APEDomainSetup.java rename to src/main/java/nl/uu/cs/ape/solver/domainconfiguration/Domain.java index 0eaab5ba..385af013 100644 --- a/src/main/java/nl/uu/cs/ape/domain/APEDomainSetup.java +++ b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/Domain.java @@ -1,28 +1,29 @@ -package nl.uu.cs.ape.domain; +package nl.uu.cs.ape.solver.domainconfiguration; +import java.io.File; import java.io.IOException; import java.util.*; -import org.json.JSONArray; import org.json.JSONException; import org.json.JSONObject; +import lombok.Getter; import lombok.extern.slf4j.Slf4j; +import nl.uu.cs.ape.automaton.ModuleAutomaton; +import nl.uu.cs.ape.automaton.TypeAutomaton; import nl.uu.cs.ape.configuration.APECoreConfig; import nl.uu.cs.ape.configuration.ToolAnnotationTag; -import nl.uu.cs.ape.constraints.ConstraintFactory; -import nl.uu.cs.ape.constraints.ConstraintFormatException; -import nl.uu.cs.ape.constraints.ConstraintTemplate; -import nl.uu.cs.ape.constraints.ConstraintTemplateParameter; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.AbstractModule; -import nl.uu.cs.ape.models.AllModules; -import nl.uu.cs.ape.models.AllTypes; -import nl.uu.cs.ape.models.AuxiliaryPredicate; -import nl.uu.cs.ape.models.ConstraintTemplateData; +import nl.uu.cs.ape.models.DomainModules; +import nl.uu.cs.ape.models.DomainTypes; import nl.uu.cs.ape.models.Module; +import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.Type; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.models.sltlxStruc.SLTLxFormula; +import nl.uu.cs.ape.solver.EncodingPredicates; /** * The {@code APEDomainSetup} class is used to store the domain information and @@ -31,73 +32,57 @@ * @author Vedran Kasalica */ @Slf4j -public class APEDomainSetup { +public class Domain extends EncodingPredicates { - /* Helper objects used to keep track of the domain quality. */ - private Set emptyTools = new HashSet<>(); - private Set wrongToolIO = new HashSet<>(); - private Set wrongToolTax = new HashSet<>(); + private static final String TOOLS_JSON_TAG = "functions"; /** * All modules/operations used in the domain. */ - private AllModules allModules; + private DomainModules allModules; /** * All data types defined in the domain. */ - private AllTypes allTypes; + private DomainTypes allTypes; /** * Prefix used to define OWL class IDs */ + @Getter private String ontologyPrefixIRI; - /** - * Object used to create temporal constraints. - */ - private ConstraintFactory constraintFactory; - - /** - * List of data gathered from the constraint file. - */ - private List unformattedConstr; - private List helperPredicates; - private List constraintsSLTLx; - /** * Maximum number of inputs that a tool can have. */ + @Getter private int maxNoToolInputs = 0; /** * Maximum number of outputs that a tool can have. */ + @Getter private int maxNoToolOutputs = 0; /** * Holds information whether the domain was annotated under the strict rules of * the output dependency. */ + @Getter private boolean useStrictToolAnnotations; - private static final String CONSTR_JSON_TAG = "constraints"; - private static final String CONSTR_ID_TAG = "constraintid"; - private static final String CONSTR_SLTLx = "formula"; - private static final String CONSTR_PARAM_JSON_TAG = "parameters"; - private static final String TOOLS_JSON_TAG = "functions"; + /* Helper objects used to keep track of the domain quality. */ + private Set emptyTools = new HashSet<>(); + private Set wrongToolIO = new HashSet<>(); + private Set wrongToolTax = new HashSet<>(); /** * Instantiates a new Ape domain setup. * * @param config the config */ - public APEDomainSetup(APECoreConfig config) { - this.unformattedConstr = new ArrayList<>(); - this.allModules = new AllModules(config); - this.allTypes = new AllTypes(config); - this.constraintFactory = new ConstraintFactory(); - this.helperPredicates = new ArrayList<>(); - this.constraintsSLTLx = new ArrayList<>(); + public Domain(APECoreConfig config) { + this.allModules = new DomainModules(config); + this.allTypes = new DomainTypes(config); this.ontologyPrefixIRI = config.getOntologyPrefixIRI(); this.useStrictToolAnnotations = config.getUseStrictToolAnnotations(); } @@ -107,85 +92,19 @@ public APEDomainSetup(APECoreConfig config) { * * @return The field {@link #allModules}. */ - public AllModules getAllModules() { + public DomainModules getAllModules() { return allModules; } - /** - * Add constraint data. - * - * @param constr Add a constraint to the list of constraints, that should be - * encoded during the execution of the synthesis. - */ - public void addConstraintData(ConstraintTemplateData constr) { - this.unformattedConstr.add(constr); - } - - /** - * Add the String that corresponds to an SLTLx formula that should be parsed to - * the list of constraints. - * - * @param formulaSLTLx - String that corresponds to an SLTLx formula that should - * be parsed - */ - public void addSLTLxConstraint(String formulaSLTLx) { - this.constraintsSLTLx.add(formulaSLTLx); - } - - /** - * Gets unformatted constraints. - * - * @return the field {@link #unformattedConstr}. - */ - public List getUnformattedConstr() { - return unformattedConstr; - } - - /** - * Gets all SLTLx constraints specified by the user in SLTLx as text. - * - * @return Set of string representations of the constraints. - */ - public List getSLTLxConstraints() { - return constraintsSLTLx; - } - - /** - * Removes all of the unformatted constraints, in order to start a new synthesis - * run. - */ - public void clearConstraints() { - this.unformattedConstr.clear(); - this.constraintsSLTLx.clear(); - } - /** * Gets all types. * * @return the field {@link #allTypes}. */ - public AllTypes getAllTypes() { + public DomainTypes getAllTypes() { return allTypes; } - /** - * Gets constraint factory. - * - * @return the field {@link #constraintFactory}. - */ - public ConstraintFactory getConstraintFactory() { - return constraintFactory; - } - - /** - * Adding each constraint format in the set of all cons. formats. method - * should be called only once all the data types and modules have been - * initialized. - */ - public void initializeConstraints() { - constraintFactory.initializeConstraints(allModules, allTypes); - } - /** * Trim taxonomy boolean. * @@ -199,97 +118,6 @@ public boolean trimTaxonomy() { return succRun; } - /** - * Return the {@link ConstraintTemplate} that corresponds to the given ID, or - * null if the constraint with the given ID does not exist. - * - * @param constraintID ID of the {@code ConstraintTemplate}. - * @return The {@code ConstraintTemplate} that corresponds to the given ID, or - * null if the ID is not mapped to any constraint. - */ - public ConstraintTemplate getConstraintTemplate(String constraintID) { - return constraintFactory.getConstraintTemplate(constraintID); - } - - /** - * Method reads the constraints from a JSON object and updates the - * {@link APEDomainSetup} object accordingly. - * - * @param constraintsJSONArray JSON array containing the constraints - * @throws ConstraintFormatException exception in case of bad constraint json - * formatting - */ - public void updateConstraints(JSONArray constraintsJSONArray) throws ConstraintFormatException { - if (constraintsJSONArray == null) { - return; - } - String constraintID = null; - int currNode = 0; - - List constraints = APEUtils.getListFromJsonList(constraintsJSONArray, JSONObject.class); - - /* Iterate through each constraint in the list */ - for (JSONObject jsonConstraint : APEUtils.safe(constraints)) { - currNode++; - /* READ THE CONSTRAINT */ - try { - constraintID = jsonConstraint.getString(CONSTR_ID_TAG); - ConstraintTemplate currConstrTemplate = getConstraintFactory() - .getConstraintTemplate(constraintID); - if (currConstrTemplate == null) { - if (constraintID.equals("SLTLx")) { - String formulaSLTLx = jsonConstraint.getString(CONSTR_SLTLx); - if (formulaSLTLx == null) { - throw ConstraintFormatException.wrongNumberOfParameters( - getConstrErrorMsg(currNode, constraintID)); - } - this.addSLTLxConstraint(formulaSLTLx); - continue; - } else { - throw ConstraintFormatException.wrongConstraintID( - getConstrErrorMsg(currNode, constraintID)); - } - } - - List currTemplateParameters = currConstrTemplate.getParameters(); - - List jsonConstParam = APEUtils.getListFromJson(jsonConstraint, CONSTR_PARAM_JSON_TAG, - JSONObject.class); - if (currTemplateParameters.size() != jsonConstParam.size()) { - throw ConstraintFormatException.wrongNumberOfParameters( - getConstrErrorMsg(currNode, constraintID)); - } - int paramNo = 0; - List constraintParameters = new ArrayList<>(); - /* for each constraint parameter */ - for (JSONObject jsonParam : jsonConstParam) { - ConstraintTemplateParameter taxInstanceFromJson = currTemplateParameters.get(paramNo++); - TaxonomyPredicate currParameter = taxInstanceFromJson.readConstraintParameterFromJson(jsonParam, - this); - constraintParameters.add(currParameter); - } - - ConstraintTemplateData currConstr = getConstraintFactory() - .generateConstraintTemplateData(constraintID, constraintParameters); - if (constraintParameters.stream().anyMatch(Objects::isNull)) { - throw ConstraintFormatException.wrongParameter( - getConstrErrorMsg(currNode, constraintID)); - } else { - this.addConstraintData(currConstr); - } - - } catch (JSONException e) { - throw ConstraintFormatException.badFormat( - getConstrErrorMsg(currNode, constraintID)); - } - - } - } - - private String getConstrErrorMsg(int currNode, String constraintID) { - return String.format("Error at constraint no: %d, constraint ID: %s", currNode, constraintID); - } - /** * Updates the list of All Modules by annotating the existing ones (or adding * non-existing) using the I/O DataInstance from the @file. Returns the list of @@ -318,7 +146,8 @@ public boolean updateToolAnnotationsFromJson(JSONObject toolAnnotationsFile) thr /** * Creates/updates a module from a tool annotation instance from a JSON file and - * updates the list of modules ({@link AllModules}) in the domain accordingly. + * updates the list of modules ({@link DomainModules}) in the domain + * accordingly. * * @param jsonModule JSON representation of a module * @return {@code true} if the domain was updated, false otherwise. @@ -466,24 +295,6 @@ public boolean updateCWLAnnotationsFromYaml(Map cwlAnnotations) return true; } - /** - * Gets ontology prefix IRI. - * - * @return the ontology prefix IRI - */ - public String getOntologyPrefixIRI() { - return ontologyPrefixIRI; - } - - /** - * Get the maximum number of inputs that a tool can have. - * - * @return the field {@link #maxNoToolInputs}. - */ - public int getMaxNoToolInputs() { - return maxNoToolInputs; - } - /** * Update the maximum number of inputs that a tool can have, i.e. increase the * number if the current max number is smaller than the new number of inputs. @@ -496,15 +307,6 @@ public void updateMaxNoToolInputs(int currNoInputs) { } } - /** - * Get the maximum number of outputs that a tool can have. - * - * @return the field {@link #maxNoToolOutputs}. - */ - public int getMaxNoToolOutputs() { - return maxNoToolOutputs; - } - /** * Update the maximum number of outputs that a tool can have, i.e. increase the * number if the current max number is smaller than the new number of outputs. @@ -518,32 +320,104 @@ public void updateMaxNoToolOutputs(int currNoOutputs) { } /** - * Add predicate to the list of auxiliary predicates that should be encoded. + * Generate the SAT encoding of the configured domain and save it to the given + * file. * - * @param helperPredicate + * @param cnfEncoding File where the encoding should be saved. + * @param currLengthTimer + * + * @return true if the encoding was performed successfully, false otherwise. + * @throws IOException Error if taxonomies have not been setup properly. */ - public void addHelperPredicate(AuxiliaryPredicate helperPredicate) { - helperPredicates.add(helperPredicate); + public boolean domainEncoding(File cnfEncoding, int solutionSize, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) throws IOException { - } + String currLengthTimer = APEUtils.getTimerId(solutionSize); + /* + * Create constraints from the tool_annotations.json file regarding the + * Inputs/Outputs, preserving the structure of input and output fields. + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceModuleRelatedRules.moduleAnnotations(this, moduleAutomaton, typeAutomaton)); + APEUtils.timerRestartAndPrint(currLengthTimer, "Tool I/O constraints"); - /** - * Get information whether the domain was annotated under the strict rules of - * the output dependency. - * - * @return {@code true} if the strict rules apply, {@code false} otherwise. - */ - public boolean getUseStrictToolAnnotations() { - return useStrictToolAnnotations; - } + /* + * The constraints preserve the memory structure, i.e. preserve the data + * available in memory and the + * logic of referencing data from memory in case of tool inputs. + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceModuleRelatedRules.memoryStructure(this, moduleAutomaton, typeAutomaton)); + APEUtils.timerRestartAndPrint(currLengthTimer, "Memory structure encoding"); - /** - * Get the list of helper predicates used in the domain. - * - * @return List of the auxiliary helper predicates. - */ - public List getHelperPredicates() { - return helperPredicates; + /* + * Create the constraints enforcing: + * 1. Mutual exclusion of the tools + * 2. Mandatory usage of the tools - from taxonomy. + * 3. Adding the constraints enforcing the taxonomy structure. + */ + for (Pair pair : domainSetup.getAllModules().getSimplePairs()) { + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceModuleRelatedRules.moduleMutualExclusion(pair, moduleAutomaton)); + } + APEUtils.timerRestartAndPrint(currLengthTimer, "Tool exclusions encoding"); + + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceModuleRelatedRules.moduleMandatoryUsage(domainSetup.getAllModules(), moduleAutomaton)); + + SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceModuleRelatedRules + .moduleTaxonomyStructure(domainSetup.getAllModules(), rootModule, moduleAutomaton)); + APEUtils.timerRestartAndPrint(currLengthTimer, "Tool usage encoding"); + /* + * Create the constraints enforcing: + * 1. Mutual exclusion of the types/formats (according to the search model) + * 2. Mandatory usage of the types in the transition nodes (note: "empty type" + * is considered a type) + * 3. Adding the constraints enforcing the taxonomy structure. + */ + for (Pair pair : domainSetup.getAllTypes().getTypePairsForEachSubTaxonomy()) { + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceTypeRelatedRules.memoryTypesMutualExclusion(pair, typeAutomaton)); + } + APEUtils.timerRestartAndPrint(currLengthTimer, "Type exclusions encoding"); + + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceTypeRelatedRules.typeMandatoryUsage(domainSetup, typeAutomaton)); + + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceTypeRelatedRules.typeEnforceTaxonomyStructure(domainSetup.getAllTypes(), typeAutomaton)); + APEUtils.timerRestartAndPrint(currLengthTimer, "Type usage encoding"); + + /* + * Encode data ancestor relation (R) constraints. + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceModuleRelatedRules.ancestorRelationsDependency(this, moduleAutomaton, typeAutomaton)); + + /* + * Encode data equivalence/identity relation (IS) constraints. + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, + EnforceModuleRelatedRules.identityRelationsDependency(typeAutomaton)); + + /* + * Setup encoding of 'true' and 'false' atoms to ensure proper SLTLx + * interpretation. + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceSLTLxRelatedRules.setTrueFalse()); + + /* + * Encode rule that the given inputs should not be used as workflow outputs + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceTypeRelatedRules + .inputsAreNotOutputs(typeAutomaton)); + + /* + * Setup the constraints ensuring that the auxiliary predicates are properly + * used and linked to the underlying taxonomy predicates. + */ + SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceSLTLxRelatedRules + .preserveAuxiliaryPredicateRules(moduleAutomaton, typeAutomaton, domainSetup.getHelperPredicates())); } } diff --git a/src/main/java/nl/uu/cs/ape/solver/minisat/EnforceModuleRelatedRules.java b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceModuleRelatedRules.java similarity index 79% rename from src/main/java/nl/uu/cs/ape/solver/minisat/EnforceModuleRelatedRules.java rename to src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceModuleRelatedRules.java index 0a6cf0b8..e0ca1154 100644 --- a/src/main/java/nl/uu/cs/ape/solver/minisat/EnforceModuleRelatedRules.java +++ b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceModuleRelatedRules.java @@ -1,4 +1,4 @@ -package nl.uu.cs.ape.solver.minisat; +package nl.uu.cs.ape.solver.domainconfiguration; import java.util.ArrayList; import java.util.HashSet; @@ -10,15 +10,14 @@ import nl.uu.cs.ape.automaton.ModuleAutomaton; import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; -import nl.uu.cs.ape.models.AllModules; +import nl.uu.cs.ape.models.DomainModules; import nl.uu.cs.ape.models.Module; import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.AtomType; import nl.uu.cs.ape.models.enums.ConfigEnum; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; import nl.uu.cs.ape.models.sltlxStruc.SLTLxConjunction; @@ -29,6 +28,7 @@ import nl.uu.cs.ape.models.sltlxStruc.SLTLxNegatedConjunction; import nl.uu.cs.ape.models.sltlxStruc.SLTLxNegation; import nl.uu.cs.ape.models.sltlxStruc.SLTLxXOR; +import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; /** * The {@code ModuleUtils} class is used to encode SLTLx constraints based on @@ -57,17 +57,18 @@ private EnforceModuleRelatedRules() { * the required INPUT * and OUTPUT types of the modules. */ - public static Set moduleAnnotations(SATSynthesisEngine synthesisInstance) { + public static Set moduleAnnotations(Domain domain, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); - fullEncoding.addAll(toolInputTypes(synthesisInstance)); + fullEncoding.addAll(toolInputTypes(domain, moduleAutomaton, typeAutomaton)); - fullEncoding.addAll(toolOutputTypes(synthesisInstance)); + fullEncoding.addAll(toolOutputTypes(domain, moduleAutomaton, typeAutomaton)); return fullEncoding; } /** * Return a CNF formula that preserves the memory structure that is being used - * (e.g. 'shared memory'), i.e. ensures that the referenced items are available + * (shared memory), i.e. ensures that the referenced items are available * according to the mem. structure and that the input type and the referenced * type from the memory represent the same data. * @@ -77,13 +78,14 @@ public static Set moduleAnnotations(SATSynthesisEngine synthesisIn * the required * memory structure implementation. */ - public static Set memoryStructure(SATSynthesisEngine synthesisInstance) { + public static Set memoryStructure(Domain domain, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); - fullEncoding.addAll(allowDataReferencing(synthesisInstance.getTypeAutomaton())); + fullEncoding.addAll(allowDataReferencing(typeAutomaton)); fullEncoding.addAll(usageOfGeneratedTypes(synthesisInstance)); - fullEncoding.addAll(dataReference(synthesisInstance.getDomainSetup(), - synthesisInstance.getTypeAutomaton())); + fullEncoding.addAll(dataReference(domain, + typeAutomaton)); return fullEncoding; } @@ -95,9 +97,9 @@ public static Set memoryStructure(SATSynthesisEngine synthesisInst * information specific for it. * @return Set of SLTLx formulas that represent the constraints. */ - public static Set ancestorRelationsDependency(SATSynthesisEngine synthesisInstance) { + public static Set ancestorRelationsDependency(Domain domain, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); - TypeAutomaton typeAutomaton = synthesisInstance.getTypeAutomaton(); /** * Encode reflexivity and transitivity of the relation. @@ -115,8 +117,8 @@ public static Set ancestorRelationsDependency(SATSynthesisEngine s * - restrict that empty types don't depend on anything */ fullEncoding.addAll(restrictAncestorRelationDomain(typeAutomaton)); - fullEncoding.addAll(ancestorRelRestrictOverModules(synthesisInstance)); - fullEncoding.addAll(ancestorRelDependencyOverModules(synthesisInstance)); + fullEncoding.addAll(ancestorRelRestrictOverModules(domain.getAllTypes().getEmptyType(), typeAutomaton)); + fullEncoding.addAll(ancestorRelDependencyOverModules(domain.getAllTypes().getEmptyType(), typeAutomaton)); fullEncoding.addAll(ancestorRelOverDataReferencing(typeAutomaton)); return fullEncoding; @@ -150,19 +152,20 @@ public static Set identityRelationsDependency(TypeAutomaton typeAu * * @return Set of SLTLx formulas that represent the constraints. */ - private static Set toolInputTypes(SATSynthesisEngine synthesisInstance) { + private static Set toolInputTypes(Domain domain, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); /* For each module.. */ - for (TaxonomyPredicate potentialModule : synthesisInstance.getDomainSetup().getAllModules().getModules()) { + for (TaxonomyPredicate potentialModule : domain.getAllModules().getModules()) { /* ..which is a Tool.. */ if ((potentialModule instanceof Module)) { Module module = (Module) potentialModule; /* ..iterate through all the states.. */ - for (State moduleState : synthesisInstance.getModuleAutomaton().getAllStates()) { + for (State moduleState : moduleAutomaton.getAllStates()) { int moduleNo = moduleState.getLocalStateNumber(); /* ..and for each state and input state of that module state.. */ - List currInputStates = synthesisInstance.getTypeAutomaton().getUsedTypesBlock(moduleNo - 1) + List currInputStates = typeAutomaton.getUsedTypesBlock(moduleNo - 1) .getStates(); List moduleInputs = module.getModuleInput(); for (State currInputState : currInputStates) { @@ -198,7 +201,7 @@ private static Set toolInputTypes(SATSynthesisEngine synthesisInst moduleState), new SLTLxAtom( AtomType.USED_TYPE, - synthesisInstance.getEmptyType(), + domain.getAllTypes().getEmptyType(), currInputState))); } } @@ -218,11 +221,11 @@ private static Set toolInputTypes(SATSynthesisEngine synthesisInst * @return String representing the constraints required to ensure that the * {@link AtomType#MEM_TYPE_REFERENCE} are implemented correctly. */ - private static Set dataReference(APEDomainSetup domainSetup, TypeAutomaton typeAutomaton) { + private static Set dataReference(Domain domain, TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); /* For each type instance */ - for (TaxonomyPredicate currType : domainSetup.getAllTypes().getTypes()) { + for (TaxonomyPredicate currType : domain.getAllTypes().getTypes()) { if (currType.isSimplePredicate() || currType.isEmptyPredicate()) { /* ..for each state in which type can be used .. */ for (State currUsedTypeState : typeAutomaton.getAllUsedTypesStates()) { @@ -318,7 +321,7 @@ private static Set allowDataReferencing(TypeAutomaton typeAutomato fullEncoding.add(new SLTLxDisjunction(allPossibilities)); /* Defining that each input can reference only one state in the shared memory */ - for (Pair pair : getPredicatePairs(possibleMemStates)) { + for (Pair pair : getPredicatePairs(possibleMemStates)) { fullEncoding.add( new SLTLxNegatedConjunction( new SLTLxAtom( @@ -468,15 +471,14 @@ private static Set ancestorRelOverDataReferencing(TypeAutomaton ty * * @return Set of SLTLx formulas that represent the constraints. */ - private static Set ancestorRelDependencyOverModules(SATSynthesisEngine synthesisInstance) { - TypeAutomaton typeAutomaton = synthesisInstance.getTypeAutomaton(); + private static Set ancestorRelDependencyOverModules(Type emptyType, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); /** For tool inputs and outputs */ for (int i = 0; i < typeAutomaton.getUsedTypesBlocks().size() - 1; i++) { Block currInputBlock = typeAutomaton.getUsedTypesBlock(i); Block currMemBlock = typeAutomaton.getMemoryTypesBlock(i + 1); - Type emptyType = synthesisInstance.getEmptyType(); // For each output state.. for (State currMemState : currMemBlock.getStates()) { @@ -515,10 +517,9 @@ private static Set ancestorRelDependencyOverModules(SATSynthesisEn * * @return Set of SLTLx formulas that represent the constraints. */ - private static Set ancestorRelRestrictOverModules(SATSynthesisEngine synthesisInstance) { - TypeAutomaton typeAutomaton = synthesisInstance.getTypeAutomaton(); + private static Set ancestorRelRestrictOverModules(Type emptyType, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); - Type emptyType = synthesisInstance.getEmptyType(); for (int i = 0; i < typeAutomaton.getUsedTypesBlocks().size() - 1; i++) { Block currInputBlock = typeAutomaton.getUsedTypesBlock(i); @@ -716,123 +717,6 @@ private static Set relationalSymmetry(AtomType binRel, TypeAutomat return fullEncoding; } - /** - * Function returns the encoding that ensures that tool outputs are used - * according to the configuration, e.g. if the config specifies that all - * workflow inputs have to be used, then each of them has to be referenced at - * least once. - * - * @param synthesisInstance - instance of the synthesis engine - * - * @return Set of SLTLx formulas that represent the constraints. - */ - private static Set usageOfGeneratedTypes(SATSynthesisEngine synthesisInstance) { - - Type emptyType = synthesisInstance.getEmptyType(); - TypeAutomaton typeAutomaton = synthesisInstance.getTypeAutomaton(); - Set fullEncoding = new HashSet<>(); - /* - * Setting up the constraints that ensure usage of the generated types in the - * memory, (e.g. all workflow inputs and at least one of each of the tool - * outputs needs to be used in the program, unless they are empty.) - */ - for (Block currBlock : typeAutomaton.getMemoryTypesBlocks()) { - int blockNumber = currBlock.getBlockNumber(); - /* If the memory is provided as input */ - if (blockNumber == 0) { - /* In case that all workflow inputs need to be used */ - if (synthesisInstance.getRunConfig().getUseWorkflowInput() == ConfigEnum.ALL) { - for (State currMemoryState : currBlock.getStates()) { - Set allPossibilities = new HashSet<>(); - - allPossibilities.add( - new SLTLxAtom( - AtomType.MEMORY_TYPE, - emptyType, - currMemoryState)); - - for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { - allPossibilities.add( - new SLTLxAtom( - AtomType.MEM_TYPE_REFERENCE, - currMemoryState, - inputState)); - } - fullEncoding.add(new SLTLxDisjunction(allPossibilities)); - } - /* In case that at least one workflow input need to be used */ - } else if (synthesisInstance.getRunConfig().getUseWorkflowInput() == ConfigEnum.ONE) { - Set allPossibilities = new HashSet<>(); - for (State currMemoryState : currBlock.getStates()) { - if (currMemoryState.getLocalStateNumber() == 0) { - allPossibilities.add( - new SLTLxAtom( - AtomType.MEMORY_TYPE, - emptyType, - currMemoryState)); - } - for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { - allPossibilities.add( - new SLTLxAtom( - AtomType.MEM_TYPE_REFERENCE, - currMemoryState, - inputState)); - } - } - fullEncoding.add(new SLTLxDisjunction(allPossibilities)); - } - /* In case that none of the workflow input has to be used, do nothing. */ - } else { - /* In case that all generated data need to be used. */ - if (synthesisInstance.getRunConfig().getUseAllGeneratedData() == ConfigEnum.ALL) { - for (State currMemoryState : currBlock.getStates()) { - Set allPossibilities = new HashSet<>(); - allPossibilities.add( - new SLTLxAtom( - AtomType.MEMORY_TYPE, - emptyType, - currMemoryState)); - for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { - allPossibilities.add( - new SLTLxAtom( - AtomType.MEM_TYPE_REFERENCE, - currMemoryState, - inputState)); - } - fullEncoding.add(new SLTLxDisjunction(allPossibilities)); - } - /* - * In case that at least one of the generated data instances per tool need to be - * used. - */ - } else if (synthesisInstance.getRunConfig().getUseAllGeneratedData() == ConfigEnum.ONE) { - Set allPossibilities = new HashSet<>(); - for (State currMemoryState : currBlock.getStates()) { - if (currMemoryState.getLocalStateNumber() == 0) { - allPossibilities.add( - new SLTLxAtom( - AtomType.MEMORY_TYPE, - emptyType, - currMemoryState)); - } - for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { - allPossibilities.add( - new SLTLxAtom( - AtomType.MEM_TYPE_REFERENCE, - currMemoryState, - inputState)); - } - } - fullEncoding.add(new SLTLxDisjunction(allPossibilities)); - } - /* In case that none generated data has to be used do nothing. */ - - } - } - - return fullEncoding; - } - /** * Return the CNF representation of the output type constraints for all tools * regarding @typeAutomaton, for the synthesis concerning @moduleAutomaton.
@@ -842,20 +726,21 @@ private static Set usageOfGeneratedTypes(SATSynthesisEngine synthe * * @return Set of SLTLx formulas that represent the constraints. */ - private static Set toolOutputTypes(SATSynthesisEngine synthesisInstance) { + private static Set toolOutputTypes(Domain domain, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); // for each module - for (TaxonomyPredicate potentialModule : synthesisInstance.getDomainSetup().getAllModules().getModules()) { + for (TaxonomyPredicate potentialModule : domain.getAllModules().getModules()) { // that is a Tool if ((potentialModule instanceof Module)) { Module module = (Module) potentialModule; // iterate through all the states - for (State moduleState : synthesisInstance.getModuleAutomaton().getAllStates()) { + for (State moduleState : moduleAutomaton.getAllStates()) { int moduleNo = moduleState.getLocalStateNumber(); // and for each state and output state of that module state - List currOutputStates = synthesisInstance.getTypeAutomaton().getMemoryTypesBlock(moduleNo) + List currOutputStates = typeAutomaton.getMemoryTypesBlock(moduleNo) .getStates(); List moduleOutputs = module.getModuleOutput(); for (int i = 0; i < currOutputStates.size(); i++) { @@ -886,7 +771,7 @@ private static Set toolOutputTypes(SATSynthesisEngine synthesisIns moduleState), new SLTLxAtom( AtomType.MEMORY_TYPE, - synthesisInstance.getEmptyType(), + domain.getAllTypes().getEmptyType(), currOutputStates.get(i)))); } } @@ -907,7 +792,7 @@ private static Set toolOutputTypes(SATSynthesisEngine synthesisIns * @return The Set of SLTLx formulas that represent the constraints. */ - public static Set moduleMutualExclusion(Pair pair, ModuleAutomaton moduleAutomaton) { + public static Set moduleMutualExclusion(Pair pair, ModuleAutomaton moduleAutomaton) { Set fullEncoding = new HashSet<>(); @@ -937,7 +822,7 @@ public static Set moduleMutualExclusion(Pair pair, * @param moduleAutomaton Module automaton. * @return Set of SLTLx formulas that represent the constraints. */ - public static Set moduleMandatoryUsage(AllModules allModules, ModuleAutomaton moduleAutomaton) { + public static Set moduleMandatoryUsage(DomainModules allModules, ModuleAutomaton moduleAutomaton) { Set fullEncoding = new HashSet<>(); if (allModules.getModules().isEmpty()) { @@ -975,7 +860,7 @@ public static Set moduleMandatoryUsage(AllModules allModules, Modu * taxonomy * classifications. */ - public static Set moduleTaxonomyStructure(AllModules allModules, TaxonomyPredicate currModule, + public static Set moduleTaxonomyStructure(DomainModules allModules, TaxonomyPredicate currModule, ModuleAutomaton moduleAutomaton) { Set fullEncoding = new HashSet<>(); @@ -994,7 +879,7 @@ public static Set moduleTaxonomyStructure(AllModules allModules, T * @param currModule Module that should be used. * @param moduleState State in which the module should be used. */ - private static Set moduleTaxonomyStructureForState(AllModules allModules, + private static Set moduleTaxonomyStructureForState(DomainModules allModules, TaxonomyPredicate currModule, State moduleState) { SLTLxAtom superModuleState = new SLTLxAtom(AtomType.MODULE, currModule, moduleState); @@ -1044,8 +929,8 @@ private static Set moduleTaxonomyStructureForState(AllModules allM * modules are not returned, only the unique pairs of modules that are * representing actual tools. */ - public static List> getPredicatePairs(List predicateList) { - List> pairs = new ArrayList<>(); + public static List> getPredicatePairs(List predicateList) { + List> pairs = new ArrayList<>(); for (int i = 0; i < predicateList.size() - 1; i++) { for (int j = i + 1; j < predicateList.size(); j++) { diff --git a/src/main/java/nl/uu/cs/ape/solver/minisat/EnforceSLTLxRelatedRules.java b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceSLTLxRelatedRules.java similarity index 99% rename from src/main/java/nl/uu/cs/ape/solver/minisat/EnforceSLTLxRelatedRules.java rename to src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceSLTLxRelatedRules.java index 957666f2..97aaf518 100644 --- a/src/main/java/nl/uu/cs/ape/solver/minisat/EnforceSLTLxRelatedRules.java +++ b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceSLTLxRelatedRules.java @@ -1,4 +1,4 @@ -package nl.uu.cs.ape.solver.minisat; +package nl.uu.cs.ape.solver.domainconfiguration; import java.util.Collection; import java.util.HashSet; diff --git a/src/main/java/nl/uu/cs/ape/solver/minisat/EnforceTypeRelatedRules.java b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceTypeRelatedRules.java similarity index 71% rename from src/main/java/nl/uu/cs/ape/solver/minisat/EnforceTypeRelatedRules.java rename to src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceTypeRelatedRules.java index 8e10042d..8bbf17f6 100644 --- a/src/main/java/nl/uu/cs/ape/solver/minisat/EnforceTypeRelatedRules.java +++ b/src/main/java/nl/uu/cs/ape/solver/domainconfiguration/EnforceTypeRelatedRules.java @@ -1,4 +1,4 @@ -package nl.uu.cs.ape.solver.minisat; +package nl.uu.cs.ape.solver.domainconfiguration; import java.util.ArrayList; import java.util.HashSet; @@ -9,15 +9,14 @@ import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.automaton.TypeAutomaton; import nl.uu.cs.ape.configuration.APEConfigException; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; -import nl.uu.cs.ape.models.AllTypes; +import nl.uu.cs.ape.models.DomainTypes; import nl.uu.cs.ape.models.AuxTypePredicate; import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.LogicOperation; import nl.uu.cs.ape.models.enums.AtomType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; import nl.uu.cs.ape.models.sltlxStruc.SLTLxDisjunction; @@ -51,10 +50,10 @@ private EnforceTypeRelatedRules() { * @param typeAutomaton - System that represents states in the workflow * @return String representation of constraints. */ - public static Set memoryTypesMutualExclusion(Pair pair, TypeAutomaton typeAutomaton) { + public static Set memoryTypesMutualExclusion(Pair pair, TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); - PredicateLabel firstPair = pair.getFirst(); - PredicateLabel secondPair = pair.getSecond(); + Predicate firstPair = pair.getFirst(); + Predicate secondPair = pair.getSecond(); // mutual exclusion of types in all the states (those that represent general // memory) for (State memTypeState : typeAutomaton.getAllMemoryTypesStates()) { @@ -81,10 +80,10 @@ public static Set memoryTypesMutualExclusion(Pair * @param typeAutomaton - System that represents states in the workflow * @return String representation of constraints. */ - public static Set usedTypeMutualExclusion(Pair pair, TypeAutomaton typeAutomaton) { + public static Set usedTypeMutualExclusion(Pair pair, TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); - PredicateLabel firstPair = pair.getFirst(); - PredicateLabel secondPair = pair.getSecond(); + Predicate firstPair = pair.getFirst(); + Predicate secondPair = pair.getSecond(); // mutual exclusion of types in all the states (those that represent general // memory) // mutual exclusion of types in all the states (those that represent used @@ -113,7 +112,7 @@ public static Set usedTypeMutualExclusion(Pair pai * @param typeAutomaton - System that represents states in the workflow * @return String representation of constraints. */ - public static Set typeMandatoryUsage(APEDomainSetup domainSetup, TypeAutomaton typeAutomaton) { + public static Set typeMandatoryUsage(Domain domainSetup, TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); Type empty = domainSetup.getAllTypes().getEmptyType(); Type dataType = AuxTypePredicate.generateAuxiliaryPredicate( @@ -163,7 +162,7 @@ public static Set typeMandatoryUsage(APEDomainSetup domainSetup, T * @return The String representation of constraints enforcing taxonomy * classifications. */ - public static Set typeEnforceTaxonomyStructure(AllTypes allTypes, TypeAutomaton typeAutomaton) { + public static Set typeEnforceTaxonomyStructure(DomainTypes allTypes, TypeAutomaton typeAutomaton) { Set fullEncoding = new HashSet<>(); // taxonomy enforcement of types in in all the states (those that represent // general memory and used data instances) @@ -231,86 +230,6 @@ private static Set typeEnforceTaxonomyStructureForState(TaxonomyPr return fullEncoding; } - /** - * Encodes rules that ensure the initial workflow input. - * - * @param allTypes Set of all the types in the domain - * @param program_inputs Input types for the program. - * @param typeAutomaton Automaton representing the type states in the model - * @return The String representation of the initial input encoding. - * @throws APEConfigException Exception thrown when one of the output types is - * not defined in the taxonomy. - */ - public static Set workflowInputs(AllTypes allTypes, List program_inputs, - TypeAutomaton typeAutomaton) throws APEConfigException { - Set fullEncoding = new HashSet<>(); - - List workflowInputStates = typeAutomaton.getWorkflowInputBlock().getStates(); - for (int i = 0; i < workflowInputStates.size(); i++) { - State currState = workflowInputStates.get(i); - if (i < program_inputs.size()) { - Type currType = program_inputs.get(i); - if (allTypes.get(currType.getPredicateID()) == null) { - throw APEConfigException.workflowIODataTypeNotInDomain(currType.getPredicateID()); - } - fullEncoding.add( - new SLTLxAtom( - AtomType.MEMORY_TYPE, - currType, - currState)); - } else { - /* Forcing in the rest of the input states to be empty types. */ - fullEncoding.add( - new SLTLxAtom( - AtomType.MEMORY_TYPE, - allTypes.getEmptyType(), - currState)); - } - } - return fullEncoding; - } - - /** - * Encodes the rules that ensure generation of the workflow output. - * - * @param allTypes Set of all the types in the domain - * @param program_outputs Output types for the program. - * @param typeAutomaton Automaton representing the type states in the model - * @return String representation of the workflow output encoding. - * @throws APEConfigException Exception thrown when one of the output types is - * not defined in the taxonomy. - */ - public static Set workdlowOutputs(AllTypes allTypes, List program_outputs, - TypeAutomaton typeAutomaton) throws APEConfigException { - Set fullEncoding = new HashSet<>(); - - List workflowOutputStates = typeAutomaton.getWorkflowOutputBlock().getStates(); - for (int i = 0; i < workflowOutputStates.size(); i++) { - if (i < program_outputs.size()) { - TaxonomyPredicate currType = program_outputs.get(i); - if (allTypes.get(currType.getPredicateID()) == null) { - throw APEConfigException.workflowIODataTypeNotInDomain(currType.getPredicateID()); - } - fullEncoding.add( - new SLTLxAtom( - AtomType.USED_TYPE, - currType, - workflowOutputStates.get(i))); - - } else { - /* Forcing in the rest of the input states to be empty types. */ - fullEncoding.add( - new SLTLxAtom( - AtomType.USED_TYPE, - allTypes.getEmptyType(), - workflowOutputStates.get(i))); - } - - } - - return fullEncoding; - } - /** * Encodes rules that ensure that the initial workflow inputs are not used as * workflow outputs. diff --git a/src/main/java/nl/uu/cs/ape/solver/minisat/SATOutput.java b/src/main/java/nl/uu/cs/ape/solver/minisat/SATOutput.java index 177f1fdb..4fe6e3a1 100644 --- a/src/main/java/nl/uu/cs/ape/solver/minisat/SATOutput.java +++ b/src/main/java/nl/uu/cs/ape/solver/minisat/SATOutput.java @@ -4,12 +4,12 @@ import nl.uu.cs.ape.automaton.State; import nl.uu.cs.ape.utils.APEUtils; -import nl.uu.cs.ape.models.AllModules; +import nl.uu.cs.ape.models.DomainModules; import nl.uu.cs.ape.models.AuxiliaryPredicate; import nl.uu.cs.ape.models.Module; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.AtomType; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxLiteral; import nl.uu.cs.ape.solver.SolutionInterpreter; @@ -29,35 +29,35 @@ public class SATOutput extends SolutionInterpreter { /** * List of all the literals provided by the solution. */ - private final List literals; + private final List literals = new ArrayList<>(); /** * List of all the positive literals provided by the solution. */ - private final List positiveLiterals; + private final List positiveLiterals = new ArrayList<>(); /** * List of only relevant (positive) literals that represent implemented * modules/tools. */ - private final List relevantModules; + private final List relevantModules = new ArrayList<>(); /** * List of only relevant (positive) literals that represent simple types. */ - private final List relevantTypes; + private final List relevantTypes = new ArrayList<>(); /** * List of all the relevant types and modules combined. */ - private final List relevantElements; + private final List relevantElements = new ArrayList<>(); /** * List of all the references for the types in the memory, when used as tool * inputs. */ - private final List references2MemTypes; - private final Set usedTypeStates; + private final List references2MemTypes = new ArrayList<>(); + private final Set usedTypeStates = new HashSet<>(); /** * true if the there is no solution to the problem. Problem is UNASATISFIABLE. @@ -73,13 +73,6 @@ public class SATOutput extends SolutionInterpreter { */ public SATOutput(int[] satSolution, SATSynthesisEngine synthesisInstance) { unsat = false; - literals = new ArrayList<>(); - positiveLiterals = new ArrayList<>(); - relevantModules = new ArrayList<>(); - relevantTypes = new ArrayList<>(); - relevantElements = new ArrayList<>(); - references2MemTypes = new ArrayList<>(); - usedTypeStates = new HashSet<>(); for (int mappedLiteral : satSolution) { if (mappedLiteral >= synthesisInstance.getMappings().getInitialNumOfMappedAtoms()) { SLTLxLiteral currLiteral = new SLTLxLiteral(Integer.toString(mappedLiteral), @@ -88,7 +81,7 @@ public SATOutput(int[] satSolution, SATSynthesisEngine synthesisInstance) { if (!currLiteral.isNegated()) { positiveLiterals.add(currLiteral); if (currLiteral.getPredicate() instanceof AuxiliaryPredicate) { - continue; + // No action needed, skip to the next iteration } else if (currLiteral.getPredicate() instanceof Module) { /* add all positive literals that describe tool implementations */ relevantElements.add(currLiteral); @@ -130,13 +123,6 @@ public SATOutput(int[] satSolution, SATSynthesisEngine synthesisInstance) { */ public SATOutput() { unsat = true; - literals = null; - positiveLiterals = null; - relevantModules = null; - relevantTypes = null; - relevantElements = null; - references2MemTypes = null; - usedTypeStates = null; } /** @@ -221,7 +207,7 @@ public String getRelevantSolution() { * @return List of {@link Module}s in the order they appear in the solution * workflow. */ - public List getRelevantSolutionModules(AllModules allModules) { + public List getRelevantSolutionModules(DomainModules allModules) { List solutionModules = new ArrayList<>(); if (unsat) { return null; diff --git a/src/main/java/nl/uu/cs/ape/solver/minisat/SATSynthesisEngine.java b/src/main/java/nl/uu/cs/ape/solver/minisat/SATSynthesisEngine.java index 5f602be1..96347c92 100644 --- a/src/main/java/nl/uu/cs/ape/solver/minisat/SATSynthesisEngine.java +++ b/src/main/java/nl/uu/cs/ape/solver/minisat/SATSynthesisEngine.java @@ -12,19 +12,24 @@ import nl.uu.cs.ape.automaton.ModuleAutomaton; import nl.uu.cs.ape.automaton.TypeAutomaton; import nl.uu.cs.ape.configuration.APERunConfig; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEFiles; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.SATAtomMappings; import nl.uu.cs.ape.models.Type; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxFormula; import nl.uu.cs.ape.models.sltlxStruc.SLTLxVariableOccurrenceCollection; import nl.uu.cs.ape.solver.SynthesisEngine; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; +import nl.uu.cs.ape.solver.domainconfiguration.EncodeDomainConfig; +import nl.uu.cs.ape.solver.domainconfiguration.EnforceModuleRelatedRules; +import nl.uu.cs.ape.solver.domainconfiguration.EnforceSLTLxRelatedRules; +import nl.uu.cs.ape.solver.domainconfiguration.EnforceTypeRelatedRules; import nl.uu.cs.ape.solver.solutionStructure.SolutionWorkflow; import nl.uu.cs.ape.solver.solutionStructure.SolutionsList; +import nl.uu.cs.ape.solver.userspecification.EnforceUserConstraints; import java.io.File; import java.io.FileInputStream; @@ -52,7 +57,7 @@ public class SATSynthesisEngine implements SynthesisEngine { * Object that contains all the domain information. */ @Getter - private final APEDomainSetup domainSetup; + private final Domain domainSetup; /** * APE library configuration object. @@ -75,7 +80,6 @@ public class SATSynthesisEngine implements SynthesisEngine { /** * CNF encoding of the problem. */ - @Getter private File cnfEncoding; /** @@ -126,7 +130,7 @@ public class SATSynthesisEngine implements SynthesisEngine { * @param workflowLength Workflow length * @throws IOException - Error if the temp file cannot be created */ - public SATSynthesisEngine(APEDomainSetup domainSetup, SolutionsList allSolutions, + public SATSynthesisEngine(Domain domainSetup, SolutionsList allSolutions, APERunConfig runConfig, int workflowLength) throws IOException { this.domainSetup = domainSetup; this.allSolutions = allSolutions; @@ -160,80 +164,17 @@ public boolean synthesisEncoding() throws IOException { return false; } /* Generate the automaton */ - String currLengthTimer = "length" + this.getSolutionSize(); + String currLengthTimer = APEUtils.getTimerId(this.getSolutionSize()); + APEUtils.timerStart(currLengthTimer, runConfig.getDebugMode()); APEUtils.timerRestartAndPrint(currLengthTimer, "Automaton encoding"); /* - * Create constraints from the tool_annotations.json file regarding the - * Inputs/Outputs, preserving the structure of input and output fields. - */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceModuleRelatedRules.moduleAnnotations(this)); - APEUtils.timerRestartAndPrint(currLengthTimer, "Tool I/O constraints"); - - /* - * The constraints preserve the memory structure, i.e. preserve the data - * available in memory and the - * logic of referencing data from memory in case of tool inputs. - */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceModuleRelatedRules.memoryStructure(this)); - APEUtils.timerRestartAndPrint(currLengthTimer, "Memory structure encoding"); - - /* - * Create the constraints enforcing: - * 1. Mutual exclusion of the tools - * 2. Mandatory usage of the tools - from taxonomy. - * 3. Adding the constraints enforcing the taxonomy structure. - */ - for (Pair pair : domainSetup.getAllModules().getSimplePairs()) { - SLTLxFormula.appendCNFToFile(cnfEncoding, this, - EnforceModuleRelatedRules.moduleMutualExclusion(pair, moduleAutomaton)); - } - APEUtils.timerRestartAndPrint(currLengthTimer, "Tool exclusions encoding"); - - SLTLxFormula.appendCNFToFile(cnfEncoding, this, - EnforceModuleRelatedRules.moduleMandatoryUsage(domainSetup.getAllModules(), moduleAutomaton)); - - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceModuleRelatedRules - .moduleTaxonomyStructure(domainSetup.getAllModules(), rootModule, moduleAutomaton)); - APEUtils.timerRestartAndPrint(currLengthTimer, "Tool usage encoding"); - /* - * Create the constraints enforcing: - * 1. Mutual exclusion of the types/formats (according to the search model) - * 2. Mandatory usage of the types in the transition nodes (note: "empty type" - * is considered a type) - * 3. Adding the constraints enforcing the taxonomy structure. - */ - for (Pair pair : domainSetup.getAllTypes().getTypePairsForEachSubTaxonomy()) { - SLTLxFormula.appendCNFToFile(cnfEncoding, this, - EnforceTypeRelatedRules.memoryTypesMutualExclusion(pair, typeAutomaton)); - } - APEUtils.timerRestartAndPrint(currLengthTimer, "Type exclusions encoding"); - - SLTLxFormula.appendCNFToFile(cnfEncoding, this, - EnforceTypeRelatedRules.typeMandatoryUsage(domainSetup, typeAutomaton)); - - SLTLxFormula.appendCNFToFile(cnfEncoding, this, - EnforceTypeRelatedRules.typeEnforceTaxonomyStructure(domainSetup.getAllTypes(), typeAutomaton)); - APEUtils.timerRestartAndPrint(currLengthTimer, "Type usage encoding"); - - /* - * Encode data ancestor relation (R) constraints. - */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceModuleRelatedRules.ancestorRelationsDependency(this)); - - /* - * Encode data equivalence/identity relation (IS) constraints. - */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, - EnforceModuleRelatedRules.identityRelationsDependency(typeAutomaton)); - - /* - * Setup encoding of 'true' and 'false' atoms to ensure proper SLTLx - * interpretation. + * Encode the configured domain for the given workflow length and save it to the + * file. */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceSLTLxRelatedRules.setTrueFalse()); + domainSetup.domainEncoding(cnfEncoding, this.getSolutionSize(), moduleAutomaton, typeAutomaton); /* * Workflow I/O are encoded the last in order to @@ -242,20 +183,14 @@ public boolean synthesisEncoding() throws IOException { * * Encode the workflow input. */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceTypeRelatedRules + SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceUserConstraints .workflowInputs(domainSetup.getAllTypes(), runConfig.getProgramInputs(), typeAutomaton)); /* * Encode the workflow output */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceTypeRelatedRules + SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceUserConstraints .workdlowOutputs(domainSetup.getAllTypes(), runConfig.getProgramOutputs(), typeAutomaton)); - /* - * Encode rule that the given inputs should not be used as workflow outputs - */ - SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceTypeRelatedRules - .inputsAreNotOutputs(typeAutomaton)); - /* * Encode the constraints from the file based on the templates (manual * templates) @@ -321,11 +256,11 @@ public List synthesisExecution() throws IOException { } /** - * Gets cnf encoding. + * Gets cnf encoding content as string. * - * @return the cnf encoding + * @return The cnf encoding content as string. */ - public String getCnfEncoding() { + public String getCnfEncodingContent() { return cnfEncoding.toString(); } diff --git a/src/main/java/nl/uu/cs/ape/solver/minisat/SatEncodingUtils.java b/src/main/java/nl/uu/cs/ape/solver/minisat/SatEncodingUtils.java deleted file mode 100644 index 674e711d..00000000 --- a/src/main/java/nl/uu/cs/ape/solver/minisat/SatEncodingUtils.java +++ /dev/null @@ -1,94 +0,0 @@ -package nl.uu.cs.ape.solver.minisat; - -import java.util.List; -import java.util.Set; - -import lombok.AccessLevel; -import lombok.NoArgsConstructor; -import lombok.extern.slf4j.Slf4j; -import nl.uu.cs.ape.automaton.ModuleAutomaton; -import nl.uu.cs.ape.automaton.TypeAutomaton; -import nl.uu.cs.ape.domain.APEDomainSetup; -import nl.uu.cs.ape.models.ConstraintTemplateData; -import nl.uu.cs.ape.models.SATAtomMappings; -import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; -import nl.uu.cs.ape.models.sltlxStruc.SLTLxFormula; -import nl.uu.cs.ape.parserSLTLx.SLTLxSATVisitor; - -@Slf4j -@NoArgsConstructor(access = AccessLevel.PRIVATE) -public class SatEncodingUtils { - - /** - * Encode APE constraints string. - * - * @param synthesisEngine - * - * @param domainSetup Domain information, including all the existing tools - * and types. - * @param mappings Mapping function. - * @param moduleAutomaton Module automaton. - * @param typeAutomaton Type automaton. - * @return The CNF representation of the SLTLx constraints in our project. - */ - public static String encodeAPEConstraints(SATSynthesisEngine synthesisEngine, APEDomainSetup domainSetup, - SATAtomMappings mappings, - ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton) { - - StringBuilder cnfSLTLx = new StringBuilder(); - int currConst = 0; - - for (ConstraintTemplateData constraint : domainSetup.getUnformattedConstr()) { - currConst++; - /* ENCODE THE CONSTRAINT */ - if (domainSetup.getConstraintTemplate(constraint.getConstraintID()) == null) { - log.warn("Constraint ID provided: '" + constraint.getConstraintID() - + "' is not valid. Constraint skipped."); - } else { - String currConstrEncoding = constraintSATEncoding(constraint.getConstraintID(), - constraint.getParameters(), domainSetup, moduleAutomaton, typeAutomaton, mappings); - if (currConstrEncoding == null) { - log.warn("Error in constraint file. Constraint no: " + currConst + ". Constraint skipped."); - } else { - cnfSLTLx.append(currConstrEncoding); - } - } - } - - /* - * Parse the constraints specified in SLTLx. - */ - for (String constraint : domainSetup.getSLTLxConstraints()) { - Set sltlxFormulas = SLTLxSATVisitor.parseFormula(synthesisEngine, constraint); - for (SLTLxFormula sltlxFormula : sltlxFormulas) { - sltlxFormula.getConstraintCNFEncoding(synthesisEngine) - .forEach(cnfSLTLx::append); - } - } - - return cnfSLTLx.toString(); - } - - /** - * Function used to provide SAT encoding of a constrain based on the constraint - * ID specified and provided parameters. - * - * @param constraintID ID of the constraint. - * @param list Parameters for the constraint template. - * @param domainSetup Domain information, including all the existing tools - * and types. - * @param moduleAutomaton Module automaton. - * @param typeAutomaton Type automaton. - * @param mappings Mapping function. - * @return String representation of the SAT encoding for the specified - * constraint. - */ - public static String constraintSATEncoding(String constraintID, List list, - APEDomainSetup domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, - SATAtomMappings mappings) { - - return domainSetup.getConstraintTemplate(constraintID).getConstraint(list, domainSetup, moduleAutomaton, - typeAutomaton, mappings); - } - -} diff --git a/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionWorkflow.java b/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionWorkflow.java index fee06167..6318f63f 100644 --- a/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionWorkflow.java +++ b/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionWorkflow.java @@ -41,33 +41,33 @@ public class SolutionWorkflow { * List of module nodes ordered according to their position in the workflow. */ @Getter - private List moduleNodes; + private final List moduleNodes = new ArrayList<>(); /** * List of memory type nodes provided as the initial workflow input, ordered * according the initial description (config.json file). */ @Getter - private List workflowInputTypeStates; + private final List workflowInputTypeStates = new ArrayList<>(); /** * List of used type nodes provided as the final workflow output, ordered * according the initial description (config.json file). */ @Getter - private List workflowOutputTypeStates; + private final List workflowOutputTypeStates = new ArrayList<>(); /** * Map of all {@code ModuleNodes}, where key value is the {@link State} provided * by the {@link ModuleAutomaton}. */ - private Map mappedModuleNodes; + private final Map mappedModuleNodes = new HashMap<>(); /** * Map of all {@code MemTypeNode}, where key value is the {@link State} provided * by the {@link TypeAutomaton}. */ - private Map mappedMemoryTypeNodes; + private final Map mappedMemoryTypeNodes = new HashMap<>(); /** * Mapping used to allow us to determine the correlation between the usage of @@ -76,7 +76,7 @@ public class SolutionWorkflow { * {@link AtomType#USED_TYPE} and a {@link ModuleNode}.
* If the second is NULL, the data is used as WORKFLOW OUTPUT. */ - private Map usedType2ToolMap; + private final Map usedType2ToolMap = new HashMap<>(); /** * Non-structured solution obtained directly from the SAT output. @@ -121,6 +121,7 @@ public class SolutionWorkflow { /** * Index of the solution. */ + @Getter private int index; /** @@ -133,13 +134,6 @@ public class SolutionWorkflow { */ private SolutionWorkflow(ModuleAutomaton toolAutomaton, TypeAutomaton typeAutomaton) throws ExceptionInInitializerError { - this.moduleNodes = new ArrayList<>(); - this.workflowInputTypeStates = new ArrayList<>(); - this.workflowOutputTypeStates = new ArrayList<>(); - this.mappedModuleNodes = new HashMap<>(); - this.mappedMemoryTypeNodes = new HashMap<>(); - this.usedType2ToolMap = new HashMap<>(); - ModuleNode prev = null; for (State currState : toolAutomaton.getAllStates()) { ModuleNode currNode = new ModuleNode(currState); @@ -350,12 +344,4 @@ public void setIndex(int i) { this.index = i; } - /** - * Gets index. - * - * @return The index of the solution in all the solutions. - */ - public int getIndex() { - return this.index; - } } diff --git a/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionsList.java b/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionsList.java index df92831e..fe860ffa 100644 --- a/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionsList.java +++ b/src/main/java/nl/uu/cs/ape/solver/solutionStructure/SolutionsList.java @@ -21,7 +21,7 @@ @Slf4j public class SolutionsList { - private List solutions; + private List solutions = new ArrayList<>(); /** * Max number of solutions that should be found. @@ -31,7 +31,7 @@ public class SolutionsList { /** * Mapping of predicates into integers (for SAT encoding). */ - private final SATAtomMappings mappings; + private final SATAtomMappings mappings = new SATAtomMappings(); /** * Current solution index. @@ -64,16 +64,8 @@ public class SolutionsList { * @param runConfig - setup configuration for the synthesis run. */ public SolutionsList(APERunConfig runConfig) { - this.solutions = new ArrayList(); this.runConfig = runConfig; - /* - * Provides mapping from each atom/predicate to a number/string, and vice versa - */ - if (runConfig.getSolverType() == SolverType.SAT) { - this.mappings = new SATAtomMappings(); - } else { - throw new APEConfigException("Solver type has to be SAT."); - } + /* Variables defining the current and maximum lengths and solutions count. */ this.maxSolutions = runConfig.getMaxNoSolutions(); if (this.maxSolutions > 100) { diff --git a/src/main/java/nl/uu/cs/ape/solver/userspecification/EnforceRunConfiguration.java b/src/main/java/nl/uu/cs/ape/solver/userspecification/EnforceRunConfiguration.java new file mode 100644 index 00000000..b630eaf9 --- /dev/null +++ b/src/main/java/nl/uu/cs/ape/solver/userspecification/EnforceRunConfiguration.java @@ -0,0 +1,134 @@ +package nl.uu.cs.ape.solver.userspecification; + +import java.util.HashSet; +import java.util.Set; + +import nl.uu.cs.ape.automaton.Block; +import nl.uu.cs.ape.automaton.ModuleAutomaton; +import nl.uu.cs.ape.automaton.State; +import nl.uu.cs.ape.automaton.TypeAutomaton; +import nl.uu.cs.ape.models.Type; +import nl.uu.cs.ape.models.enums.AtomType; +import nl.uu.cs.ape.models.enums.ConfigEnum; +import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; +import nl.uu.cs.ape.models.sltlxStruc.SLTLxDisjunction; +import nl.uu.cs.ape.models.sltlxStruc.SLTLxFormula; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; + +public class EnforceRunConfiguration { + + /** + * Function returns the encoding that ensures that tool outputs are used + * according to the configuration, e.g. if the config specifies that all + * workflow inputs have to be used, then each of them has to be referenced at + * least once. + * + * @param synthesisInstance - instance of the synthesis engine + * + * @return Set of SLTLx formulas that represent the constraints. + private static Set usageOfGeneratedTypes(Domain domain, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton) { + + Type emptyType = synthesisInstance.getEmptyType(); + Set fullEncoding = new HashSet<>(); + /* + * Setting up the constraints that ensure usage of the generated types in the + * memory, (e.g. all workflow inputs and at least one of each of the tool + * outputs needs to be used in the program, unless they are empty.) + */ + for (Block currBlock : typeAutomaton.getMemoryTypesBlocks()) { + int blockNumber = currBlock.getBlockNumber(); + /* If the memory is provided as input */ + if (blockNumber == 0) { + /* In case that all workflow inputs need to be used */ + if (synthesisInstance.getRunConfig().getUseWorkflowInput() == ConfigEnum.ALL) { + for (State currMemoryState : currBlock.getStates()) { + Set allPossibilities = new HashSet<>(); + + allPossibilities.add( + new SLTLxAtom( + AtomType.MEMORY_TYPE, + emptyType, + currMemoryState)); + + for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { + allPossibilities.add( + new SLTLxAtom( + AtomType.MEM_TYPE_REFERENCE, + currMemoryState, + inputState)); + } + fullEncoding.add(new SLTLxDisjunction(allPossibilities)); + } + /* In case that at least one workflow input need to be used */ + } else if (synthesisInstance.getRunConfig().getUseWorkflowInput() == ConfigEnum.ONE) { + Set allPossibilities = new HashSet<>(); + for (State currMemoryState : currBlock.getStates()) { + if (currMemoryState.getLocalStateNumber() == 0) { + allPossibilities.add( + new SLTLxAtom( + AtomType.MEMORY_TYPE, + emptyType, + currMemoryState)); + } + for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { + allPossibilities.add( + new SLTLxAtom( + AtomType.MEM_TYPE_REFERENCE, + currMemoryState, + inputState)); + } + } + fullEncoding.add(new SLTLxDisjunction(allPossibilities)); + } + /* In case that none of the workflow input has to be used, do nothing. */ + } else { + /* In case that all generated data need to be used. */ + if (synthesisInstance.getRunConfig().getUseAllGeneratedData() == ConfigEnum.ALL) { + for (State currMemoryState : currBlock.getStates()) { + Set allPossibilities = new HashSet<>(); + allPossibilities.add( + new SLTLxAtom( + AtomType.MEMORY_TYPE, + emptyType, + currMemoryState)); + for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { + allPossibilities.add( + new SLTLxAtom( + AtomType.MEM_TYPE_REFERENCE, + currMemoryState, + inputState)); + } + fullEncoding.add(new SLTLxDisjunction(allPossibilities)); + } + /* + * In case that at least one of the generated data instances per tool need to be + * used. + */ + } else if (synthesisInstance.getRunConfig().getUseAllGeneratedData() == ConfigEnum.ONE) { + Set allPossibilities = new HashSet<>(); + for (State currMemoryState : currBlock.getStates()) { + if (currMemoryState.getLocalStateNumber() == 0) { + allPossibilities.add( + new SLTLxAtom( + AtomType.MEMORY_TYPE, + emptyType, + currMemoryState)); + } + for (State inputState : typeAutomaton.getUsedStatesAfterBlockNo(blockNumber - 1)) { + allPossibilities.add( + new SLTLxAtom( + AtomType.MEM_TYPE_REFERENCE, + currMemoryState, + inputState)); + } + } + fullEncoding.add(new SLTLxDisjunction(allPossibilities)); + } + /* In case that none generated data has to be used do nothing. */ + + } + } + + return fullEncoding; + }} diff --git a/src/main/java/nl/uu/cs/ape/solver/userspecification/EnforceUserConstraints.java b/src/main/java/nl/uu/cs/ape/solver/userspecification/EnforceUserConstraints.java new file mode 100644 index 00000000..426d7894 --- /dev/null +++ b/src/main/java/nl/uu/cs/ape/solver/userspecification/EnforceUserConstraints.java @@ -0,0 +1,181 @@ +package nl.uu.cs.ape.solver.userspecification; + +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import lombok.AccessLevel; +import lombok.NoArgsConstructor; +import lombok.extern.slf4j.Slf4j; +import nl.uu.cs.ape.automaton.ModuleAutomaton; +import nl.uu.cs.ape.automaton.State; +import nl.uu.cs.ape.automaton.TypeAutomaton; +import nl.uu.cs.ape.configuration.APEConfigException; +import nl.uu.cs.ape.models.DomainTypes; +import nl.uu.cs.ape.models.ConstraintTemplateData; +import nl.uu.cs.ape.models.SATAtomMappings; +import nl.uu.cs.ape.models.Type; +import nl.uu.cs.ape.models.enums.AtomType; +import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; +import nl.uu.cs.ape.models.sltlxStruc.SLTLxFormula; +import nl.uu.cs.ape.parserSLTLx.SLTLxSATVisitor; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; +import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; + +@Slf4j +@NoArgsConstructor(access = AccessLevel.PRIVATE) +public class EnforceUserConstraints { + + /** + * Encodes rules that ensure the initial workflow input. + * + * @param allTypes Set of all the types in the domain + * @param program_inputs Input types for the program. + * @param typeAutomaton Automaton representing the type states in the model + * @return The String representation of the initial input encoding. + * @throws APEConfigException Exception thrown when one of the output types is + * not defined in the taxonomy. + */ + public static Set workflowInputs(DomainTypes allTypes, List program_inputs, + TypeAutomaton typeAutomaton) throws APEConfigException { + Set fullEncoding = new HashSet<>(); + + List workflowInputStates = typeAutomaton.getWorkflowInputBlock().getStates(); + for (int i = 0; i < workflowInputStates.size(); i++) { + State currState = workflowInputStates.get(i); + if (i < program_inputs.size()) { + Type currType = program_inputs.get(i); + if (allTypes.get(currType.getPredicateID()) == null) { + throw APEConfigException.workflowIODataTypeNotInDomain(currType.getPredicateID()); + } + fullEncoding.add( + new SLTLxAtom( + AtomType.MEMORY_TYPE, + currType, + currState)); + } else { + /* Forcing in the rest of the input states to be empty types. */ + fullEncoding.add( + new SLTLxAtom( + AtomType.MEMORY_TYPE, + allTypes.getEmptyType(), + currState)); + } + } + return fullEncoding; + } + + /** + * Encodes the rules that ensure generation of the workflow output. + * + * @param allTypes Set of all the types in the domain + * @param program_outputs Output types for the program. + * @param typeAutomaton Automaton representing the type states in the model + * @return String representation of the workflow output encoding. + * @throws APEConfigException Exception thrown when one of the output types is + * not defined in the taxonomy. + */ + public static Set workdlowOutputs(DomainTypes allTypes, List program_outputs, + TypeAutomaton typeAutomaton) throws APEConfigException { + Set fullEncoding = new HashSet<>(); + + List workflowOutputStates = typeAutomaton.getWorkflowOutputBlock().getStates(); + for (int i = 0; i < workflowOutputStates.size(); i++) { + if (i < program_outputs.size()) { + TaxonomyPredicate currType = program_outputs.get(i); + if (allTypes.get(currType.getPredicateID()) == null) { + throw APEConfigException.workflowIODataTypeNotInDomain(currType.getPredicateID()); + } + fullEncoding.add( + new SLTLxAtom( + AtomType.USED_TYPE, + currType, + workflowOutputStates.get(i))); + + } else { + /* Forcing in the rest of the input states to be empty types. */ + fullEncoding.add( + new SLTLxAtom( + AtomType.USED_TYPE, + allTypes.getEmptyType(), + workflowOutputStates.get(i))); + } + + } + + return fullEncoding; + } + + /** + * Encode APE constraints string. + * + * @param synthesisEngine + * + * @param domainSetup Domain information, including all the existing tools + * and types. + * @param mappings Mapping function. + * @param moduleAutomaton Module automaton. + * @param typeAutomaton Type automaton. + * @return The CNF representation of the SLTLx constraints in our project. + */ + public static String encodeAPEConstraints(SATSynthesisEngine synthesisEngine, Domain domainSetup, + SATAtomMappings mappings, + ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton) { + + StringBuilder cnfSLTLx = new StringBuilder(); + int currConst = 0; + + for (ConstraintTemplateData constraint : domainSetup.getUnformattedConstr()) { + currConst++; + /* ENCODE THE CONSTRAINT */ + if (domainSetup.getConstraintTemplate(constraint.getConstraintID()) == null) { + log.warn("Constraint ID provided: '" + constraint.getConstraintID() + + "' is not valid. Constraint skipped."); + } else { + String currConstrEncoding = constraintSATEncoding(constraint.getConstraintID(), + constraint.getParameters(), domainSetup, moduleAutomaton, typeAutomaton, mappings); + if (currConstrEncoding == null) { + log.warn("Error in constraint file. Constraint no: " + currConst + ". Constraint skipped."); + } else { + cnfSLTLx.append(currConstrEncoding); + } + } + } + + /* + * Parse the constraints specified in SLTLx. + */ + for (String constraint : domainSetup.getSLTLxConstraints()) { + Set sltlxFormulas = SLTLxSATVisitor.parseFormula(synthesisEngine, constraint); + for (SLTLxFormula sltlxFormula : sltlxFormulas) { + sltlxFormula.getConstraintCNFEncoding(synthesisEngine) + .forEach(cnfSLTLx::append); + } + } + + return cnfSLTLx.toString(); + } + + /** + * Function used to provide SAT encoding of a constrain based on the constraint + * ID specified and provided parameters. + * + * @param constraintID ID of the constraint. + * @param list Parameters for the constraint template. + * @param domainSetup Domain information, including all the existing tools + * and types. + * @param moduleAutomaton Module automaton. + * @param typeAutomaton Type automaton. + * @param mappings Mapping function. + * @return String representation of the SAT encoding for the specified + * constraint. + */ + public static String constraintSATEncoding(String constraintID, List list, + Domain domainSetup, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, + SATAtomMappings mappings) { + + return domainSetup.getConstraintTemplate(constraintID).getConstraint(list, domainSetup, moduleAutomaton, + typeAutomaton, mappings); + } +} diff --git a/src/main/java/nl/uu/cs/ape/solver/userspecification/UserSpecification.java b/src/main/java/nl/uu/cs/ape/solver/userspecification/UserSpecification.java new file mode 100644 index 00000000..79528ebb --- /dev/null +++ b/src/main/java/nl/uu/cs/ape/solver/userspecification/UserSpecification.java @@ -0,0 +1,187 @@ +package nl.uu.cs.ape.solver.userspecification; + +import java.util.ArrayList; +import java.util.List; +import java.util.Objects; + +import org.json.JSONArray; +import org.json.JSONException; +import org.json.JSONObject; + +import lombok.Getter; +import lombok.NoArgsConstructor; +import nl.uu.cs.ape.constraints.ConstraintFactory; +import nl.uu.cs.ape.constraints.ConstraintFormatException; +import nl.uu.cs.ape.constraints.ConstraintTemplate; +import nl.uu.cs.ape.constraints.ConstraintTemplateParameter; +import nl.uu.cs.ape.models.DomainModules; +import nl.uu.cs.ape.models.DomainTypes; +import nl.uu.cs.ape.models.AuxiliaryPredicate; +import nl.uu.cs.ape.models.ConstraintTemplateData; +import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.solver.EncodingPredicates; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; +import nl.uu.cs.ape.utils.APEUtils; + +@NoArgsConstructor +public class UserSpecification extends EncodingPredicates { + + private static final String CONSTR_ID_TAG = "constraintid"; + private static final String CONSTR_SLTLx = "formula"; + private static final String CONSTR_PARAM_JSON_TAG = "parameters"; + + /** + * Object used to create temporal constraints. + */ + @Getter + private final ConstraintFactory constraintFactory = new ConstraintFactory(); + + /** + * List of user specified constraint information. The constraint data is later + * provided to {@link ConstraintTemplate ConstraintTemplates}. + */ + @Getter + private final List unformattedConstr = new ArrayList<>(); + /** + * List of helper predicates that are used to encode the constraints. + */ + @Getter + private final List helperPredicates = new ArrayList<>(); + + /** + * List of constraints provided as Strings in SLTLx format. + */ + @Getter + private final List constraintsSLTLx = new ArrayList<>(); + + /** + * Add constraint data. + * + * @param constr Add a constraint to the list of constraints, that should be + * encoded during the execution of the synthesis. + */ + public void addConstraintData(ConstraintTemplateData constr) { + this.unformattedConstr.add(constr); + } + + /** + * Add the String that corresponds to an SLTLx formula that should be parsed to + * the list of constraints. + * + * @param formulaSLTLx - String that corresponds to an SLTLx formula that should + * be parsed + */ + public void addSLTLxConstraint(String formulaSLTLx) { + this.constraintsSLTLx.add(formulaSLTLx); + } + + /** + * Removes all of the unformatted constraints, in order to start a new synthesis + * run. + */ + public void clearConstraints() { + this.unformattedConstr.clear(); + this.constraintsSLTLx.clear(); + } + + /** + * Method reads the constraints from a JSON object and updates the + * {@link Domain} object accordingly. + * + * @param constraintsJSONArray JSON array containing the constraints + * @throws ConstraintFormatException exception in case of bad constraint json + * formatting + */ + public void updateConstraints(JSONArray constraintsJSONArray) throws ConstraintFormatException { + if (constraintsJSONArray == null) { + return; + } + String constraintID = null; + int currNode = 0; + + List constraints = APEUtils.getListFromJsonList(constraintsJSONArray, JSONObject.class); + + /* Iterate through each constraint in the list */ + for (JSONObject jsonConstraint : APEUtils.safe(constraints)) { + currNode++; + /* READ THE CONSTRAINT */ + try { + constraintID = jsonConstraint.getString(CONSTR_ID_TAG); + ConstraintTemplate currConstrTemplate = getConstraintFactory() + .getConstraintTemplate(constraintID); + if (currConstrTemplate == null) { + if (constraintID.equals("SLTLx")) { + String formulaSLTLx = jsonConstraint.getString(CONSTR_SLTLx); + if (formulaSLTLx == null) { + throw ConstraintFormatException.wrongNumberOfParameters( + getConstrErrorMsg(currNode, constraintID)); + } + this.addSLTLxConstraint(formulaSLTLx); + continue; + } else { + throw ConstraintFormatException.wrongConstraintID( + getConstrErrorMsg(currNode, constraintID)); + } + } + + List currTemplateParameters = currConstrTemplate.getParameters(); + + List jsonConstParam = APEUtils.getListFromJson(jsonConstraint, CONSTR_PARAM_JSON_TAG, + JSONObject.class); + if (currTemplateParameters.size() != jsonConstParam.size()) { + throw ConstraintFormatException.wrongNumberOfParameters( + getConstrErrorMsg(currNode, constraintID)); + } + int paramNo = 0; + List constraintParameters = new ArrayList<>(); + /* for each constraint parameter */ + for (JSONObject jsonParam : jsonConstParam) { + ConstraintTemplateParameter taxInstanceFromJson = currTemplateParameters.get(paramNo++); + TaxonomyPredicate currParameter = taxInstanceFromJson.readConstraintParameterFromJson(jsonParam, + this); + constraintParameters.add(currParameter); + } + + ConstraintTemplateData currConstr = getConstraintFactory() + .generateConstraintTemplateData(constraintID, constraintParameters); + if (constraintParameters.stream().anyMatch(Objects::isNull)) { + throw ConstraintFormatException.wrongParameter( + getConstrErrorMsg(currNode, constraintID)); + } else { + this.addConstraintData(currConstr); + } + + } catch (JSONException e) { + throw ConstraintFormatException.badFormat( + getConstrErrorMsg(currNode, constraintID)); + } + + } + } + + private String getConstrErrorMsg(int currNode, String constraintID) { + return String.format("Error at constraint no: %d, constraint ID: %s", currNode, constraintID); + } + + /** + * Adding each constraint format in the set of all cons. formats. method + * should be called only once all the data types and modules have been + * initialized. + */ + public void initializeConstraints(DomainModules allModules, DomainTypes allTypes) { + constraintFactory.initializeConstraints(allModules, allTypes); + } + + /** + * Return the {@link ConstraintTemplate} that corresponds to the given ID, or + * null if the constraint with the given ID does not exist. + * + * @param constraintID ID of the {@code ConstraintTemplate}. + * @return The {@code ConstraintTemplate} that corresponds to the given ID, or + * null if the ID is not mapped to any constraint. + */ + public ConstraintTemplate getConstraintTemplate(String constraintID) { + return constraintFactory.getConstraintTemplate(constraintID); + } + +} diff --git a/src/main/java/nl/uu/cs/ape/utils/APEUtils.java b/src/main/java/nl/uu/cs/ape/utils/APEUtils.java index 447c6ecb..ffdf5c9c 100644 --- a/src/main/java/nl/uu/cs/ape/utils/APEUtils.java +++ b/src/main/java/nl/uu/cs/ape/utils/APEUtils.java @@ -7,17 +7,17 @@ import org.json.JSONObject; import nl.uu.cs.ape.configuration.APERunConfig; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.models.ConstraintTemplateData; import nl.uu.cs.ape.models.Module; import nl.uu.cs.ape.models.Pair; import nl.uu.cs.ape.models.SATAtomMappings; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.LogicOperation; -import nl.uu.cs.ape.models.logic.constructs.PredicateLabel; +import nl.uu.cs.ape.models.logic.constructs.Predicate; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtom; import nl.uu.cs.ape.models.sltlxStruc.SLTLxAtomVar; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import nl.uu.cs.ape.solver.minisat.SATSynthesisEngine; import java.io.*; @@ -164,7 +164,7 @@ public static List getListFromJsonList(JSONArray jsonArray, Class claz * @param domainSetup Domain information, including all the existing tools and * types. */ - public static void debugPrintout(APERunConfig runConfig, APEDomainSetup domainSetup) { + public static void debugPrintout(APERunConfig runConfig, Domain domainSetup) { String line = "-------------------------------------------------------------"; if (runConfig.getDebugMode()) { @@ -622,8 +622,8 @@ public static void printMemoryStatus(boolean debugMode) { * @param set - Set of PredicateLabel that should be used to create the pairs * @return Set of unique pairs. */ - public static Set> getUniquePairs(Collection set) { - Set> pairs = new HashSet<>(); + public static Set> getUniquePairs(Collection set) { + Set> pairs = new HashSet<>(); set.stream().forEach(ele1 -> set.stream().filter(ele2 -> ele1.compareTo(ele2) < 0) .forEach(ele2 -> pairs.add(new Pair<>(ele1, ele2)))); return pairs; @@ -645,4 +645,14 @@ public static Set> getUniquePairs(Collection set1, Collection return pairs; } + /** + * Get a unique timer ID for the given solution size. + * + * @param solutionSize - size of the solution + * @return A unique timer ID for the given solution size + */ + public static String getTimerId(int solutionSize) { + return "length" + solutionSize; + } + } diff --git a/src/main/java/nl/uu/cs/ape/domain/BioToolsAPI.java b/src/main/java/nl/uu/cs/ape/utils/BioToolsAPI.java similarity index 98% rename from src/main/java/nl/uu/cs/ape/domain/BioToolsAPI.java rename to src/main/java/nl/uu/cs/ape/utils/BioToolsAPI.java index 6ddbf45d..07bf2915 100644 --- a/src/main/java/nl/uu/cs/ape/domain/BioToolsAPI.java +++ b/src/main/java/nl/uu/cs/ape/utils/BioToolsAPI.java @@ -1,4 +1,4 @@ -package nl.uu.cs.ape.domain; +package nl.uu.cs.ape.utils; import java.io.File; import java.io.IOException; @@ -13,8 +13,6 @@ import lombok.NoArgsConstructor; import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.configuration.ToolAnnotationTag; -import nl.uu.cs.ape.utils.APEFiles; -import nl.uu.cs.ape.utils.APEUtils; import okhttp3.OkHttpClient; import okhttp3.Request; import okhttp3.Response; diff --git a/src/main/java/nl/uu/cs/ape/domain/OWLReader.java b/src/main/java/nl/uu/cs/ape/utils/OWLReader.java similarity index 96% rename from src/main/java/nl/uu/cs/ape/domain/OWLReader.java rename to src/main/java/nl/uu/cs/ape/utils/OWLReader.java index be54911d..d2c033ac 100644 --- a/src/main/java/nl/uu/cs/ape/domain/OWLReader.java +++ b/src/main/java/nl/uu/cs/ape/utils/OWLReader.java @@ -1,4 +1,4 @@ -package nl.uu.cs.ape.domain; +package nl.uu.cs.ape.utils; import org.apache.commons.io.FileExistsException; import org.semanticweb.owlapi.apibinding.OWLManager; @@ -10,10 +10,12 @@ import lombok.extern.slf4j.Slf4j; import nl.uu.cs.ape.models.AbstractModule; -import nl.uu.cs.ape.models.AllModules; -import nl.uu.cs.ape.models.AllTypes; +import nl.uu.cs.ape.models.DomainModules; +import nl.uu.cs.ape.models.DomainTypes; import nl.uu.cs.ape.models.Type; import nl.uu.cs.ape.models.enums.NodeType; +import nl.uu.cs.ape.solver.domainconfiguration.APEDimensionsException; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import java.io.File; import java.util.*; @@ -32,9 +34,9 @@ public class OWLReader { /** File containing the ontology */ private final File ontologyFile; /** List of all modules in the domain */ - private final AllModules allModules; + private final DomainModules allModules; /** List of all types in the domain */ - private final AllTypes allTypes; + private final DomainTypes allTypes; /** Mapping from each dimension to the list of the types within it */ private Map> typeDimensions = new HashMap<>(); @@ -56,7 +58,7 @@ public class OWLReader { * types. * @param ontologyFile Path to the OWL file. */ - public OWLReader(APEDomainSetup domain, File ontologyFile) { + public OWLReader(Domain domain, File ontologyFile) { this.ontologyFile = ontologyFile; this.allModules = domain.getAllModules(); this.allTypes = domain.getAllTypes(); @@ -124,8 +126,8 @@ public static boolean verifyOntology(File ontologyFile, String ontologyPrefixIRI throws APEDimensionsException, OWLOntologyCreationException, FileExistsException { final OWLOntologyManager manager = OWLManager.createOWLOntologyManager(); - AllModules allModules = new AllModules(toolTaxonomyRoot); - AllTypes allTypes = new AllTypes(dataDimensionRoots); + DomainModules allModules = new DomainModules(toolTaxonomyRoot); + DomainTypes allTypes = new DomainTypes(dataDimensionRoots); OWLOntology ontology = null; if (ontologyFile.exists()) { ontology = manager.loadOntologyFromOntologyDocument(ontologyFile); diff --git a/src/test/java/nl/uu/cs/ape/sat/test/configuration/APEConfigTagTest.java b/src/test/java/nl/uu/cs/ape/sat/test/configuration/APEConfigTagTest.java index 1ba0eb86..347a8d29 100644 --- a/src/test/java/nl/uu/cs/ape/sat/test/configuration/APEConfigTagTest.java +++ b/src/test/java/nl/uu/cs/ape/sat/test/configuration/APEConfigTagTest.java @@ -5,9 +5,9 @@ import nl.uu.cs.ape.configuration.APERunConfig; import nl.uu.cs.ape.configuration.tags.APEConfigTag; import nl.uu.cs.ape.configuration.tags.validation.ValidationResults; -import nl.uu.cs.ape.domain.APEDomainSetup; import nl.uu.cs.ape.utils.APEUtils; import nl.uu.cs.ape.sat.test.utils.TestResources; +import nl.uu.cs.ape.solver.domainconfiguration.Domain; import org.json.JSONObject; import org.junit.jupiter.api.Test; @@ -114,7 +114,7 @@ public void runValidationTest() throws IOException, OWLOntologyCreationException .put("constraints_path", TestResources.getAbsoluteResourcePath("cli/gmt/constraints_e0.json")) .put("solutions_dir_path", TestResources.getAbsoluteResourcePath("cli/gmt")); - APEDomainSetup domainSetup = new APE(correct_config).getDomainSetup(); + Domain domainSetup = new APE(correct_config).getDomainSetup(); ValidationResults results = APERunConfig.validate(correct_config, domainSetup); diff --git a/src/test/java/nl/uu/cs/ape/sat/test/utils/GitHubRepo.java b/src/test/java/nl/uu/cs/ape/sat/test/utils/GitHubRepo.java index 88b03ae7..e9546a61 100644 --- a/src/test/java/nl/uu/cs/ape/sat/test/utils/GitHubRepo.java +++ b/src/test/java/nl/uu/cs/ape/sat/test/utils/GitHubRepo.java @@ -30,13 +30,12 @@ public class GitHubRepo { private String absoluteLocalRoot; private String repository; private String commit; - private HashMap files; + private final HashMap files = new HashMap<>(); public GitHubRepo(String repository, String commitOrBranch) { this.absoluteLocalRoot = Paths.get(TestResources.getAbsoluteRoot(), "temp").toString(); this.repository = repository; this.commit = commitOrBranch; - this.files = new HashMap<>(); } public String getRoot() {