Weird behaviour with Alloy language

[EMJzero]

I need to include a model written in Alloy (an horrible language that somewhat allows for first-order-logic constructs, don't learn it, trust me, I used it only this once because I was forced to and I regret it) into my latex document, ffcode worked really well untill I started using some more elaborate logical expressions, mainly the second sets of curly brackes that follows each "sig", after that it stops treating the text as code halfway through. I suppose the unconventional syntax causes some kind of issue.

This is only part of the code, but its enough to demonstrate the undesirable behaviour:

\begin{ffcode}
   sig Date {
    unixTime: one Int
    } {
        unixTime >= 0
    }
    //Radomly chosen by Alloy
    one sig Now extends Date {}

    sig Location {}
    sig Email {}
    sig UserName {}
    sig Password {}
    sig CompanyName {}
    sig PaymentMethod {}

    abstract sig Bool {}
    one sig True extends Bool {}
    one sig False extends Bool {}

    sig User {
        userName: one UserName,
        email: one Email,
        password: one Password,
        paymentMethod: one PaymentMethod,
        bookings: set Booking
    } {
        //No user can have two overlapping bookings
        all b1, b2: Booking | (b1 in bookings and b2 in bookings)
        implies
        (b1 = b2 or (b1.startDate.unixTime < b2.startDate.unixTime and b1.endDate.unixTime <= b2.startDate.unixTime) or
        (b2.startDate.unixTime < b1.startDate.unixTime and b2.endDate.unixTime <= b1.startDate.unixTime))
    }

    //Force that a booking of a eMSP is made by a user registered in that eMSP, even tho the eMSP is only one...
    sig Booking {
        startDate: one Date,
        endDate: one Date,
        isActive: one Bool,
        socket: one Socket
    } {
        startDate.unixTime < endDate.unixTime
        and (isActive = True implies startDate.unixTime <= Now.unixTime and Now.unixTime <= endDate.unixTime)
        and (isActive = True implies socket.connectedVehicle != none)
    }

    fact noBookingsWithoutUsers {
        all b: Booking | (one u: User | b in u.bookings)
    }

    fact noExpiredBookings {
        all b: Booking | b.endDate.unixTime >= Now.unixTime
    }

    fact noOverlappingSocketBookings {
        /*
        or ((b1.startDate.unixTime < b2.startDate.unixTime implies b1.endDate.unixTime <= b2.startDate.unixTime) and (b1.startDate.unixTime > b2.startDate.unixTime implies b2.endDate.unixTime <= b1.startDate.unixTime))
        */
        all b1, b2: Booking | (b1 = b2 or b1.socket != b2.socket or (b1.startDate.unixTime < b2.startDate.unixTime and b1.endDate.unixTime <= b2.startDate.unixTime)
        or (b2.startDate.unixTime < b1.startDate.unixTime and b2.endDate.unixTime <= b1.startDate.unixTime))
    }

    run {} for 12 but 6 Int, exactly 3 User, exactly 3 CS, exactly 2 CPMS, exactly 3 Booking
\end{ffcode}

Here is a picture of the unexpected behaviour:

[yegor256]

@EMJzero this looks like a very weird problem indeed. It belongs to the minted package, I think. We only use it, with some pre-configuration. I suggest you wait a bit until we do this: https://github.com/yegor256/ffcode/issues/21 Otherwise, just try to break the code into two parts, maybe it will help.

[EMJzero]

Thank you, after a bit of experimenting I found that, as you suggested, ending and beginning again the ffcode at the right place indeed fixes the issue for now! I will surely give it a try once more when the move to fancyvrb is complete!

As an example, the above code is fixed with:

...
    sig User {
        userName: one UserName,
        email: one Email,
        password: one Password,
        paymentMethod: one PaymentMethod,
        bookings: set Booking
    } {
        //No user can have two overlapping bookings
        all b1, b2: Booking | (b1 in bookings and b2 in bookings)
        implies
        (b1 = b2 or (b1.startDate.unixTime < b2.startDate.unixTime and b1.endDate.unixTime <= b2.startDate.unixTime) or
        (b2.startDate.unixTime < b1.startDate.unixTime and b2.endDate.unixTime <= b1.startDate.unixTime))
    }
\end{ffcode}
\begin{ffcode}

    //Force that a booking of a eMSP is made by a user registered in that eMSP, even tho the eMSP is only one...
    sig Booking {
        startDate: one Date,
        endDate: one Date,
        isActive: one Bool,
        socket: one Socket
    }
...