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

*From*: Jeremy Wright <jeremy@xxxxxxxxxxxx>*Date*: Mon, 1 Nov 2021 15:36:01 -0700*References*: <CAC2JkJsjSGQ5ZpYiBKLGzw0p7QimMmVTmgvCMzK3JFHKJi1e0w@mail.gmail.com> <11632bd3-f810-730b-d093-8e37b9f97c70@gmail.com> <CAC2JkJv5u0=+S4=q-f4aGbFKiXkkvnUgvwtwEnJec6_Q+L2TRQ@mail.gmail.com> <CAEPrOm+nVWitUvCr+sHjM80VhJkHQNx6-RO8Vg99do+TuQNztw@mail.gmail.com> <b883fa15-b77f-4b3c-a5cd-8323efe90f76n@googlegroups.com>

Thank you Alex, and Leslie for your responses. This was very beneficial.

Alex, I did not know the term "vacuous truth". Putting a term on this construct helped me understand logical-implication a bit more clearly.

A member of my study group pointed out that Pressler's post https://pron.github.io/posts/tlaplus_part3#machine-closure-and-fairness helped them understand Leslie's comments a bit better. Thank you all, for engaging with my question. It's wonderful to have a helpful community behind our tool.

Thank you again,

Jeremy

On Fri, Oct 29, 2021 at 11:33 PM Leslie Lamport <tlaplus.ll@xxxxxxxxx> wrote:

Jeremy,You have discovered what makes the TLA logic better than any othertemporal logic for dealing with liveness. The practical way tospecify safety properties is with a state machine. In TLA, that's theInit /\ [][Next]_vars part of the spec. Hundreds (probably thousands)of ways of specifying a state machines have been proposed. They allmore or less work for specifying safety. But safety just says whatmay happen. It's nice to be able to say that your system must dosomething, which means that you have to add a liveness property.Temporal logic is the best way I know to describe liveness properties.However, the only way to add a liveness property to a state machinethat makes the state machine understandable is to add a fairnessproperty. If S is a safety property, adding a fairness property meanswriting S /\ L where L is a liveness property that doesn't add anysafety property. What that means is the S /\ L does not rule outanything that may happen that S allows to happen. More precisely,note that Init /\ [][Next]_var is false of a behavior if and only ifeither Init is false on the initial state or [Next]_var is false onsome pair of successive states. So, we can talk about it beingtrue on a finite behavior. L is a fairness property for S ifany finite behavior satisfying S can be extended to an infinite behaviorsatisfying S /\ L. (Instead of saying that L is a liveness propertyfor S, we usually say that the pair S,L is machine closed.)The problem with your spec is that the liveness property <>[](A=0) isnot a fairness property for your safety spec Init /\ [][Next]_vars.It's an egregious form of non-fairness that rules out all finitebehaviors satisfying the safety property. But you can get intotrouble by writing less extreme examples. You almost never want toadd a liveness property that is not fairness. (I've written one specduring my career that did it.) But I know of no way to tell if anarbitrary liveness property is a fairness property for your spec.And, I don't know any easy way to make sure you're writing a fairnessproperty in any temporal logic except TLA.In TLA it's very simple. You just write your liveness conditionas the conjunction of formulas of the form WF_vars(Act) orSF_vars(Act), where Next can be written as Act \/ SomethingElse.If you don't follow that rule, you're asking for trouble.LeslieP.S. The one spec I've written that used a non-fairness livenessproperty was for the condition that database people callserializability. The fact that I had to do that to get a simple specwas a sign that serializability, although it looks like a simple,reasonable condition, is actually very weird when you examine itclosely.L.--On Friday, October 29, 2021 at 4:13:09 PM UTC-7 alex.m.w...@xxxxxxxxx wrote:Are you familiar with the concept of vacuous truth? It’s the idea that, if you can’t prove something false, then it’s true by default. This is the principle behind implication: P => Q is true (vacuously) even when P is false.Remember that “correctness” generally means that your Spec implies some property. You are constructing purposefully contradictory Specs which actually evaluate to false since they cannot be satisfied by any state space, and false implies the vacuous truth of any and all other logical statements.Maybe TLC could throw a warning here, I think that’s fair. But, it’s just a case of a formal system doing exactly what we tell to.On Fri, Oct 29, 2021 at 6:21 PM Jeremy Wright <jer...@xxxxxxxxxxxx> wrote:Thank you for the response Hillel, but I still think there is something I don't understand. It seems that if I setup a Spec with no behaviors, I can ask TLC anything and it will tell me it's okay. This bothers me.The spec's I'm using here are "obvious", however if I design a more complex system, and I make a mistake such that my system system has no valid behaviors, TLC won't tell me there is a problem. Not only will TLC not compain, it tells me there are no problems for ANY property I ask it to check.For example:I'll restate the video, for those that prefer to read.I define a spec with 1 and only 1 state.

------------------------------ MODULE nonsense ------------------------------

EXTENDS TLC, Integers

VARIABLES A

vars == A

Init == A = 1

Next == A' = 1

EventuallyRubbish == <>(A = 999)

Spec == Init /\ [][Next]_vars /\ <>[](A = 0)

=============================================================================The Spec includes a temporal property which is not in the state space. There is no state where A=0, but TLC never warns me that my system does nothing. Here it is obviously not in the state space, but a more complex system that might not be so obvious. I recall the phrase, "beware of success", but this feels fragile to me. Am I missing something fundamental about how I express the Spec line?Thank you for your time.Sincerely,Jeremy--On Thu, Oct 28, 2021 at 4:05 PM Hillel Wayne <hwa...@xxxxxxxxx> wrote:--The problem is the line

Spec==Init/\[][Next]_vars/\EventuallySortedAsc/\EventuallySortedDesSince there are no models whereEventuallySortedAsc/\EventuallySortedDes,Spec = FALSE. If you change it to

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

Then it should work as expected.

H

On 10/28/2021 1:17 PM, Jeremy Wright wrote:

--Hello,

I am trying to write a simple spec for sorting. However, I've expressed a temporal property that I feel shouldn't be valid, yet TLC permits it.

Here is a video walkthrough of my question: https://www.loom.com/share/25f4eaaecd914d158551cbc061104a06

This spec is intended to be a simple abstraction of what sorting is. A sequence is (potentially) unsorted, then in one magical step it's sorted. I'm applying a refinement to it in another spec to show that, for example, bubble sort implements "sort by magic".

However, I have two temporal properties, which I feel conflict.

IsSortedAsc(seq) == \A a,b \in 1..N: a < b => seq[a] <= seq[b]

IsSortedDes(seq) == \A a,b \in 1..N: a < b => seq[a] >= seq[b]

EventuallySortedDes == <>[]IsSortedDes(A)

EventuallySortedAsc == <>[]IsSortedAsc(A)

I'm trying to express that eventually, the sequence is sorted In Ascending order or Descending Order. When I apply a model that checks if both are simultaneously true, TLC says this is successful.

Model Screenshot:

Thank you for any potential help. I fully expect I'm doing something incorrect, but I'm not quite sure where.

Sincerely,Jeremy Wright

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC2JkJsjSGQ5ZpYiBKLGzw0p7QimMmVTmgvCMzK3JFHKJi1e0w%40mail.gmail.com.

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/11632bd3-f810-730b-d093-8e37b9f97c70%40gmail.com.

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC2JkJv5u0%3D%2BS4%3Dq-f4aGbFKiXkkvnUgvwtwEnJec6_Q%2BL2TRQ%40mail.gmail.com.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b883fa15-b77f-4b3c-a5cd-8323efe90f76n%40googlegroups.com.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC2JkJsV0DsMNpEojwvV%3Dtc2rKiGnoMJSGP95jqNF5c6hmvTiA%40mail.gmail.com.

**Follow-Ups**:**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec***From:*Jeremy Wright

**References**:**[tlaplus] Trouble Verifying Sorting Property on A Simple Spec***From:*Jeremy Wright

**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec***From:*Hillel Wayne

**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec***From:*Jeremy Wright

**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec***From:*Alex Weisberger

**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Removing item taken from CHOOSE** - Next by Date:
**[tlaplus] How to specify broadcasting a message** - Previous by thread:
**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec** - Next by thread:
**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec** - Index(es):