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

[tlaplus] Trouble Verifying Sorting Property on A Simple Spec



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:
image.png

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.