Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec

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:

Code: https://github.com/JeremyLWright/specs/blob/master/algorithm/nonsense/nonsense.tla

Video Demo: https://www.loom.com/share/36be2872d50043ca9875cc305692450d

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 <hwayne@xxxxxxxxx> wrote:

The problem is the line

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

Since there are no models where EventuallySortedAsc/\ 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 my Spec: https://github.com/JeremyLWright/specs/blob/master/algorithm/sort/sort.tla

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.