Util.tla

-------------------------------- MODULE Util --------------------------------
EXTENDS Sequences, Functions, Naturals, TLC
\* Simple utility functions
intersects(a, b) == a \cap b # {}
max(s) == CHOOSE i \in s : (~\E j \in s : j > i)
min(s) == CHOOSE i \in s : (~\E j \in s : j < i)

ReduceSet(op(_, _), set, base) ==
  LET iter[s \in SUBSET set] ==
        IF s = {} THEN base
        ELSE LET x == CHOOSE x \in s: TRUE
             IN  op(x, iter[s \ {x}])
  IN  iter[set]

ReduceSeq(op(_, _), seq, acc) == FoldFunction(op, acc, seq)

Index(seq, e) ==  CHOOSE i \in 1..Len(seq): seq[i] = e
    
SeqToSet(s) == {s[i] : i \in DOMAIN s}
Last(seq) == seq[Len(seq)]
IsEmpty(seq) == Len(seq) = 0
\* Remove all occurrences of `elem` from `seq`
Remove(seq, elem) == SelectSeq(seq, LAMBDA e: e /= elem)

\* Dual to UNION on intersect
INTERSECTION(setOfSets) == ReduceSet(\intersect, setOfSets, UNION setOfSets)

\* Borrowed from Stephan Merz. TLA+ Case Study: A Resource Allocator. [Intern report] A04-R-101 || merz04a, 2004, 20 p. ffinria-00107809f
(* The set of permutations of a finite set, represented as sequences.  *)
PermSeqs(S) ==
  LET perms[ss \in SUBSET S] ==
       IF ss = {} THEN { << >> }
       ELSE LET ps == [ x \in ss |-> 
                        { Append(sq,x) : sq \in perms[ss \ {x}] } ]
            IN  UNION { ps[x] : x \in ss }
  IN  perms[S]

\* Helper to write "unit test" ASSUMES which print when false
test(lhs, rhs) == lhs /= rhs => Print(<<lhs, " IS NOT ", rhs>>, FALSE)


=============================================================================
\* Modification History
\* Last modified Sun Aug 05 16:44:44 ET 2023 by murat
\* Created Tue Apr 28 16:43:24 CEST 2020 by tim