fmod IPS is
    protecting INT .

    sort IntStr .
    sort IPSTuple .
    sort IPSstr .

    op _(_) : IPSstr Int -> IPSTuple [prec 1] .
    op _(_) : IntStr Int -> Int [prec 1] .

    op U : -> Int .

    op _,_,_ : Int Int Int -> IPSTuple .
    op _,_,_ : IntStr IntStr IntStr -> IPSstr .

    *** Think of this as a next-state function
    op ips : IPSTuple -> IPSTuple .

    vars A B C : Int .
    var T : Int .

    *** Equations for the IPS next-state function
    ceq ips(A,B,C) = (U,U,U) if (A == U) or (B == U) or (C == U) .
    eq ips(A,B,C) = (A, B, A * B + C) [owise] .

endfm

fmod CONV-IMP is
    protecting IPS .

    sort ConvState .

    op _,_,_,_ : IPSTuple IPSTuple IPSTuple IPSTuple -> ConvState .

    op convImp : Int IntStr -> ConvState .
    ops conv1 conv2 conv3 conv4 : Int IntStr -> IPSTuple .
    ops W4 W3 W2 W1 : -> Int .

    op C : IPSTuple -> Int .

    var X : IntStr .
    var T : Int .
    vars I J K : Int .

    eq W1 = 1 .
    eq W2 = -1 .
    eq W3 = 1 .
    eq W4 = -1 .

    eq C(I,J,K) = K .

    eq convImp(T,X) = (conv1(T,X), conv2(T,X), conv3(T,X), conv4(T,X)) .

    eq conv1(T,X) = ips(W1,X(T - 3),0) .
    eq conv2(T,X) = ips(W2,X(T - 2), C(conv1(T - 1, X))) .
    eq conv3(T,X) = ips(W3,X(T - 1), C(conv2(T - 1, X)) . *** Missing bracket
    eq conv4(T,X) = ips(W4,X(T), C(conv3(T - 1, X))) .
endfm