Information Technology Reference
In-Depth Information
S-TLA Inconsistency:
We define an S-TLA inconsistency as a predicate con-
taining constrained variables, constants, and constants operators [9]. Informally,
an inconsistency denotes a combination of hypotheses that must not be observed
inside a system behavior. Semantically it is true or false for a state. If it is true
for a state
t
, then the system transition on the way to that state should not be
followed. Hereinafter, we denote an S-TLA inconsistency using the symbol
⊥
.
S-TLA Action and Hypothesis:
An S-TLA action is a conjunct between two
expressions. The former is optional, of type boolean, denotes some hypotheses,
and contains assumed and non-assumed variables. The latter is the old TLA
action containing primed and unprimed variables. Semantically, given an incon-
sistency
⊥
,
an S-TLA action
A
is true for a pair of states
s, t
iff,
V
F
:
s
(
v
)
/v, t
(
v
)
/v
)=
true
: By replacing each unprimed flexible
variable in action
-
A
(
∀
v
∈
by
s
(
v
); the value of
v
in state
s
, and each primed
flexible one by
t
(
v
), the boolean resultant expression equals true.
A
V
C
:
s
(
v
)
/v, t
(
v
)
/v
)=
true
: By replacing each non-assumed con-
strained variable
v
in the action
-
A
(
∀
v
∈
by
s
(
v
) and each assumed constrained
one
v
by
t
(
v
), the boolean resultant expression equals true.
A
-
∀
:
s
(
v
)
/v
=
t
(
v
)
/v
: The set of constrained variables
whose values have been stated by a hypothesis (e.g. different from
v
∈
V
c
/ s
(
v
)
=
∇
)some-
where before, retain the same value in state
s
and
t
.
-
⊥
(
t
)=
false
: The predicate
⊥
must not hold in the state
t
,thatis(
t
⊥
).
S-TLA Specification Formula:
We introduce the predicate
IsTrue
A
(
⊥
)tobe
equal true if and only if
⊥
is true further to the execution of action
A
. We define
NI
v
(
N
,
⊥
)
, No Inconsistency
on action
N
as: NI
v
(
N
,
⊥
)
≡
enabled
N∧
¬
IsTrue
N
(
⊥
)
⇒N
v
to states: if action
N
is enabled and if its execution does
not let inconsistency
occurs. We define
φ
as the
system specification formula that generates an infinite behavior
=
⊥
equal true, then action
N
s
0
, s
1
, s
2
, ...
(denoting the system progression) where no inconsistency
⊥
is holding in any
state
s
i
∈
. The resultant form is as follows:
φ
∃
x
:
Init
∧
[
N
]
v
∧
L
∧
NI
v
(
). Except the quoted syntactically and semantically modifications, the
remaining TLA notions including Fairness, stuttering, and temporal modalities
are preserved.
N
,
⊥
4S-TLA
+
: A Formal Language for Writing Specifications
We define S-TLA
+
as a language for writing specifications in S-TLA, it embodies
TLA
+
[6] with some add-ons in the module structure (the lowest granular part
of a TLA
+
specification,) and in the constant and non constant operators. TLA
+
is the high-level specification language that is based on TLA, and extended by
notations of set theory (Zermelo Fraenkel set theory) and syntactic structur-
ing mechanisms. To describe S-TLA
+
, we concentrate only on the introduced
modifications as outlined hereinafter:
