of 18
Contracts of Reactivity
?
Tung Phan-Minh
1
and Richard M. Murray
2
1
Department of Mechanical Engineering
tung@caltech.edu
2
Department of Control and Dynamical Systems
California Institute of Technology, Pasadena CA 91125, USA
Abstract.
We present a theory of contracts that is centered around
reacting to failures and explore it from a general assume-guarantee per-
spective as well as from a concrete context of automated synthesis from
linear temporal logic (LTL) specifications, all of which are compliant
with a contract metatheory introduced by Benveniste et al. We also
show how to obtain an automated procedure for synthesizing reactive
assume-guarantee contracts and implementations that capture ideas like
optimality and robustness based on assume-guarantee lattices computed
from antitone Galois connection fixpoints. Lastly, we provide an example
of a “reactive GR(1)” contract and a simulation of its implementation.
Keywords:
Design by contracts
·
Modeling uncertainties
·
Formal spec-
ifications
·
Reactive synthesis.
1 Introduction
Automating correctness and improving productivity motivate the development
of formal contracts in the compositional design of large and complex engineer-
ing systems (e.g., [20]). Abstractly speaking, a contract [5] is a su
ciently un-
ambiguous specification of a system that allows for a certain level of freedom
5
in
implementation
. Considering the collaborative nature of modern design and
manufacturing, a contract must also clearly describe the requirements of the
en-
vironment
that the system being specified is intended to operate in so that when
the system and its environment are
interconnected
, i.e., allowed to interact, the
desired behavior materializes.
10
A premise central to the field of formal methods is the idea that the mathe-
matical model being verified is the “right” abstraction of the system in question.
Oftentimes, especially for physical systems, this is not the case since the added
details would make the model too large to be verified e
ciently, if at all [13].
Model uncertainties, environmental disturbances, simplifying assumptions etc.
15
must be accounted for separately, often using heuristics. In the reactive syn-
thesis setting [6], attempts have been made to automatically generate systems
that satisfy specifications with some measure of robustness to certain classes of
?
Supported by DENSO International America, Inc., the Jack Kent Cooke Foundation,
and the NSF VeHICaL project.
Submitted, Int'l Conf on Formal Modeling and Analysis of Timed Systems (FORMATS) 2019
http://www.cds.caltech.edu/~murray/preprints/pm19-formats_s.pdf
2
T. Phan-Minh and R. M. Murray
uncertainties. For instance, [17] exploits “locality” to compute modal
μ
-calculus
fixpoints [3] that enable patching system strategies in the presence of updated in-
20
formation about the game graph. Similarly, [10] discusses a way to recover from
a finite number of unexpected actuation or sensing errors with pre-computed
safe strategies that attempt to bring the system back to the nominal control tra-
jectory. In addition to making specific assumptions on the environment, these
methods also rely on the fact that such recovery strategies are always feasible
25
for the original set of objectives. On the specification side of things, [4] repre-
sents an elementary and direct means to add “reparation” handling to contract
automata. Unfortunately, the obligation to define contract states and transitions
explicitly does not make the automaton approach amenable to expressing and
extracting complex properties.
30
Consider a standard
assume-guarantee
style design specification
'
S
for a
parking garage system
S
operated by robot valets of the form
'
S
:
=
A
)
G
(see [24] for a concrete specification in TLA
+
), where
A
encodes a set of input
constraints or
assumptions
such as garage topology, quantity of the valets, as
well as their quality, such as how fast they can park and retrieve cars, and
G
35
consists of
guarantees
the system must provide in the event that the constraints
in
A
are satisfied, such as an upper bound on the maximum wait times for
customers. Under this assume-guarantee framework, any system that satisfies
the requirement
unless a constraint in
A
is violated, all guarantees in
G
are provided
40
is said to implement the contract. We argue that this formalism often results in
a system that is
1.
fragile
: this contract is not robust to disturbances: if a car runs out of fuel
and thereby invalidates the assumption on the performance of the valet as-
signed to it, are other valets suddenly allowed to indiscriminately or even
45
completely abandon their responsibilities? According to
'
S
, the answer is
yes even though the “intuitively correct” answer is that they should not.
2.
underpromising
: the guarantee must often be very conservative when it must
hold against the worst case assumptions as well the most forgiving ones:
consider an abnormally slow valet biasing the guaranteed worst wait time.
50
3.
maladaptive
: since there is only one assumption and guarantee pair (
A, G
),
it is not possible to adapt to changes in
A
nor to update guarantees in
G
.
Even if more pairs are allowed, there is no clear procedure on how to specify
controlling or switching between specific assumptions and guarantees when
such an opportunity arises.
55
To address these issues, we propose a contract formalism that explicitly takes into
account the notion of uncertainty in the system being modelled and emphasizes
its obligation to adapt to possible changes in the behavior of the environment.
The structure of the paper is as follows: in the first part of Section 2, a standard
formal definition of assume-guarantee contracts is given as a point of reference.
60
In the second part of Section 2, the idea of “generative e
ects” is introduced and
Contracts of Reactivity
3
used to motivate our framework. In Section 3, our theory of reactive contracts
is presented and contrasted with the non-reactive formalism. In Section 4, we
specialize this theory to the context of GR(1) games and derive a procedure
for formulating and synthesizing their reactive contracts. In Section 5, we apply
65
results from Section 4 to a concrete example/simulation and explore the notion
of optimality and robustness.
2 Contracts and E
ects
2.1 Assume-guarantee contracts
For the sake of conciseness, we will only cover assume-guarantee contracts de-
70
fined over a common set of Boolean variables
V
called the
alphabet
.Onewill
see that a more detailed variant with local alphabets where a variable can also
be labelled either as input or output is indeed more expressive (e.g., the notion
of closedness/openness can be directly defined) but not required to introduce
the notion of reactivity. For any set
X
,let
X
!
be the set of infinite sequences
75
generated from
X
, namely
{
h
x
i
i
1
i
=0
|
x
i
2
X
}
,
X
be the free monoid on
X
,
and 2
X
be the powerset of
X
.Define
X
1
as
X
[
X
!
. In accordance with the
metatheory presented in [5], which will, from this point on, be referred to as
“the metatheory”, we term any pair of collections of
environments
and
imple-
mentations
a contract. The theory of assume-guarantee contracts is a model of
80
this metatheory and can be described as follows.
Definition 1 (Behaviors and Assertions).
A behavior
is an element of
B
:
=(2
V
)
!
. An assertion
A
is a subset of
B
, namely,
A
2
2
B
.
We lift the set of all assertions 2
B
to a Boolean algebra by defining a unary
operator
¬
and two binary operators
^
,
_
on it in the standard way: if
A, A
1
,A
2
85
are assertions, then
¬
A
:
=
B\
A
,
A
1
_
A
2
:
=
A
1
[
A
2
,
A
1
^
A
2
:
=
A
1
\
A
2
.
The induced partial ordering relation
on 2
B
is simply the subset relation
. Additionally, we define the secondary binary operator
)
in
A
1
)
A
2
as a
shorthand for
¬
A
1
_
A
2
.
A
component
M
is an assertion designated as such. Usually, the assertion
90
characterizing a component is restricted to a subset of
V
, which can be thought
of as input/output variables associated with that component. This is due to the
fact that most components are intended to be interconnected with others. If
M
1
and
M
2
are components, the
interconnection
binary operator
is defined by
M
1
M
2
:
=
M
1
^
M
2
. It is clear that
is commutative and associative, and
95
that the set of all components is closed under it. We note that depending on how
the variables and assertions making up the components being interconnected are
defined,
can assume the meaning of either a parallel, series, coproduct, or feed-
back connection [8]. In fact, the definition of contracts (and the corresponding
algebra) restricts components satisfying them in a way that renders transparent
100
the meaning of their interconnection.
4
T. Phan-Minh and R. M. Murray
Definition 2 (Contracts).
An assume-guarantee contract
C
is a pair of as-
sertions
(
A, G
)
, called the assumption and the guarantee respectively. The set of
environments of
C
, denoted by
E
C
, captures all components
E
such that
E
A
(1)
105
In other words,
E
C
=2
A
. The set of implementations of
C
, denoted by
M
C
,
consists of all components
M
such that
8
E
2
E
C
.M
E
G
(2)
Example 1.
Let
V
=
{
x, y
}
and
C
=(
A, G
)where
A
:
=
{
|
x
2
i
,
i
mod 2
6
=
0
}
and
G
:
=
{
|
y
2
i
,
i
mod 2 = 0
}
. Let
1
:
=
h
{
y
}
,
{
x
}
,
?
,
{
x
}
,
?
,...
i
and
110
2
:
=
h
{
y
}
,
{
x
}
,
{
y
}
,
{
x
}
,...
i
.If
E
:
=
{
1
,
2
}
then
E
2
E
C
because
1
,
2
2
A
.
Let
M
1
:
=
{
1
}
and
M
2
:
=
{
2
}
.Then
M
1
62
M
C
because
M
1
E
=
{
1
}
62
G
.
However, one can check that
M
2
2
M
C
. Note that if
M
3
:
=
?
,then
M
3
2
M
C
as
well. The interpretation here is that
M
3
satisfies the assume-guarantee semantics
of
C
vacuously.
115
Since 2
B
is a Boolean algebra (and hence a Heyting algebra [7]), we infer from
inequality (2) and the definition of
that
8
E
2
E
C
.M
¬
E
_
G
. Choosing
E
=
A
in inequality (1) gives
M
¬
A
_
G
. The converse is also true because
¬
E
_
G
is antitone in
E
.Thus,wehaveshown
Proposition 1.
Given
C
=(
A, G
)
, a component
M
satisfies
M
2
M
C
if and
120
only if
M
A
)
G
(3)
Proposition 1 characterizes implementations
M
of
C
as those components whose
behaviors either do not conform to the behaviors specified in
A
or are compatible
with
G
. Specifically, it says that
M
C
=2
A
)
G
.Since
125
A
)
(
A
)
G
)=
¬
A
_
(
¬
A
_
G
)=
¬
A
_
G
=
A
)
G,
(4)
inequalities (1) and (3) yield
Proposition 2.
If
C
=(
A, G
)
and
C
=(
A, A
)
G
)
, then
M
C
=
M
C
and
E
C
=
E
C
.
It may be seen from equation (4) why any assume-guarantee contract of the
130
form
C
=(
A, A
)
G
) is called
saturated
. By the metatheory, we will consider
contracts that have the same sets of environments and implementations to be
equal, and so by Proposition 2, every contract
C
has a unique saturated
canonical
form
C
. This saturated form is often convenient to use when doing contract
algebra. In particular, it can also shed light on the meaning of the conjunction
135
operation, which motivates our development of “reactive contracts”. To describe
the conjunction, we will need the idea of contract refinement.
Definition 3.
We say contract
C
1
=(
A
1
,G
1
)
refines a contract
C
2
=(
A
2
,G
2
)
and write
C
1
C
2
if
M
C
1
M
C
2
and
E
C
2
E
C
1
.
Contracts of Reactivity
5
Clearly,
is a binary relation that is reflexive and transitive and hence is a
140
preorder for the set of all contracts on
B
. Again, since any two contracts that
have the same sets of environments and implementations are considered equal,
is a partial order. The
conjunction
of two contracts
C
1
and
C
2
, denoted by
C
1
^
C
2
, is a contract that is their largest common lower bound (or meet) with
respect to
. Formally,
C
1
^
C
2
:
=sup
{C|C
C
1
^
C
C
2
}
. For any contract
C
,
145
we have
E
C
=2
A
and
M
C
=2
A
)
G
. Therefore, if
C
C
1
,
C
2
, then by Definition 3,
M
C
M
C
1
\
M
C
2
=2
A
1
)
G
1
\
2
A
2
)
G
2
=2
(
A
1
)
G
1
)
^
(
A
2
)
G
2
)
and 2
A
1
_
A
2
=2
A
1
[
2
A
2
=
E
C
1
[
E
C
2
E
C
(since the intersection/union of powersets of two sets is the
powerset of their intersection/union). By the fact that (
A
1
)
G
1
)
^
(
A
2
)
G
2
)
is saturated, we have
C
1
^
C
2
=(
A
1
_
A
2
,
(
A
1
)
G
1
)
^
(
A
2
)
G
2
)). By induction,
150
one can show the following
Proposition 3.
If for
i
=1
,
2
,...,n
,
C
i
are assume-guarantee contracts, then
^
n
i
=1
C
i
=(
_
n
i
=1
A
i
,
^
n
i
=1
A
i
)
G
i
)
(5)
Note that we can apply an analogous argument to the disjunction of contracts
(defined as their join) to conclude that the set of all saturated contracts forms a
155
complete lattice. Equation (5) shows that the “parametric contract” formalism
given in [15] is exactly the result of applying the conjunction operation to the
constituent contracts. That is, if
M
is an implementation of the conjunction
^
i
C
i
containing
such that
2
E
where
E
is an environment of
^
i
C
i
,then
there exists at least a
k
2
{
1
,
2
,...,n
}
such that
2
A
k
and for all such
k
,
160
2
G
k
. In other words, for any behavior
in which the environment satisfies
any assumption
A
k
in
{
A
1
,A
2
,...,A
n
}
,thesystemmust
react
by providing
the corresponding guarantee
G
k
. Thus in contract conjunctions, 1) the reactions
are defined by pairing each
A
k
with the corresponding
G
k
and 2)
A
k
)
G
k
must hold over the sequence
in its entirety. The second restriction is partially
165
relaxed in the “dynamic contract” formalism, used for instance in [16], where
assumptions are allowed to change over fixed time intervals. Our reactive contract
framework will 1) remove the one-to-one restriction to allow for a more flexible
assumption-guarantee pairing process, 2) enforces
immediate
guarantee reactions
to assumption changes
directly
on each element
2
B
, and 3) enables automated
170
synthesis. To motivate this development, we will briefly go over the idea of
generative e
ects.
2.2 Generative e
ects
The principle of semantic compositionality states that “the meaning of an ex-
pression is a function of the meanings of its parts” [22]. One may attempt to
175
interpret this view in the context of system engineering when they replace “ex-
pressions” with “systems” and “meanings” with “properties”. Let
S
be the space
of systems,
:
S
S
!
S
be a system-valued infix operator termed
intercon-
nection
,
C
be the set of
all properties
, and
C
S
:
=
{
|
:
S
!
C
}
consisting
of functions mapping each system to a property it satisfies. In general, given
180
2
C
S
and
, it would be helpful if we can find a binary operation + such that
6
T. Phan-Minh and R. M. Murray
(
S
1
S
2
)=
(
S
1
)+
(
S
2
). Sometimes, for the right classes of systems, prop-
erties, and interconnections, such a + operator does, in fact, exist. For example,
+ can be constructed from a multiplication operation followed by a comparison
operation for dynamical systems characterized by the notation of “finite-gain
L
185
stability” that are interconnected by feedback [14]. Sources of failures to capture
such a + operator may also arise from to poor choice of
, inexact modelling,
lack of observability, mechanical fatigue etc. For example, consider a game in
which two fair coins
c
1
and
c
2
are tossed independently and a reward is given
every time both come up the same (both heads or both tails) and let
be the
190
property: there is a “pattern” for winning. Then if we only observe
c
1
or
c
2
separately, because the coins are fair, there is no “pattern”.
Generative e
ects
are properties resulting from interactions of composed sys-
tems that cannot be
explained
by observing individual components [1]. For en-
gineering systems, it makes sense to safeguard against the unpredictability of
195
these e
ects with
contingency planning
as opposed to simply relying on cer-
tain assumptions to hold and blaming the environment when they do not. Our
metatheory-compliant formulation of reactive contracts will formalize this idea.
3 Reactive Contracts
3.1 Reactivity
200
Let
B
be as before. For each
2
B
and
i, j
2
N
:0
i<j
, we denote
by
i
!
j
the subsequence of
spanning from
i
up to
but not including
j
,
namely
h
i
i
j
1
k
=
i
, and by
i
!1
the infinite sequence
h
k
i
1
k
=
i
. For
A
B
and
k
0, denote by Pref
k
(
A
) the set of all prefixes of behaviors in
A
of length
k
,
Pref
k
(
A
)
:
=
{
0
!
k
|
2
A
}
and Pref(
A
)
:
=
[
1
k
=0
Pref
k
(
A
), the set of all prefixes
205
of
A
. Let
·
be the
sequence concatenation
operation mapping from (Pref(
B
)
Pref(
B
))
[
(Pref(
B
)
B
)toPref(
B
)
[
B
defined in the obvious way.
Definition 4 (Witness).
Let
2
B
,A
B
and
i, j
2
N
0
[
{
1
}
:
i<j
.
We say that
is a witness for
A
from
i
up until
j
and write
|
=
i
!
j
A
if
i
!
j
2
Pref
(
A
)
[
A
.If
j
6
=
1
, we consider the witness relation as being strict
210
and write
|
=
s
i
!
j
A
if
|
=
i
!
j
A
but
6
|
=
i
!
j
+1
A
.If
j
=
1
, the witness relation
is always strict.
To describe and keep track of assumption changes, we appeal to the notion of
assigning
signatures
(or labels) to each behavior that undergoes those changes.
Definition 5 (Signature).
Given a set of assertions
A
2
B
,an
A
-signature
215
is any nonempty sequence
=
h
k
i
m
k
=0
2
A
1
where
m
2
N
>
0
[
{
1
}
.If
m<
1
,
we say
2
B
is a witness for
and put
|
=
if there exists a partitioning
sequence
h
i
k
i
m
k
=0
in
N
0
satisfying
0=
i
0
<i
1
<...<i
m
such that with
i
m
+1
:
=
1
, we have
8
k
2
{
0
,
1
,...,m
}
.
|
=
i
k
!
i
k
+1
k
.
(6)
220
Contracts of Reactivity
7
We say that
is a strict witness for the signature
and write
|
=
s
if the
witness relation in equation
(6)
is strict. Analogously, if
m
=
1
, then
|
=
if
there exists a (strictly monotone) partitioning sequence
h
i
k
i
1
k
=0
in
N
0
satisfy-
ing
i
0
=0
and equation
(6)
with
{
0
,
1
,...,m
}
replaced by
N
0
.
In general, a given
2
B
may be a strict witness for more than one signature
225
in
A
1
. For example, if
A
=
{
A
1
,A
2
}
where
A
1
\
A
2
6
=
?
, then any behavior
2
A
1
\
A
2
satisfies
|
=
s
h
A
j
i
for
j
2
{
1
,
2
}
. This may still be the case even
when
A
1
\
A
2
=
?
. For
V
=
{
x, y
}
.
A
1
=
{{
x
}}
!
and
A
2
=
{{
y
}}
!
[
{
}
where
satisfies
k
=
{
x
}
for
k
= 0 and
k
=
{
y
}
, otherwise. Then
|
=
s
h
A
1
,A
2
i
and
|
=
s
h
A
2
i
. This non-uniqueness makes it unclear as to which assumption
230
change sequence should be considered and how/when to properly react to it.
Being able to restrict the set of assumptions so that this does not happen is
necessary because in order to react at all, the system must be able to know which
assumption to operate under next. The following proposition gives a su
cient
condition.
235
Proposition 4.
Let
A
be a collection of assertions, then
8
2
A
1
.
8
2
B
.
|
=
s
)
(
8
2
A
1
.
|
=
s
)
=
)
(7)
if
8
A
1
,A
2
2
A
.A
1
6
=
A
2
)
Pref
1
(
A
1
)
\
Pref
1
(
A
2
)=
?
.
(8)
Proof.
Assume that
A
satisfies (8). Let
,
2
A
1
and
2
B
be such that
|
=
s
and
|
=
s
. Let
m
2
N
[
{
1
}
be the length of
. By the fact that
0
2
Pref
1
(
0
)
\
Pref
1
(
0
) and
8
A
2
A
.A
6
=
0
)
Pref
1
(
A
)
\
Pref
1
(
0
)=
?
,
we conclude
0
=
0
. Suppose that up to
n<m
,
k
=
k
for all
k
satisfying
0
k
n
. We will show that
n
+1
and
n
+1
are defined and equal to one
another. Indeed, since
n<m
,the(
n
+ 1)
th
term of
,
n
+1
, exists. Let
h
i
k
i
m
k
=0
be a partitioning sequence for
|
=
s
given by Definition 5. By strictness and the
induction hypothesis, we have
i
n
!
(
i
n
+1
+1)
6
|
=
n
=
n
.Since
|
=
s
, it follows
that
n
+1
exists as well. From
|
=
s
,if
n
+2
m
,wehave
|
=
s
i
n
+1
!
i
n
+2
n
+1
and, in particular,
i
n
+1
2
Pref
1
(
n
+1
)
\
Pref
1
(
n
+1
), which by (8) yields
n
+1
=
n
+1
.If
n
+2
>m
,then
|
=
s
i
n
+1
!1
n
+1
, arguing similarly, we arrive
at the additional conclusion that
also has length
m
. This implies (7).
ut
Any
A
that satisfies (8) is called
initially disjoint
. Hence, Proposition 4 says that
240
if
A
is a set of assertions that are initially disjoint then any behavior is a strict
witness for at most one
A
-signature. Let
B
A
:
=
{
2
B|
9
2
A
1
.
|
=
s
}
,the
set of behaviors that have
A
-signatures. If
A
is initially disjoint, then the function
U
A
:
B
A
!
A
1
mapping each
2
B
A
to the unique signature
U
A
(
)
2
A
1
for which it is a witness is well-defined. Finally, for any
M
B
A
, we denote by
245
U
A
(
M
) the set of signatures generated by
M
, namely,
{U
A
(
)
|
2
M
}
.
3.2 Contracts
Definition 6 (Reactive contracts).
A reactive assume-guarantee contract
C
is a 4-tuple
(
A
,
G
,
,R
)
such that
8
T. Phan-Minh and R. M. Murray
1.
A
,
G
2
B
are called the assumption and guarantee sets respectively.
A
is
250
required to be initially disjoint.
2.
A
1
is called the contingency set, consisting of assumption change sce-
narios that may happen.
3.
R
(
A
G
)
1
is called the reaction set.
Observe that
A
and
G
are not necessarily of the same cardinality and that
255
from each
r
2
R
, we can obtain an unique
A
-signature by “projecting away the
G
dimension”. We denote the projection function by
A
:
R
!
A
1
so that
A
(
h
A
k
,G
k
i
m
k
=0
)
:
=
h
A
k
i
m
k
=0
for any
h
A
k
,G
k
i
m
k
=0
2
R
.
Definition 7 (Environment).
An environment for a reactive contract
C
=
(
A
,
G
,
,R
)
is any
E
B
A
such that
U
A
(
E
)
, namely each
2
E
is a strict
260
witness for some
A
-signature in
.
Thus, for a reactive contract, assumptions about its environment’s behaviors
are allowed to change according to the contingency specified in
. As these
assumptions change, the system should provide the corresponding guarantees as
specified by the reaction set
R
. We characterize
R
via the following definitions.
265
Definition 8 (Reactive satisfaction).
Let
2
B
,
r
=
h
(
A
k
,G
k
)
i
m
k
=0
2
R
,we
say that
reactively satisfies
r
and write
|
=
r
if the following hold
1.
|
=
s
A
(
r
)
with the partitioning sequence
h
i
k
i
m
k
=0
.
2. (a) If
m<
1
, then
8
k
2
{
0
,
1
,...,m
}
.
i
k
!
i
k
+1
|
=
G
k
with
i
m
+1
:
=
1
.
(b) otherwise,
8
k
2
N
0
.
i
k
!
i
k
+1
|
=
G
k
.
270
Definition 9 (Implementation).
An implementation of a reactive contract
C
=(
A
,
G
,
,R
)
is any
M
B
such that for any environment
E
of
C
, we have
8
2
(
M
\
E
)
.
9
r
2
R.
|
=
r
^
A
(
r
)=
U
A
(
)
.
Intuitively, an implementation consists of all behaviors
in which either the
assumptions do not change according to
,i.e.,
U
A
(
)
62
, or the system reacts
275
according to instructions specified by the set
R
, namely there exists a reaction
r
2
R
, such that
reactively satisfies
r
,inwhichthesystemtriesitsbestto
satisfy the guarantee corresponding to the current assumption for as long as the
latter holds and is required to immediately adapt to any new assumption and
commit itself to the new obligation. Let us compare this machinery to “standard”
280
assume-guarantee contracts. First, we mention that the following holds.
Proposition 5.
Corresponding to each any standard assume-guarantee contract
C
=(
A, G
)
is a reactive assume-guarantee contract
C
r
=(
A
,
G
,
,R
)
with
A
=
{
A
}
,
G
=
{
G
}
,
=
{
h
A
i
}
and
R
=
{
h
(
A, G
)
i
}
such that
C
=
C
r
in the sense
that they have same sets of environments and implementations.
285
Recall that any parametric assume-guarantee contract is simply the conjunction
of a set of “standard” assume-guarantee contracts (which is again a standard
assume-guarantee contract) by Proposition 5, there is a reactive version for it.
In particular, when all assumptions are initially disjoint, we have the following
the generalization of Proposition 5.
290
Contracts of Reactivity
9
Proposition 6.
If
n
1
,
{
A
1
,A
2
,...,A
n
}
is a set of initially disjoint asser-
tions and for
i
2
{
1
,
2
,...,n
}
,
C
i
=(
A
i
,G
i
)
are assume-guarantee contracts,
then there exists a reactive assume-guarantee contract
C
r
such that
^
n
i
=1
C
=
C
r
.
Proof.
Let
C
r
=(
A
,
G
,
,R
)bedefinedwith
A
:
=
{
A
1
,A
2
,...,A
n
}
295
G
:
=
{
G
1
,G
2
,...,G
n
}
:
=
{
h
A
1
i
,
h
A
2
i
,...,
h
A
n
i
}
R
:
=
{
h
(
A
1
,G
1
)
i
,
h
(
A
2
,G
2
)
i
,...,
h
(
A
n
,G
n
)
i
}
Then,
E
2
E
C
if and only if
,8
2
E.
2_
n
i
=1
A
i
,8
2
E.
9
i
2
{
1
,
2
,...,n
}
.
2
A
i
,8
2
E.
9
i
2
{
1
,
2
,...,n
}
.
U
A
(
)=
h
A
i
i✓
which holds if and only if
E
2
E
C
r
. Also,
M
2
M
C
,8
2
M.
2^
n
i
=1
(
A
i
)
G
i
). Since the
A
i
’s are initially disjoint, and therefore disjoint, there are two
cases: either
2^
n
i
=1
¬
A
i
, in which case
U
A
(
)
62
, or there is an
A
i
such that
2
A
i
^
G
i
, in which case,
|
=
h
(
A
i
,G
i
)
i
and
U
A
(
)=
A
(
h
(
A
i
,G
i
)
i
)=
h
A
i
i
.
This implies
M
2
M
C
r
. On the other hand,
M
2
M
C
r
implies
8
2
M
,either
|
=
h
(
A
i
,G
i
)
i
for some
i
2
{
1
,
2
,...,n
}
, which by Definition 8, implies that
2
A
i
^
G
i
, or
U
A
(
)
62
, which implies that
2^
n
i
=1
¬
A
i
.
ut
The following example shows the greater flexibility o
ered by reactive con-
tracts over parametric ones.
300
Example 2.
Let
A
1
,A
2
be initially disjoint and
C
=(
A
1
_
A
2
,
(
A
1
)
G
1
)
^
(
A
2
)
G
2
) and
̃
C
r
=(
̃
A
,
̃
G
,
̃
,
̃
R
)where
̃
A
=
{
A
1
,A
2
}
,
̃
G
=
{
G
1
,G
2
}
,
̃
=
{
h
A
1
i
,
h
A
2
i
,
h
A
1
,A
2
i
}
,
̃
R
=
{
h
(
A
1
,G
1
)
i
,
h
(
A
2
,G
2
)
i
,
h
(
A
1
,G
1
)
,
(
A
2
,G
2
)
i
}
. We can
see
̃
C
r
C
from the fact that by Proposition 6,
C
=
C
r
=(
A
,
G
,
,R
)where
A
=
̃
A
,
G
=
̃
G
,
=
{
h
A
1
i
,
h
A
2
i
}
, and
R
=
{
h
(
A
1
,G
1
)
i
,
h
(
A
2
,G
2
)
i
}
.With
305
the inclusion of
h
(
A
1
,G
1
)
,
(
A
2
,G
2
)
i
in
̃
R
,
̃
C
r
is receptive to environments whose
behaviors exhibit a change in assumptions from
A
1
to
A
2
and requires imple-
mentations to adapt accordingly by changing their guarantee from
G
1
to
G
2
.On
the other hand,
C
r
only specifies the set of implementations to be those behaviors
in which either neither
A
1
or
A
2
is satisfied or at least a pair (
A
i
,G
i
) is always
310
satisfied.
In a similar manner to standard assume-guarantee contracts, we can talk about
the (saturated) canonical form of reactive assume-guarantee contracts. First, let
R
,
(
A
G
)
1
, the set of all (
A
G
)-signatures and
)
R
:
=
{
r
|
r
2
R
^
A
(
r
)
62
}
[
R
, the set of all (
A
G
)-signatures that are either a reaction
315
in
R
or have an assumption change sequence not specified in the contingency
.
The proof of the following proposition is given in the appendix.
Proposition 7.
If
C
=(
A
,
G
,
,R
)
is a reactive contract, then the canonical
form of
C
defined as
C
?
:
=(
A
,
G
,
,
)
R
)
satisfies
C
?
=
C
.