diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index b4960939c..8df858da5 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -296,9 +296,9 @@ namespace spot virtual const twa_graph_state* get_init_state() const override { unsigned n = get_init_state_number(); - if (SPOT_UNLIKELY(is_univ_dest(n))) + if (SPOT_UNLIKELY(is_alternating())) throw std::runtime_error - ("get_init_state() does not work with universal initial states"); + ("the abstract interface does not support alternating automata"); return state_from_number(n); } diff --git a/spot/twaalgos/are_isomorphic.cc b/spot/twaalgos/are_isomorphic.cc index 127b5c6fa..fbb327822 100644 --- a/spot/twaalgos/are_isomorphic.cc +++ b/spot/twaalgos/are_isomorphic.cc @@ -132,6 +132,9 @@ namespace spot bool isomorphism_checker::is_isomorphic_(const const_twa_graph_ptr aut) { + if (aut->is_alternating()) + throw std::runtime_error + ("isomorphism_checker does not yet support alternation"); trival autdet = aut->prop_deterministic(); if (ref_deterministic_) { diff --git a/spot/twaalgos/canonicalize.cc b/spot/twaalgos/canonicalize.cc index 3870c5449..5bc93235b 100644 --- a/spot/twaalgos/canonicalize.cc +++ b/spot/twaalgos/canonicalize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et // Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -73,6 +73,9 @@ namespace spot twa_graph_ptr canonicalize(twa_graph_ptr aut) { + if (aut->is_alternating()) + throw std::runtime_error + ("canonicalize does not yet support alternation"); std::vector state2class(aut->num_states(), 0); state2class[aut->get_init_state_number()] = 1; size_t distinct_classes = 2; diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index 689d6c537..fb67593f4 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -219,6 +219,9 @@ namespace spot state_t initial_state(const const_twa_graph_ptr& twa_p) { + if (twa_p->is_alternating()) + throw std::runtime_error + ("couvreur99_new does not support alternation"); return twa_p->get_init_state_number(); } diff --git a/spot/twaalgos/cycles.cc b/spot/twaalgos/cycles.cc index b4bb7a519..2d52aaeed 100644 --- a/spot/twaalgos/cycles.cc +++ b/spot/twaalgos/cycles.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -27,6 +27,9 @@ namespace spot info_(aut_->num_states(), aut_->num_states()), sm_(map) { + if (aut_->is_alternating()) + throw std::runtime_error + ("enumerate_cycles does not support alternation"); } void diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index c9ae1b9cc..c47b19836 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -197,6 +197,9 @@ namespace spot if (!a->acc().is_generalized_buchi()) throw std::runtime_error ("degeneralize() can only works with generalized Büchi acceptance"); + if (a->is_alternating()) + throw std::runtime_error + ("degeneralize() does not support alternation"); bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl; diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 068b59cae..c18230d1c 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -579,6 +579,9 @@ namespace spot bool pretty_print, bool use_scc, bool use_simulation, bool use_stutter) { + if (a->is_alternating()) + throw std::runtime_error + ("tgba_determinize() does not support alternation"); if (a->prop_deterministic()) return std::const_pointer_cast(a); diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index 8a6073160..c481a910c 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -37,6 +37,10 @@ namespace spot // we used to have, was motivated by issue #188. bool is_unambiguous(const const_twa_graph_ptr& aut) { + if (aut->is_alternating()) + throw std::runtime_error + ("is_unambiguous() does not support alternation"); + trival u = aut->prop_unambiguous(); if (u.is_known()) return u.is_true(); diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc index e7ab80ba1..b9c03cb3f 100644 --- a/spot/twaalgos/isweakscc.cc +++ b/spot/twaalgos/isweakscc.cc @@ -26,9 +26,12 @@ namespace spot bool scc_has_rejecting_cycle(scc_info& map, unsigned scc) { + auto aut = map.get_aut(); + if (aut->is_alternating()) + throw std::runtime_error + ("scc_has_rejecting_cycle() does not support alternation"); // We check that by cloning the SCC and complementing its // acceptance condition. - auto aut = map.get_aut(); std::vector keep(aut->num_states(), false); auto& states = map.states_of(scc); for (auto s: states) @@ -42,6 +45,9 @@ namespace spot bool is_inherently_weak_scc(scc_info& map, unsigned scc) { + if (map.get_aut()->is_alternating()) + throw std::runtime_error + ("is_inherently_weak_scc() does not support alternation"); // Weak SCCs are inherently weak. if (is_weak_scc(map, scc)) return true; @@ -54,6 +60,10 @@ namespace spot bool is_weak_scc(scc_info& map, unsigned scc) { + if (map.get_aut()->is_alternating()) + throw std::runtime_error + ("is_weak_scc() does not support alternation"); + // Rejecting SCCs are weak. if (map.is_rejecting_scc(scc)) return true; @@ -65,6 +75,9 @@ namespace spot is_complete_scc(scc_info& map, unsigned scc) { auto a = map.get_aut(); + if (a->is_alternating()) + throw std::runtime_error + ("is_complete_scc() does not support alternation"); for (auto s: map.states_of(scc)) { bool has_succ = false; @@ -86,6 +99,10 @@ namespace spot bool is_terminal_scc(scc_info& map, unsigned scc) { + if (map.get_aut()->is_alternating()) + throw std::runtime_error + ("is_terminal_scc() does not support alternation"); + // If all transitions use all acceptance conditions, the SCC is weak. return (map.is_accepting_scc(scc) && map.used_acc_of(scc).size() == 1 diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 7218e2150..83b5404a5 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -43,6 +43,10 @@ namespace spot twa_graph_ptr& cpy, Trans trans, unsigned int init) { + if (old->is_alternating()) + throw std::runtime_error + ("transform_accessible() does not support alternation"); + std::vector todo; std::vector seen(old->num_states(), -1U); @@ -101,6 +105,10 @@ namespace spot twa_graph_ptr& cpy, Trans trans, unsigned int init) { + if (old->is_alternating()) + throw std::runtime_error + ("transform_copy() does not support alternation"); + // Each state in cpy corresponds to a unique state in old. cpy->new_states(old->num_states()); cpy->set_init_state(init); diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index a164a90e2..4bf78f32c 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -474,6 +474,10 @@ namespace spot twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a) { + if (a->is_alternating()) + throw std::runtime_error + ("minimize_monitor() does not support alternation"); + hash_set* final = new hash_set; hash_set* non_final = new hash_set; twa_graph_ptr det_a = tgba_powerset(a); @@ -491,6 +495,10 @@ namespace spot twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a) { + if (a->is_alternating()) + throw std::runtime_error + ("minimize_wdba() does not support alternation"); + hash_set* final = new hash_set; hash_set* non_final = new hash_set; @@ -605,6 +613,10 @@ namespace spot const_twa_graph_ptr aut_neg_f, bool reject_bigger) { + if (aut_f->is_alternating()) + throw std::runtime_error + ("minimize_obligation() does not support alternation"); + auto min_aut_f = minimize_wdba(aut_f); if (reject_bigger) diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index f7ddd9496..cd3752aca 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -46,6 +46,9 @@ namespace spot unsigned right_state, bool and_acc) { + if (left->is_alternating() || right->is_alternating()) + throw std::runtime_error + ("product() does not support alternating automata"); std::unordered_map s2n; std::deque> todo; diff --git a/spot/twaalgos/randomize.cc b/spot/twaalgos/randomize.cc index b00e71bf1..963751101 100644 --- a/spot/twaalgos/randomize.cc +++ b/spot/twaalgos/randomize.cc @@ -29,6 +29,10 @@ namespace spot randomize(twa_graph_ptr& aut, bool randomize_states, bool randomize_edges) { + if (aut->is_alternating()) + throw std::runtime_error + ("randomize() does not yet support alternation"); + if (!randomize_states && !randomize_edges) return; auto& g = aut->get_graph(); diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 8a0e1276c..11525d38c 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -29,6 +29,9 @@ namespace spot { if (old->prop_state_acc()) return old; + if (old->is_alternating()) + throw std::runtime_error + ("sbacc() does not support alternation"); scc_info si(old); diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 5cff2cd42..d3f7a1985 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -276,6 +276,10 @@ namespace spot twa_graph_ptr scc_filter_apply(const_twa_graph_ptr aut, scc_info* given_si, Args&&... args) { + if (aut->is_alternating()) + throw std::runtime_error + ("scc_filter() does yet not support alternation"); + unsigned in_n = aut->num_states(); twa_graph_ptr filtered = make_twa_graph(aut->get_dict()); diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index ba3d66488..541118274 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -160,6 +160,9 @@ namespace spot if (!has_separate_sets(in)) throw std::runtime_error ("direct_simulation() requires separate Inf and Fin sets"); + if (in->is_alternating()) + throw std::runtime_error + ("direct_simulation() does not yet support alternation"); scc_info_.reset(new scc_info(in));