liblts_aut.cpp File Reference

Go to the source code of this file.

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::lts
	The main LTS namespace.

Functions
static void	read_newline (std::istream &is, const std::size_t line_no)
static void	read_natural_number_to_string (std::istream &is, std::string &s, const std::size_t line_no)
template<class AUT_LTS_TYPE >
static std::size_t	find_label_index (const std::string &s, mcrl2::utilities::unordered_map< action_label_string, std::size_t > &labs, AUT_LTS_TYPE &l)
static void	check_state (std::size_t state, std::size_t number_of_states, std::size_t line_no)
static void	check_states (mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &probability_state, std::size_t number_of_states, std::size_t line_no)
static void	read_probabilistic_state (std::istream &is, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &result, const std::size_t line_no)
static void	read_aut_header (std::istream &is, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &initial_state, std::size_t &num_transitions, std::size_t &num_states)
static bool	read_initial_part_of_an_aut_transition (std::istream &is, std::size_t &from, std::string &label, const std::size_t line_no)
static bool	read_aut_transition (std::istream &is, std::size_t &from, std::string &label, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &target_probabilistic_state, const std::size_t line_no)
static bool	read_aut_transition (std::istream &is, std::size_t &from, std::string &label, std::size_t &to, const std::size_t line_no)
static size_t	add_probablistic_state (mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &probabilistic_state, probabilistic_lts_aut_t &l, mcrl2::utilities::unordered_map< std::size_t, std::size_t > &indices_of_single_probabilistic_states, mcrl2::utilities::unordered_map< mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t > &indices_of_multiple_probabilistic_states)
static void	read_from_aut (probabilistic_lts_aut_t &l, std::istream &is)
static void	read_from_aut (lts_aut_t &l, std::istream &is)
static void	write_probabilistic_state (const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &prob_state, std::ostream &os)
static void	write_to_aut (const probabilistic_lts_aut_t &l, std::ostream &os)
static void	write_to_aut (const lts_aut_t &l, std::ostream &os)

Function Documentation

add_probablistic_state()

static size_t add_probablistic_state ( mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &  probabilistic_state, probabilistic_lts_aut_t &  l, mcrl2::utilities::unordered_map< std::size_t, std::size_t > &  indices_of_single_probabilistic_states, mcrl2::utilities::unordered_map< mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t > &  indices_of_multiple_probabilistic_states  )

static

Definition at line 350 of file liblts_aut.cpp.

check_state()

static void check_state ( std::size_t  state, std::size_t  number_of_states, std::size_t  line_no  )

static

Definition at line 86 of file liblts_aut.cpp.

check_states()

static void check_states ( mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &  probability_state, std::size_t  number_of_states, std::size_t  line_no  )

static

Definition at line 95 of file liblts_aut.cpp.

find_label_index()

template<class AUT_LTS_TYPE >

static std::size_t find_label_index ( const std::string &  s, mcrl2::utilities::unordered_map< action_label_string, std::size_t > &  labs, AUT_LTS_TYPE &  l  )

static

Definition at line 67 of file liblts_aut.cpp.

read_aut_header()

static void read_aut_header ( std::istream &  is, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &  initial_state, std::size_t &  num_transitions, std::size_t &  num_states  )

static

Definition at line 185 of file liblts_aut.cpp.

read_aut_transition() [1/2]

static bool read_aut_transition ( std::istream &  is, std::size_t &  from, std::string &  label, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &  target_probabilistic_state, const std::size_t  line_no  )

static

Definition at line 300 of file liblts_aut.cpp.

read_aut_transition() [2/2]

static bool read_aut_transition ( std::istream &  is, std::size_t &  from, std::string &  label, std::size_t &  to, const std::size_t  line_no  )

static

Definition at line 325 of file liblts_aut.cpp.

read_from_aut() [1/2]

static void read_from_aut ( lts_aut_t &  l, std::istream &  is  )

static

Definition at line 442 of file liblts_aut.cpp.

read_from_aut() [2/2]

static void read_from_aut ( probabilistic_lts_aut_t &  l, std::istream &  is  )

static

Definition at line 384 of file liblts_aut.cpp.

read_initial_part_of_an_aut_transition()

static bool read_initial_part_of_an_aut_transition ( std::istream &  is, std::size_t &  from, std::string &  label, const std::size_t  line_no  )

static

Definition at line 236 of file liblts_aut.cpp.

read_natural_number_to_string()

static void read_natural_number_to_string ( std::istream &  is, std::string &  s, const std::size_t  line_no  )

static

Definition at line 50 of file liblts_aut.cpp.

read_newline()

static void read_newline ( std::istream &  is, const std::size_t  line_no  )

static

Definition at line 19 of file liblts_aut.cpp.

read_probabilistic_state()

static void read_probabilistic_state ( std::istream &  is, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &  result, const std::size_t  line_no  )

static

Definition at line 115 of file liblts_aut.cpp.

write_probabilistic_state()

static void write_probabilistic_state ( const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &  prob_state, std::ostream &  os  )

static

Definition at line 493 of file liblts_aut.cpp.

write_to_aut() [1/2]

static void write_to_aut ( const lts_aut_t &  l, std::ostream &  os  )

static

Definition at line 536 of file liblts_aut.cpp.

write_to_aut() [2/2]

static void write_to_aut ( const probabilistic_lts_aut_t &  l, std::ostream &  os  )

static

Definition at line 520 of file liblts_aut.cpp.