164
A. Cimatti et al.
Reachability. For all local requirements c and all phases i, it holds that if i − 1
is not reachable then so is phase i, i.e., ¬r
c
i−1 → ¬r
c
i . Moreover, we require the
monotonicity over time, i.e., r
c
i → (s
c
i−1 ≺ s
c
i ).
Bounds. For all local requirements c and all phases i, c can move to i only if
it respects the bounds [l
c
i , u
c
i ] of phase i, namely r
c
i → (l
c
i ≤ t
c
i − t
c
i−1 ≤ u
c
i ). If
u
c
i = ∞, then we add only the left-most inequality.
Signal and State dependencies. Consider a local requirement c and one of its
phases i. Since we have only a finite number of phases, we can preprocess both
signal and state dependencies to remove from them all negations, as explained
in the extended version of the paper
4 ; this means that every atom in φ
c
i and ψ
c
i
occurs positive.
We want c to reach i only if all its signal and state dependencies are satisfied.
For signal dependencies, we require the time point in which c enters i to be
strictly greater
5 than the time point of the entry of the target phase and smaller
than or equal to the time point of the exit of the target phase.
r
c
i → φ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ s
c
i s
d
j+1 )]
Moreover, we have to guarantee that the state dependencies hold as well. In
particular, if phase i is reachable, then surely the time point in which c enters i
has to be strictly greater than the time point in which the other local requirement
reaches the target phase.
r
c
i → ψ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ s
c
i )]
Since state dependencies are invariant properties, i.e., they have to hold for each
time instant a local requirement is in a particular phase, if one state dependency
is violated at some time point of phase i − 1, then phase i is not reachable. The
contrapositive means that if phase i is reachable, then the state dependencies of
phase i − 1 have to be invariant for phase i − 1, namely:
r
c
i → ∀ s(s
c
i−1
s s
c
i → ψ
c
i−1 [(d, j) → (r
d
j ∧ s
d
j ≺
s s
d
j+1 )])
(1)
Illegal States. If phase i of local requirement c is not reachable, i.e., i is an illegal
state, then there exists a time point s
c
ill such that, for all the next (remaining)
time points ¯
s between s
c
ill and the upperbound of the transition, at least one
dependency is not satisfied.
(r
c
i−1 ∧ ¬r
c
i ) → ∃s
c
ill ∀¯ s(s
c
ill ¯
s s
c
i−1 + u
c
i−1 → VIOLATION(¯ s))
(2)
4 http://users.dimi.uniud.it/ ∼ luca.geatti/tricker.html
5 This allows us to model the observability of the events: c first observes d entering
its phase j and then moves.
A. Cimatti et al.
Reachability. For all local requirements c and all phases i, it holds that if i − 1
is not reachable then so is phase i, i.e., ¬r
c
i−1 → ¬r
c
i . Moreover, we require the
monotonicity over time, i.e., r
c
i → (s
c
i−1 ≺ s
c
i ).
Bounds. For all local requirements c and all phases i, c can move to i only if
it respects the bounds [l
c
i , u
c
i ] of phase i, namely r
c
i → (l
c
i ≤ t
c
i − t
c
i−1 ≤ u
c
i ). If
u
c
i = ∞, then we add only the left-most inequality.
Signal and State dependencies. Consider a local requirement c and one of its
phases i. Since we have only a finite number of phases, we can preprocess both
signal and state dependencies to remove from them all negations, as explained
in the extended version of the paper
4 ; this means that every atom in φ
c
i and ψ
c
i
occurs positive.
We want c to reach i only if all its signal and state dependencies are satisfied.
For signal dependencies, we require the time point in which c enters i to be
strictly greater
5 than the time point of the entry of the target phase and smaller
than or equal to the time point of the exit of the target phase.
r
c
i → φ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ s
c
i s
d
j+1 )]
Moreover, we have to guarantee that the state dependencies hold as well. In
particular, if phase i is reachable, then surely the time point in which c enters i
has to be strictly greater than the time point in which the other local requirement
reaches the target phase.
r
c
i → ψ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ s
c
i )]
Since state dependencies are invariant properties, i.e., they have to hold for each
time instant a local requirement is in a particular phase, if one state dependency
is violated at some time point of phase i − 1, then phase i is not reachable. The
contrapositive means that if phase i is reachable, then the state dependencies of
phase i − 1 have to be invariant for phase i − 1, namely:
r
c
i → ∀ s(s
c
i−1
s s
c
i → ψ
c
i−1 [(d, j) → (r
d
j ∧ s
d
j ≺
s s
d
j+1 )])
(1)
Illegal States. If phase i of local requirement c is not reachable, i.e., i is an illegal
state, then there exists a time point s
c
ill such that, for all the next (remaining)
time points ¯
s between s
c
ill and the upperbound of the transition, at least one
dependency is not satisfied.
(r
c
i−1 ∧ ¬r
c
i ) → ∃s
c
ill ∀¯ s(s
c
ill ¯
s s
c
i−1 + u
c
i−1 → VIOLATION(¯ s))
(2)
4 http://users.dimi.uniud.it/ ∼ luca.geatti/tricker.html
5 This allows us to model the observability of the events: c first observes d entering
its phase j and then moves.