stutter.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2014-2017, 2019 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/twa/twagraph.hh>
 
 
namespace spot
{
  SPOT_API twa_graph_ptr
  sl(const_twa_graph_ptr aut);
 
  SPOT_API twa_graph_ptr
  sl2_inplace(twa_graph_ptr aut);
 
  SPOT_API twa_graph_ptr
  sl2(const_twa_graph_ptr aut);
 
  SPOT_API twa_graph_ptr
  closure_inplace(twa_graph_ptr aut);
 
  SPOT_API twa_graph_ptr
  closure(const_twa_graph_ptr aut);
 
  SPOT_API bool
  is_stutter_invariant(formula f, twa_graph_ptr aut_f = nullptr);
 
  SPOT_API bool
  is_stutter_invariant(twa_graph_ptr aut_f,
                       const_twa_graph_ptr aut_nf = nullptr,
                       int algo = 0);
 
  SPOT_API trival
  check_stutter_invariance(twa_graph_ptr aut_f,
                           formula f = nullptr,
                           bool do_not_determinize = false,
                           bool find_counterexamples = false);
 
 
  SPOT_API std::vector<bool>
  stutter_invariant_states(const_twa_graph_ptr pos,
                           const_twa_graph_ptr neg = nullptr);
 
  SPOT_API std::vector<bool>
  stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos);
 
  SPOT_API void
  highlight_stutter_invariant_states(twa_graph_ptr pos,
                                     formula f_pos, unsigned color = 0);
  SPOT_API void
  highlight_stutter_invariant_states(twa_graph_ptr pos,
                                     const_twa_graph_ptr neg = nullptr,
                                     unsigned color = 0);
 
  SPOT_API std::vector<bdd>
  stutter_invariant_letters(const_twa_graph_ptr pos,
                            const_twa_graph_ptr neg = nullptr);
 
  SPOT_API std::vector<bdd>
  stutter_invariant_letters(const_twa_graph_ptr pos, formula f_pos);
 
 
  SPOT_API int
  is_stutter_invariant_forward_closed(twa_graph_ptr aut,
                                      const std::vector<bool>& sistates);
 
  SPOT_API std::vector<bool>
  make_stutter_invariant_forward_closed_inplace
  (twa_graph_ptr aut, const std::vector<bool>& sistates);
 
}