lts.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LTS_LTS_H
#define MCRL2_LTS_LTS_H
 
#include <string>
#include <vector>
#include <cstdio>
#include <iostream>
#include <algorithm>
#include <cassert>
#include <set>
#include <map>
#include "mcrl2/lts/transition.h"
#include "mcrl2/lts/lts_type.h"
 
 
namespace mcrl2
{
 
namespace lts
{
 
class lts_default_base
{
  public:
    lts_type type()
    {
      return lts_none;
    }
 
    void swap(lts_default_base& )
    {
      // Does intentionally not provide any action.
    }
 
    bool operator==(const lts_default_base&) const
    {
      return true;
    }
};
 
 
template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE = lts_default_base>
class lts: public LTS_BASE
{
  public:
 
    typedef STATE_LABEL_T state_label_t;
 
    typedef ACTION_LABEL_T action_label_t;
 
    typedef LTS_BASE base_t;
 
    typedef typename std::vector < STATE_LABEL_T >::size_type states_size_type;
 
    typedef typename std::vector < ACTION_LABEL_T >::size_type labels_size_type;
 
    typedef typename std::vector<transition>::size_type transitions_size_type;
 
    static constexpr bool is_probabilistic_lts=false;
 
  protected:
 
    states_size_type m_nstates;
    states_size_type m_init_state;
    std::vector<transition> m_transitions;
    std::vector<STATE_LABEL_T> m_state_labels;
    std::vector<ACTION_LABEL_T> m_action_labels; // At position 0 we always find the label that corresponds to tau.
    // The following set contains the labels that are recorded as being hidden. 
    // This allows tools to apply reductions assuming that these actions are hidden, but still provide
    // feedback, for instance using counter examples, using the original action name. 
    std::set<labels_size_type> m_hidden_label_set; 
 
    // Auxiliary function. Rename the labels according to the action_rename_map;
    void rename_labels(const std::map<labels_size_type, labels_size_type>& action_rename_map)
    {
      if (action_rename_map.size()>0)    // Check whether there is something to rename.
      {
        for(transition& t: m_transitions)
        {
          auto i = action_rename_map.find(t.label());
          if (i!=action_rename_map.end())
          { 
            t=transition(t.from(),i->second,t.to());
          }
        }
      }
    }
 
    // Auxiliary function. a is the partially hidden action label of which the original
    // action label occurred at position i. 
    // If label a exists at position j, set action_rename_map[i]:=j;
    // if a does not occur, adapt the action labels by setting label i to j.
    void store_action_label_to_be_renamed(const ACTION_LABEL_T& a, 
                                          const labels_size_type i, 
                                          std::map<labels_size_type, labels_size_type>& action_rename_map)
    {
      bool found=false;
      for (labels_size_type j=0; !found && j< num_action_labels(); ++j)
      {
        if (a==action_label(j))
        { 
          if (i!=j)
          {
            action_rename_map[i]=j;
          }
          found=true;
        }
      }
      if (!found) // a!=action_label(j) for any j, then rename action_label(i) to a. 
      { 
        set_action_label(i,a);
      }
    }
 
  public:
 
    lts()
     : m_nstates(0)
    {
      m_action_labels.push_back(ACTION_LABEL_T::tau_action());
    }
 
    lts(const lts& l):
      LTS_BASE(l), 
      m_nstates(l.m_nstates),
      m_init_state(l.m_init_state),
      m_transitions(l.m_transitions),
      m_state_labels(l.m_state_labels),
      m_action_labels(l.m_action_labels),
      m_hidden_label_set(l.m_hidden_label_set)
    {
      assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
    }
 
    lts& operator=(const lts& l) 
    {
      static_cast<LTS_BASE&>(*this)=l;
      m_nstates = l.m_nstates;
      m_init_state = l.m_init_state;
      m_transitions = l.m_transitions;
      m_state_labels = l.m_state_labels;
      m_action_labels = l.m_action_labels;
      m_hidden_label_set = l.m_hidden_label_set;
      assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
      return *this;
    }
 
    bool operator==(const lts& other) const
    {
      return static_cast<const LTS_BASE&>(*this)==static_cast<const LTS_BASE&>(other) &&
             m_nstates == other.m_nstates &&
             m_init_state == other.m_init_state &&
             m_transitions == other.m_transitions &&
             m_state_labels == other.m_state_labels &&
             m_action_labels == other.m_action_labels &&
             m_hidden_label_set == other.m_hidden_label_set;
    }
 
    void swap(lts& l)
    {
      static_cast<LTS_BASE&>(*this).swap(static_cast<LTS_BASE&>(l));
      {
        const states_size_type aux=m_init_state;
        m_init_state=l.m_init_state;
        l.m_init_state=aux;
      }
      {
        const states_size_type aux=m_nstates;
        m_nstates=l.m_nstates;
        l.m_nstates=aux;
      }
      m_transitions.swap(l.m_transitions);
      m_state_labels.swap(l.m_state_labels);
      m_action_labels.swap(l.m_action_labels);
      assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
      assert(l.m_action_labels.size()>0 && l.m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
      m_hidden_label_set.swap(l.m_hidden_label_set);
    }
 
    states_size_type num_states() const
    {
      return m_nstates;
    }
 
    std::vector<STATE_LABEL_T>& state_labels()
    {
      return m_state_labels;
    }
 
    const std::vector<STATE_LABEL_T>& state_labels() const
    {
      return m_state_labels;
    }
 
    states_size_type num_state_labels() const
    {
      return m_state_labels.size();
    }
 
    void set_num_states(const states_size_type n, const bool has_state_labels = true)
    {
      m_nstates = n;
      if (has_state_labels)
      {
        if (m_state_labels.size() > 0)
        {
          m_state_labels.resize(n);
        }
        else
        {
          m_state_labels = std::vector<STATE_LABEL_T>(n);
        }
      }
      else
      {
        m_state_labels = std::vector<STATE_LABEL_T>();
      }
    }
 
    transitions_size_type num_transitions() const
    {
      return m_transitions.size();
    }
 
    void set_num_action_labels(const labels_size_type n)
    {
      m_action_labels.resize(n);
      assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
    } 
 
    labels_size_type num_action_labels() const
    {
      assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
      return m_action_labels.size();
    }
 
    states_size_type initial_state() const
    {
      return m_init_state;
    }
 
    void set_initial_state(const states_size_type state)
    {
      assert(state<m_nstates);
      m_init_state = state;
    }
 
    states_size_type add_state(const STATE_LABEL_T& label=STATE_LABEL_T())
    {
      if (label!=STATE_LABEL_T())
      {
        m_state_labels.resize(m_nstates);
        m_state_labels.push_back(label);
      }
      return m_nstates++;
    }
 
    labels_size_type add_action(const ACTION_LABEL_T& label)
    {
      if (label==ACTION_LABEL_T::tau_action())
      {
        return const_tau_label_index;
      }
      assert(std::find(m_action_labels.begin(),m_action_labels.end(),label)==m_action_labels.end()); // Action labels must be unique. 
      const labels_size_type label_index=m_action_labels.size();
      m_action_labels.push_back(label);
      return label_index;
    }
 
    const labels_size_type tau_label_index() const
    {
      return const_tau_label_index;
    }
 
    void set_state_label(const states_size_type state, const STATE_LABEL_T& label)
    {
      assert(state<m_nstates);
      assert(m_nstates==m_state_labels.size());
      m_state_labels[state] = label;
    }
 
    const std::vector<ACTION_LABEL_T>& action_labels() const
    {
      return m_action_labels;
    } 
 
    void set_action_label(const labels_size_type action, const ACTION_LABEL_T& label)
    {
      assert(action<m_action_labels.size());
      assert((action==const_tau_label_index) == (label==ACTION_LABEL_T::tau_action())); // a tau action is always stored at index 0.
      assert(m_action_labels[action] == label ||
             std::find(m_action_labels.begin(),m_action_labels.end(),label)==m_action_labels.end()); // Action labels must be unique. 
      m_action_labels[action] = label;
    }
 
    const std::set<labels_size_type>& hidden_label_set() const
    {
      return m_hidden_label_set;
    }
 
    std::set<labels_size_type>& hidden_label_set()
    {
      return m_hidden_label_set;
    }
 
    void set_hidden_label_set(const std::set<labels_size_type>& m)
    {
      m_hidden_label_set=m;
    }
 
    labels_size_type apply_hidden_label_map(const labels_size_type action) const
    {
      if (m_hidden_label_set.count(action)>0)
      {
        return tau_label_index();
      }
      return action;
    }
 
    STATE_LABEL_T state_label(const states_size_type state) const
    {
      assert(state<m_nstates);
      assert(m_nstates==m_state_labels.size());
      return m_state_labels[state];
    }
 
    bool is_probabilistic(const states_size_type state) const
    {
      (void)state;  // Suppress an unused variable warning. 
      assert(state<m_nstates);
      return false;
    }
 
    ACTION_LABEL_T action_label(const labels_size_type action) const
    {
      assert(action < m_action_labels.size());
      return m_action_labels[action];
    }
 
    void clear_transitions(const std::size_t n=0)
    {
      m_transitions = std::vector<transition>();
      m_transitions.reserve(n);
    }
 
    void clear_actions()
    {
      m_action_labels.clear();
      m_action_labels.push_back(ACTION_LABEL_T::tau_action());
      m_hidden_label_set.clear();
    }
 
    void clear_state_labels()
    {
      m_state_labels.clear();
    }
 
    void clear()
    {
      clear_state_labels();
      clear_actions();
      clear_transitions();
      m_nstates = 0;
    }
 
    const std::vector<transition>& get_transitions() const
    {
      return m_transitions;
    }
 
    std::vector<transition>& get_transitions()
    {
      return m_transitions;
    }
 
    void add_transition(const transition& t)
    {
      m_transitions.push_back(t);
    }
 
    bool is_tau(labels_size_type action) const
    {
      assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
      return (action==const_tau_label_index);
    }
 
 
    void record_hidden_actions(const std::vector<std::string>& tau_actions)
    {
      if (tau_actions.size()==0)
      {
        return;
      }
 
      std::map<labels_size_type, labels_size_type> action_rename_map;
      for (labels_size_type i=0; i< num_action_labels(); ++i)
      {
        ACTION_LABEL_T a=action_label(i);
        a.hide_actions(tau_actions);
        if (a==ACTION_LABEL_T::tau_action())  
        {
          if (i!=const_tau_label_index)
          {
            m_hidden_label_set.insert(i);
          }
        }
        else if (a!=action_label(i))
        {
          /* In this the action_label i is changed by the tau_actions but not renamed to tau.
             We check whether a maps onto another action label index. If yes, it is added to 
             the rename map, and we explicitly rename transition labels with this label afterwards.
             If no, we rename the action label.
          */
          store_action_label_to_be_renamed(a, i, action_rename_map);
        }
      }
 
      rename_labels(action_rename_map);
    }
 
    void apply_hidden_actions(const std::vector<std::string>& tau_actions)
    {
      if (tau_actions.size()==0)
      { 
        return;
      }
      
      std::map<labels_size_type, labels_size_type> action_rename_map;
      for (labels_size_type i=0; i< num_action_labels(); ++i)
      {
        ACTION_LABEL_T a=action_label(i);
        a.hide_actions(tau_actions);
#ifndef NDEBUG
        ACTION_LABEL_T b=a;
        b.hide_actions(tau_actions);
        assert(a==b); // hide_actions applied twice yields the same result as applying it once.
#endif
        store_action_label_to_be_renamed(a, i, action_rename_map);
      }
    
      rename_labels(action_rename_map);
    }
 
    bool has_state_info() const
    {
      return m_state_labels.size() > 0;
    }
 
    bool has_action_info() const
    {
      return m_action_labels.size() > 1;
    }
};
 
}
}
 
#endif // MCRL2_LTS_LTS_H