ALF11 — Non-deterministic behavior on "if statement"

The non-deterministic behavior is an issue to evaluate the correctness of algorithm written in ALF. it is very difficult to test and check non determinist behavior. The formal approach use for ALF is the good right but also support a determinitic behavior.

Sequential if statement clauses are deterministic

Alf syntax allows both sequential clauses (if/else if/else) and concurrent clauses (if/or if). As the name indicates, the execution of sequential clauses is sequential and determinate, just as for a traditional if statement. So, one can avoid introducing indeterminate behavior by just not using concurrent clauses.

(One can also annotate an if statement as @determinate, which indicates that at most one condition will evaluate to true. This asserts determinate behavior even when using concurrent clauses. However, it is a modeler responsibility to ensure this assertion is true, and there is no required language check of this.)