122
8 Generating Droplet Sequences
Eq. 8.3), and (3) all channels with less time steps (i.e., the successors for an entity
are given by the function succ : C ∪ M → P(C ∪ M)) already contain other
droplets (i.e., part 3 of Eq. 8.3). This motivates the following replacement:
= hd f,t−1 [hSteps(f )]
1
∧ hd e,t−1 = 0 ∧ pd e,t−1 = 0
2
∧
{g∈succ(f ):hSteps(g)
3
.
(8.3)
• In all other cases, it is necessary to check if one of the predecessors (i.e., the
predecessors for an entity are given by the function pred : C ∪ M →
P(C ∪ M)) contains a header, which leafs the predecessor in the next time
step t (i.e., hd f,t−1 [hSteps(f )]). If so, this header enters e. This motivates the
following replacement:
=
f ∈pred(e)
hd f,t−1 [hSteps(f )].
(8.4)
These constraints are adopted to also ensure the flow of the payload droplet but, due
to their similarity, are not explicitly shown here.
Passing this formulation to an SMT-solver now already ensures the correct flow
of droplets. However, it does not ensure that the experiments are executed or that no
droplets coalesce.
Enforcing the Experiment
Initially, before the execution of the experiment starts (at t = 0), it is ensured that
the microfluidic network does not already contain droplets, i.e.
e∈C∪M
hd e,0 = 0 ∧ pd e,0 = 0.
(8.5)
The payload droplet has to be routed through the sequence of the desired modules
defined by the experiment φ. In order to ensure this execution of φ, it is enforced that
each module defined in φ executes at some time step its operation on the payload
droplet. Therefore, all bit vectors pd e,t representing the modules contained in φ
have to be greater than 1 at some time 1 ≤ t ≤ T up . In contrast, the payload droplet
is not allowed to traverse any module not contained in the experiment (i.e., M \ φ).
Therefore, those pd e,t vectors are enforced to be equal to 0 all time. This motivates
the constraint:
e∈φ
T up
t=1
pd e,t > 0 ∧
e∈M\φ
T up
t=1
pd e,t = 0.
(8.6)
8 Generating Droplet Sequences
Eq. 8.3), and (3) all channels with less time steps (i.e., the successors for an entity
are given by the function succ : C ∪ M → P(C ∪ M)) already contain other
droplets (i.e., part 3 of Eq. 8.3). This motivates the following replacement:
= hd f,t−1 [hSteps(f )]
1
∧ hd e,t−1 = 0 ∧ pd e,t−1 = 0
2
∧
{g∈succ(f ):hSteps(g)
3
.
(8.3)
• In all other cases, it is necessary to check if one of the predecessors (i.e., the
predecessors for an entity are given by the function pred : C ∪ M →
P(C ∪ M)) contains a header, which leafs the predecessor in the next time
step t (i.e., hd f,t−1 [hSteps(f )]). If so, this header enters e. This motivates the
following replacement:
=
f ∈pred(e)
hd f,t−1 [hSteps(f )].
(8.4)
These constraints are adopted to also ensure the flow of the payload droplet but, due
to their similarity, are not explicitly shown here.
Passing this formulation to an SMT-solver now already ensures the correct flow
of droplets. However, it does not ensure that the experiments are executed or that no
droplets coalesce.
Enforcing the Experiment
Initially, before the execution of the experiment starts (at t = 0), it is ensured that
the microfluidic network does not already contain droplets, i.e.
e∈C∪M
hd e,0 = 0 ∧ pd e,0 = 0.
(8.5)
The payload droplet has to be routed through the sequence of the desired modules
defined by the experiment φ. In order to ensure this execution of φ, it is enforced that
each module defined in φ executes at some time step its operation on the payload
droplet. Therefore, all bit vectors pd e,t representing the modules contained in φ
have to be greater than 1 at some time 1 ≤ t ≤ T up . In contrast, the payload droplet
is not allowed to traverse any module not contained in the experiment (i.e., M \ φ).
Therefore, those pd e,t vectors are enforced to be equal to 0 all time. This motivates
the constraint:
e∈φ
T up
t=1
pd e,t > 0 ∧
e∈M\φ
T up
t=1
pd e,t = 0.
(8.6)