Information Technology Reference
In-Depth Information
Then we will check the conditions of extension morphisms according to definition 14:
•
Obviously
σ
γ
is surjective and
σ
α
is injective.
•
There exists a formula
α
, which contains only channels from (V
2
−
σ
α
(V
1
)),
and
α
is satisfiable,
t
I
2
⇔
σ
(I
1
)
∧
α
. As
α
⇔
ac = true, this condition
holds.
For every g
∈
Γ
2
where
σ
γ
(g) is defined,
•
If v
∈
loc(V
1
) and g
∈
D
2
(
σ
α
(v)), then there exists a formula
α
, which con-
tains only primed channels from (V
2
'
−
σ
α
(V
1
)'), and
α
is satisfiable,
t
σ
(L
1
(
σ
γ
(g))) ⇒ (R
2
(g,
σ
α
(v))
⇔
σ
α
(R
1
(
σ
γ
(g), v))
∧
α
) .
o
For action button_confirm,
α
⇔
ac' = false, this condition holds.
o
For action button_cancel,
α
⇔
ac' = true, this condition holds.
o
For action order_ret,
α
⇔
ac' = true, this condition holds.
•
If v
σ
γ
(g)). Since the mappings of
channels and actions are the identity and the actions in P
2
maintain the effect
of assignments to the mapped channels of P
1
, this condition will hold.
∈
loc(V
1
), g
∈
D
2
(
σ
α
(v)), then v
∈
D
1
(
t
(
σ
(L
1
(
σ
γ
(g))) ⇒ L
2
(g)). For each action button_select(id: int), bt_g ⇒ bt_g
∨
ac.
σ
γ
(g))) ⇒ U
2
(g)). The progress guards of each mapped action are the same.
t
(
σ
(U
1
(
Lemma 2.
The new functional requirement cannot be achieved by regulating or refin-
ing the controller component.
Proof
The enabling guards of these button_select actions cannot be strengthened because, in
that case, all the buttons will be disabled after the customer selects one item button.
The justification for this statement is as follows:
Suppose we have regulated or refined the controller component, then, in the target
component, the enabling guards of the button_select actions will be strengthened; say
one of the actions is g, its enabling guard is f and f ⇒
(bt_g) (bt_g must be trans-
lated). According to the definition of regulative superposition and refinement mor-
phism, we have R
2
(g,
σ
σ
γ
(g), bt_g)). Since bt_g is set to false after
the button_select action is called in the old controller, we know that
σ
(bt_g)) ⇒
σ
(R
1
(
(bt_g) should
also be set to false after the execution of g in the extended controller. Because we
have f ⇒
σ
(bt_g)' is false, we know f' must
be false. Therefore, after the button_select action is executed in the target component,
this action will be blocked, which means this item button is disabled.
σ
(bt_g) and it should hold all the time, if
σ
3.3.2 The Extension of Payment Options
We expect that instead of only accepting payment consisting of nickels, dimes, quar-
ters and loonies, the vending machine system can also accept payment including one
cent pieces and make the correct change. It is clear that we cannot refine or regulate
component slot to achieve this goal, because we must modify its action get_pay and
relax its enabling guard, which is not allowed in regulative superpositions and refine-
ment morphisms. Therefore, we have to apply an extension morphism to the slot by
modifying the get_pay action as follows and obtain the extended slot component.
Search WWH ::
Custom Search