Execution¶

This page documents the execution model of the language, focusing on how Statements can be used to sequentially manipulate Valuations.

Input¶

To allow the transformation from input to output valuations, the input must first be prepared for execution. This is done by creating variables that use the execution_input/2 function symbol as a name.

execution_input(ExecutionName, Name)

Name	Description
`ExecutionName`	The name of the execution for which the input variable is being created.
`Name`	The name of the variable representing the input value.

Example

Defining an input variable with some value for a specific execution:

variable_define(execution_input(my_exec, a), val(int, 5)).

This creates a variable a with the integer value 5 for the execution my_exec.

Output¶

After execution, the output values will appear as variables using the execution_output/2 function symbol as a name.

Note

Output Variables do not necessarily have to appear in the input. Meaning, they also do not have to be declared beforehand. They will be created during execution as needed.

execution_output(ExecutionName, Name)

Name	Description
`ExecutionName`	The name of the execution for which the output variable is being created.
`Name`	The name of the variable representing the output value.

Assign¶

Statement

Transformations are done by using the assign/2 function symbol. This assigns the Valuation of a given Expression to a given variable within the context of a Statement.

assign(Name, Expression)

Name	Description
`Name`	The name of the variable to which the result of the expression will be assigned.
`Expression`	The Expression whose result will be assigned to the variable.

Example

A simple assignment of a constant value to a variable:

assign(c, val(int, 5))

In this example, the variable c is assigned the integer value 5.

Control Flow¶

For more complex executions, control flow statements can be used to combine multiple statements into one execution, or to create conditional executions.

Sequence¶

Statement

Multiple statements can be combined into a sequence using the seq2/2 function symbol. This allows for executing multiple statements in order.

One crucial aspect of sequences is that the output of the first statement becomes the input for the second statement.

seq2(Statement1, Statement2)

Name	Description
`Statement1`	The first Statement to be executed.
`Statement2`	The second Statement to be executed after the first.

Example

Combining two statements into a sequence:

ADD_ONE = assign(a, operation(add, (variable(a), (val(int,1),())))),
seq2(
    ADD_ONE,
    ADD_ONE
)

In this example, the variable a is incremented by 1 twice in sequence. Since the output of the first assignment becomes the input for the second, the final value of a will be increased by 2.

If¶

Statement

The if/3 function symbol allows for conditional execution of statements based on the evaluation of an expression.

if(Condition, ThenStatement, ElseStatement)

Name	Description
`Condition`	An Expression that evaluates to a boolean value, determining which statement
`ThenStatement`	The Statement to execute if the condition is true.
`ElseStatement`	The Statement to execute if the condition is false.

Example

A conditional execution based on the value of a variable:

if(
    operation(gt, (variable(a), (val(int, 10),()))),
    assign(b, val(int, 1)),
    assign(b, val(int, 0))
)

In this example, if the variable a is greater than 10, the variable b is assigned the value 1. Otherwise, b is assigned the value 0.

No Operation¶

Statement

The noop/0 function symbol represents a no-operation statement. It performs no action and leaves the input valuation unchanged.

noop

Example

A no-operation statement in an if-else construct:

if(
    operation(gt, (variable(a), (val(int, 10),()))),
    assign(a, val(int, 10)),
    noop
)

In this example, if the variable a is greater than 10, it is assigned the value 10. Otherwise, no operation is performed, and a remains unchanged. Effectively, this clamps the value of a to a maximum of 10.

Assert¶

Statement

The assert/1 function symbol is used to enforce conditions during execution. If the condition evaluates to false, the execution fails. A failed execution behaves the same as a failed ensure, making the entire model unsatisfiable.

assert(Condition)

Name	Description
`Condition`	An Expression that evaluates to a bool value. If false, the execution fails.

Example

An assertion to ensure a variable meets a specific condition:

assert(
    operation(gt, (variable(a), (val(int, 0),())))
)

In this example, the execution will fail if the variable a is not greater than 0.

Declare¶

Declaration Label Support

The execution_declare predicate declares a statement and controls whether it runs.

execution_declare(Name, Statement, Input, Output)
execution_declare(Name, Statement, Input, Output, Condition)
execution_declare(Name, Statement, Input, Output, Condition, Label)

Name	Description
`Name`	A unique identifier for the execution.
`Statement`	The Statement to be executed.
`Input`	A List of terms representing the input to the statement.
`Output`	A List of terms representing the output of the statement.
`Condition`	A boolean Expression controlling execution. Defaults to `val(bool,true)`.
`Label`	An optional label for diagnostics. Defaults to `Name`.

The statement runs when Condition evaluates to true. When it evaluates to false, outputs have value none, and assertions and Python integrity checks within the execution do not reject the model. The condition is evaluated outside the statement's local variable context; use variable(execution_input(Name, X)) to refer to an execution input.

Example

Declaring an execution with a simple assignment statement:

execution_declare(my_exec, S, (a,()), (a,())) :-
    S = assign(a, val(int, 3)).

This declares and runs my_exec, assigning the integer value 3 to a.

Example

Running an execution only when a boolean variable is true:

variable_declare(run,boolDomain).
execution_declare(my_exec, assign(a,val(int,3)), (), (a,()), variable(run)).

The former execution_run predicate is no longer used by CH. Remove unconditional run facts; move conditional execution into the declaration's Condition argument. For labelled declarations, insert the condition before the label.

Note

Flat CH has not yet migrated to this interface and still uses its previous declaration/run predicates.