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

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Mon, 8 Apr 2019 08:02:55 +0300

Hello,

I'm trying to write my first proofs in TLAPS, and get stuck.

In the attached file is the simplified version of the specification.

It was constructed to illustrate that problematic part of the proof.

The specification describes a system, where some variable should not change after it was set.

Thank you in advance

Karolis Petrauskas

I'm trying to write my first proofs in TLAPS, and get stuck.

In the attached file is the simplified version of the specification.

It was constructed to illustrate that problematic part of the proof.

The specification describes a system, where some variable should not change after it was set.

CONSTANT P \* A set of peers.

CONSTANT V \* A set of values

VARIABLE v

NV == CHOOSE nv : nv \notin V

Init == v = [p \in P |-> NV]

Act1 == \E pp \in P, vv \in V :

IF v[pp] = NV

THEN v' = [v EXCEPT ![pp] = vv]

ELSE UNCHANGED v

Act2 == UNCHANGED v

Next == Act1 \/ Act2

Spec == Init /\ [][Next]_v

TypeOK == v \in [P -> V \cup {NV}]

VARIABLE v

NV == CHOOSE nv : nv \notin V

Init == v = [p \in P |-> NV]

Act1 == \E pp \in P, vv \in V :

IF v[pp] = NV

THEN v' = [v EXCEPT ![pp] = vv]

ELSE UNCHANGED v

Act2 == UNCHANGED v

Next == Act1 \/ Act2

Spec == Init /\ [][Next]_v

TypeOK == v \in [P -> V \cup {NV}]

The property I'm trying to prove is formulated as follows:

Stable == \A xp \in P, xv \in V: [] ((v[xp] = xv) => [] (v[xp] = xv))

I managed to prove "Spec => [] TypeOK", and for "Spec => Stable" I'm now try to prove an inductive Invariant:

StableIndInv == \A p \in P : v[p] # NV /\ Next => v[p] = v'[p]

The attempt that looks closest to the proof is the following:

THEOREM Attempt1 == StableIndInv

<1>1. SUFFICES ASSUME NEW p \in P

PROVE v[p] # NV /\ Next => v[p] = v'[p]

BY DEF StableIndInv

<1>2. SUFFICES ASSUME v[p] # NV

PROVE Next => v[p] = v'[p]

OBVIOUS

<1>3. SUFFICES ASSUME Next

PROVE v = v' \* Here v[p] reduced to v.

OBVIOUS

<1>4. CASE Act1

<2>1. ASSUME NEW vv \in V

PROVE Act1!(p, vv) => v = v'

<3>2. CASE v[p] = NV BY <1>2, <3>2

<3>3. CASE v[p] # NV BY <1>2, <3>3

<3>q. QED BY <2>1, <3>2, <3>3

<2>q. QED BY <1>4, <2>1 DEF Act1

<1>5. CASE Act2

BY <1>5 DEF Act2

<1>q. QED BY <1>3, <1>4, <1>5 DEF Next

<1>1. SUFFICES ASSUME NEW p \in P

PROVE v[p] # NV /\ Next => v[p] = v'[p]

BY DEF StableIndInv

<1>2. SUFFICES ASSUME v[p] # NV

PROVE Next => v[p] = v'[p]

OBVIOUS

<1>3. SUFFICES ASSUME Next

PROVE v = v' \* Here v[p] reduced to v.

OBVIOUS

<1>4. CASE Act1

<2>1. ASSUME NEW vv \in V

PROVE Act1!(p, vv) => v = v'

<3>2. CASE v[p] = NV BY <1>2, <3>2

<3>3. CASE v[p] # NV BY <1>2, <3>3

<3>q. QED BY <2>1, <3>2, <3>3

<2>q. QED BY <1>4, <2>1 DEF Act1

<1>5. CASE Act2

BY <1>5 DEF Act2

<1>q. QED BY <1>3, <1>4, <1>5 DEF Next

The problem (as I see it) is that I cannot relate <1>4 with its proof (<2>q or <2>1?).

I think the question is: how to prove that Act1!(p, vv) implies Act1.

In the attached file there is another attempt to prove this invariant (Attempt0),

but for me the Attempt1 looks closer to what it should be.

The same property was proved trivially for a specification, were variable

v had a value (v \in V) instead of function (v \in [P -> V]).

It would be very helpful to get some directions or comments.

Thank you in advance

Karolis Petrauskas

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

**Attachment:
TestStable.tla**

**Follow-Ups**:**Re: [tlaplus] TLAPS, first steps***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: [noob] Liveness property not violated as expected** - Next by Date:
**Re: [tlaplus] TLAPS, first steps** - Previous by thread:
**Re: [tlaplus] How do I extract particular mapping from each element in a set?** - Next by thread:
**Re: [tlaplus] TLAPS, first steps** - Index(es):