[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# operator \sim_x' as defined in erratum differs from TOPLAS

• From: Ioannis Filippidis <jfili...@xxxxxxxxx>
• Date: Tue, 1 Nov 2016 00:52:40 -0700 (PDT)

Dear Dr. Lamport, TLA+ Users Group,

The operator \sim_x' appears to be defined differently in the book's errata (version of 28 Oct 2016)
than in the 1994 TOPLAS paper "The temporal logic of actions".

--------------------------------------- EXAMPLE ---------------------------------------

For example, in ZF, let

sigma == [
n \in Nat |->
IF n = 0
THEN [ x |-> 1, y |-> "a" ]
ELSE IF n = 1
THEN [ x |-> 2, y |-> "a" ]
ELSE [ x |-> 2, y |-> "b" ] ]

tau == [
n \in Nat |->
IF n = 0
THEN [ x |-> 999, y |-> "a" ]
ELSE [ x |-> 999, y |-> "b" ] ]

-----------------------------------------------------------------------------------------------

Using TOPLAS (with Natural defined as in the book, and using the notation
\sim_x to encapsulate the first two conjuncts from Eq.(49)):

sigma \sim_x tau ==
\E rho:
/\ IsABehavior(rho)
/\ Natural(rho) = Natural(sigma)
/\ rho =_x tau

Natural(sigma) = [
0 |-> [ x |-> 1, y |-> "a" ],
1 |-> [ x |-> 2, y |-> "a" ],
2 |-> [ x |-> 2, y |-> "b" ] ]

PROPOSITION  Rho1 ==
\A rho:
/\ IsABehavior(rho)
/\ rho =_x tau
=> rho["y"] = "b"
PROOF SKETCH:
BY axiom about function equality,
DOMAIN tau = Nat,
DEF IsABehavior,
\A n \in Nat:  DOMAIN rho[n] = VarNames,
"y" \in VarNames,
DEF tau,
DEF =_x.

PROPOSITION  NaturalRho1 ==
\A rho:
/\ IsABehavior(rho)
/\ rho =_x tau
=> Natural(rho)["y"] = "b"
PROOF SKETCH:
BY Rho1,
DEF Natural,
DEF =_x,
DEF tau,
"a" # "b".

PROPOSITION  Unequal ==
\A rho:
/\ IsABehavior(rho)
/\ rho =_x tau
=> Natural(rho) # Natural(sigma)
PROOF SKETCH:
BY NaturalRho1,
DEF Natural,
axiom about function equality.

THEOREM  ~ (sigma \sim_x \tau)
PROOF SKETCH:
BY Unequal, DEF \sim_x.

-----------------------------------------------------------------------------------------------

Using the erratum from 28 Oct 2016:

Overwrite(p, var, value) == [
n \in Nat |->
[ p[n] EXCEPT ![var] = value ] ]

sigma \sim_x tau ==
\E value:
Natural(Overwrite(sigma, "x", value)) =
Natural(Overwrite(tau, "x", value))

PROPOSITION  Misc ==
/\ Overwrite(sigma, "x", 999) = [
n \in Nat |->
IF n = 0
THEN [ x |-> 999, y |-> "a" ]
ELSE IF n = 1
THEN [ x |-> 999, y |-> "a" ]
ELSE [ x |-> 999, y |-> "b" ] ]

/\ Overwrite(tau, "x", 999) = tau

/\ Natural(Overwrite(sigma, "x", 999)) = [
0 |-> [ x |-> 999, y |-> "a" ],
1 |-> [ x |-> 999, y |-> "b" ] ]

/\ Natural(Overwrite(tau, "x", 999)) = [
0 |-> [ x |-> 999, y |-> "a" ],
1 |-> [ x |-> 999, y |-> "b" ] ]

THEOREM  sigma \sim_x tau
PROOF SKETCH:
BY Misc, DEF \sim_x

================================================

The above example also demonstrates that the TOPLAS paper defines the
operator \sim_x' to be noncommutative, whereas the erratum defines
a commutative operator.

If the above reasoning is correct, then should the erratum be
considered a revision, or should we continue to use the TOPLAS definition?

The TOPLAS definition seems closer to physical intuition.
It does not allow "squeezing" sigma' too much to obtain tau'.
If there are steps in sigma' that change the unhidden variable x',
then those steps are preserved as nonstuttering ones in Natural(sigma)',
and so should appear as nonstuttering steps in both rho' and tau'.

This ensures that the "refined" behavior tau' has at least as many nonstuttering
steps as the "coarser" behavior sigma'. Otherwise (using the erratum),
tau' could omit steps that in sigma' change the unhidden x',
even though those steps could represent visible behavior of other components.
Of course, a shorter tau' can always be elongated by stuttering,
so this may leave the definition of temporal quantification unaffected.

Two weeks ago, I observed the difference between the earlier erratum (from Oct 2005)
and TOPLAS, and was working on proving it. In case they may be useful to someone,
I have attached the relevant TLA+ file, and a Python script that
applies this earlier definition to the TOPLAS example.

Best regards,
Ioannis Filippidis

Attachment: about_temporal_quantifiers.tla
Description: Binary data

#!/usr/bin/env python
"""Compute the unstuttering map as in: Lamport, "Specifying systems"."""

def unstutter(s):
"""Remove repetitions of states from behavior s."""
m = len(s)
dom = {f(n, s): n for n in range(m)}
k = len(dom)
assert set(dom) == set(range(k)), dom
r = [s[dom[n]] for n in range(k)]
return r

def f(n, s):
"""Map index n to index of stutter-free behavior."""
if n == 0:
return 0
assert n > 0, n
r = f(n - 1, s)
if s[n] != s[n - 1]:
r += 1
return r

def sim_up_to_var(sigma, tau, var):
"""Return True if behaviors sigma, tau similar modulo var."""
t = unstutter(tau)
s = unstutter(sigma)
r = list()
for n, state in enumerate(t):
d = dict(state)
d[var] = s[n][var]
r.append(d)
print('[n \in DOMAIN t |-> t[n] EXCEPT ![var] = s[n][var]] =')
pprint_behavior(r)
return s == r

def main():
"""Example from 1994 Lamport TOPLAS."""
tau = [
dict(x=1, y='a'),
dict(x=2, y='a'),
dict(x=2, y='b')]
sigma = [
dict(x=999, y='a'),
dict(x=999, y='a'),
dict(x=999, y='b')]
# makes domains equal, but still not (sigma ~_x tau)
# sigma.append(dict(x=3, y='b'))
t = unstutter(tau)
s = unstutter(sigma)
print('Natural(tau) =')
pprint_behavior(t)
print('Natural(sigma) =')
pprint_behavior(s)
var = 'x'
sim = sim_up_to_var(sigma, tau, var)
if sim:
print('sigma ~_x tau')
else:
print('not (sigma ~_x tau)')

def pprint_behavior(t):
"""Pretty print behavior t."""
for state in t:
print(state)
print('\n')

if __name__ == '__main__':
main()