Operation - on FBag incorrect

[jkeiren]

Consider the following excerpt from mcrl2i. This illustrates that the - operation on finite sets has unexpected effects.

mCRL2 interpreter (type h for help)
? e {true:1} - {false:1}
{false: 1, true: 1}

Note that correctness of the operation is dependant on the order of the operands.

mCRL2 interpreter (type h for help)
? e {false:1} - {true:1}
{false: 1}

The issue was observed by @wsinnema.

[jkeiren]

The modified rewrite rule is still not correct. A test case showing this is the following:

mCRL2 interpreter (type h for help)
? e {true:1} - {false:1, true:1}
{true: 1}

The expected output is {:}.

[mlaveaux]

The generate_data_types.py script refuses to run locally (even using python2) so I can not test this, but the rule:

    <(e,d) -> -(@fbag_cons(d,p,b),@fbag_cons(e,q,c)) = @fbag_cons(d,p,-(b,c));

does not take into account that the element d with multiplicity p can still occur in the remainder c. Therefore, it should still take the difference between the left bag and the remainder c, such that rule becomes:

    <(e,d) -> -(@fbag_cons(d,p,b),@fbag_cons(e,q,c)) = -(@fbag_cons(d,p,b), c);

[jkeiren]

@mlaveaux indeed, and I am already working on the fix.

Will commit with tests shortly.