From d80ca1fb47405a26eb16a8b05de2e369750063f5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Jan 2017 08:08:08 +0100 Subject: [PATCH] sat: reject alternating inputs * spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Here. --- spot/twaalgos/dtbasat.cc | 9 ++++++--- spot/twaalgos/dtwasat.cc | 3 +++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index b3b31e195..e9b2e029e 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche +// et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -715,9 +715,12 @@ namespace spot dtba_sat_synthetize(const const_twa_graph_ptr& a, int target_state_number, bool state_based) { + if (a->is_alternating()) + throw std::runtime_error + ("dtba_sat_synthetize() does not support alternating automata"); if (!a->acc().is_buchi()) throw std::runtime_error - ("dtba_sat() can only work with Büchi acceptance"); + ("dtba_sat_synthetize() 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/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index bcbf1171d..38547ebbf 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -992,6 +992,9 @@ namespace spot int target_state_number, bool state_based, bool colored) { + if (a->is_alternating()) + throw std::runtime_error + ("dtwa_sat_synthetize() does not support alternating automata"); if (target_state_number == 0) return nullptr; trace << "dtwa_sat_synthetize(..., nacc = " << target_acc_number