spot/spot/twaalgos/word.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 <spot/twaalgos/emptiness.hh>

namespace spot
{
  /// \brief An infinite word stored as a lasso.
  ///
  /// This is not exactly a word in the traditional sense because we
  /// use boolean formulas instead of letters.  So technically a
  /// twa_word can represent a set of words.
  ///
  /// This class only represent lasso-shaped words using two list of
  /// BDDs: one list of the prefix, one list for the cycle.
  struct SPOT_API twa_word final
  {
    twa_word(const bdd_dict_ptr& dict) noexcept;
    twa_word(const twa_run_ptr& run) noexcept;
    ~twa_word()
    {
      dict_->unregister_all_my_variables(this);
    }

    /// \brief Simplify a lasso-shaped word.
    ///
    /// The simplified twa_word may represent a subset of the actual
    /// words represented by the original twa_word.  The typical
    /// use-case is that a counterexample generated by an
    /// emptiness-check was converted into a twa_word (maybe accepting
    /// several words) and we want to present a simpler word as a
    /// counterexample to the user.   ltlcross does that, for instance.
    ///
    /// This method performs three reductions:
    ///
    /// - If all the formulas on the cycle are compatible, the cycle
    /// will be reduced to a loop with the intersection of all
    /// formulas.
    ///
    /// - If the end of the prefix can be folded into the cycle,
    /// remove those letters, and rotate the cycle accordingly.
    ///
    /// - If any formula contains a disjunction, replace it by a
    /// single operand.
    void simplify();

    /// \brief Use all atomic proposition.
    ///
    /// Make sure each letters actually use all variables in \a aps.
    /// By default, missing variables are introduced as negative,
    /// but setting \a positive to true will reverse that.
    void use_all_aps(bdd aps, bool positive = false);

    typedef std::list<bdd> seq_t;
    seq_t prefix;
    seq_t cycle;

    bdd_dict_ptr get_dict() const
    {
      return dict_;
    }

    /// \brief Convert the twa_word as an automaton.
    ///
    /// Convert the twa_word into a lasso-shaped automaton
    /// with "true" acceptance condition.
    ///
    /// This is useful to evaluate a word on an automaton.
    twa_graph_ptr as_automaton() const;

    /// \brief Check if a the twa_word intersect another automaton.
    ///
    /// If the twa_word actually represent a word (i.e., if each
    /// Boolean formula that label its steps have a unique satisfying
    /// valuation), this is equivalent to a membership test.
    bool intersects(const_twa_ptr aut) const
    {
      return as_automaton()->intersects(aut);
    }

    /// \brief Print a twa_word
    ///
    /// Words are printed as
    /// \code
    /// BF;BF;...;BF;cycle{BF;BF;...;BF}
    /// \endcode
    ///
    /// where BF denote Boolean Formulas.  The prefix part (before
    /// cycle{...}) can be empty.  The cycle part (inside cycle{...})
    /// may not be empty.
    SPOT_API
    friend std::ostream& operator<<(std::ostream& os, const twa_word& w);
  private:
    bdd_dict_ptr dict_;
  };

  /// \brief Create an empty twa_word
  ///
  /// Note that empty twa_word are invalid and cannot be printed.
  /// After creating an empty twa_word, you should at least populate
  /// the cycle.
  inline twa_word_ptr make_twa_word(const bdd_dict_ptr& dict)
  {
    return std::make_shared<twa_word>(dict);
  }

  /// Create a twa_word from a twa_run
  inline twa_word_ptr make_twa_word(const twa_run_ptr& run)
  {
    return std::make_shared<twa_word>(run);
  }

  /// \brief Parse a twa_word.
  ///
  /// The input should have the form
  /// \code
  /// BF;BF;...;BF;cycle{BF;BF;...;BF}
  /// \endcode
  /// where BF can be any Boolean formula, and the prefix
  /// sequence (before cycle{...}) may be empty.
  ///
  /// \param word the string to parse
  /// \param dict the bdd_dict where atomic propositions should be registered
  SPOT_API
  twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict);
}