From a6aa799a17f4d5860c8fce24891ff8216226323e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 30 Jul 2021 11:18:57 +0200 Subject: [PATCH] adjust for BuDDy change * spot/twaalgos/mealy_machine.cc, python/buddy.i: Rename bdd_has_common_assignement to bdd_have_common_assignment. --- python/buddy.i | 6 +++--- spot/twaalgos/mealy_machine.cc | 12 ++++++------ 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/python/buddy.i b/python/buddy.i index 423e2e5d5..b0068dfaa 100644 --- a/python/buddy.i +++ b/python/buddy.i @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2014, 2016 Laboratoire de Recherche et -// Développement de l'EPITA. +// Copyright (C) 2010, 2011, 2012, 2014, 2016, 2021 Laboratoire de +// Recherche et Développement de l'EPITA. // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -188,7 +188,7 @@ double bdd_satcountlnset(const bdd &r, const bdd &varset); int bdd_nodecount(const bdd &r); int* bdd_varprofile(const bdd &r); double bdd_pathcount(const bdd &r); -int bdd_has_common_assignement(const bdd &l, const bdd &r); +int bdd_have_common_assignment(const bdd &l, const bdd &r); void bdd_fprinttable(FILE *file, const bdd &r); void bdd_printtable(const bdd &r); void bdd_fprintset(FILE *file, const bdd &r); diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index fa105ef7c..b687218de 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -975,7 +975,7 @@ namespace if (p1.second > p2.second) continue; inc_player.set(p1.second, p2.second, - !bdd_has_common_assignement( + !bdd_have_common_assignment( bdd_from_int((int) p1.first), bdd_from_int((int) p2.first))); assert(inc_player.get(p1.second, p2.second) @@ -1005,7 +1005,7 @@ namespace if (!is_p_incomp(e1.dst - n_env, e2.dst - n_env)) continue; //Compatible -> no prob // Reachable under same letter? - if (bdd_has_common_assignement(e1.cond, e2.cond)) + if (bdd_have_common_assignment(e1.cond, e2.cond)) { trace << s1 << " and " << s2 << " directly incomp " "due to successors " << e1.dst << " and " << e2.dst @@ -1039,7 +1039,7 @@ namespace // Have already been treated continue; // Now we need to actually check it - if (bdd_has_common_assignement(ei.cond, ej.cond)) + if (bdd_have_common_assignment(ei.cond, ej.cond)) { trace << ei.dst << " and " << ej.dst << " tagged incomp" " due to " << i << " and " << j << '\n'; @@ -3088,7 +3088,7 @@ namespace false); if (inserted) it->second = - bdd_has_common_assignement(c_list1[c1_idx], + bdd_have_common_assignment(c_list1[c1_idx], c_list2[c2_idx]); if (!it->second) incomp_cubes_list.emplace_back((int) c1_idx, @@ -3673,7 +3673,7 @@ namespace spot { // check if el_env.cond intersects with the unspecified of // sr. If so the sequence is not applicable -> false - if (bdd_has_common_assignement(ucr[sr], el_env.cond)) + if (bdd_have_common_assignment(ucr[sr], el_env.cond)) { if (verbose) std::cerr << "State " << sl << " of left is not completely" @@ -3688,7 +3688,7 @@ namespace spot { // if they can be taken at the same time, the output // of r must implies the one of left - if (bdd_has_common_assignement(el_env.cond, er_env.cond)) + if (bdd_have_common_assignment(el_env.cond, er_env.cond)) { const auto& er_p = get_p_edge_r(er_env); if (!bdd_implies(er_p.cond, el_p.cond))