gtec.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// 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 <stack>
#include <spot/twaalgos/gtec/status.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/emptiness_stats.hh>
 
namespace spot
{
 
 
  SPOT_API emptiness_check_ptr
  couvreur99(const const_twa_ptr& a, option_map options = option_map());
 
#ifndef SWIG
  class SPOT_API couvreur99_check:
    // We inherit from ec_statistics first to work around GCC bug #90309.
    // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=90309#c6
    public ec_statistics, public emptiness_check
  {
  public:
    couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
 
    virtual ~couvreur99_check();
 
    virtual emptiness_check_result_ptr check() override;
 
    virtual std::ostream& print_stats(std::ostream& os) const override;
 
    std::shared_ptr<const couvreur99_check_status> result() const;
 
  protected:
    std::shared_ptr<couvreur99_check_status> ecs_;
    void remove_component(const state* start_delete);
 
    bool poprem_;
    unsigned removed_components;
 
    unsigned get_removed_components() const;
    unsigned get_vmsize() const;
  };
 
  class SPOT_API couvreur99_check_shy final: public couvreur99_check
  {
  public:
    couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map());
    virtual ~couvreur99_check_shy();
 
    virtual emptiness_check_result_ptr check() override;
 
  protected:
    struct successor {
      acc_cond::mark_t acc; 
      const spot::state* s; 
      successor(acc_cond::mark_t acc, const spot::state* s) noexcept
        : acc(acc), s(s) {}
    };
 
    // We use five main data in this algorithm:
    // * couvreur99_check::root, a stack of strongly connected components (SCC),
    // * couvreur99_check::h, a hash of all visited nodes, with their order,
    //   (it is called "Hash" in Couvreur's paper)
    // * arc, a stack of acceptance conditions between each of these SCC,
    std::stack<acc_cond::mark_t> arc; 
    // * num, the number of visited nodes.  Used to set the order of each
    //   visited node,
    int num; 
    // * todo, the depth-first search stack.  This holds pairs of the
    //   form (STATE, SUCCESSORS) where SUCCESSORS is a list of
    //   (ACCEPTANCE_CONDITIONS, STATE) pairs.
    typedef std::list<successor> succ_queue;
 
    // Position in the loop seeking known successors.
    succ_queue::iterator pos; 
 
    struct todo_item
    {
      const state* s; 
      int n; 
      succ_queue q; 
      todo_item(const state* s, int n, couvreur99_check_shy* shy);
    };
 
    typedef std::list<todo_item> todo_list;
    todo_list todo; 
 
    void clear_todo();
 
    bool group_;
    // If the "group2" option is set (it implies "group"), we
    // reprocess the successor states of SCC that have been merged.
    bool group2_;
  };
#endif
 
}