Subsections

• Constraints on atomic formulae
• Constraints on complex formulae

2.3 Explicit determinism

  The definition of explicit determinism follows its name. Determinism is marked in the syntax of the formula. Advantages of explicit determinism are :

• trivial decidability,
• easy use.

To mark explicit determinism, we introduce a new special predicate represented by the := operator. The := predicate is used in $\mbox{GDMO}^+$[GDM97]. The set of atomic logical formulae made on this predicate is a subset of the set of atomic logical formulae made on equality predicate.

The := predicate does not specify all determinism of a logical formula (for example $0<y \land y<2$ is deterministic in the set of natural integers). This predicate can be introduced in every logical formalism but some constraints are imposed. For example, the formula :

 

x'+y':=4

is not allowed because it is not deterministic, and is in contradiction with the := predicate intention to mark determinism.

Constraints on the := predicate can be separated into two categories :

• constraints on atomic formulae defined with the := predicate ;
• constraints on complex formulae containing an atomic formula defined with the := predicate.

Constraints on atomic formulae

The := predicate is represented by a symbol often used to define assignment in many programmation languages. In the case of simulation, we decide to consider this predicate as an assignment. In the first place, we define a direction of evaluation of an atomic formula based on the := predicate. We assign the right operand to the left operand. In the second place, only decorated variables can be modified, so the left operand is composed of exactly one decorated variable.

Finally, let's take the example of the formula :

 

x':=y'+2

This formula is not deterministic because we do not known the value of y'. Furthermore, not any decorated variables must appear in the right operand.

We summarize the syntax of an atomic formula based on the := predicate by these generic formulae :

• x':=...
• f'(p₁,p₂,...):=...

where not any decorated variables appear in any p_i.

Constraints on complex formulae

The $\lor$ and $\neg$ connectors are by definition non-deterministic, so an atomic formula based on the := predicate cannot be an operand of these connectors. On the contrary, the $\land$ connector is by definition deterministic, so an atomic formula based on the := predicate can be an operand of this connector. Some examples :

• $x':=1 \lor x':=2 \mbox{ is invalid.}$
• $\neg(x':=1) \mbox{ is invalid.}$
• $x':=1 \land x':=2 \mbox{ is valid.}$

The last formula is declared valid by the determinism evaluation. Logical evaluation of this formula is false.

An universally quantified formula can be deterministic, so an atomic formula based on the := predicate can be in the scope of an universally quantified formula. To achieve this, the iterative set related to the universally quantified formula must be known, i.e. no decorated variable occurrence is referenced in this iterative set. For example, a valid universally quantified formula and containing an atomic formula based on the := predicate is :  

$$\forall i \in \{1,2,3,4\} \verb*+ + \vert \verb*+ + f'(i) := f(i) + 1$$ (6)

where f is a table.

In contrast to an universally quantified formula, an existentially quantified formula is not deterministic. Such formula can be evaluate to true for one or many values defined in its iterative set. A possible choice between these values enforces no determinism of an existentially quantified formula. The formula :  

$$\exists i \in \{2,3,4,5\} \verb*+ + \vert \verb*+ + (i \mbox{ modulo } 2)=0 \verb*+ + \land \verb*+ + f'(i) := 5$$ (7)

is invalid because two iterative values (2 and 4) evaluate the formula to true, furthermore, we do not know which of f(2) value or f(4) value must be modified.

An atomic formula based on the := predicate can be referenced in THEN and ELSE branches of a conditional operator if the condition of the formula based on the conditional operator is known, i.e. no decorated variable occurrence is referenced in this condition. For instance, this formula :  

$$\mbox{IF } x=y \mbox{ THEN } x':=1 \mbox{ ELSE } x':=2$$ (8)

is valid.

Our approach is practical, so the constraints that we define in this sub section are very restrictive. This restrictive choice permits a syntactic solution to determine whether a formula is deterministic, i.e. we do not use semantic properties to determine if a formula is deterministic but merely a syntactic algorithm which determines if a formula is deterministic.