From f0b1b9438f6dd7116bc043f66ef3cbafc4b80e36 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 Feb 2015 22:59:33 +0100 Subject: [PATCH] Prefix many algorithms with runtime_error for unexpected acceptance * src/tgba/tgbagraph.cc (merge_transitions): Disable acceptance merging if Fin acceptance is used. * src/tgbaalgos/degen.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc: Throw an exception if an unsupported type of acceptance is received. --- src/tgba/tgbagraph.cc | 8 ++++++-- src/tgbaalgos/degen.cc | 4 ++++ src/tgbaalgos/dtbasat.cc | 7 +++++-- src/tgbaalgos/dtgbasat.cc | 3 +++ src/tgbaalgos/isweakscc.cc | 7 ++++++- src/tgbaalgos/lbtt.cc | 4 ++++ src/tgbaalgos/minimize.cc | 4 ++++ src/tgbaalgos/neverclaim.cc | 4 +++- src/tgbaalgos/safety.cc | 8 ++++++++ src/tgbaalgos/sccfilter.cc | 6 +++++- src/tgbaalgos/simulation.cc | 4 ++++ 11 files changed, 52 insertions(+), 7 deletions(-) diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc index a27016789..ac6535089 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/tgba/tgbagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de // l'Epita. // // This file is part of Spot, a model checking library. @@ -83,7 +83,11 @@ namespace spot tend = out; out = in = 2; - if (in < tend) + // FIXME: We could should also merge transitions when using + // fin_acceptance, but the rule for Fin sets are different than + // those for Inf sets, (and we need to be careful if a set is used + // both as Inf and Fin) + if ((in < tend) && !acc().uses_fin_acceptance()) { typedef graph_t::trans_storage_t tr_t; g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs) diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 712d0c030..881343d4f 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -190,6 +190,10 @@ namespace spot bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels) { + if (!a->acc().is_generalized_buchi()) + throw std::runtime_error + ("degeneralize() can only work with generalized Büchi acceptance"); + bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl; bdd_dict_ptr dict = a->get_dict(); diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index c581d7361..fefff6535 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -739,6 +739,9 @@ namespace spot dtba_sat_synthetize(const const_tgba_digraph_ptr& a, int target_state_number, bool state_based) { + if (!a->acc().is_buchi()) + throw std::runtime_error + ("dtba_sat() can only work with Büchi acceptance"); if (target_state_number == 0) return nullptr; trace << "dtba_sat_synthetize(..., states = " << target_state_number diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index dbfc0c661..1798a91ff 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -877,6 +877,9 @@ namespace spot unsigned target_acc_number, int target_state_number, bool state_based) { + if (!a->acc().is_generalized_buchi()) + throw std::runtime_error + ("dtgba_sat() can only work with generalized Büchi acceptance"); if (target_state_number == 0) return nullptr; trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index edcf540ae..d5229e961 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -67,6 +67,10 @@ namespace spot bool is_inherently_weak_scc(scc_info& map, unsigned scc) { + if (!map.get_aut()->acc().uses_fin_acceptance()) + throw std::runtime_error + ("is_inherently_weak_scc() cannot work with Fin acceptance"); + // If no cycle is accepting, the SCC is weak. if (!map.is_accepting_scc(scc)) return true; @@ -81,7 +85,8 @@ namespace spot is_weak_scc(scc_info& map, unsigned scc) { // If no cycle is accepting, the SCC is weak. - if (!map.is_accepting_scc(scc)) + if (!map.is_accepting_scc(scc) + && !map.get_aut()->acc().uses_fin_acceptance()) return true; // If all transitions use the same acceptance set, the SCC is weak. return map.used_acc_of(scc).size() == 1; diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 2fae7df41..f3db37255 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -135,6 +135,10 @@ namespace spot std::ostream& lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba) { + if (!g->acc().is_generalized_buchi()) + throw std::runtime_error + ("LBTT only supports generalized Büchi acceptance"); + lbtt_bfs b(g, os, sba); b.run(); return os; diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 0ee4b7a73..d9d61a52e 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -493,6 +493,10 @@ namespace spot tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a) { + if (a->acc().uses_fin_acceptance()) + throw std::runtime_error + ("minimize_wdba cannot work with Fin acceptance"); + hash_set* final = new hash_set; hash_set* non_final = new hash_set; diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 90ad8becb..66bbf73ae 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -204,7 +204,9 @@ namespace spot never_claim_reachable(std::ostream& os, const const_tgba_ptr& g, const char* options) { - assert(g->acc().num_sets() <= 1); + if (!(g->acc().is_buchi() || g->acc().is_true())) + throw std::runtime_error + ("Never claim output only supports Büchi acceptance"); never_claim_output d(os, options); auto aut = std::dynamic_pointer_cast(g); if (!aut) diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index ecd02dfd7..72127c239 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -27,6 +27,10 @@ namespace spot is_guarantee_automaton(const const_tgba_digraph_ptr& aut, const scc_info* si) { + if (aut->acc().uses_fin_acceptance()) + throw std::runtime_error + ("is_guarantee_automaton() does not support Fin acceptance"); + // Create an scc_info if the user did not give one to us. bool need_si = !si; if (need_si) @@ -64,6 +68,10 @@ namespace spot bool is_safety_mwdba(const const_tgba_digraph_ptr& aut) { + if (!(aut->acc().is_buchi() || aut->acc().is_true())) + throw std::runtime_error + ("is_safety_mwdba() should be called on a Buchi automaton"); + for (auto& t: aut->transitions()) if (!aut->acc().accepting(t.acc)) return false; diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 8ad356225..8f50f63c7 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -249,8 +249,12 @@ namespace spot template tgba_digraph_ptr scc_filter_apply(const_tgba_digraph_ptr aut, - scc_info* given_si, Args&&... args) + scc_info* given_si, Args&&... args) { + if (!aut->acc().is_generalized_buchi()) + throw std::runtime_error + ("scc_filter() works only with generalized Büchi acceptance"); + tgba_digraph_ptr filtered = make_tgba_digraph(aut->get_dict()); unsigned in_n = aut->num_states(); // Number of input states. if (in_n == 0) // Nothing to filter. diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 2b7714828..bd2196103 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -188,6 +188,10 @@ namespace spot all_class_var_(bddtrue), original_(in) { + if (in->acc().uses_fin_acceptance()) + throw std::runtime_error + ("direct_simulation() does not yet support Fin acceptance"); + // Call get_init_state_number() before anything else as it // might add a state. unsigned init_state_number = in->get_init_state_number();