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

sat: reject alternating inputs

Browse source 
* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-18 08:08:08 +01:00
parent 5939ca4e85
commit d80ca1fb47
2 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
spot/twaalgos/dtbasat.cc
View file

@ -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

3
spot/twaalgos/dtwasat.cc
View file

@ -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