fmod MUX is
    protecting INT .

    sort BoolStr .
    
    op _(_) : BoolStr Int -> Bool .
    op mux : BoolStr BoolStr BoolStr -> BoolStr .
    
    vars X Y B : BoolStr .
    var T : Int .
    
    ceq mux(X,Y,B)(T) = X(T) if B(T) == true .
    ceq mux(X,Y,B)(T) = Y(T) if B(T) == false .
endfm

fmod MUX-RUN is
    protecting MUX .
    
    ops a b c : -> BoolStr .
    
    *** a and b are data streams
    eq a(0) = true .
    eq a(1) = false .
    eq a(2) = true .
    eq a(3) = false .
    
    eq b(0) = false .
    eq b(1) = true .
    eq b(2) = false .
    eq b(3) = true .
    
    *** c is the control stream
    eq c(0) = true .
    eq c(1) = true .
    eq c(2) = false .
    eq c(3) = false .
endfm

*** value at time 0 - should be true
red mux(a,b,c)(0) .

*** value at time 1 - should be false
red mux(a,b,c)(1) .

*** value at time 2 - should be false
red mux(a,b,c)(2) .

*** value at time 3 - should be true
red mux(a,b,c)(3) .