Safe Decomposition of Startup Requirements
163
on has no constraints on the location variables. The situation is different for
automaton B, for which the transition to on is labelled with 2 ≤ c B ≤ 4 and
c B := 0, and also with ψ on := (l A = on), that is the state dependency of phase
B.on; moreover, ψ on is also an invariant for the second location of automaton
B, since it is a state dependency.
Given a network S := A 1 × · · · × A n of TASVs, the problem of consistency
checking can be expressed as the reachability of location (A 1 .last, . . . , A n .last) ∈
V S . A deadlock of a TASV A is defined as a state (v, t) ∈ V A × R such that A
can take neither a timed nor a discrete transition from (v, t). We call livelock
a state (v, t) such that A can take only timed transitions. The compatibility
checking problem can be expressed as the problem of checking if there exists a
trace of S such that (i) either the trace is finite and its final state is a deadlock
of S; we can check this property by adding a sink location to the TASV S to
which all locations can transition to and by checking the reachability of it; (ii) or
the trace is infinite and there exists a location v ∈ V S and a point k ≥ 0 such
that l S = v = (A 1 .last, . . . , A n .last), for all the states after k in the trace,
where the i
th component of v together with the time of the current state is a
livelock for automata A i , for some 1 ≤ i ≤ n. The second point is fundamental
for local requirements featuring infinite bounds: in these automata, it is not
sufficient to check for deadlocks, since a timed transition could be always enabled;
instead, an illegal state can be described by a trace of the system that reaches a
livelock whose location has no invariants attached and then stays constantly in
this location. Having reached a livelock, the automaton can proceed only with
timed moves: in particular, it can’t proceed to the next location because its
dependencies are violated. We can check the second point in this way: we first
add a sink location sink
Ai
v for each location v ∈ A i (and of course a transition
from the latter to the former), for each 1 ≤ i ≤ n, and we attach to it the
invariant ¬inv
loc
Ai (v). Now, in the product S of these modified automata, we look
for a trace such that, from a certain time point onwards, it stays constantly in
a location (l 1 , . . . , l n ) such that at least one l i is a sink state. This property can
be formalized in Linear Temporal Logic as F G(
1≤i≤n,v∈Ai sink
Ai
v ).
3.2 Encoding into SMT(DL)
We describe the encoding into SMT(DL) (Satisfiability Modulo Theory of Difference Logic) for the problems of consistency checking and compatibility checking. For all 1 ≤ c ≤ n and 1 ≤ i ≤ |c|, we introduce the following variables:
(i) r
c
i ∈ B represents the fact that phase i of local requirement c is reachable;
(ii) s
c
i = (t
c
i , p
c
i ) represents the superdense time instant in which local requirement c enters phase i, where t
c
i ∈ R and p
c
i ∈ N. We can compare two superdensevalued variables (t, p) and (t
, p
) with the lexicographical order, which we define
as follows: (t, p) (t
, p
) iff t ≤ t
∧ (t = t
→ p ≤ p
). We now give the set of
(conjunctively related) constraints which form our SMT(DL) encoding.
Initialization. Each local requirement starts in its first phase at the same time,
i.e., the real time point 0. Hence, for all 1 ≤ c ≤ n, we add the constraint t
c
0 = 0.
163
on has no constraints on the location variables. The situation is different for
automaton B, for which the transition to on is labelled with 2 ≤ c B ≤ 4 and
c B := 0, and also with ψ on := (l A = on), that is the state dependency of phase
B.on; moreover, ψ on is also an invariant for the second location of automaton
B, since it is a state dependency.
Given a network S := A 1 × · · · × A n of TASVs, the problem of consistency
checking can be expressed as the reachability of location (A 1 .last, . . . , A n .last) ∈
V S . A deadlock of a TASV A is defined as a state (v, t) ∈ V A × R such that A
can take neither a timed nor a discrete transition from (v, t). We call livelock
a state (v, t) such that A can take only timed transitions. The compatibility
checking problem can be expressed as the problem of checking if there exists a
trace of S such that (i) either the trace is finite and its final state is a deadlock
of S; we can check this property by adding a sink location to the TASV S to
which all locations can transition to and by checking the reachability of it; (ii) or
the trace is infinite and there exists a location v ∈ V S and a point k ≥ 0 such
that l S = v = (A 1 .last, . . . , A n .last), for all the states after k in the trace,
where the i
th component of v together with the time of the current state is a
livelock for automata A i , for some 1 ≤ i ≤ n. The second point is fundamental
for local requirements featuring infinite bounds: in these automata, it is not
sufficient to check for deadlocks, since a timed transition could be always enabled;
instead, an illegal state can be described by a trace of the system that reaches a
livelock whose location has no invariants attached and then stays constantly in
this location. Having reached a livelock, the automaton can proceed only with
timed moves: in particular, it can’t proceed to the next location because its
dependencies are violated. We can check the second point in this way: we first
add a sink location sink
Ai
v for each location v ∈ A i (and of course a transition
from the latter to the former), for each 1 ≤ i ≤ n, and we attach to it the
invariant ¬inv
loc
Ai (v). Now, in the product S of these modified automata, we look
for a trace such that, from a certain time point onwards, it stays constantly in
a location (l 1 , . . . , l n ) such that at least one l i is a sink state. This property can
be formalized in Linear Temporal Logic as F G(
1≤i≤n,v∈Ai sink
Ai
v ).
3.2 Encoding into SMT(DL)
We describe the encoding into SMT(DL) (Satisfiability Modulo Theory of Difference Logic) for the problems of consistency checking and compatibility checking. For all 1 ≤ c ≤ n and 1 ≤ i ≤ |c|, we introduce the following variables:
(i) r
c
i ∈ B represents the fact that phase i of local requirement c is reachable;
(ii) s
c
i = (t
c
i , p
c
i ) represents the superdense time instant in which local requirement c enters phase i, where t
c
i ∈ R and p
c
i ∈ N. We can compare two superdensevalued variables (t, p) and (t
, p
) with the lexicographical order, which we define
as follows: (t, p) (t
, p
) iff t ≤ t
∧ (t = t
→ p ≤ p
). We now give the set of
(conjunctively related) constraints which form our SMT(DL) encoding.
Initialization. Each local requirement starts in its first phase at the same time,
i.e., the real time point 0. Hence, for all 1 ≤ c ≤ n, we add the constraint t
c
0 = 0.