Skip to content

Nondeterministic Instructions

Jump to bottom
Victor Mataré edited this page Jul 22, 2020 · 2 revisions

Nondeterminisms are intended the be used within a planned block, where they will be resolved in such a way that the entire block becomes executable.

Nondeterministic choice

Syntax:

choose {
    IMPERATIVE_STATEMENT
    [ IMPERATIVE_STATEMENT ... ]
}

Choose one of the given IMPERATIVE_STATEMENTs for execution.

Fails: When the chosen IMPERATIVE_STATEMENT fails.

Possible: Iff at least one of the given IMPERATIVE_STATEMENTs is possible.

Nondeterministic argument choice

Syntax:

pick (TYPE VAR_NAME [ in SET ])
    IMPERATIVE_STATEMENT

Choose an argument for the given code block. Usually, IMPERATIVE_STATEMENT will somewhere refer to VAR_NAME, e.g. as an argument in an action call.

Fails: When IMPERATIVE_STATEMENT fails.

Possible: Iff IMPERATIVE_STATEMENT is possible for at least one assignment of a value out of SET to VAR_NAME.

Clone this wiki locally