spins_kripke.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018, 2019, 2020 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/bricks/brick-hash>
#include <spot/bricks/brick-hashset>
#include <spot/kripke/kripke.hh>
#include <spot/ltsmin/spins_interface.hh>
#include <spot/misc/fixpool.hh>
#include <spot/misc/mspool.hh>
#include <spot/misc/intvcomp.hh>
#include <spot/misc/intvcmp2.hh>
#include <spot/twacube/cube.hh>
 
namespace spot
{
  typedef int* cspins_state;
 
  struct cspins_state_equal
  {
    bool operator()(const cspins_state lhs, const cspins_state rhs) const
    {
      return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
    }
  };
 
  struct cspins_state_hash
  {
    size_t operator()(const cspins_state that) const
    {
      return that[0];
    }
  };
 
  class cspins_state_manager final
  {
  public:
    cspins_state_manager(unsigned int state_size, int compress);
 
    int* unbox_state(cspins_state s) const;
 
    cspins_state alloc_setup(int* dst, int* cmp, size_t cmpsize);
 
    void decompress(cspins_state s, int* uncompressed, unsigned size) const;
 
    void  dealloc(cspins_state s);
 
    unsigned int size() const;
 
  private:
    fixed_size_pool<pool_type::Unsafe> p_;
    multiple_size_pool msp_;
    bool compress_;
    const unsigned int state_size_;
    void (*fn_compress_)(const int*, size_t, int*, size_t&);
    void (*fn_decompress_)(const int*, size_t, int*, size_t);
  };
 
  // \brief This structure is used as a parameter during callback when
  // generating states from the shared librarie produced by LTSmin.
  struct inner_callback_parameters
  {
    cspins_state_manager* manager;   // The state manager
    std::vector<cspins_state>* succ; // The successors of a state
    int* compressed;                 // Area to store compressed state
    int* uncompressed;               // Area to store uncompressed state
    bool compress;                   // Should the state be compressed?
    bool selfloopize;                // Should the state be selfloopized
  };
 
  class cspins_iterator final
  {
  public:
    // Inner struct used to pack the various arguments required by the iterator
    struct cspins_iterator_param
    {
      cspins_state s;
      const spot::spins_interface* d;
      cspins_state_manager& manager;
      inner_callback_parameters& inner;
      cube cond;
      bool compress;
      bool selfloopize;
      spot::cubeset& cubeset;
      int dead_idx;
      unsigned tid;
    };
 
    cspins_iterator(const cspins_iterator&) = delete;
    cspins_iterator(cspins_iterator&) = delete;
 
    cspins_iterator(cspins_iterator_param& p);
    void recycle(cspins_iterator_param& p);
    ~cspins_iterator();
 
    void next();
    bool done() const;
    cspins_state state() const;
    cube condition() const;
 
  private:
    unsigned compute_index() const;
 
    inline void setup_iterator(cspins_state s,
                               const spot::spins_interface* d,
                               cspins_state_manager& manager,
                               inner_callback_parameters& inner,
                               cube& cond,
                               bool compress,
                               bool selfloopize,
                               cubeset& cubeset,
                               int dead_idx);
 
    std::vector<cspins_state> successors_;
    unsigned int current_;
    cube cond_;
    unsigned tid_;
  };
 
 
  // A specialisation of the template class kripke that is thread safe.
  template<>
  class kripkecube<cspins_state, cspins_iterator> final
  {
    // Define operators that are available for atomic proposition
     enum class relop
       {
         OP_EQ_VAR,        // 1 == a
         OP_NE_VAR,        // 1 != a
         OP_LT_VAR,        // 1 < a
         OP_GT_VAR,        // 1 > a
         OP_LE_VAR,        // 1 <= a
         OP_GE_VAR,        // 1 >= a
         VAR_OP_EQ,        // a == 1
         VAR_OP_NE,        // a != 1
         VAR_OP_LT,        // a < 1
         VAR_OP_GT,        // a >= 1
         VAR_OP_LE,        // a <= 1
         VAR_OP_GE,        // a >= 1
         VAR_OP_EQ_VAR,    // a == b
         VAR_OP_NE_VAR,    // a != b
         VAR_OP_LT_VAR,    // a < b
         VAR_OP_GT_VAR,    // a > b
         VAR_OP_LE_VAR,    // a <= b
         VAR_OP_GE_VAR,    // a >= b
         VAR_DEAD          // The atomic proposition used to label deadlock
       };
 
    // Structure for complex atomic proposition
    struct one_prop
    {
      int lval;                 // Index of left variable or raw number
      relop op;                 // The operator
      int rval;                 // Index or right variable or raw number
    };
 
    // Data structure to store complex atomic propositions
    typedef std::vector<one_prop> prop_set;
    prop_set pset_;
 
  public:
    kripkecube(spins_interface_ptr sip, bool compress,
               std::vector<std::string> visible_aps,
               bool selfloopize, std::string dead_prop,
               unsigned int nb_threads);
    ~kripkecube();
    cspins_state initial(unsigned tid);
    std::string to_string(const cspins_state s, unsigned tid = 0) const;
    cspins_iterator* succ(const cspins_state s, unsigned tid);
    void recycle(cspins_iterator* it, unsigned tid);
 
    const std::vector<std::string> ap();
 
    unsigned get_threads();
 
  private:
    void match_aps(std::vector<std::string>& aps, std::string dead_prop);
 
    void compute_condition(cube c, cspins_state s, unsigned tid = 0);
 
    spins_interface_ptr sip_;        // The interface to the shared library
    const spot::spins_interface* d_; // To avoid numerous sip_.get()
    cspins_state_manager* manager_;  // One manager per thread
    bool compress_;                  // Should a compression be performed
 
    // One per threads to store no longer used iterators (and save memory)
    std::vector<std::vector<cspins_iterator*>> recycle_;
 
    inner_callback_parameters* inner_; // One callback per thread
    cubeset cubeset_;                  // A single cubeset to manipulate cubes
    bool selfloopize_;                 // Should selfloopize be performed
    int dead_idx_;                     // If yes, index of the "dead ap"
    std::vector<std::string> aps_;     // All the atomic propositions
    unsigned int nb_threads_;          // The number of threads used
  };
 
  typedef std::shared_ptr<spot::kripkecube<spot::cspins_state,
                                           spot::cspins_iterator>>
  ltsmin_kripkecube_ptr;
 
}
 
#include <spot/ltsmin/spins_kripke.hxx>