Declare asynchronous transitions

Declare asynchronous transitions#

By default, reachability properties (e.g., x >= y) are computed with regards to the Most Permissive update mode. However, this can be restricted with the scope_reachability context.

In the context of scope_reachabbility(max_change=1), trajectories are computed by changing at most 1 component. This boils down to consider only one transition with the (fully) asynchronous mode:

with bo.scope_reachability(max_changes=1):
    x = ~bo.obs({"A":1,"B":0,"C":0})
    y = ~bo.obs({"A":1,"B":1,"C":0})
    x >= y  # realized by one fully-asynchronous transition