fmod SEARCH is
    pr META-UTILS .
    pr RANDOM .

    vars M L : Qid .
    vars T : Term .
    var TL : TermList .
    vars B B2 : Bound .
    vars N C : Nat .
    var LABELS : QidList .
    var RT : Result4Tuple? .

    ***(
        Generate a sequence of states with a bound number
        - Qid -> a name of Module
        - Term -> an initil term
        - Nat -> a random seed
        - Bound -> a bound number
    )
    op genSeq : Qid Term Nat Bound -> TermList .
    eq genSeq(M, empty, N, B) = empty .
    eq genSeq(M, T, N, 0) = empty .
    eq genSeq(M, T, N, B) = initGenSeq(M, T, normalize(N), B, getLabels(upModule(M, false))) .

    ***(
        init before generating sequence of states
    )
    op initGenSeq : Qid Term Nat Bound QidList -> TermList .
    eq initGenSeq(M, T, N, B, LABELS) = $genSeq(M, T, N, B, LABELS, empty) .

    ***(
        start to generate a sequence of states
    )
    op $genSeq : Qid Term Nat Bound QidList TermList -> TermList .
    eq $genSeq(M, empty, N, B, LABELS, TL) = TL .
    eq $genSeq(M, T, N, 0, LABELS, TL) = TL .
    
    *** trick: a quick random
    eq $genSeq(M, T, N, B, LABELS, TL) = $genSeq(
        M,
        nextTerm(getSuccessors(M, T, LABELS), random(N)),
        N + 1,
        sd(B, 1),
        LABELS,
        (TL, T)
    ) .

    ***(
        get all possible successors
    )
    op getSuccessors : Qid Term QidList -> TermList .
    eq getSuccessors(M, empty, LABELS) = empty .
    eq getSuccessors(M, T, nil) = empty .
    eq getSuccessors(M, T, (L LABELS)) = findRuleSuccessors(M, T, L), getSuccessors(M, T, LABELS) .  

    ***(
        find all corresponding successors by a rule
    )
    op findRuleSuccessors : Qid Term Qid -> TermList .
    eq findRuleSuccessors(M, T, L) = findRuleSuccessors(
        metaXapply(upModule(M, false), T, L, none, 0, unbounded, 0),
        M,
        T,
        L,
        0
    ) .

    ***( Todo: Fix metaXapply in ceq
    ceq findRuleSuccessors(M, T, L, N) = if stateTransition? :: ResultTriple 
                                        then (getTerm(stateTransition?) , findRuleSuccessors(M, T, L, N + 1)) 
                                        else empty 
                                        fi 
                                        if stateTransition? := metaXapply(upModule(M, false), T, L, none, 0, unbounded, N) .
    eq findRuleSuccessors(M, T, L, N) = empty [owise] .
    )

    ***(
        Recurion to get all possible rule is applied. Start from 0 - the first mached.
    )
    op findRuleSuccessors : Result4Tuple? Qid Term Qid Nat -> TermList  .
    eq findRuleSuccessors(failure, M, T, L, N) = empty .
    eq findRuleSuccessors(RT, M, T, L, N) = getTerm(RT) , findRuleSuccessors(
        metaXapply(upModule(M, false), T, L, none, 0, unbounded, N + 1),
        M,
        T,
        L,
        N + 1
    ) .

    ***(
        A random selecttion from a TermList 
    )
    op nextTerm : TermList Nat -> Term .
    eq nextTerm(empty, N) = empty .
    eq nextTerm(TL, N) = getTermByIndex(TL, N rem sizeTermList(TL)) .

endfm