mCRL2
Loading...
Searching...
No Matches
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 343 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 178 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 293 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 318 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 435 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 377 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 229 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 108 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 486 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 529 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 513 of file liblts_aut.cpp.