From 04a630a154d1b7599d4559de698584660b0da1ec Mon Sep 17 00:00:00 2001 From: Vedran Kasalica Date: Tue, 7 Jun 2022 20:34:49 +0200 Subject: [PATCH 1/6] Added 3 new SLTLx templates Added 3 templates Improved template descriptions --- .../cs/ape/constraints/ConstraintFactory.java | 88 ++++++- .../ape/core/implSAT/SATSynthesisEngine.java | 2 +- .../sltlxStruc/SLTLxVarQuantification.java | 4 +- .../ape/models/sltlxStruc/SLTLxVariable.java | 2 +- .../SLTLxTemplateFormula.java | 238 +++++++++++++----- .../java/nl/uu/cs/ape/utils/APEUtils.java | 18 ++ 6 files changed, 284 insertions(+), 68 deletions(-) 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 4953aa5f..7773531f 100644 --- a/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java +++ b/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java @@ -192,10 +192,26 @@ public boolean initializeConstraints(AllModules allModules, AllTypes allTypes) { /* - * ID: m_in_label + * ID: operation_input */ - currTemplate = new Constraint_use_m_in_label("m_in_label", moduleNlabel, - "Use operation ${parameter_1} with data labeled ${parameter_2} as one of the inputs."); + currTemplate = new Constraint_use_module_with_input("operation_input", moduleNlabel, + "Use the operation with an input of the given type."); + addConstraintTemplate(currTemplate); + + /* + * ID: operation_output + */ + currTemplate = new Constraint_use_module_with_output("operation_output", moduleNlabel, + "Use the operation to generate an output of the given type."); + addConstraintTemplate(currTemplate); + + + + /* + * ID: connected_op + */ + currTemplate = new Constraint_connected_modules("connected_op", moduleParam2, + "1st operation should generate an output used by the 2nd operation."); addConstraintTemplate(currTemplate); /* @@ -765,10 +781,10 @@ public String getConstraint(List parameters, APEDomainSetup d /** * Implements constraints of the form:
- * Use operation ${parameter_1} with data labeled ${parameter_2} as one of the inputs. + * Use operation ${parameter_1} with input labeled ${parameter_2}. * {@link #getConstraint}. */ - public class Constraint_use_m_in_label extends ConstraintTemplate { + public class Constraint_use_module_with_input extends ConstraintTemplate { /** * Instantiates a new Constraint use type. * @@ -776,7 +792,7 @@ public class Constraint_use_m_in_label extends ConstraintTemplate { * @param parametersNo the parameters no * @param description the description */ - protected Constraint_use_m_in_label(String id, List parametersNo, String description) { + protected Constraint_use_module_with_input(String id, List parametersNo, String description) { super(id, parametersNo, description); } @@ -788,8 +804,66 @@ public String getConstraint(List parameters, APEDomainSetup d return null; } - return SLTLxTemplateFormula.use_m_in_label(parameters.get(0), parameters.get(1), moduleAutomaton, typeAutomaton, mappings); + return SLTLxTemplateFormula.use_module_input(parameters.get(0), parameters.get(1), moduleAutomaton, typeAutomaton, mappings); } } + /** + * Implements constraints of the form:
+ * Use operation ${parameter_1} to generate output labeled ${parameter_2} + * {@link #getConstraint}. + */ + public class Constraint_use_module_with_output extends ConstraintTemplate { + /** + * Instantiates a new Constraint use type. + * + * @param id the id + * @param parametersNo the parameters no + * @param description the description + */ + protected Constraint_use_module_with_output(String id, List parametersNo, String description) { + super(id, parametersNo, description); + } + + @Override + public String getConstraint(List parameters, APEDomainSetup domainSetup, + ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + if (parameters.size() != this.getNoOfParameters()) { + super.throwParametersError(parameters.size()); + return null; + } + + return SLTLxTemplateFormula.use_module_output(parameters.get(0), parameters.get(1), moduleAutomaton, typeAutomaton, mappings); + } + } + + /** + * Implements constraints of the form:
+ * 1st operation should generate an output used by the 2nd operation + * subsequently using the function {@link #getConstraint}. + */ + public class Constraint_connected_modules extends ConstraintTemplate { + /** + * Instantiates a new Constraint if then module. + * + * @param id the id + * @param parameterTypes the parameter types + * @param description the description + */ + protected Constraint_connected_modules(String id, List parameterTypes, + String description) { + super(id, parameterTypes, description); + } + + @Override + public String getConstraint(List parameters, APEDomainSetup domainSetup, + ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + if (parameters.size() != this.getNoOfParameters()) { + super.throwParametersError(parameters.size()); + return null; + } + return SLTLxTemplateFormula.connected_modules(parameters.get(0), parameters.get(1),domainSetup, moduleAutomaton, typeAutomaton, mappings); + } + } + } diff --git a/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java b/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java index 6d0fcef9..d1645b6d 100644 --- a/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java +++ b/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java @@ -226,7 +226,7 @@ public boolean synthesisEncoding() throws IOException { * Additional SLTLx constraints. TODO - provide a proper interface */ // SLTLxFormula.appendCNFToFile(cnfEncoding, this, SLTLxSATVisitor.parseFormula(this, -// "!F Exists (?x1) (<'operation_0004'(?x1,?x1;)> true)")); +// "Exists (?x) 'birds'(?x) & F (<'psxyz_P'(?x;)> true)")); // "!Exists (?x1) (<'Transform'(;?x1)> true) & (<'Transform'(?x1;)> true)")); // "G(Forall (?x1) (<'Transform'(?x1;)> true) -> (X G (Forall (?x2) (<'Transform'(?x2;)> true) -> ! R(?x1,?x2))))")); // "true"); 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 66155cc6..16f40557 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 @@ -31,7 +31,7 @@ public Set getCNFEncoding(int stateNo, SLTLxVariableSubstitutionCollecti clauses.addAll(formula.getCNFEncoding(stateNo, newVarMappping, synthesisEngine)); /** Ensure that the variables and states they substitute satisfy the same properties. * The rules have to be applied after visiting the bound formula (as done in the previous step). */ - clauses.addAll(flatBindedVariable.getVariableSubstitutionToPresereProperties(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(flatBindedVariable.getVariableSubstitutionToPreserveProperties(stateNo, newVarMappping, synthesisEngine)); clauses.addAll(flatBindedVariable.getVariableMutualExclusion(stateNo, newVarMappping, synthesisEngine)); return clauses; } @@ -44,7 +44,7 @@ public Set getNegatedCNFEncoding(int stateNo, SLTLxVariableSubstitutionC clauses.addAll(formula.getNegatedCNFEncoding(stateNo, newVarMappping, synthesisEngine)); /** Ensure that the variables and states they substitute satisfy the same properties. * The rules have to be applied after visiting the bound formula (as done in the previous step). */ - clauses.addAll(flatBindedVariable.getVariableSubstitutionToPresereProperties(stateNo, newVarMappping, synthesisEngine)); + clauses.addAll(flatBindedVariable.getVariableSubstitutionToPreserveProperties(stateNo, newVarMappping, synthesisEngine)); clauses.addAll(flatBindedVariable.getVariableMutualExclusion(stateNo, newVarMappping, synthesisEngine)); return clauses; } 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 ea4c8961..255b99e7 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 @@ -145,7 +145,7 @@ public Set getUniversalCNFEncoding(int stateNo, SLTLxVariableSubstitutio * @param synthesisEngine - synthesis engine * @return Set of clauses that encode the possible variable substitution. */ - public Set getVariableSubstitutionToPresereProperties(int stateNo, SLTLxVariableSubstitutionCollection variableSubtitutions, SATSynthesisEngine synthesisEngine) { + public Set getVariableSubstitutionToPreserveProperties(int stateNo, SLTLxVariableSubstitutionCollection variableSubtitutions, SATSynthesisEngine synthesisEngine) { Set allFacts = new HashSet<>(); SLTLxVariableOccuranceCollection varOccurances = synthesisEngine.getVariableUsage(); 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 4e34047d..1a84c8da 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 @@ -1,6 +1,11 @@ package nl.uu.cs.ape.models.templateFormulas; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; import java.util.List; +import java.util.Map; +import java.util.Set; import nl.uu.cs.ape.automaton.Block; import nl.uu.cs.ape.automaton.ModuleAutomaton; @@ -8,10 +13,13 @@ import nl.uu.cs.ape.automaton.TypeAutomaton; import nl.uu.cs.ape.models.AbstractModule; 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.AtomType; import nl.uu.cs.ape.models.logic.constructs.TaxonomyPredicate; +import nl.uu.cs.ape.utils.APEDomainSetup; +import nl.uu.cs.ape.utils.APEUtils; /** * The class is used to represent a predefined SLTLx constraints according to a template, and to generate the @@ -30,7 +38,7 @@ public abstract class SLTLxTemplateFormula { private boolean sign; /** - * Instantiates a new SLTL formula. + * Instantiates a new SLTLx formula. * * @param predicate the predicate */ @@ -72,7 +80,7 @@ public boolean getSign() { } /** - * Function returns the formula that was specified under the SLTL operator.
+ * Function returns the formula that was specified under the SLTLx operator.
* Currently only predicates. * * @return StateInterface ({@link AbstractModule}, {@link Module} or {@link Type}). @@ -82,9 +90,9 @@ public TaxonomyPredicate getSubFormula() { } /** - * Returns the type of the SLTL formula [F, G or X]. + * Returns the type of the SLTLx formula [F, G or X]. * - * @return String [F, G or X], depending on the type of SLTL formula. + * @return String [F, G or X], depending on the type of SLTLx formula. */ public abstract String getType(); @@ -96,7 +104,7 @@ public TaxonomyPredicate getSubFormula() { * @param typeStateBlocks Automaton of all the type states. * @param workflowElement type of the workflow element ({@link AtomType#MODULE}, {@link AtomType#MEM_TYPE_REFERENCE} etc.) * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public abstract String getCNF(ModuleAutomaton moduleAutomaton, List typeStateBlocks, AtomType workflowElement, SATAtomMappings mappings); @@ -108,7 +116,7 @@ public TaxonomyPredicate getSubFormula() { * @param then_predicate Predicate that is enforced by if_predicate. * @param moduleAutomaton Module automaton. * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String ite_module(TaxonomyPredicate if_predicate, TaxonomyPredicate then_predicate, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings) { @@ -137,7 +145,7 @@ public static String ite_module(TaxonomyPredicate if_predicate, TaxonomyPredicat * @param moduleAutomaton Module automaton. * @param typeBlocks Type blocks (corresponding to the memory or used type states). * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String ite_type(TaxonomyPredicate if_predicate, TaxonomyPredicate then_predicate, AtomType typeElement, ModuleAutomaton moduleAutomaton, List typeBlocks, SATAtomMappings mappings) { @@ -173,7 +181,7 @@ public static String ite_type(TaxonomyPredicate if_predicate, TaxonomyPredicate * @param then_not_predicate Module that is forbidden by if_predicate. * @param moduleAutomaton Module automaton. * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String itn_module(TaxonomyPredicate if_predicate, TaxonomyPredicate then_not_predicate, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings) { @@ -203,7 +211,7 @@ public static String itn_module(TaxonomyPredicate if_predicate, TaxonomyPredicat * @param moduleAutomaton Module automaton. * @param typeBlocks Type blocks (corresponding to the memory or used type states). * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String itn_type(TaxonomyPredicate if_predicate, TaxonomyPredicate then_not_predicate, AtomType typeElement, ModuleAutomaton moduleAutomaton, List typeBlocks, SATAtomMappings mappings) { @@ -241,7 +249,7 @@ public static String itn_type(TaxonomyPredicate if_predicate, TaxonomyPredicate * @param first_module_in_sequence Predicate that is enforced by second_predicate. * @param moduleAutomaton Module automaton. * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String depend_module(TaxonomyPredicate second_module_in_sequence, TaxonomyPredicate first_module_in_sequence, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings) { @@ -324,7 +332,7 @@ public static String prev_module(TaxonomyPredicate second_module_in_sequence, Ta * @param last_module The module. * @param moduleAutomaton Automaton of all the module states. * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String useAsLastModule(TaxonomyPredicate last_module, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings) { @@ -345,7 +353,7 @@ public static String useAsLastModule(TaxonomyPredicate last_module, ModuleAutoma * @param n The absolute position in the solution. * @param moduleAutomaton Automaton of all the module states. * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String useAsNthModule(TaxonomyPredicate module, int n, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings) { @@ -366,7 +374,7 @@ public static String useAsNthModule(TaxonomyPredicate module, int n, ModuleAutom * @param n Number of repetitions. * @param moduleAutomaton Automaton of all the module states. * @param mappings Set of the mappings for the literals. - * @return The String CNF representation of the SLTL formula. + * @return The String CNF representation of the SLTLx formula. */ public static String useModuleNtimes(TaxonomyPredicate module, int n, ModuleAutomaton moduleAutomaton, SATAtomMappings mappings) { @@ -391,62 +399,178 @@ public static String useModuleNtimes(TaxonomyPredicate module, int n, ModuleAuto * @param mappings Set of the mappings for the literals. * @return */ - public static String use_m_in_label(TaxonomyPredicate module, TaxonomyPredicate inputType, + public static String use_module_input(TaxonomyPredicate module, TaxonomyPredicate inputType, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { - StringBuilder constraints = new StringBuilder(); - /* For each module state in the workflow */ - for (State moduleState : moduleAutomaton.getAllStates()) { - int moduleNo = moduleState.getLocalStateNumber(); - /* ..and for each input state of that module state.. */ - List currInputStates = typeAutomaton.getUsedTypesBlock(moduleNo - 1).getStates(); - /* Encode: if module was used in the module state */ - constraints.append("-") - .append(mappings.add(module, moduleState, AtomType.MODULE)).append(" "); - for (State currInputState : currInputStates) { - /* - * .. the corresponding data type needs to be provided in one of the input - * states - */ - constraints = constraints - .append(mappings.add(inputType, currInputState, AtomType.USED_TYPE)) - .append(" "); - } - constraints.append("0\n"); - } + + StringBuilder constraints = new StringBuilder(); + Set allCombinations = new HashSet<>(); + Map opOrderStates = new HashMap<>(); + Map > opInputs = new HashMap<>(); + + int automatonSize = moduleAutomaton.getAllStates().size(); + for (int opNo = 0; opNo < automatonSize; opNo++) { + + int currOp = mappings.getNextAuxNum(); + allCombinations.add(currOp); + + opOrderStates.put(currOp, moduleAutomaton.getAllStates().get(opNo)); + + opInputs.put(currOp, typeAutomaton.getUsedTypesBlock(opNo).getStates()); + + } + // at least one of the states must be valid + for(Integer currComb : allCombinations) { + constraints.append(currComb + " "); + } + constraints.append("0\n"); + + // each state enforces usage of the corresponding tools and input + for(Integer currComb : allCombinations) { + // enforce tools + constraints.append("-" + currComb + " ") + .append(mappings.add(module, opOrderStates.get(currComb), AtomType.MODULE)) + .append(" 0\n"); + //enforce output/input dependencies + constraints.append("-" + currComb + " "); + for(State currState : opInputs.get(currComb)) { + constraints.append(mappings.add(inputType, currState, AtomType.USED_TYPE)) + .append(" "); + } + constraints.append("0\n"); + + } + return constraints.toString(); } - /** + + /** * Creates a CNF representation of the Constraint:
- * Use module with data inputType as one of the inputs. + * Use module with data outputType as one of the outputs. * * @param module Module to be used. - * @param inputNo Type of one of the input types. + * @param outputType Type of one of the input types. * @param moduleAutomaton The module automaton * @param typeAutomaton The type automaton. * @param mappings Set of the mappings for the literals. * @return */ - public static String use_m_with_dependence(TaxonomyPredicate module, int inputNo, + public static String use_module_output(TaxonomyPredicate module, TaxonomyPredicate outputType, ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { - StringBuilder constraints = new StringBuilder(); - /* For each module state in the workflow */ - for (State moduleState : moduleAutomaton.getAllStates()) { - int moduleNo = moduleState.getLocalStateNumber(); - /* ..and for each input state of that module state.. */ - List currInputStates = typeAutomaton.getUsedTypesBlock(moduleNo - 1).getStates(); - /* Encode: if module was used in the module state */ - constraints.append("-") - .append(mappings.add(module, moduleState, AtomType.MODULE)).append(" "); - for (State currInputState : currInputStates) { - /* - * .. one of the inputs should depend on the inputNo workflow input - */ - constraints = constraints - .append(mappings.add(typeAutomaton.getWorkflowInputBlock().getState(inputNo-1), currInputState, AtomType.R_RELATON)) - .append(" "); - } - constraints.append("0\n"); - } + + StringBuilder constraints = new StringBuilder(); + Set allCombinations = new HashSet<>(); + Map opOrderStates = new HashMap<>(); + Map > onOutputs = new HashMap<>(); + + int automatonSize = moduleAutomaton.getAllStates().size(); + for (int opNo = 0; opNo < automatonSize; opNo++) { + + int currOp = mappings.getNextAuxNum(); + allCombinations.add(currOp); + + opOrderStates.put(currOp, moduleAutomaton.getAllStates().get(opNo)); + + onOutputs.put(currOp, typeAutomaton.getMemoryTypesBlock(opNo + 1).getStates()); + + } + // at least one of the states must be valid + for(Integer currComb : allCombinations) { + constraints.append(currComb + " "); + } + constraints.append("0\n"); + + // each state enforces usage of the corresponding tools and input + for(Integer currComb : allCombinations) { + // enforce tools + constraints.append("-" + currComb + " ") + .append(mappings.add(module, opOrderStates.get(currComb), AtomType.MODULE)) + .append(" 0\n"); + //enforce output/input dependencies + constraints.append("-" + currComb + " "); + for(State currState : onOutputs.get(currComb)) { + constraints.append(mappings.add(outputType, currState, AtomType.MEM_TYPE_REFERENCE)) + .append(" "); + } + constraints.append("0\n"); + + } + + return constraints.toString(); + } + + + /** + * Creates a CNF representation of the Constraint:
+ * 1st operation should generate an output used by the 2nd operation. + * + * @param first_predicate - Module type that generates the data as output + * @param second_predicate - Module type that uses the generated data as input + * @param domainSetup - setup of the domain + * @param moduleAutomaton - module automaton. + * @param typeAutomaton - type automaton + * @param mappings - Set of the mappings for the literals. + * @return The String CNF representation of the SLTLx formula. + */ + public static String connected_modules(TaxonomyPredicate first_predicate, TaxonomyPredicate second_predicate, APEDomainSetup domainSetup, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + StringBuilder constraints = new StringBuilder(); + Set allCombinations = new HashSet<>(); + Map> opOrderStates = new HashMap<>(); + Map> > opOutInPairs= new HashMap<>(); + + int automatonSize = moduleAutomaton.getAllStates().size(); + for (int op1 = 0; op1 < automatonSize-1; op1++) { + for (int op2 = op1 + 1; op2 < automatonSize; op2++) { + + int currComb = mappings.getNextAuxNum(); + allCombinations.add(currComb); + + opOrderStates.put(currComb, new Pair(moduleAutomaton.getAllStates().get(op1), moduleAutomaton.getAllStates().get(op2))); + + List op1outputs = typeAutomaton.getMemoryTypesBlock(op1 + 1).getStates(); + List op2inputs = typeAutomaton.getUsedTypesBlock(op2).getStates(); + + Set> statePairs = APEUtils.getUniquePairs(op1outputs, op2inputs); + opOutInPairs.put(currComb, statePairs); + + } + } + // at least one of the combinations must be valid + for(Integer currComb : allCombinations) { + constraints.append(currComb + " "); + } + constraints.append("0\n"); + + // each combination enforces usage of the corresponding tools and output/inputs + for(Integer currComb : allCombinations) { + // enforce tools + constraints.append("-" + currComb + " ") + .append(mappings.add(first_predicate, opOrderStates.get(currComb).getFirst(), AtomType.MODULE)) + .append(" 0\n"); + constraints.append("-" + currComb + " ") + .append(mappings.add(second_predicate, opOrderStates.get(currComb).getSecond(), AtomType.MODULE)) + .append(" 0\n"); + //enforce output/input dependencies + constraints.append("-" + currComb + " "); + for(Pair currPair : opOutInPairs.get(currComb)) { + constraints.append(mappings.add(currPair.getFirst(), currPair.getSecond(), AtomType.MEM_TYPE_REFERENCE)) + .append(" "); + } + constraints.append("0\n"); + + } + return constraints.toString(); + } + + /** + * Simple method that combines a pair of integers into a unique String. + * @param int1 - first integer + * @param int2 - second integer + * @return Unique combination of the pair, as String. + */ + private static String combine(int int1, int int2) { + return int1 + "_" + int2; } + } 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 740b9e89..5efbe9db 100644 --- a/src/main/java/nl/uu/cs/ape/utils/APEUtils.java +++ b/src/main/java/nl/uu/cs/ape/utils/APEUtils.java @@ -981,6 +981,7 @@ public static void printMemoryStatus(boolean debugMode) { System.out.print("\n[" + memoryStatus.toString()+ "]\t" + totalMemMB + "\tMB \r"); } + /** * Get all unique pairs of PredicateLabels within the collection. * @param set - Set of PredicateLabel that should be used to create the pairs @@ -996,4 +997,21 @@ public static Set> getUniquePairs(Collection Set> getUniquePairs(Collection set1, Collection set2) { + Set> pairs = new HashSet>(); + set1.stream().forEach(ele1 -> { + set2.stream().forEach(ele2 -> { + pairs.add(new Pair(ele1, ele2)); + }); + }); + return pairs; + } + } From 441b70b9529268b9d82941fe89f2ae74bf56156a Mon Sep 17 00:00:00 2001 From: Vedran Kasalica Date: Wed, 8 Jun 2022 01:02:30 +0200 Subject: [PATCH 2/6] Adding 2 new constraint templates Added constraints templates and a CLI parameter for no of solutions --- src/main/java/nl/uu/cs/ape/Main.java | 19 ++++- .../cs/ape/constraints/ConstraintFactory.java | 73 ++++++++++++++++- .../SLTLxTemplateFormula.java | 81 +++++++++++++++++++ 3 files changed, 171 insertions(+), 2 deletions(-) diff --git a/src/main/java/nl/uu/cs/ape/Main.java b/src/main/java/nl/uu/cs/ape/Main.java index f7651b08..051965bf 100644 --- a/src/main/java/nl/uu/cs/ape/Main.java +++ b/src/main/java/nl/uu/cs/ape/Main.java @@ -2,12 +2,15 @@ import guru.nidi.graphviz.attribute.Rank.RankDir; import nl.uu.cs.ape.configuration.APEConfigException; +import nl.uu.cs.ape.configuration.APERunConfig; import nl.uu.cs.ape.core.solutionStructure.SolutionsList; import nl.uu.cs.ape.utils.APEUtils; import org.json.JSONException; +import org.json.JSONObject; import org.semanticweb.owlapi.model.OWLOntologyCreationException; +import java.io.File; import java.io.IOException; /** @@ -24,8 +27,16 @@ public class Main { */ public static void main(String[] args) { String path; + int solutionsNo = -1; if (args.length == 1) { path = args[0]; + } else if(args.length == 2) { + path = args[0]; + try { + solutionsNo = Integer.parseInt(args[1]); + } catch (NumberFormatException e) { + System.err.println("Second parameter is not an integer."); + } } else { path = "./config.json"; } @@ -49,8 +60,14 @@ public static void main(String[] args) { SolutionsList solutions; try { + JSONObject runConfigJson = APEUtils.readFileToJSONObject(new File(path)); + APERunConfig runConfig = new APERunConfig(runConfigJson, apeFramework.getDomainSetup()); + + if(solutionsNo > 0) { + runConfig.setMaxNoSolutions(solutionsNo); + } // run the synthesis and retrieve the solutions - solutions = apeFramework.runSynthesis(path); + solutions = apeFramework.runSynthesis(runConfig); } catch (APEConfigException e) { System.err.println("Error in synthesis execution. APE configuration error:"); 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 7773531f..0592b192 100644 --- a/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java +++ b/src/main/java/nl/uu/cs/ape/constraints/ConstraintFactory.java @@ -206,7 +206,6 @@ public boolean initializeConstraints(AllModules allModules, AllTypes allTypes) { addConstraintTemplate(currTemplate); - /* * ID: connected_op */ @@ -214,6 +213,21 @@ public boolean initializeConstraints(AllModules allModules, AllTypes allTypes) { "1st operation should generate an output used by the 2nd operation."); addConstraintTemplate(currTemplate); + + /* + * ID: not_connected_op + */ + currTemplate = new Constraint_not_connected_modules("not_connected_op", moduleParam2, + "1st operation should never generate an output used by the 2nd operation."); + addConstraintTemplate(currTemplate); + + /* + * ID: not_repeat_op + */ + currTemplate = new Constraint_not_repeat_modules("not_repeat_op", moduleParam1, + "No operation that belongs to the subtree should be repeated over."); + addConstraintTemplate(currTemplate); + /* * ID: gen_t @@ -865,5 +879,62 @@ public String getConstraint(List parameters, APEDomainSetup d return SLTLxTemplateFormula.connected_modules(parameters.get(0), parameters.get(1),domainSetup, moduleAutomaton, typeAutomaton, mappings); } } + + /** + * Implements constraints of the form:
+ * 1st operation should not generate an output used by the 2nd operation + * subsequently using the function {@link #getConstraint}. + */ + public class Constraint_not_connected_modules extends ConstraintTemplate { + /** + * Instantiates a new Constraint if then module. + * + * @param id the id + * @param parameterTypes the parameter types + * @param description the description + */ + protected Constraint_not_connected_modules(String id, List parameterTypes, + String description) { + super(id, parameterTypes, description); + } + @Override + public String getConstraint(List parameters, APEDomainSetup domainSetup, + ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + if (parameters.size() != this.getNoOfParameters()) { + super.throwParametersError(parameters.size()); + return null; + } + return SLTLxTemplateFormula.not_connected_modules(parameters.get(0), parameters.get(1),domainSetup, moduleAutomaton, typeAutomaton, mappings); + } + } + + /** + * Implements constraints of the form:
+ * No operation that belongs to the subtree should be repeated over. + * {@link #getConstraint}. + */ + public class Constraint_not_repeat_modules extends ConstraintTemplate { + /** + * Instantiates a new Constraint last module. + * + * @param id the id + * @param parametersNo the parameters no + * @param description the description + */ + protected Constraint_not_repeat_modules(String id, List parametersNo, + String description) { + super(id, parametersNo, description); + } + + @Override + public String getConstraint(List parameters, APEDomainSetup domainSetup, + ModuleAutomaton moduleAutomaton, TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + if (parameters.size() != this.getNoOfParameters()) { + super.throwParametersError(parameters.size()); + return null; + } + return SLTLxTemplateFormula.notRepeatModules(parameters.get(0), domainSetup, moduleAutomaton, typeAutomaton, mappings); + } + } } 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 1a84c8da..b58a029e 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 @@ -562,6 +562,87 @@ public static String connected_modules(TaxonomyPredicate first_predicate, Taxono return constraints.toString(); } + + /** + * Creates a CNF representation of the Constraint:
+ * 1st operation should not generate an output used by the 2nd operation. + * + * @param first_predicate - Module type that generates the data as output + * @param second_predicate - Module type that uses the generated data as input + * @param domainSetup - setup of the domain + * @param moduleAutomaton - module automaton. + * @param typeAutomaton - type automaton + * @param mappings - Set of the mappings for the literals. + * @return The String CNF representation of the SLTLx formula. + */ + public static String not_connected_modules(TaxonomyPredicate first_predicate, TaxonomyPredicate second_predicate, APEDomainSetup domainSetup, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + StringBuilder constraints = new StringBuilder(); + + int automatonSize = moduleAutomaton.getAllStates().size(); + for (int op1 = 0; op1 < automatonSize-1; op1++) { + for (int op2 = op1 + 1; op2 < automatonSize; op2++) { + + State firstModuleState = moduleAutomaton.get(op1); + State secondModuleState = moduleAutomaton.get(op2); + + List op1outputs = typeAutomaton.getMemoryTypesBlock(op1 + 1).getStates(); + List op2inputs = typeAutomaton.getUsedTypesBlock(op2).getStates(); + + // Ensure that either the 2 operations are not used consequently, or that they are not connected + Set> statePairs = APEUtils.getUniquePairs(op1outputs, op2inputs); + for(Pair currIOpair : statePairs) { + constraints.append("-").append(mappings.add(first_predicate, firstModuleState, AtomType.MODULE)).append(" "); + constraints.append("-" + + mappings.add(currIOpair.getFirst(), currIOpair.getSecond(), AtomType.MEM_TYPE_REFERENCE) + " "); + constraints.append("-" + + mappings.add(second_predicate, secondModuleState, AtomType.MODULE) + + " 0\n"); + } + + } + } + + return constraints.toString(); + } + + + public static String notRepeatModules(TaxonomyPredicate predicate, APEDomainSetup domainSetup, ModuleAutomaton moduleAutomaton, + TypeAutomaton typeAutomaton, SATAtomMappings mappings) { + StringBuilder constraints = new StringBuilder(); + + int automatonSize = moduleAutomaton.getAllStates().size(); + for (int op1 = 0; op1 < automatonSize-1; op1++) { + for (int op2 = op1 + 1; op2 < automatonSize; op2++) { + + State firstModuleState = moduleAutomaton.get(op1); + State secondModuleState = moduleAutomaton.get(op2); + + List op1outputs = typeAutomaton.getMemoryTypesBlock(op1 + 1).getStates(); + List op2inputs = typeAutomaton.getUsedTypesBlock(op2).getStates(); + + // Ensure that either each operation is not used consequently, or that they are not connected + Set> statePairs = APEUtils.getUniquePairs(op1outputs, op2inputs); + for(Pair currIOpair : statePairs) { + // filter all operations + domainSetup.getAllModules().getElementsFromSubTaxonomy(predicate).stream() + .filter(x -> x.isSimplePredicate()).forEach(operation ->{ + + constraints.append("-").append(mappings.add(operation, firstModuleState, AtomType.MODULE)).append(" "); + constraints.append("-" + + mappings.add(currIOpair.getFirst(), currIOpair.getSecond(), AtomType.MEM_TYPE_REFERENCE) + " "); + constraints.append("-" + + mappings.add(operation, secondModuleState, AtomType.MODULE) + + " 0\n"); + }); + } + + } + } + + return constraints.toString(); + } + /** * Simple method that combines a pair of integers into a unique String. From 2c5f95d5802e434a151999a209e81815347d4f3d Mon Sep 17 00:00:00 2001 From: Vedran Kasalica Date: Fri, 10 Jun 2022 16:38:12 +0200 Subject: [PATCH 3/6] Add total encoding runtime message --- src/main/java/nl/uu/cs/ape/APE.java | 1 + .../java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java | 4 +++- src/main/java/nl/uu/cs/ape/utils/APEUtils.java | 7 +++++-- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/main/java/nl/uu/cs/ape/APE.java b/src/main/java/nl/uu/cs/ape/APE.java index 14b2a8c0..ddeea215 100644 --- a/src/main/java/nl/uu/cs/ape/APE.java +++ b/src/main/java/nl/uu/cs/ape/APE.java @@ -354,6 +354,7 @@ private SolutionsList executeSynthesis(APERunConfig runConfig) throws IOExceptio System.out.println(allSolutions.getFlag().getMessage()); long runTimeMS = APEUtils.timerPrintSolutions(globalTimerID, allSolutions.getNumberOfSolutions()); + allSolutions.setSolvingTime(runTimeMS); return allSolutions; } diff --git a/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java b/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java index d1645b6d..eb714df6 100644 --- a/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java +++ b/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java @@ -89,6 +89,8 @@ public class SATSynthesisEngine implements SynthesisEngine { */ private SLTLxVariableOccuranceCollection varUsage; + public static double encodingTime = 0; + /** * Setup of an instance of the SAT synthesis engine. * @@ -262,7 +264,7 @@ public boolean synthesisEncoding() throws IOException { long problemSetupTimeElapsedMillis = System.currentTimeMillis() - problemSetupStartTime; System.out.println("Total problem setup time: " + (problemSetupTimeElapsedMillis / 1000F) + " sec."); - + encodingTime += problemSetupTimeElapsedMillis; return true; } 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 5efbe9db..19123e22 100644 --- a/src/main/java/nl/uu/cs/ape/utils/APEUtils.java +++ b/src/main/java/nl/uu/cs/ape/utils/APEUtils.java @@ -611,8 +611,11 @@ public static long timerPrintSolutions(String timerID, int solutionsFound) { return -1; } long printTime = System.currentTimeMillis() - timers.get(timerID); - System.out.println( - "\nAPE found " + solutionsFound + " solutions. Total solving time: " + (printTime / 1000F) + " sec."); + System.out.println("\n" + + "APE found " + solutionsFound + " solutions.\n" + + "Total APE runtime: " + (printTime / 1000F) + " sec.\n" + + "Total encoding time: \t" + (SATSynthesisEngine.encodingTime / 1000F) + " sec."); + System.out.println(); return printTime; } From 1a653fb4e1999662bb2d56c19df49953aefeaa91 Mon Sep 17 00:00:00 2001 From: Vedran Kasalica Date: Mon, 13 Jun 2022 23:36:07 +0200 Subject: [PATCH 4/6] Forbid usage of workflow inputs as outputs --- pom.xml | 2 +- .../core/implSAT/EnforceTypeRelatedRules.java | 30 ++++++++++++++++++- .../ape/core/implSAT/SATSynthesisEngine.java | 20 +++++++++++-- .../java/nl/uu/cs/ape/utils/APEUtils.java | 5 ++-- 4 files changed, 51 insertions(+), 6 deletions(-) diff --git a/pom.xml b/pom.xml index 96227f9c..fe46b8be 100644 --- a/pom.xml +++ b/pom.xml @@ -4,7 +4,7 @@ 4.0.0 io.github.sanctuuary APE - 2.0.1 + 2.0.2 jar io.github.sanctuuary:APE APE is a command line tool and an API for the automated exploration of possible computational pipelines (workflows) from large collections of computational tools. diff --git a/src/main/java/nl/uu/cs/ape/core/implSAT/EnforceTypeRelatedRules.java b/src/main/java/nl/uu/cs/ape/core/implSAT/EnforceTypeRelatedRules.java index f99a797c..ed6e5ff1 100644 --- a/src/main/java/nl/uu/cs/ape/core/implSAT/EnforceTypeRelatedRules.java +++ b/src/main/java/nl/uu/cs/ape/core/implSAT/EnforceTypeRelatedRules.java @@ -24,6 +24,7 @@ import nl.uu.cs.ape.models.sltlxStruc.SLTLxNegatedConjunction; import nl.uu.cs.ape.models.sltlxStruc.SLTLxNegation; import nl.uu.cs.ape.utils.APEDomainSetup; +import nl.uu.cs.ape.utils.APEUtils; /** * The {@code EnforceTypeRelatedRules} class is used to encode SLTLx constraints based on the @@ -237,7 +238,7 @@ private static Set typeEnforceTaxonomyStructureForState (TaxonomyP public static Set workflowInputs(AllTypes allTypes, List program_inputs, TypeAutomaton typeAutomaton) throws APEConfigException { Set fullEncoding = new HashSet(); - List workflowInputStates = typeAutomaton.getMemoryTypesBlock(0).getStates(); + List workflowInputStates = typeAutomaton.getWorkflowInputBlock().getStates(); for (int i = 0; i < workflowInputStates.size(); i++) { State currState = workflowInputStates.get(i); if (i < program_inputs.size()) { @@ -300,4 +301,31 @@ public static Set workdlowOutputs(AllTypes allTypes, List pr return fullEncoding; } + + /** + * Encodes rules that ensure that the initial workflow inputs are not used as workflow outputs. + * + * @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 inputsAreNotOutputs(AllTypes allTypes, List program_inputs, TypeAutomaton typeAutomaton) throws APEConfigException { + Set fullEncoding = new HashSet(); + + List workflowInputStates = typeAutomaton.getWorkflowInputBlock().getStates(); + List workflowOutputStates = typeAutomaton.getWorkflowOutputBlock().getStates(); + for(Pair pairIO : APEUtils.getUniquePairs(workflowInputStates, workflowOutputStates) ) { + fullEncoding.add( + new SLTLxNegation( + new SLTLxAtom( + AtomType.MEM_TYPE_REFERENCE, + pairIO.getFirst(), + pairIO.getSecond()))); + } + return fullEncoding; + } + + } diff --git a/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java b/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java index eb714df6..7899c121 100644 --- a/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java +++ b/src/main/java/nl/uu/cs/ape/core/implSAT/SATSynthesisEngine.java @@ -89,8 +89,16 @@ public class SATSynthesisEngine implements SynthesisEngine { */ private SLTLxVariableOccuranceCollection varUsage; + /** + * Static variable used to count the encoding time of the APE instance run, strictly used to display the APE CLI run stats. + */ public static double encodingTime = 0; + /** + * Static variable used to count the SAT solving time of the APE instance run, strictly used to display the APE CLI run stats. + */ + public static double satSolvingTime = 0; + /** * Setup of an instance of the SAT synthesis engine. * @@ -212,6 +220,11 @@ public boolean synthesisEncoding() throws IOException { */ SLTLxFormula.appendCNFToFile(cnfEncoding, this, EnforceTypeRelatedRules.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(domainSetup.getAllTypes(), runConfig.getProgramOutputs(), typeAutomaton)); + /* * Encode the constraints from the file based on the templates (manual templates) */ @@ -248,7 +261,6 @@ public boolean synthesisEncoding() throws IOException { int clauses = APEUtils.countLines(cnfEncoding); String sat_input_header = "p cnf " + variables + " " + clauses + "\n"; APEUtils.timerRestartAndPrint(currLengthTimer, "Reading rows"); - satInputFile = APEUtils.concatIntoFile(sat_input_header, cnfEncoding); cnfEncoding.delete(); @@ -263,7 +275,7 @@ public boolean synthesisEncoding() throws IOException { long problemSetupTimeElapsedMillis = System.currentTimeMillis() - problemSetupStartTime; - System.out.println("Total problem setup time: " + (problemSetupTimeElapsedMillis / 1000F) + " sec."); + System.out.println("Total problem setup time: " + (problemSetupTimeElapsedMillis / 1000F) + " sec (" + clauses + " clauses)."); encodingTime += problemSetupTimeElapsedMillis; return true; } @@ -339,20 +351,24 @@ private List runMiniSAT(InputStream sat_input, int solutionsFo } catch (ParseFormatException e) { System.out.println("Error while parsing the cnf encoding of the problem by the MiniSAT solver."); System.err.println(e.getMessage()); + return solutions; } catch (ContradictionException e) { if (solutionsFound == 0) { System.err.println("Unsatisfiable"); + return solutions; } } catch (TimeoutException e) { System.err.println("Timeout. Total solving took longer than the timeout: " + globalTimeoutMs + " ms."); } catch (IOException e) { System.err.println("Internal error while parsing the encoding."); + return solutions; } if (solutionsFound == 0 || solutionsFound % 500 != 0) { realTimeElapsedMillis = System.currentTimeMillis() - realStartTime; System.out.println("Found " + solutionsFound + " solutions. Solving time: " + (realTimeElapsedMillis / 1000F) + " sec."); + satSolvingTime += realTimeElapsedMillis; } return solutions; 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 19123e22..80637f79 100644 --- a/src/main/java/nl/uu/cs/ape/utils/APEUtils.java +++ b/src/main/java/nl/uu/cs/ape/utils/APEUtils.java @@ -613,8 +613,9 @@ public static long timerPrintSolutions(String timerID, int solutionsFound) { long printTime = System.currentTimeMillis() - timers.get(timerID); System.out.println("\n" + "APE found " + solutionsFound + " solutions.\n" - + "Total APE runtime: " + (printTime / 1000F) + " sec.\n" - + "Total encoding time: \t" + (SATSynthesisEngine.encodingTime / 1000F) + " sec."); + + "Total APE runtime: \t\t" + (printTime / 1000F) + " sec.\n" + + "Total encoding time: \t\t" + (SATSynthesisEngine.encodingTime / 1000F) + " sec.\n" + + "Total SAT solving time: \t" + (SATSynthesisEngine.satSolvingTime / 1000F) + " sec."); System.out.println(); return printTime; } From a1c575fa302254946cc5d05d3af8ca7be8caf090 Mon Sep 17 00:00:00 2001 From: Vedran Kasalica Date: Tue, 30 Aug 2022 16:36:15 +0200 Subject: [PATCH 5/6] Fix - clean all constraints before re-run Clean both, NL templates and SLTLx constraints before synthesis re-run --- src/main/java/nl/uu/cs/ape/utils/APEDomainSetup.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/java/nl/uu/cs/ape/utils/APEDomainSetup.java b/src/main/java/nl/uu/cs/ape/utils/APEDomainSetup.java index fee9f004..b8a759e6 100644 --- a/src/main/java/nl/uu/cs/ape/utils/APEDomainSetup.java +++ b/src/main/java/nl/uu/cs/ape/utils/APEDomainSetup.java @@ -152,6 +152,7 @@ public List getSLTLxConstraints(){ */ public void clearConstraints() { this.unformattedConstr.clear(); + this.constraintsSLTLx.clear(); } /** From bd5fe435af69f19078fd30d0636f901fdd27cd1a Mon Sep 17 00:00:00 2001 From: Vedran Kasalica Date: Tue, 30 Aug 2022 16:37:29 +0200 Subject: [PATCH 6/6] Update to v2.0.3 --- pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pom.xml b/pom.xml index fe46b8be..e515f486 100644 --- a/pom.xml +++ b/pom.xml @@ -4,7 +4,7 @@ 4.0.0 io.github.sanctuuary APE - 2.0.2 + 2.0.3 jar io.github.sanctuuary:APE APE is a command line tool and an API for the automated exploration of possible computational pipelines (workflows) from large collections of computational tools.