Acceptance Testing Tutorial 3: Set Quantifiers and Sorting

Set-valued scenario execution is work in progress. This tutorial covers specification and validation only. The executable tutorial runs one pick-and-place scenario.

This tutorial extends Tutorial 1 from one object to a set of objects while reusing the same scene. The complete model is sorting.bdd.

Declare set-valued variables

var robot
set var target-objects
var pick-workspace
set var place-workspaces

The singular variables identify the acting robot and source workspace. The set variables describe the objects and their allowed destinations.

Quantify the criteria

for all applies the nested Given–When–Then clauses to every selected object:

for all ( var object in <target-objects> ) {
    Given:
        object-at-pick: holds(
            <object> is located at <pick-workspace>,
            before <E_PICK_START>
        )

    When:
        Behaviour (ns=tutorial) sort-object-behavior {
            duration: from <E_PICK_START> until <E_PLACE_END>
            <robot> picks <object> and places at <place-workspaces>
        }

    Then:
        object-at-place: holds(
            <object> is located at <place-workspaces>,
            after <E_PLACE_END>
        )
}

An additional fluent describes the aggregate outcome:

Then:
    objects-sorted: holds(
        <target-objects> are sorted into <place-workspaces>,
        after <E_PLACE_END>
    )

Bind set variations

variation:
    set var <sorting-template.target-objects>:
        select 1 combinations from <pickplace_objects>
    var <sorting-template.pick-workspace>: {
        <pickplace_workspaces.table-ws>
    }
    set var <sorting-template.place-workspaces>: {
        { <pickplace_workspaces.bin-ws> }
    }
    var <sorting-template.robot>: agn set <pickplace_agents>

The one-object selection keeps this model valid against the small tutorial scene. Add more objects before selecting larger combinations.

Validate the specification

textx check sorting.bdd

The command must report OK. Do not add this model to a graph manifest, launch file, or integration test until set-valued scenario execution is supported.