emptiness.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 <map>
#include <list>
#include <iosfwd>
#include <bddx.h>
#include <spot/misc/optionmap.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/emptiness_stats.hh>
 
namespace spot
{
  struct twa_run;
  typedef std::shared_ptr<twa_run> twa_run_ptr;
  typedef std::shared_ptr<const twa_run> const_twa_run_ptr;
 
 
  class SPOT_API emptiness_check_result
  {
  public:
    emptiness_check_result(const const_twa_ptr& a,
                           option_map o = option_map())
      : a_(a), o_(o)
    {
    }
 
    virtual
    ~emptiness_check_result()
    {
    }
 
    virtual twa_run_ptr accepting_run();
 
    const const_twa_ptr&
    automaton() const
    {
      return a_;
    }
 
    // / Return the options parameterizing how the accepting run is computed.
    const option_map&
    options() const
    {
      return o_;
    }
 
    const char* parse_options(char* options);
 
    virtual const unsigned_statistics* statistics() const;
 
  protected:
    virtual void options_updated(const option_map& old);
 
    const_twa_ptr a_;                
    option_map o_;                
  };
 
  typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;
 
  class SPOT_API emptiness_check:
    public std::enable_shared_from_this<emptiness_check>
  {
  public:
    emptiness_check(const const_twa_ptr& a, option_map o = option_map())
      : a_(a), o_(o)
    {
    }
    virtual ~emptiness_check();
 
    const const_twa_ptr&
    automaton() const
    {
      return a_;
    }
 
    const option_map&
    options() const
    {
      return o_;
    }
 
    const char* parse_options(char* options);
 
    virtual bool safe() const;
 
    virtual emptiness_check_result_ptr check() = 0;
 
    virtual const unsigned_statistics* statistics() const;
 
    virtual const ec_statistics* emptiness_check_statistics() const;
 
    virtual std::ostream& print_stats(std::ostream& os) const;
 
    virtual void options_updated(const option_map& old);
 
  protected:
    const_twa_ptr a_;                
    option_map o_;                
  };
 
  typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;
 
  class emptiness_check_instantiator;
  typedef std::shared_ptr<emptiness_check_instantiator>
    emptiness_check_instantiator_ptr;
 
  class SPOT_API emptiness_check_instantiator
  {
  public:
    emptiness_check_ptr instantiate(const const_twa_ptr& a) const;
 
    const option_map&
    options() const
    {
      return o_;
    }
 
    option_map&
    options()
    {
      return o_;
    }
 
    unsigned int min_sets() const;
 
    unsigned int max_sets() const;
  protected:
    emptiness_check_instantiator(option_map o, void* i);
 
    option_map o_;
    void *info_;
  };
 
  SPOT_API emptiness_check_instantiator_ptr
  make_emptiness_check_instantiator(const char* name, const char** err);
 
 
 
 
 
  struct SPOT_API twa_run final
  {
    struct step {
      const state* s;
      bdd label;
      acc_cond::mark_t acc;
 
      step(const state* s, bdd label, acc_cond::mark_t acc) noexcept
        : s(s), label(label), acc(acc)
      {
      }
      step() = default;
    };
 
    typedef std::list<step> steps;
 
    steps prefix;
    steps cycle;
    const_twa_ptr aut;
 
    ~twa_run();
    twa_run(const const_twa_ptr& aut) noexcept
      : aut(aut)
    {
    }
    twa_run(const twa_run& run);
    twa_run& operator=(const twa_run& run);
 
    void ensure_non_empty_cycle(const char* where) const;
 
    twa_run_ptr reduce() const;
 
    twa_run_ptr project(const const_twa_ptr& other, bool right = false);
 
    bool replay(std::ostream& os, bool debug = false) const;
 
    void highlight(unsigned color);
 
    twa_graph_ptr as_twa(bool preserve_names = false) const;
 
    SPOT_API
    friend std::ostream& operator<<(std::ostream& os, const twa_run& run);
  };
 
}