ABL_with_partial_repayments.cfg

SPECIFICATION Spec

CONSTANTS
    P <- const_P
    C <- const_C
    N <- const_N
    M <- const_M
    RateDue <- const_RateDue
    RateEarly <- const_RateEarly
    RateCollateralPenalty <- const_RateCollateralPenalty
    RatesLate <- const_RatesLate
    S <- const_S
    BLOCKS_IN_PERIOD <- const_BLOCKS_IN_PERIOD
    START_BLOCK <- const_START_BLOCK
    C_UNCOND <- const_C_UNCOND

INVARIANT TypeOK
INVARIANT ConsistentProgress
INVARIANT ConsistentRepayment
INVARIANT ConsistentEnforcement
INVARIANT ConsistentRemainder
INVARIANT ConsistentPeriods

ACTION_CONSTRAINT Logging