Describe desired workflows

This page describes how to specify the workflows to be generated by the APE library. The workflows are specified using a JSON configuration file as described in in the previous section. The initial description of the problem is given by the workflow inputs and outputs described in the configuration file. In addition, the configuration file references a constraint file that specifies the constraints that the workflow must satisfy. The constraints are used to guide the workflow synthesis process and ensure that the generated workflows meet the requirements of the problem. This page describes how to specify the constraints in the constraint file.

Constraint file is a JSON document that contains a list of constraints that must be satisfied by each generated workflow. In case constraints are contradicting each other (e.g., “Use tool X” and “Never use tool X”) so solution will be found. The constraints can be specified in two ways: using predefined templates or using SLTL^x (Semantic Linear Time Temporal Logic extended) constraints. The predefined templates are a set of common constraints that can be used to specify the relationships between the operations in the workflow. The SLTL^x constraints are more flexible and allow the user to define complex constraints using logical formulas. The following sections describe how to specify constraints using predefined templates and SLTL^x constraints.

Constraint Templates

As an example we will present one of the constraint templates, namely “if then generate type” is represented as follows:

{
   "constraintid": "use_m",
   "description": "Use the specified tool in the solution.",
   "parameters": [
          ["${parameter_1}"]
   ]
}

"${parameter_1}" represent a tool or an abstract operation from the domain taxonomy. The following encoding represents a use of such constraint in practice (tag "description" is not obligatory):

{
   "constraintid": "gen_ite_t",
   "parameters": [
      ["Transformation"]
   ]
}

The constraint is interpreted as: “A tool that performs Transformation must be used in the workflow.”

All pre-defined constraints that can be used:

ID	Description
ite_m	If we use operation ${parameter_1}, then use ${parameter_2} subsequently.
itn_m	If we use operation ${parameter_1}, then do not use ${parameter_2} subsequently.
depend_m	If we use operation ${parameter_1}, then we must have used ${parameter_2} prior to it.
next_m	If we use operation ${parameter_1}, then use ${parameter_2} as a next operation in the sequence.
prev_m	If we use operation ${parameter_1}, then we must have used ${parameter_2} as a previous operation in the sequence.
use_m	Use operation ${parameter_1} in the solution.
nuse_m	Do not use operation ${parameter_1} in the solution.
last_m	Use ${parameter_1} as last operation in the solution.
use_t	Use type ${parameter_1} in the solution.
gen_t	Generate type ${parameter_1} in the solution.
nuse_t	Do not use type ${parameter_1} in the solution.
ngen_t	Do not generate type ${parameter_1} in the solution.
use_ite_t	If we have used data type ${parameter_1}, then use type ${parameter_2} subsequently.
gen_ite_t	If we have generated data type ${parameter_1}, then generate type ${parameter_2} subsequently.
use_itn_t	If we have used data type ${parameter_1}, then do not use type ${parameter_2} subsequently.
gen_itn_t	If we have generated data type ${parameter_1}, then do not generate type ${parameter_2} subsequently.
operation_input	Use the operation with an input of the given type.
operation_output	Use the operation to generate an output of the given type.
connected_op	The 1st operation should generate an output used bt the 2nd operation.
not_connected_op	The 1st operation should never generate an output sued by the 2nd operation.
not_repeat_op	No operation that belongs to the subtree should be repeated within the workflow.

SLTL^x constraints

SLTL^x (Semantic Linear Time Temporal Logic extended) allows the user to define constraints using logical formulas. For example, the following constraint prevents an operation within the subtree Transformation from using the same input twice:

{
   "constraintid": "SLTLx",
   "formula": "!F Exists (?x) (<'Transformation'(?x,?x;)> true)"
}

The formula above can be broken down as follows:

• !: negation operator

• F: Finally operator - the formula holds at some point in the future (future in Time Logics can be seen as the following states in the workflow)

• Exists: Existential quantifier

• ?x: variable

• <Transformation’(?x,?x;)> true : after applying operation Transformation with at least 2 distinct inputs ?x and ?x we reach a state where the formula holds (true). Notice that the semicolon ; is used to separate the inputs and outputs of the operation. In our specification no outputs were specified.

The formula above can be interpreted as: “It is not the case that in the workflow there exists an operation Transformation that uses the same input twice.”

This second example specifies a constraint which makes sure a workflow input is used only once. To tell APE which inputs are not to be used twice, the workflow inputs have been labeled as “Input” in the run configuration file:

 "inputs": [
  {
    "data_0006": ["data_9003"],
    "format_1915": ["format_3989"],
    "APE_label": ["Input"]
  },
  {
    "data_0006": ["data_9003"],
    "format_1915": ["format_3989"],
    "APE_label": ["Input"]
  },
  {
    "data_0006": ["data_9001"],
    "format_1915": ["format_1929", "format_3331"],
    "APE_label": ["Input"]
  }
],

The labeled inputs can now be used in the SLTL^x formula:

{
   "constraintid": "SLTLx",
   "formula": "! Exists (?x) ('Input'(?x) & (F <'Tool'(?x;)> F <'Tool'(?x;)> true))"
}

In our example Tool is the root of the tool taxonomy, therefore it’s the most general type of operation. The formula above can be broken down as follows:

• !: negation operator

• Exists: Existential quantifier

• ?x: variable

• 'Input'(?x): the variable ?x is of type Input

• &: logical AND operator

• F: Finally operator - the formula holds at some point in the future (future in Time Logics can be seen as the following states in the workflow)

• <'Tool'(?x;)> X: after applying operation Tool with input ?x we reach a state where the formula X holds (in our case, the formula X is F <'Tool'(?x;)> true)

• F <'Tool'(?x;)> true: at some point in the future, the operation Tool with input ?x is applied and the formula holds (true)

The formula above can be interpreted as: “It is not the case that in the workflow there exists an input that is used twice.”

SLTL^x syntax

This document provides a list of syntax options available in the SLTL^x logic.

Formulas (formula)

A formula can be one of the following:

1. true

2. ( formula )

3. < TOOL > formula

4. CONSTANT ( VARIABLE )

5. VARIABLE = VARIABLE

6. ! formula

7. Forall ( VARIABLE ) formula

8. Exists ( VARIABLE ) formula

9. UN_MODAL formula

10. formula BIN_CONNECTIVE formula

11. formula BIN_MODAL formula

12. R ( VARIABLE , VARIABLE )

Binary Connectives (BIN_CONNECTIVE)

• & (AND)

• | (OR)

• -> (IMPL)

• <-> (EQUIVALENT)

Unary Modal Operators (UN_MODAL)

• G (GLOBALLY)

• F (FINALLY)

• X (NEXT STEP)

Binary Modal Operators (BIN_MODAL)

• U (SLTL_UNTIL)

Tool (TOOL)

A TOOL is defined as:

CONSTANT ( VARIABLE,...,VARIABLE ; VARIABLE,...,VARIABLE )

Variables (VARIABLE)

• A variable is denoted by a ? followed by alphanumeric characters or underscores.

Tokens

• true: The constant true.

• VARIABLE: A variable starting with ?.

• CONSTANT: A constant enclosed in single quotes '.

• R: Relation.

• U: Until.

• G: Globally.

• F: Finally.

• X: Next.

• |: OR.

• &: AND.

• ->: Implies.

• <->: Equivalent.

• =: Equals.

• !: Negation.

• Exists: Existential quantifier.

• Forall: Universal quantifier.

Examples

1. !F Exists (?x) (<'Transformation'(?x,?x;)> true) - No operation within the subtree Transformation uses the same input twice.

2. ! Exists (?x) ('Input'(?x) & (F <'Tool'(?x;)> F <'Tool'(?x;)> true)) - No Input is used twice (where Input is a custom label added to all the inputs).

See SLTL:sup:`x Constraints <#sltlx-constraints>`_ for more detailed explanation of the constraints.