tlaplus / examples Goto Github PK

LOCAL INSTANCE Sequences

LOCAL Max(n, m) == IF n < m THEN m ELSE n

RECURSIVE ToBase2(_, _)
ToBase2(d, b) == IF d > 0 
                     THEN ToBase2(d \div 2, b) \o <<d % 2>>
                     ELSE b

ToBase10(b) == LET d[i \in DOMAIN b] == IF i = 1 
                                          THEN b[Len(b) + 1 - i] * (2^(i-1)) 
                                          ELSE b[Len(b) + 1 - i] * (2^(i-1)) + d[i - 1]
               IN d[Len(b)]
LOCAL And2(x,y) == LET bx == ToBase2(x, <<>>)
                      by == ToBase2(y, <<>>)
                      and == [ i \in DOMAIN bx \cup DOMAIN by |-> 
                                     IF bx[i] = 1 /\ by[i] = 1 THEN 1 ELSE 0 ]
                  IN ToBase10(and)

------------------------------- MODULE TLCMC -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, TestGraphs

(***************************************************************************)
(* Converts the given Sequence seq into a Set of all the                  *) 
(* Sequence's elements. In other words, the image of the function          *)
(* that seq is.                                                            *)
(***************************************************************************)
SeqToSet(seq) == {seq[i] : i \in 1..Len(seq)} 

(***************************************************************************)
(* Returns a Set of those permutations created out of the elements of Set  *)
(* set which satisfies Filter.                                               *)
(***************************************************************************)
SetToSeqs(set, Filter(_)) == UNION {{perm \in [1..Cardinality(set) -> set]: 
                            \* A filter applied on each permutation
                            \* generated by [S -> T]       
                            Filter(perm)}}

(***************************************************************************)
(* Returns a Set of all possible permutations with distinct elements     *)
(* created out of the elements of Set set. All elements of set occur in    *)
(* in the sequence.                                                        *)
(***************************************************************************)
SetToDistSeqs(set) == SetToSeqs(set, 
                    LAMBDA p: Cardinality(SeqToSet(p)) = Cardinality(set))

(***************************************************************************)
(* A (state) graph G is a directed cyclic graph.                           *)
(*                                                                         *)
(* A graph G is represented by a record with 'states' and 'actions'        *)
(* components, where G.states is the set of states and G.actions[s] is the *)
(* set of transitions of s -- that is, all states t such that there is an  *)
(* action (arc) from s to t.                                               *)
(***************************************************************************)
IsGraph(G) == /\ {"states", "initials", "actions"} = DOMAIN G
              /\ G.actions \in [G.states -> SUBSET G.states]
              /\ G.initials \subseteq G.states

(***************************************************************************)
(* A set of all permutations of the initial states of G.                    *)
(***************************************************************************)
SetOfAllPermutationsOfInitials(G) == SetToDistSeqs(G.initials)

(***************************************************************************)
(* A Set of successor states state.                                        *)
(***************************************************************************)
SuccessorsOf(state, SG) == {successor \in SG.actions[state]:
                            successor \notin {state}}

(***************************************************************************)
(* The predecessor of v in a forest t is the first element of the pair     *)
(* <<predecessor, successor>> nested in a sequence of pairs. In an actual  *)
(* implementation such as TLC, pair[1] is rather an index into t than      *)
(* an id of an actual state.                                               *)
(***************************************************************************)
Predecessor(t, v) == SelectSeq(t, LAMBDA pair: pair[2] = v)[1][1]

CONSTANT StateGraph, ViolationStates, null

ASSUME \* The given StateGraph is actually a graph
       \/ IsGraph(StateGraph)
       \* The violating states are vertices in the state graph.
       \/ ViolationStates \subseteq StateGraph.states

(***************************************************************************
The PlusCal code of the model checker algorithm
--fair algorithm ModelChecker {
	variables
              \* A FIFO containing all unexplored states. A simple
              \* set provides no order, but TLC should explore the
              \* StateGraph in either BFS (or DFS => LIFO).
              \* Note that S is initialized with each
              \* possible permutation of the initial states
              \* here because there is no defined order
              \* of initial states.
              S \in SetOfAllPermutationsOfInitials(StateGraph),
              \* A set of already explored states.      
              C = {},
              \* The state currently being explored in scsr
              state = null,
              \* The set of state's successor states	          
              successors = {},
              \* Counter
              i = 1,
              \* A path from some initial state ending in a
              \* state in violation.
              counterexample = <<>>,
              \* A sequence of pairs such that a pair is a
              \* sequence <<predecessor, successors>>.
              T = <<>>;
	{
       (* Check initial states for violations. We could
          be clever and check the inital states as part
          of the second while loop. However, we then
          either check all states twice or add unchecked
          states to S. *)
       init: while (i \leq Len(S)) {
             \*  Bug in thesis: 
             \*state := Head(S);
             state := S[i]; 
             \* state is now fully explored,
             \* thus exclude it from any
             \* futher exploration if graph
             \* exploration visits it again
             \* due to a cycle. 
             C := C \cup {state};
             i := i + 1;
             if (state \in ViolationStates) {
                     counterexample := <<state>>;
                     \* Terminate model checking
                     goto trc;
             };
       };
       \* Assert that all initial states have been explored.
       initPost: assert C = SeqToSet(S);

       (* Explores all successor states 
          until no new successors are found
          or a violation has been detected. *)
       scsr: while (Len(S) # 0) {
            \* Assign the first element of
            \* S to state. state is
            \* what is currently being checked.
            state := Head(S);
            \* Remove state from S.
            S := Tail(S);
            
            \* For each unexplored successor 'succ' do:
            successors := SuccessorsOf(state, StateGraph) \ C;
            if (SuccessorsOf(state, StateGraph) = {}) {
                \* Iff there exists no successor besides
                \* the self-loop, the system has reached
                \* a deadlock state.
                counterexample := <<state>>;
                goto trc;
            };
            each: while (successors # {}) {
                with (succ \in successors) {
                     \* Exclude succ in this while loop.
                     successors := successors \ {succ};

                     \* Mark successor globally visited.
                     C := C \cup {succ}; S := S \o <<succ>>;
                     
                     \* Append succ to T and add it
                     \* to the list of unexplored states.
                     T  := T \o << <<state,succ>> >>;
                     
                     \* Check state for violation of a
                     \* safety property (simplified 
                     \* to a check of set membership.
                     if (succ \in ViolationStates) {
                       counterexample := <<succ>>;
                       \* Terminate model checking
                       goto trc;
                     };
                };
            };
       };
       (* Model Checking terminated without finding
          a violation. *)
       \* No states left unexplored and no ViolationState given.
       assert S = <<>> /\ ViolationStates = {};
       goto Done;
       
       (* Create a counterexample, that is a path
          from some initial state to a state in
          ViolationStates. In the Java implementation
          of TLC, the path is a path of fingerprints. 
          Thus, a second, guided state exploration
          resolves fingerprints to actual states. *)
       trc : while (TRUE) {
                if (Head(counterexample) \notin StateGraph.initials) {
                   counterexample := <<Predecessor(T, Head(counterexample))>> \o counterexample;
                } else {
                   assert counterexample # <<>>;
                   goto Done;
                };
       };
	}        
}
 ***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES S, C, state, successors, i, counterexample, T, pc

vars == << S, C, state, successors, i, counterexample, T, pc >>

Init == (* Global variables *)
        /\ S \in SetOfAllPermutationsOfInitials(StateGraph)
        /\ C = {}
        /\ state = null
        /\ successors = {}
        /\ i = 1
        /\ counterexample = <<>>
        /\ T = <<>>
        /\ pc = "init"

init == /\ pc = "init"
        /\ IF i \leq Len(S)
              THEN /\ state' = S[i]
                   /\ C' = (C \cup {state'})
                   /\ i' = i + 1
                   /\ IF state' \in ViolationStates
                         THEN /\ counterexample' = <<state'>>
                              /\ pc' = "trc"
                         ELSE /\ pc' = "init"
                              /\ UNCHANGED counterexample
              ELSE /\ pc' = "initPost"
                   /\ UNCHANGED << C, state, i, counterexample >>
        /\ UNCHANGED << S, successors, T >>

initPost == /\ pc = "initPost"
            /\ Assert(C = SeqToSet(S), 
                      "Failure of assertion at line 116, column 18.")
            /\ pc' = "scsr"
            /\ UNCHANGED << S, C, state, successors, i, counterexample, T >>

scsr == /\ pc = "scsr"
        /\ IF Len(S) # 0
              THEN /\ state' = Head(S)
                   /\ S' = Tail(S)
                   /\ successors' = SuccessorsOf(state', StateGraph) \ C
                   /\ IF SuccessorsOf(state', StateGraph) = {}
                         THEN /\ counterexample' = <<state'>>
                              /\ pc' = "trc"
                         ELSE /\ pc' = "each"
                              /\ UNCHANGED counterexample
              ELSE /\ Assert(S = <<>> /\ ViolationStates = {}, 
                             "Failure of assertion at line 164, column 8.")
                   /\ pc' = "Done"
                   /\ UNCHANGED << S, state, successors, counterexample >>
        /\ UNCHANGED << C, i, T >>

each == /\ pc = "each"
        /\ IF successors # {}
              THEN /\ \E succ \in successors:
                        /\ successors' = successors \ {succ}
                        /\ C' = (C \cup {succ})
                        /\ S' = S \o <<succ>>
                        /\ T' = T \o << <<state,succ>> >>
                        /\ IF succ \in ViolationStates
                              THEN /\ counterexample' = <<succ>>
                                   /\ pc' = "trc"
                              ELSE /\ pc' = "each"
                                   /\ UNCHANGED counterexample
              ELSE /\ pc' = "scsr"
                   /\ UNCHANGED << S, C, successors, counterexample, T >>
        /\ UNCHANGED << state, i >>

trc == /\ pc = "trc"
       /\ IF Head(counterexample) \notin StateGraph.initials
             THEN /\ counterexample' = <<Predecessor(T, Head(counterexample))>> \o counterexample
                  /\ pc' = "trc"
             ELSE /\ Assert(counterexample # <<>>, 
                            "Failure of assertion at line 177, column 20.")
                  /\ pc' = "Done"
                  /\ UNCHANGED counterexample
       /\ UNCHANGED << S, C, state, successors, i, T >>

Next == init \/ initPost \/ scsr \/ each \/ trc
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

Live == ViolationStates # {} => <>[](/\ Len(counterexample) > 0
                                     /\ counterexample[Len(counterexample)] \in ViolationStates
                                     /\ counterexample[1] \in StateGraph.initials)

=============================================================================

----------------------------- MODULE TestGraphs -----------------------------
EXTENDS Sequences, Integers
(***************************************************************************)
(* The definitions of some graphs, paths, etc.  used for testing the       *)
(* definitions and the algorithm with the TLC model checker.               *)
(***************************************************************************)

\* Graph 1.
G1 == [states |-> 1..4,
       initials |-> {1,2},
       actions  |-> << {1,2}, {1,3}, {4}, {3} >>
       ]
V1 == {4}

\* Graph 1a.
G1a == [states |-> 1..4,
       initials |-> {3},
       actions  |-> << {1, 2}, {1, 3}, {4}, {3} >>]
\* Graph-wise it's impossible to reach state 1 from state 3
V1a == {1}

\* Graph 2. This graph is actually a forest of two graphs
\*    {1,2} /\ {3,4,5}. {1,2} are an SCC.
G2 == [states |-> 1..5,
       initials |-> {1,3},
       actions  |-> << {1, 2}, {1}, {4, 5}, {}, {} >> ]
V2 == {2,5}      

\* Graph 3.       
G3 == [states |-> 1..4,
       initials |-> {2},
       actions  |-> << {1,2}, {2,3}, {3,4}, {1,4} >> ]
V3 == {1}
      
\* Graph 4.
G4 == [states |-> 1..9,
       initials |-> {1,2,3},
       actions  |-> << {3}, {4}, {5}, {6}, {7}, {7}, {8, 9}, {}, {4} >> ]
V4 == {8}
      
\* Graph 5.
G5 == [states |-> 1..9,
       initials |-> {9},
       actions  |-> << {4,2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {2} >> ]
V5 == {8}

\* Graph 6.
G6 == [states |-> 1..5,
       initials |-> {5},
       actions  |-> << {2,4,5}, {2}, {1}, {4}, {3} >> ]
V6 == {2}

\* Graph Medium (node 22 is a sink)
G7 == [states |-> 1..50,
       initials |-> {1},
       actions  |-> << {8,35},{15,46,22,23,50},{20,26,34},{5,18,28,37,43},{18,28},{44},{14,29},{42,45},{20,49},{10,12,31,47},
       {1,8,29,30,35,42},{22,31},{10,12,22,27},{23,24,48},{9,22,49},{9,35,50},{10},{21,25,39},{7,29,33,43},{16,41},{},
       {4,36,39,47},{7},{12,22,23},{5,6,39,44},{3,35},{10,13,17},{6,25,33,32,43},{23,30,40,45},{23,50},{24,38},
       {19,33},{6,7,14,38,48},{3,9,20},{3,20,41},{10,38,47},{21,43},{6,10,36,48},{36,38,39},{19,43},{16},
       {29,45},{32},{38,39},{40},{9,15,16,50},{17},{24,31},{13,22,34},{35,23,50} >> ]
V7 == {50}

\* Graph 8.
G8 == [states |-> 1..4,
       initials |-> {1},
       actions |-> <<{1,2},{2,3},{3,4},{4}>>]
V8 == {}

\* Graph 9.
G9 == [states |-> {1},
       initials |-> {1},
       actions |-> <<{1}>>]
V9 == {1}

\* Graph 10.
G10 == [states |-> {},
       initials |-> {},
       actions |-> <<{}>>]
V10 == {}

\* Graph 11.
G11 == [states |-> 1..10,
       initials |-> {},
       actions |-> <<{}>>]
V11 == {}

\* Graph 12.
G12 == [states |-> 1..3,
       initials |-> {1,2,3},
       actions |-> <<{},{},{}>>]
V12 == {1}

\* Graph 13 (simple sequence.
G13 == [states |-> 1..3,
       initials |-> {1},
       actions |-> <<{2},{3},{}>>]
V13 == {}

=============================================================================

---- MODULE F ----
EXTENDS Naturals, FiniteSets, Sequences

(* 1. Set of all permutations of {"T","L","A"} including repetitions. *)
PermsWithReps(S) ==
    [ 1..Cardinality(S) -> S ]
    
ASSUME 
    PermsWithReps({"T","L","A"}) =
        {<<"T", "T", "T">>, <<"T", "T", "L">>, <<"T", "T", "A">>, 
            <<"T", "L", "T">>, <<"T", "L", "L">>, <<"T", "L", "A">>, 
            <<"T", "A", "T">>, <<"T", "A", "L">>, <<"T", "A", "A">>, 
            <<"L", "T", "T">>, <<"L", "T", "L">>, <<"L", "T", "A">>, 
            <<"L", "L", "T">>, <<"L", "L", "L">>, <<"L", "L", "A">>, 
            <<"L", "A", "T">>, <<"L", "A", "L">>, <<"L", "A", "A">>, 
            <<"A", "T", "T">>, <<"A", "T", "L">>, <<"A", "T", "A">>, 
            <<"A", "L", "T">>, <<"A", "L", "L">>, <<"A", "L", "A">>, 
            <<"A", "A", "T">>, <<"A", "A", "L">>, <<"A", "A", "A">>}

(* 2. All combinations of a two-digit lock. *)
TwoDigitLock ==
    [1..2 -> 0..9]

ASSUME
    /\ (0..9) \X (0..9) = TwoDigitLock
    /\ {<<n,m>> : n,m \in 10..19} \notin SUBSET TwoDigitLock

(* 3. All combinations of a three-digit lock. *)
ThreeDigitLock ==
    [1..3 -> 0..9]

ASSUME
    /\ (0..9) \X (0..9) \X (0..9) = ThreeDigitLock
    /\ {<<n,m,o>> : n,m,o \in 10..19} \notin SUBSET ThreeDigitLock

(* 4. All pairs (including repetitions) of the natural numbers. *)
PairsOfNaturals ==
    [1..2 -> Nat]

ASSUME
    {<<n,m>> : n,m \in 0..100} \subseteq PairsOfNaturals

(* 5. All triples... *)
TriplesOfNaturals ==
    [1..3 -> Nat]

ASSUME
    {<<n,m,o>> : n,m,o \in 0..25} \subseteq TriplesOfNaturals

(* 6. Set of all pairs and triples... *)
PairsAndTriplesOfNaturals ==
    [1..2 -> Nat] \cup [1..3 -> Nat]

ASSUME
    /\ {<<n,m>> : n,m \in 0..100} \subseteq PairsAndTriplesOfNaturals
    /\ {<<n,m,o>> : n,m,o \in 0..25} \subseteq PairsAndTriplesOfNaturals

(* 7. What is the Cardinality of 3. ? *)
Cardinality3 ==
    Cardinality(ThreeDigitLock)

ASSUME Cardinality3 = 1000

(* 8. What is the Cardinality of 6. (PairsAndTriplesOfNaturals) ? *)

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

(* 9. The range/image/co-domain of a function. *)
Range(f) == { f[x]: x \in DOMAIN f }

ASSUME Range([a |-> 1, b |-> 2, c |-> 3]) = 1..3

(* 10. The permutations of a set _without_ repetition. *)
Perms(S) ==
    { f \in [S -> S] :
        Range(f) = S }

ASSUME Perms({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

Perms2(S) ==
    \* If for all w in S there exists a v in S for which f[v]=w,
    \* there can be no repetitions as a consequence. The predicate
    \* demands for all elements of S to be in the range of f.
    { f \in [S -> S] :
        \A w \in S :
            \E v \in S : f[v]=w }

ASSUME Perms2({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

Perms3(S) ==
    { f \in [S -> S] :
        \A i,j \in DOMAIN f :
            i # j => f[i] # f[j] }

ASSUME Perms3({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

(* 11. Reverse a sequence (a function with domain 1..N). *)
Reverse(seq) ==
    [ i \in 1..Len(seq) |-> seq[Len(seq)+1 - i] ]

ASSUME Reverse(<<1, 2, 3>>) = <<3, 2, 1>>
ASSUME Reverse(<<>>) = <<>>

(* 12. An (infix) operator to quickly define a function mapping an x to a y.  *)
x :> y ==
    [ e \in {x} |-> y ]

ASSUME "x" :> 42 = [ x |-> 42 ]

(* 13. Merge two functions f and g *)
f ++ g ==
  [x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]

ASSUME <<1,2,3>> ++ [i \in 1..6 |-> i] = <<1, 2, 3, 4, 5, 6>>

(* 14. Advanced!!! Inverse of a function f (swap the domain and range). *)
Inverse(f) ==
   CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s

ASSUME Inverse(("a" :> 0) ++ ("b" :> 1) ++ ("c" :> 2)) =
              ((0 :> "a") ++ (1 :> "b") ++ (2 :> "c"))
====

-------------------------- MODULE SyntaxExcercises --------------------------
(* The idea is that learners get the spec with the operator _definitions_ replaced 
    with TRUE. A learner can then check their definitions with TLC. *)
EXTENDS Integers, Sequences, TLC

(***************************************************************************)
(* The set of the fibonacci numbers: 1,1,2,3,5,8,13,...                    *)
(***************************************************************************)
MyNat == 1..21 \* perhaps, introduce model definitions right away?
fib[n \in MyNat] == IF n <= 2 THEN 1 ELSE fib[n-1] + fib[n-2]

ASSUME fib[12] = 144

RECURSIVE fibRecurse(_)
fibRecurse(n) == IF n <= 2 THEN 1 ELSE fibRecurse(n - 1) + fibRecurse(n - 2)

ASSUME fibRecurse(12) = 144

(***************************************************************************)
(* The set of fibonacci numbers in the range [10,20).                      *)
(***************************************************************************)
FibSet == { fib[n] : n \in 10..19 }

ASSUME FibSet = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}

FibSetRecurse == { fibRecurse(n) : n \in 10..19 }

ASSUME FibSetRecurse = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}

(***************************************************************************)
(* The sequence of fibonacci numbers in the range [10,20).                 *)
(***************************************************************************)
FibSeq == [ e \in 1..10 |-> fib[e+9] ]

ASSUME FibSeq = <<55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181>>

(***************************************************************************)
(* The range of a function func.                                           *)
(***************************************************************************)
Range(func) == { func[e] : e \in DOMAIN func }

(* Change the 5., 10, 15. element of a function f to "abc", "def" and "ghi" *)
(* TCommit video Minute 12:30 *)
Replace(func, pos, value) == [func EXCEPT ![pos] = value ]

ASSUME [ i \in 1..3 |-> i^2 ] = Replace(Replace(Replace([i \in 1..3 |-> 0], 1, 1), 2, 4), 3, 9)

(***************************************************************************)
(* Excercise page 235/70                                                   *)
(* The sequence obtained by removing the i-th element of seq.              *)
(***************************************************************************)
Remove(seq, i) == [ j \in (1..Len(seq) - 1) |-> (IF j < i THEN seq[j] ELSE seq[j+1]) ]

(***************************************************************************)
(* Excercise page 341/91                                                   *)
(* Recursive definition of the Len(seq) _operator_ with Tail.              *)
(***************************************************************************)
RECURSIVE RecLen(_)
RecLen(seq) == IF seq = <<>> THEN 0
               ELSE 1 + RecLen(Tail(seq))

(***************************************************************************)
(* An alternative variant which treats seq as the function it is and       *)
(* returns the maximum of its DOMAIN which corresponds to the number of    *)
(* elements in seq.                                                        *)
(***************************************************************************)
DomLen(seq) == CHOOSE m \in (DOMAIN seq): (DOMAIN seq) = 1..m

(***************************************************************************)
(* Write an operator that returns the cardinality of a given set.          *)
(***************************************************************************)
RECURSIVE Card(_)
Card(S) == IF S = {} THEN 0 ELSE 1 + Card(S \ {CHOOSE e \in S : TRUE})

ASSUME Card({}) = 0 /\ Card({1,1,2,2,3,3}) = 3

(***************************************************************************)
(* Write an operator that takes a tuple/sequence and, if the tuple is      *)
(* length two, returns the reversed tuple, and otherwise raises an error.  *)
(***************************************************************************)
ReverseOfTwo(seq) == IF Len(seq) = 2 THEN <<seq[2], seq[1]>>
                                     ELSE Assert(FALSE, "")

ASSUME <<4,5>> = ReverseOfTwo(<<5,4>>)

(***************************************************************************)
(* Write an operator that takes a sequence seq and, if the sequence is of  *)
(* uneven length, returns the reversed sequence, otherwise return seq.     *)
(***************************************************************************)
Uneven(n) == n % 2 = 1
Reverse(seq) == [ i \in 1..Len(seq) |-> seq[Len(seq) - (i-1)] ]
ReverseUneven(seq) == IF Uneven(Len(seq)) THEN Reverse(seq)
                                     ELSE seq

ASSUME <<1,2,3,4,5>> = ReverseUneven(<<5,4,3,2,1>>)
ASSUME <<1,2,3,4>> = ReverseUneven(<<1,2,3,4>>)

(* Sum of elements in seq *)

(***************************************************************************)
(* Remove those elements from sequence seq for which Filter(_) holds.      *)
(***************************************************************************)
RECURSIVE Subseq(_,_)
Subseq(Filter(_), seq) == IF seq = <<>>
                          THEN <<>>
                          ELSE IF Filter(Head(seq))
                               THEN <<Head(seq)>> \o Subseq(Filter, Tail(seq))
                               ELSE Subseq(Filter, Tail(seq))

Even(n) == ~Uneven(n)

ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = <<2,6,8,8,42>>

SelectSeq2(Test(_), s) ==
  LET S[i \in 0..Len(s)] ==
        IF i = 0 THEN << >> \* As a basis set the s[0] = <<>>
                 ELSE IF Test(s[i]) THEN S[i-1] \o <<s[i]>> \* copy previous value and concat with s[i]
                                    ELSE S[i-1] \* just copy the previous value
  IN S[Len(s)] \* The maximum (last function position) contains the collected sequence


ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = SelectSeq2(Even, <<1,2,1,3,3,6,8,8,23,42>>)

(***************************************************************************)
(* Given DOMAIN Tuple is the set of numbers Tuple is defined over, write   *)
(* an operator that gives a set of the values of the Tuple, ie the range.  *)
(***************************************************************************)




(***************************************************************************)
(* Write an operator that takes two sets S1 and S2 and determines if the   *)
(* double of every element in S1 is an element of S2.                      *)
(***************************************************************************)




(***************************************************************************)
(* Given a sequence of sets, write an operator that determines if a given  *)
(* element is found in any of the sequence’s sets.                         *)
(* IE Op("a", <<{"b", "c"}, {"a", "c"}>>) = TRUE.                            *)
(***************************************************************************)


(* Given the (built-in) set Nat (Naturals), create a subset of S whose largest element is 42. *)
(* Hint: Override Nat with 1..1000 on the Advanced Options page of the Model editor. By default *)
(* Nat is represented as a UserValue in TLC. A UserValue is _not_ enumerable, whereas a 1..1000 *)
(* is represented as a (finite) IntervalValue which subsequently can be enumerated. *)
Subset42 == { i \in Nat: i < 43 }

\*ASSUME Subset42 = 1..42


(* The inverse of a function *)
Inverse(f) == 
   CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s

ASSUME Inverse("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) = (0 :> "a" @@ 1 :> "b" @@ 2 :> "c")

(* Merge two functions f and g *)
Merge(f, g) == 
  [x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]

ASSUME Merge(<<1,2,3>>, [i \in 1..6 |-> i]) = <<1, 2, 3, 4, 5, 6>>

(* The permutations of a set *)
Perms(S) == 
    {f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}

ASSUME Perms({1,2,3}) = {<<1, 2, 3>>, <<1, 3, 2>>, <<2, 1, 3>>, <<2, 3, 1>>, <<3, 1, 2>>, <<3, 2, 1>>}
=============================================================================

   [i \in Nat |-> i^2][42]

   LET f == [i \in Nat |-> i^2] 
   IN  [f EXCEPT ![42] = 24][42]

   LET f == [i \in Nat |-> i^2] 
   IN  [f EXCEPT ![42] = @ - 24, ![24] = 42][42]
   
   LET f[i \in Nat] == IF i = 0 THEN 0 ELSE f[i-1] + i
   IN  f[42]

   [i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
                                          ELSE 42].a
   
   [i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
                                          ELSE 42].bc
   
   [a |-> 17, bc |-> 42, d |-> 42]["a"]

   [a |-> 17, bc |-> 42, d |-> 42]["bc"]

   DOMAIN [a |-> 17, bc |-> 42, d |-> 42]

   LET f(a) == [i \in Nat |-> a^i]
       g    == [j \in Nat |-> f(j)]
   IN  g[2][3]

   LET f(a) == [i \in Nat |-> a^i]
       g    == [j \in Nat |-> f(j)]
   IN  g[2][3]

   [i \in Nat, j \in 1..10 |-> i*j][3,4]

   (F => G) /\ (G => F) <=> (F <=> G)
   (~F /\ ~G) <=> (~F) \/ (~G)
   F => (F => G)
   (F => G) <=> (~G => ~F)
   (F => (G => H)) => ((F => G) => H) 
   (F <=> (G <=> H)) => ((F <=> G) <=> H) 
   (\A x : F /\ G) <=> (\A x : F)  /\ (\A x : G) 
   (\E x : F /\ G) <=> (\E x : F)  /\ (\E x : G) 
   (\A x : F \/ G) <=> (\A x : F)  \/ (\A x : G) 
   (\E x : F \/ G) <=> (\E x : F)  \/ (\E x : G) 

   (S \subseteq T) <=> (S \cup T = T)
   (S \subseteq T) <=> \A x \in S : x \in T
   (S = T) <=> (S \subseteq T) /\ (T \subseteq S)
   (S \subseteq T) <=> (S \ T = {})
   (S \ T) \cup (T \ S) = (S \cup T) \ (S \cap T)
   (S \ (T \cap U)) = (S \ T) \cup (S \ U)

   (a) <>[]<>F <=> []<>F
   (b) []<>[]F <=> []<>F
   (c) ~[](F \/ G) => <>~F /\ <>~G
   (d) []([]F => G) => ([]F => []G)
   (e) [](F => []G) => ([]F => []G)
   (f) [][A /\ B]_v <=> [][A]_v /\ [][B]_v
   (g) []<><<A /\ B>>_v <=> []<><<A>>_v  /\ []<><<B>>_v 
   (h) [][A => B]_v <=> [][<<A>>_v => B]_v 
   (i) WF_v(A) /\ WF_v(B) => WF_v(A \/ B)
   (j) SF_v(A) /\ SF_v(B) => SF_v(A \/ B)
   (k) ENABLED (A /\ B) => (ENABLED A) /\ (ENABLED B)