alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

expansions: make signature canonical

Browse source 
Linear forms are now sorted and duplicates are removed
This commit is contained in:
Antoine Martin 2025-03-04 19:20:50 +01:00
parent 4f169ad632
commit 980dc72678
2 changed files with 35 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
spot/tl/expansions.cc
View file

@ -18,9 +18,11 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h" #include "config.h"
#include <algorithm>
#include <spot/misc/minato.hh> #include <spot/misc/minato.hh>
#include <spot/priv/robin_hood.hh> #include <spot/priv/robin_hood.hh>
#include <spot/tl/expansions.hh> #include <spot/tl/expansions.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh> #include <spot/twa/bdddict.hh>
#include <spot/twa/formula2bdd.hh> #include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/remprop.hh> #include <spot/twaalgos/remprop.hh>
@ -495,6 +497,22 @@ namespace spot
} }
exp = exp_new; exp = exp_new;
} }
// sort and remove duplicates from expansion to canonicalize it for
// eventual signature use
if (exp.size() >= 2)
{
std::sort(exp.begin(), exp.end(),
[](const auto& lhs, const auto& rhs) {
bdd_less_than_stable blt;
// first sort by label, then by suffix
if (blt(lhs.first, rhs.first))
return true;
formula_ptr_less_than_bool_first flt;
return flt(lhs.second, rhs.second);
});
exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
}
} }
} }

17
spot/tl/expansions2.cc
View file

@ -18,9 +18,11 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h" #include "config.h"
#include <algorithm>
#include <spot/misc/minato.hh> #include <spot/misc/minato.hh>
#include <spot/priv/robin_hood.hh> #include <spot/priv/robin_hood.hh>
#include <spot/tl/expansions2.hh> #include <spot/tl/expansions2.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh> #include <spot/twa/bdddict.hh>
#include <spot/twa/formula2bdd.hh> #include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/remprop.hh> #include <spot/twaalgos/remprop.hh>
@ -495,6 +497,21 @@ namespace spot
} }
exp = exp_new; exp = exp_new;
} }
// sort expansion to canonicalize it for eventual signature use
if (exp.size() >= 2)
{
std::sort(exp.begin(), exp.end(),
[](const auto& lhs, const auto& rhs) {
bdd_less_than_stable blt;
// first sort by label, then by suffix
if (blt(lhs.first, rhs.first))
return true;
formula_ptr_less_than_bool_first flt;
return flt(lhs.second, rhs.second);
});
exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
}
} }
} }