Implement stable failures and impossible futures refinement#77

Merged

mlaveaux merged 64 commits intoMERCorg:mainfrom

mlaveaux:feature/impossible-futures

Mar 31, 2026

Commits on Mar 15, 2026

Added set difference to the VecSet implementation
mlaveaux
committed
Added extend to vecset.
mlaveaux
committed
Made the antichain based product construction generic, and implement stable failures refinement.
mlaveaux
committed
Moved the merging and counter example construction to a central location
mlaveaux
committed
Fixed the interface of merc-lts.
mlaveaux
committed
Implemented a first variant of the impossible futures algorithm.
mlaveaux
committed
Generate counter examples for stable failures and impossible futures.
mlaveaux
committed
Allow the is_refinement_generic to return a counter example for the inner check as well (this is needed for stable failures and impossible futures).
mlaveaux
committed
This function is actually used in compare
mlaveaux
committed
Added the function bdd_from_cube to generate a BDD from a bitvector.
mlaveaux
committed
Fixed the implementation of weak trace refinement
mlaveaux
committed
Set a proper name for the dump directory in each refinement test
mlaveaux
committed

Commits on Mar 18, 2026

Commits on Mar 19, 2026

Commits on Mar 30, 2026

Commits on Mar 31, 2026