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