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