Safe Decomposition of Startup Requirements
165
where
VIOLATION(¯ s) := ¬φ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ ¯
s s
d
j+1 )] ∨
(3)
¬ψ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ ¯
s)] ∨
(4)
∃ s(s
c
i−1
s ¯
s ∧ ¬ψ
c
i−1 [(d, j) → (r
d
j ∧ s
d
j ≺
s s
d
j+1 )]) (5)
We interpret ¯
s s
c
i−1 + u
c
i as ∀¯ p(¯ s s
c
i−1 + (u
c
i , ¯
p)) and the + symbol as the
pairwise sum. In the case the upperbound of the transition is infinite, we simply
do not add the ¯
s s
c
i−1 + u
c
i inequality. We refer to the conjunction of all these
constraints as W.
For consistency checking, we define END :=
1≤c≤n
r |c| and we call W
cons the
conjunction of W with END. We check consistency by checking the satisfiability
of W
cons .
For compatibility checking, we define ILL :=
1≤c≤n
1≤i≤|c|
¬r
c
i and we call W
ill the
conjunction of W with ILL. We check the existence of an illegal state in the
system by checking the satisfiability of W
ill , i.e., W
ill is satisfiable iff the local
requirements are not compatible.
Strict Semantics In the strict semantics setting, we forbid two events to occur at
the same real-time point. For strict semantics, the encoding is equal to W except
that we interpret ≺ and as < and ≤, respectively, and all the s
c
i variables as
single real-valued variables t
c
i ∈ R. We call S this encoding and we define S
cons
and S
ill as above.
Finite bounds and convex dependencies. Despite being very close to the problem formalization, the W encoding features a high number of quantifications,
also in alternation; therefore, in the general case, it is very burdensome for an
SMT solver to first perform quantifier elimination on W and then to solve the
resulting formula. Nevertheless, if we make some restrictions on the type of local
requirements we consider, we are able to remove upfront all the quantifiers from
W, without the need to use quantifier elimination techniques. In fact, suppose
we consider only local requirements with finite bounds and convex state dependencies (see Sec. 2). We call
W ill
fin the encoding equal to W except that Eq. (1)
is replaced by:
r
c
i → ψ
c
i−1 [(d, j) → (r
d
j ∧ s
c
i s
d
j+1 )]
(6)
and we add the following constraint:
(r
c
i−1 ∧ ¬r
c
i ) → (t
c
i = t
c
i−1 + u
c
i−1 )
(7)
and we replace Eq. (2) with:
(r
c
i−1 ∧ ¬r
c
i ) → WEAKVIOL(t
c
i )
(8)
165
where
VIOLATION(¯ s) := ¬φ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ ¯
s s
d
j+1 )] ∨
(3)
¬ψ
c
i [(d, j) → (r
d
j ∧ s
d
j ≺ ¯
s)] ∨
(4)
∃ s(s
c
i−1
s ¯
s ∧ ¬ψ
c
i−1 [(d, j) → (r
d
j ∧ s
d
j ≺
s s
d
j+1 )]) (5)
We interpret ¯
s s
c
i−1 + u
c
i as ∀¯ p(¯ s s
c
i−1 + (u
c
i , ¯
p)) and the + symbol as the
pairwise sum. In the case the upperbound of the transition is infinite, we simply
do not add the ¯
s s
c
i−1 + u
c
i inequality. We refer to the conjunction of all these
constraints as W.
For consistency checking, we define END :=
1≤c≤n
r |c| and we call W
cons the
conjunction of W with END. We check consistency by checking the satisfiability
of W
cons .
For compatibility checking, we define ILL :=
1≤c≤n
1≤i≤|c|
¬r
c
i and we call W
ill the
conjunction of W with ILL. We check the existence of an illegal state in the
system by checking the satisfiability of W
ill , i.e., W
ill is satisfiable iff the local
requirements are not compatible.
Strict Semantics In the strict semantics setting, we forbid two events to occur at
the same real-time point. For strict semantics, the encoding is equal to W except
that we interpret ≺ and as < and ≤, respectively, and all the s
c
i variables as
single real-valued variables t
c
i ∈ R. We call S this encoding and we define S
cons
and S
ill as above.
Finite bounds and convex dependencies. Despite being very close to the problem formalization, the W encoding features a high number of quantifications,
also in alternation; therefore, in the general case, it is very burdensome for an
SMT solver to first perform quantifier elimination on W and then to solve the
resulting formula. Nevertheless, if we make some restrictions on the type of local
requirements we consider, we are able to remove upfront all the quantifiers from
W, without the need to use quantifier elimination techniques. In fact, suppose
we consider only local requirements with finite bounds and convex state dependencies (see Sec. 2). We call
W ill
fin the encoding equal to W except that Eq. (1)
is replaced by:
r
c
i → ψ
c
i−1 [(d, j) → (r
d
j ∧ s
c
i s
d
j+1 )]
(6)
and we add the following constraint:
(r
c
i−1 ∧ ¬r
c
i ) → (t
c
i = t
c
i−1 + u
c
i−1 )
(7)
and we replace Eq. (2) with:
(r
c
i−1 ∧ ¬r
c
i ) → WEAKVIOL(t
c
i )
(8)