randomltl.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/tl/apcollect.hh>
#include <iosfwd>
 
#include <unordered_set>
#include <spot/misc/optionmap.hh>
#include <spot/misc/hash.hh>
#include <spot/tl/simplify.hh>
 
namespace spot
{
  class SPOT_API random_formula
  {
  public:
    random_formula(unsigned proba_size,
                   const atomic_prop_set* ap,
                   const atomic_prop_set* output_ap = nullptr,
                   std::function<bool(formula)> is_output = nullptr):
    proba_size_(proba_size), proba_(new op_proba[proba_size_]), ap_(ap),
    output_ap_(output_ap), is_output_(is_output)
    {
    }
 
    virtual ~random_formula()
    {
      delete[] proba_;
    }
 
    const atomic_prop_set* ap() const
    {
      return ap_;
    }
 
    const atomic_prop_set* output_ap() const
    {
      return output_ap_;
    }
 
    std::function<bool(formula)> is_output_fun() const
    {
      return is_output_;
    }
 
    const atomic_prop_set* patterns() const
    {
      return patterns_;
    }
 
    bool draw_literals() const
    {
      return draw_literals_;
    }
 
    void draw_literals(bool lit)
    {
      draw_literals_ = lit;
    }
 
    formula generate(int n) const;
 
    std::ostream& dump_priorities(std::ostream& os) const;
 
    const char* parse_options(char* options);
 
    bool has_unary_ops() const
    {
      return total_2_ > 0.0;
    }
 
  protected:
    void update_sums();
 
    struct op_proba
    {
      const char* name;
      int min_n;
      double proba;
      typedef formula (*builder)(const random_formula* rl, int n);
      builder build;
      void setup(const char* name, int min_n, builder build);
    };
    unsigned proba_size_;
    op_proba* proba_;
    double total_1_;
    op_proba* proba_2_;
    double total_2_;
    op_proba* proba_2_or_more_;
    double total_2_and_more_;
    const atomic_prop_set* ap_;
    const atomic_prop_set* output_ap_ = nullptr;
    const atomic_prop_set* patterns_ = nullptr;
    std::function<bool(formula)> is_output_ = nullptr;
    bool draw_literals_;
  };
 
 
  class SPOT_API random_ltl: public random_formula
  {
  public:
 
    random_ltl(const atomic_prop_set* ap,
               const atomic_prop_set* output_ap = nullptr,
               std::function<bool(formula)> is_output = nullptr,
               const atomic_prop_set* subformulas = nullptr);
 
  protected:
    void setup_proba_(const atomic_prop_set* patterns);
    random_ltl(int size, const atomic_prop_set* ap,
               const atomic_prop_set* output_ap = nullptr,
               std::function<bool(formula)> is_output = nullptr);
  };
 
  class SPOT_API random_boolean final: public random_formula
  {
  public:
 
    random_boolean(const atomic_prop_set* ap,
                   const atomic_prop_set* output_ap = nullptr,
                   std::function<bool(formula)> is_output = nullptr,
                   const atomic_prop_set* subformulas = nullptr);
  };
 
  class SPOT_API random_sere final: public random_formula
  {
  public:
 
    random_sere(const atomic_prop_set* ap);
 
    random_boolean rb;
  };
 
  class SPOT_API random_psl: public random_ltl
  {
  public:
 
    random_psl(const atomic_prop_set* ap);
 
    random_sere rs;
  };
 
  class SPOT_API randltlgenerator
  {
    typedef std::unordered_set<formula> fset_t;
 
 
  public:
    enum output_type { Bool, LTL, SERE, PSL };
    static constexpr unsigned MAX_TRIALS = 100000U;
 
    randltlgenerator(int aprops_n, const option_map& opts,
                     char* opt_pL = nullptr,
                     char* opt_pS = nullptr,
                     char* opt_pB = nullptr,
                     const atomic_prop_set* subformulas = nullptr,
                     std::function<bool(formula)> is_output = nullptr);
 
    randltlgenerator(atomic_prop_set aprops, const option_map& opts,
                     char* opt_pL = nullptr,
                     char* opt_pS = nullptr,
                     char* opt_pB = nullptr,
                     const atomic_prop_set* subformulas = nullptr,
                     std::function<bool(formula)> is_output = nullptr);
 
    ~randltlgenerator();
 
    formula next();
 
    void dump_ltl_priorities(std::ostream& os);
    void dump_bool_priorities(std::ostream& os);
    void dump_psl_priorities(std::ostream& os);
    void dump_sere_priorities(std::ostream& os);
    void dump_sere_bool_priorities(std::ostream& os);
    void remove_some_props(atomic_prop_set& s);
 
    formula GF_n();
 
  private:
    fset_t unique_set_;
    atomic_prop_set aprops_;
    atomic_prop_set aprops_out_;
 
    int opt_seed_;
    int opt_tree_size_min_;
    int opt_tree_size_max_;
    bool opt_unique_;
    bool opt_wf_;
    int opt_simpl_level_;
    tl_simplifier simpl_;
 
    int output_;
 
    random_formula* rf_ = nullptr;
    random_psl* rp_ = nullptr;
    random_sere* rs_ = nullptr;
  };
 
 
}