The "|/\|" order operator : non-determinism

Both processes P and Q are evaluated from the initial context. If both terminate, there will be at least two execution paths, showing the indeterminism.

Considering 2 processes : P and Q, with non-determinism, each is evaluated from the initial context. If both terminates, at least two executions paths will be taken into account.

Application on the most basic example

Applying this on our most basic example, the "@moe:" section looks like :

UNFORTUNATELY ON THE 2016/02/11 THE "|/\|" scheduling DOES NOT WORK FOR THIS PARTICULAR CASE OF BASIC EXAMPLE. ERROR MESSAGES APPEAR WHEN LAUNCHING THE SYMBOLIC EXECUTION :