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

*From*: Jeremy Wright <jeremy@xxxxxxxxxxxx>*Date*: Fri, 29 Oct 2021 15:21:19 -0700*Ironport-hdrordr*: A9a23:2n4Qda1maCAWAUcaYQKeFQqjBBYkLtp133Aq2lEZdPULSKDo7/xGzc53pGbJYWgqMgBHpTngAtj2fZq4z/FICOYqTMSftWXdyRuVxcRZnPrfK9OJIVy/ygZyvZ0QMpSWS+eAQGSTtK7BkUeF+q8bsZq6GcOT9JjjJ8IHd3AhV0gD1XYKNu/BKDw8eOAuP/NQf+v5l7E32gZMYU5nFPhTREN1IdQrwee73K4OTiRmO/dN0nj6sdrH0s+PL/BYti1uNg+nAo1DzYEGqWLEDhXJiYD19vYR7R6x03xa8+GRg+eq9Ke3+74ow/zX+2TYA/UcZ5Sy+AotqOXqwlcnmtvBrlMBOIBc8HXMZwiO0FfQ5zU=*References*: <CAC2JkJsjSGQ5ZpYiBKLGzw0p7QimMmVTmgvCMzK3JFHKJi1e0w@mail.gmail.com> <11632bd3-f810-730b-d093-8e37b9f97c70@gmail.com>

Thank you for the response Hillel, but I still think there is something I don't understand. I

t 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)

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

------------------------------ 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 <hwayne@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+unsubscribe@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+unsubscribe@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+unsubscribe@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.

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

**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

- Prev by Date:
**Re: [tlaplus] Viewing the SMT Encoding from TLAPM** - Next by Date:
**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec** - 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):