A toy program to sort characters with QuickSort (implemented" in TLA+)

Qsort.tla

$ ./pluspy -s modules/other/Qsort.tla
Enter input: poiuylkjhmnbvcdsxzafgtrewq
abcdefghijklmnopqrstuvwxyz

----------------------------- MODULE Qsort -----------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC, Input

\* Specification (works reasonably well for sets of cardinality <= 6
\* Takes a set as argument, produces a sorted tuple
Sort(S) == CHOOSE s \in [ 1..Cardinality(S) -> S]:
    \A i, j \in DOMAIN s: (i < j) => (s[i] < s[j])

---------------------------------------------------------------------------

Flatten[s \in Seq(Seq(Nat))] ==
    IF s = <<>> THEN <<>>
    ELSE Head(s) \o Flatten[Tail(s)]

Partition(s) ==
    LET LE(x) == x <= Head(s)
        GT(x) == x > Head(s)
    IN << SelectSeq(Tail(s), LE), << Head(s) >>, SelectSeq(Tail(s), GT) >>

---------------------------------------------------------------------------

VARIABLES data

\* Promp user to enter some data.
Init ==
    /\ data = <<>>
    /\ Print("Enter input: ", TRUE)

\* Read from stdin
Read ==
    /\ data = <<>>
    /\ LET read(p, x) == data' = <<x>>  \* No Lambdas in PlusPy, but LET/IN. 
       IN Receive(data, read)

\* Once there is input, sort it. When done, print to stdout.
Sort ==
    /\ data # <<>>
    /\ IF \E i \in 1..Len(data): Len(data[i]) > 1 /\
          data' = SubSeq(data, 1, i-1) \o Partition(data[i]) \o
                            SubSeq(data, i+1, Len(data))
       THEN TRUE
       ELSE /\ Print(Flatten[data], TRUE)  
            /\ UNCHANGED data

Next ==
    \/ Read
    \/ Sort

Spec == Init /\ [][Next]_<<data>>
=============================================================================

The read would have to convert from strings to integers to make this slightly less useless.

Originally from https://github.com/tlaplus/PlusPy/blob/master/modules/other/Qsort.tla