---------------------------- MODULE CostAlgebraMC ----------------------------
EXTENDS CostAlgebra
VARIABLE sample

Cases == {
    [base |-> -2, increases |-> <<3>>, reductions |-> <<>>, expected |-> 1],
    [base |-> 3, increases |-> <<>>, reductions |-> <<5>>, expected |-> 0],
    [base |-> 0, increases |-> <<>>, reductions |-> <<>>, expected |-> 0],
    [base |-> 4, increases |-> <<1, 2>>, reductions |-> <<3>>, expected |-> 4],
    [base |-> -3, increases |-> <<1>>, reductions |-> <<>>, expected |-> 0],
    [base |-> 2, increases |-> <<>>, reductions |-> <<1>>, expected |-> 1]
}

Init == sample \in Cases
Next == UNCHANGED sample
Spec == Init /\ [][Next]_sample
ArithmeticExamples ==
    ModifiedCost(sample.base, sample.increases, sample.reductions) = sample.expected
=============================================================================