mCRL2
Loading...
Searching...
No Matches
state.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/lps/state.h
10/// \brief The class summand.
11
12#ifndef MCRL2_LPS_STATE_H
13#define MCRL2_LPS_STATE_H
14
15#include "mcrl2/atermpp/aterm_balanced_tree.h"
16#include "mcrl2/data/data_expression.h"
17
18namespace mcrl2::lps
19{
20
21using state = atermpp::term_balanced_tree<data::data_expression>;
22
23template<class ForwardTraversalIterator, class Transformer>
24void make_state(state& result,
25 ForwardTraversalIterator p,
26 const std::size_t size,
27 Transformer transformer)
28{
29 make_term_balanced_tree(result, p, size, transformer);
30}
31
32template<class ForwardTraversalIterator>
33void make_state(state& result,
34 ForwardTraversalIterator p,
35 const std::size_t size)
36{
37 make_term_balanced_tree(result,
38 p,
39 size,
40 [](data::data_expression& result, const data::data_expression& t){ result=t; });
41}
42
43// template function overloads
44inline std::string pp(const lps::state& x)
45{
46 return atermpp::pp(x);
47}
48
49} // namespace mcrl2::lps
50
51#endif // MCRL2_LPS_STATE_H
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A list of aterm objects.
Definition aterm_list.h:26
A unordered_map class in which aterms can be stored.
action_formula(action_formula &&) noexcept=default
action_formula & operator=(const action_formula &) noexcept=default
action_formula(const atermpp::aterm &term)
action_formula(const data::data_expression &x)
\brief Constructor Z6.
action_formula(const action_formula &) noexcept=default
Move semantics.
action_formula & operator=(action_formula &&) noexcept=default
action_formula(const data::untyped_data_parameter &x)
\brief Constructor Z6.
action_formula()
\brief Default constructor X3.
action_formula(const process::untyped_multi_action &x)
\brief Constructor Z6.
\brief The and operator for action formulas
and_ & operator=(const and_ &) noexcept=default
and_ & operator=(and_ &&) noexcept=default
and_(const action_formula &left, const action_formula &right)
\brief Constructor Z14.
and_()
\brief Default constructor X3.
and_(and_ &&) noexcept=default
const action_formula & left() const
and_(const atermpp::aterm &term)
and_(const and_ &) noexcept=default
Move semantics.
const action_formula & right() const
\brief The at operator for action formulas
at(const atermpp::aterm &term)
const data::data_expression & time_stamp() const
at & operator=(at &&) noexcept=default
const action_formula & operand() const
at(const at &) noexcept=default
Move semantics.
at(at &&) noexcept=default
at()
\brief Default constructor X3.
at & operator=(const at &) noexcept=default
at(const action_formula &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
\brief The existential quantification operator for action formulas
exists(const atermpp::aterm &term)
exists & operator=(exists &&) noexcept=default
exists(exists &&) noexcept=default
exists(const exists &) noexcept=default
Move semantics.
exists()
\brief Default constructor X3.
const data::variable_list & variables() const
exists & operator=(const exists &) noexcept=default
const action_formula & body() const
exists(const data::variable_list &variables, const action_formula &body)
\brief Constructor Z14.
\brief The value false for action formulas
false_(const atermpp::aterm &term)
false_()
\brief Default constructor X3.
false_(false_ &&) noexcept=default
false_(const false_ &) noexcept=default
Move semantics.
false_ & operator=(const false_ &) noexcept=default
false_ & operator=(false_ &&) noexcept=default
\brief The universal quantification operator for action formulas
forall & operator=(const forall &) noexcept=default
const action_formula & body() const
forall & operator=(forall &&) noexcept=default
forall(const atermpp::aterm &term)
const data::variable_list & variables() const
forall()
\brief Default constructor X3.
forall(const data::variable_list &variables, const action_formula &body)
\brief Constructor Z14.
forall(const forall &) noexcept=default
Move semantics.
forall(forall &&) noexcept=default
\brief The implication operator for action formulas
const action_formula & left() const
imp(const imp &) noexcept=default
Move semantics.
imp(imp &&) noexcept=default
imp & operator=(imp &&) noexcept=default
imp(const action_formula &left, const action_formula &right)
\brief Constructor Z14.
imp()
\brief Default constructor X3.
imp & operator=(const imp &) noexcept=default
imp(const atermpp::aterm &term)
const action_formula & right() const
\brief The multi action for action formulas
multi_action(const multi_action &) noexcept=default
Move semantics.
multi_action(multi_action &&) noexcept=default
multi_action(const process::action_list &actions)
\brief Constructor Z14.
multi_action(const atermpp::aterm &term)
multi_action & operator=(const multi_action &) noexcept=default
multi_action()
\brief Default constructor X3.
const process::action_list & actions() const
multi_action & operator=(multi_action &&) noexcept=default
\brief The not operator for action formulas
not_(const action_formula &operand)
\brief Constructor Z14.
not_()
\brief Default constructor X3.
const action_formula & operand() const
not_(const atermpp::aterm &term)
not_(not_ &&) noexcept=default
not_(const not_ &) noexcept=default
Move semantics.
not_ & operator=(const not_ &) noexcept=default
not_ & operator=(not_ &&) noexcept=default
\brief The or operator for action formulas
or_ & operator=(const or_ &) noexcept=default
or_(or_ &&) noexcept=default
or_()
\brief Default constructor X3.
or_ & operator=(or_ &&) noexcept=default
or_(const action_formula &left, const action_formula &right)
\brief Constructor Z14.
or_(const atermpp::aterm &term)
or_(const or_ &) noexcept=default
Move semantics.
const action_formula & right() const
const action_formula & left() const
\brief The value true for action formulas
true_(true_ &&) noexcept=default
true_ & operator=(const true_ &) noexcept=default
true_()
\brief Default constructor X3.
true_(const true_ &) noexcept=default
Move semantics.
true_(const atermpp::aterm &term)
true_ & operator=(true_ &&) noexcept=default
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
\brief A data variable
Definition variable.h:25
Action rename specification.
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
const process::action_list & actions() const
multi_action(const process::action_list &actions=process::action_list(), data::data_expression time=data::undefined_real())
Constructor. Actions are sorted to establish the sorted-storage invariant.
Linear process specification.
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:142
action_label_lts & operator=(const action_label_lts &)=default
Copy assignment.
void hide_actions(const std::vector< std::string > &tau_actions)
Hide the actions with labels in tau_actions.
Definition lts_lts.h:163
action_label_lts(const action_label_lts &)=default
Copy constructor.
static const action_label_lts & tau_action()
Definition lts_lts.h:179
action_label_lts(const mcrl2::lps::multi_action &a)
Constructor.
Definition lts_lts.h:155
action_label_lts()=default
Default constructor.
mcrl2::state_formulas::state_formula conjunction(std::set< mcrl2::state_formulas::state_formula > terms) const
conjunction Creates a conjunction of state formulas
regular_formulas::regular_formula create_regular_formula(const mcrl2::lts::action_label_string &a) const
create_regular_formula Creates a regular formula that represents action a
regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action &a) const
create_regular_formula Creates a regular formula that represents action a
std::vector< bool > block_is_in_to_be_processed
std::map< block_index_type, block_index_type > right_child
std::vector< block_index_type > BL
bool in_same_class(const std::size_t s, const std::size_t t) const
Returns whether two states are in the same bisimulation equivalence class.
mcrl2::state_formulas::state_formula until_formula(const mcrl2::state_formulas::state_formula &phi1, const label_type &a, const mcrl2::state_formulas::state_formula &phi2)
until_formula Creates a state formula that corresponds to the until operator phi1phi2 from HMLU
std::size_t get_eq_class(const std::size_t s) const
Gives the bisimulation equivalence class number of a state.
bisim_partitioner(LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false)
Creates a bisimulation partitioner for an LTS.
~bisim_partitioner()=default
Destroys this partitioner.
std::map< block_index_type, label_type > split_by_action
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
mcrl2::state_formulas::state_formula counter_formula(std::size_t s, std::size_t t)
Creates a state formula that distinguishes state s from state t.
void order_recursively_on_tau_reachability(const state_type s, std::map< state_type, std::vector< state_type > > &inert_transition_map, std::vector< non_bottom_state > &new_non_bottom_states, std::set< state_type > &visited)
std::vector< block_index_type > to_be_processed
std::map< block_index_type, block_index_type > split_by_block
void replace_transition_system(const bool branching, const bool preserve_divergences)
Replaces the transition relation of the current lts by the transitions of the bisimulation reduced tr...
void order_on_tau_reachability(std::vector< non_bottom_state > &non_bottom_states)
void split_the_blocks_in_BL(bool &partition_is_unstable, const label_type splitter_label, const block_index_type splitter_block)
void refine_partition_until_it_becomes_stable(const bool branching, const bool preserve_divergence)
void create_initial_partition(const bool branching, const bool preserve_divergences)
std::vector< state_type > block_index_of_a_state
mcrl2::state_formulas::state_formula counter_formula_aux(const block_index_type B1, const block_index_type B2)
void check_internal_consistency_of_the_partitioning_data_structure(const bool branching, const bool preserve_divergence) const
outgoing_transitions_per_state_action_t outgoing_transitions
function object to compare two constln_t pointers based on their contents
A class that can be used to store counterexample trees and.
a base class for lts_lts_t and probabilistic_lts_t.
Definition lts_lts.h:268
static lts_type type()
Yields the type of this lts, in this case lts_lts.
Definition lts_lts.h:296
void set_process_parameters(const data::variable_list &params)
Set the state parameters for this LTS.
Definition lts_lts.h:354
lts_lts_base()=default
Default constructor.
bool operator==(const lts_lts_base &other) const
Standard equality function;.
Definition lts_lts.h:279
process::action_label_list m_action_decls
Definition lts_lts.h:272
void set_action_label_declarations(const process::action_label_list &decls)
Set the action label information for this LTS.
Definition lts_lts.h:318
const data::variable & process_parameter(std::size_t i) const
Returns the i-th parameter of the state vectors stored in this LTS.
Definition lts_lts.h:341
data::data_specification m_data_spec
Definition lts_lts.h:270
const data::variable_list & process_parameters() const
Return the process parameters stored in this LTS.
Definition lts_lts.h:333
void set_data(const data::data_specification &spec)
Set the mCRL2 data specification of this LTS.
Definition lts_lts.h:326
void swap(lts_lts_base &l) noexcept
Definition lts_lts.h:286
const process::action_label_list & action_label_declarations() const
Return action label declarations stored in this LTS.
Definition lts_lts.h:310
data::variable_list m_parameters
Definition lts_lts.h:271
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:370
lts_lts_t()=default
Creates an object containing no information.
void save(const std::string &filename) const
Save the labelled transition system to file.
void load(const std::string &filename)
Load the labelled transition system from file.
This class contains probabilistic labelled transition systems in .lts format.
Definition lts_lts.h:398
probabilistic_lts_lts_t()=default
Creates an object containing no information.
void load(const std::string &filename)
Load the labelled transition system from file.
void save(const std::string &filename) const
Save the labelled transition system to file.
A class that contains a labelled transition system.
Class for computing the signature for strong bisimulation.
Definition sigref.h:74
Class for computing the signature for branching bisimulation.
Definition sigref.h:104
Class for computing the signature for divergence preserving branching bisimulation.
Definition sigref.h:183
Signature based reductions for labelled transition systems.
Definition sigref.h:349
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:38
state_label_lts(const state_label_lts &)=default
Copy constructor.
state_label_lts operator+(const state_label_lts &l) const
An operator to concatenate two state labels.
Definition lts_lts.h:79
state_label_lts(const super &l)
Construct a state label out of list of balanced trees of data expressions, representing a state label...
Definition lts_lts.h:71
state_label_lts()=default
Default constructor.
state_label_lts(const lps::state &l)
Construct a state label out of a balanced tree of data expressions, representing a state label.
Definition lts_lts.h:64
state_label_lts & operator=(const state_label_lts &)=default
Copy assignment.
static state_label_lts number_to_label(const std::size_t n)
Create a state label consisting of a number as the only list element.
Definition lts_lts.h:94
state_label_lts(const CONTAINER &l)
Construct a single state label out of the elements in a container.
Definition lts_lts.h:55
Process specification consisting of a data specification, action labels, a sequence of process equati...
\brief An untyped multi action or data application
\brief The alt operator for regular formulas
alt(const atermpp::aterm &term)
alt()
\brief Default constructor X3.
alt & operator=(alt &&) noexcept=default
const regular_formula & right() const
alt(const regular_formula &left, const regular_formula &right)
\brief Constructor Z14.
alt(const alt &) noexcept=default
Move semantics.
alt(alt &&) noexcept=default
alt & operator=(const alt &) noexcept=default
const regular_formula & left() const
regular_formula()
\brief Default constructor X3.
regular_formula(const action_formulas::action_formula &x)
\brief Constructor Z6.
regular_formula(const atermpp::aterm &term)
regular_formula(const regular_formula &) noexcept=default
Move semantics.
regular_formula(const data::data_expression &x)
\brief Constructor Z6.
regular_formula & operator=(const regular_formula &) noexcept=default
regular_formula(regular_formula &&) noexcept=default
regular_formula & operator=(regular_formula &&) noexcept=default
\brief The seq operator for regular formulas
seq(const regular_formula &left, const regular_formula &right)
\brief Constructor Z14.
const regular_formula & right() const
seq & operator=(const seq &) noexcept=default
seq(const seq &) noexcept=default
Move semantics.
const regular_formula & left() const
seq(seq &&) noexcept=default
seq()
\brief Default constructor X3.
seq & operator=(seq &&) noexcept=default
seq(const atermpp::aterm &term)
\brief The 'trans or nil' operator for regular formulas
trans_or_nil & operator=(trans_or_nil &&) noexcept=default
trans_or_nil & operator=(const trans_or_nil &) noexcept=default
trans_or_nil(const trans_or_nil &) noexcept=default
Move semantics.
trans_or_nil(const regular_formula &operand)
\brief Constructor Z14.
trans_or_nil()
\brief Default constructor X3.
trans_or_nil(trans_or_nil &&) noexcept=default
trans_or_nil(const atermpp::aterm &term)
const regular_formula & operand() const
\brief The trans operator for regular formulas
trans(const atermpp::aterm &term)
trans(trans &&) noexcept=default
const regular_formula & operand() const
trans & operator=(const trans &) noexcept=default
trans & operator=(trans &&) noexcept=default
trans()
\brief Default constructor X3.
trans(const trans &) noexcept=default
Move semantics.
trans(const regular_formula &operand)
\brief Constructor Z14.
\brief An untyped regular formula or action formula
untyped_regular_formula()
\brief Default constructor X3.
untyped_regular_formula & operator=(untyped_regular_formula &&) noexcept=default
untyped_regular_formula & operator=(const untyped_regular_formula &) noexcept=default
untyped_regular_formula(const std::string &name, const regular_formula &left, const regular_formula &right)
\brief Constructor Z2.
untyped_regular_formula(const core::identifier_string &name, const regular_formula &left, const regular_formula &right)
\brief Constructor Z14.
const core::identifier_string & name() const
untyped_regular_formula(const untyped_regular_formula &) noexcept=default
Move semantics.
untyped_regular_formula(untyped_regular_formula &&) noexcept=default
\brief The and operator for state formulas
and_(and_ &&) noexcept=default
const state_formula & right() const
and_(const atermpp::aterm &term)
and_(const and_ &) noexcept=default
Move semantics.
and_(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
and_ & operator=(const and_ &) noexcept=default
and_()
\brief Default constructor X3.
and_ & operator=(and_ &&) noexcept=default
const state_formula & left() const
\brief The multiply operator for state formulas with values
const_multiply_alt & operator=(const const_multiply_alt &) noexcept=default
const state_formula & left() const
const_multiply_alt(const state_formula &left, const data::data_expression &right)
\brief Constructor Z14.
const_multiply_alt(const const_multiply_alt &) noexcept=default
Move semantics.
const_multiply_alt(const_multiply_alt &&) noexcept=default
const data::data_expression & right() const
const_multiply_alt(const atermpp::aterm &term)
const_multiply_alt & operator=(const_multiply_alt &&) noexcept=default
const_multiply_alt()
\brief Default constructor X3.
\brief The multiply operator for state formulas with values
const data::data_expression & left() const
const_multiply(const const_multiply &) noexcept=default
Move semantics.
const_multiply(const data::data_expression &left, const state_formula &right)
\brief Constructor Z14.
const_multiply()
\brief Default constructor X3.
const_multiply(const_multiply &&) noexcept=default
const_multiply & operator=(const const_multiply &) noexcept=default
const_multiply & operator=(const_multiply &&) noexcept=default
const_multiply(const atermpp::aterm &term)
const state_formula & right() const
\brief The timed delay operator for state formulas
delay_timed(const atermpp::aterm &term)
delay_timed()
\brief Default constructor X3.
delay_timed & operator=(const delay_timed &) noexcept=default
const data::data_expression & time_stamp() const
delay_timed(const data::data_expression &time_stamp)
\brief Constructor Z14.
delay_timed(const delay_timed &) noexcept=default
Move semantics.
delay_timed(delay_timed &&) noexcept=default
delay_timed & operator=(delay_timed &&) noexcept=default
\brief The delay operator for state formulas
delay & operator=(delay &&) noexcept=default
delay()
\brief Default constructor X3.
delay(const delay &) noexcept=default
Move semantics.
delay(delay &&) noexcept=default
delay(const atermpp::aterm &term)
delay & operator=(const delay &) noexcept=default
\brief The existential quantification operator for state formulas
exists(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
const state_formula & body() const
exists(const exists &) noexcept=default
Move semantics.
exists(exists &&) noexcept=default
exists & operator=(const exists &) noexcept=default
exists & operator=(exists &&) noexcept=default
exists()
\brief Default constructor X3.
exists(const atermpp::aterm &term)
const data::variable_list & variables() const
\brief The value false for state formulas
false_(false_ &&) noexcept=default
false_ & operator=(const false_ &) noexcept=default
false_ & operator=(false_ &&) noexcept=default
false_(const atermpp::aterm &term)
false_(const false_ &) noexcept=default
Move semantics.
false_()
\brief Default constructor X3.
\brief The universal quantification operator for state formulas
const state_formula & body() const
forall(const atermpp::aterm &term)
const data::variable_list & variables() const
forall & operator=(const forall &) noexcept=default
forall & operator=(forall &&) noexcept=default
forall(const forall &) noexcept=default
Move semantics.
forall(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
forall(forall &&) noexcept=default
forall()
\brief Default constructor X3.
\brief The implication operator for state formulas
imp()
\brief Default constructor X3.
imp(imp &&) noexcept=default
imp(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
imp & operator=(const imp &) noexcept=default
const state_formula & left() const
const state_formula & right() const
imp(const atermpp::aterm &term)
imp(const imp &) noexcept=default
Move semantics.
imp & operator=(imp &&) noexcept=default
\brief The infimum over a data type for state formulas
infimum(const infimum &) noexcept=default
Move semantics.
infimum()
\brief Default constructor X3.
infimum(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
infimum & operator=(infimum &&) noexcept=default
const data::variable_list & variables() const
const state_formula & body() const
infimum(const atermpp::aterm &term)
infimum(infimum &&) noexcept=default
infimum & operator=(const infimum &) noexcept=default
\brief The may operator for state formulas
const state_formula & operand() const
may()
\brief Default constructor X3.
const regular_formulas::regular_formula & formula() const
may & operator=(const may &) noexcept=default
may & operator=(may &&) noexcept=default
may(const regular_formulas::regular_formula &formula, const state_formula &operand)
\brief Constructor Z14.
may(may &&) noexcept=default
may(const atermpp::aterm &term)
may(const may &) noexcept=default
Move semantics.
\brief The minus operator for state formulas
minus & operator=(minus &&) noexcept=default
minus(minus &&) noexcept=default
minus(const minus &) noexcept=default
Move semantics.
minus(const atermpp::aterm &term)
minus(const state_formula &operand)
\brief Constructor Z14.
const state_formula & operand() const
minus & operator=(const minus &) noexcept=default
minus()
\brief Default constructor X3.
\brief The mu operator for state formulas
const core::identifier_string & name() const
const data::assignment_list & assignments() const
mu(const mu &) noexcept=default
Move semantics.
mu(const std::string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z2.
mu(const core::identifier_string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z14.
mu & operator=(const mu &) noexcept=default
mu(mu &&) noexcept=default
mu & operator=(mu &&) noexcept=default
mu(const atermpp::aterm &term)
mu()
\brief Default constructor X3.
const state_formula & operand() const
\brief The must operator for state formulas
must(must &&) noexcept=default
must & operator=(must &&) noexcept=default
must(const atermpp::aterm &term)
must(const regular_formulas::regular_formula &formula, const state_formula &operand)
\brief Constructor Z14.
const regular_formulas::regular_formula & formula() const
must(const must &) noexcept=default
Move semantics.
const state_formula & operand() const
must()
\brief Default constructor X3.
must & operator=(const must &) noexcept=default
\brief The not operator for state formulas
not_(not_ &&) noexcept=default
not_(const not_ &) noexcept=default
Move semantics.
not_ & operator=(const not_ &) noexcept=default
not_ & operator=(not_ &&) noexcept=default
not_()
\brief Default constructor X3.
not_(const atermpp::aterm &term)
const state_formula & operand() const
not_(const state_formula &operand)
\brief Constructor Z14.
\brief The nu operator for state formulas
nu(const atermpp::aterm &term)
nu(nu &&) noexcept=default
nu(const core::identifier_string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z14.
nu()
\brief Default constructor X3.
nu & operator=(const nu &) noexcept=default
nu & operator=(nu &&) noexcept=default
const core::identifier_string & name() const
nu(const std::string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z2.
const state_formula & operand() const
nu(const nu &) noexcept=default
Move semantics.
const data::assignment_list & assignments() const
\brief The or operator for state formulas
or_(or_ &&) noexcept=default
or_()
\brief Default constructor X3.
or_(const or_ &) noexcept=default
Move semantics.
or_(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
or_ & operator=(const or_ &) noexcept=default
const state_formula & right() const
or_ & operator=(or_ &&) noexcept=default
or_(const atermpp::aterm &term)
const state_formula & left() const
\brief The plus operator for state formulas with values
plus & operator=(plus &&) noexcept=default
plus & operator=(const plus &) noexcept=default
plus(const plus &) noexcept=default
Move semantics.
const state_formula & left() const
plus(const atermpp::aterm &term)
plus()
\brief Default constructor X3.
const state_formula & right() const
plus(plus &&) noexcept=default
plus(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
state_formula(const state_formula &) noexcept=default
Move semantics.
state_formula()
\brief Default constructor X3.
state_formula(state_formula &&) noexcept=default
bool has_time() const
Returns true if the formula is timed.
state_formula(const data::untyped_data_parameter &x)
\brief Constructor Z6.
state_formula & operator=(state_formula &&) noexcept=default
state_formula(const data::data_expression &x)
\brief Constructor Z6.
state_formula(const atermpp::aterm &term)
state_formula & operator=(const state_formula &) noexcept=default
\brief The sum over a data type for state formulas
sum(const sum &) noexcept=default
Move semantics.
sum(sum &&) noexcept=default
sum(const atermpp::aterm &term)
sum(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
sum & operator=(sum &&) noexcept=default
sum()
\brief Default constructor X3.
const data::variable_list & variables() const
const state_formula & body() const
sum & operator=(const sum &) noexcept=default
\brief The supremum over a data type for state formulas
supremum & operator=(supremum &&) noexcept=default
supremum(supremum &&) noexcept=default
supremum(const atermpp::aterm &term)
supremum()
\brief Default constructor X3.
supremum(const supremum &) noexcept=default
Move semantics.
supremum & operator=(const supremum &) noexcept=default
const state_formula & body() const
const data::variable_list & variables() const
supremum(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
\brief The value true for state formulas
true_()
\brief Default constructor X3.
true_ & operator=(const true_ &) noexcept=default
true_(true_ &&) noexcept=default
true_(const true_ &) noexcept=default
Move semantics.
true_(const atermpp::aterm &term)
true_ & operator=(true_ &&) noexcept=default
\brief The state formula variable
variable & operator=(const variable &) noexcept=default
variable(const core::identifier_string &name, const data::data_expression_list &arguments)
\brief Constructor Z14.
variable(const variable &) noexcept=default
Move semantics.
variable(const std::string &name, const data::data_expression_list &arguments)
\brief Constructor Z2.
variable()
\brief Default constructor X3.
variable & operator=(variable &&) noexcept=default
const core::identifier_string & name() const
const data::data_expression_list & arguments() const
variable(variable &&) noexcept=default
variable(const atermpp::aterm &term)
\brief The timed yaled operator for state formulas
yaled_timed(yaled_timed &&) noexcept=default
yaled_timed & operator=(const yaled_timed &) noexcept=default
yaled_timed()
\brief Default constructor X3.
yaled_timed & operator=(yaled_timed &&) noexcept=default
yaled_timed(const yaled_timed &) noexcept=default
Move semantics.
yaled_timed(const data::data_expression &time_stamp)
\brief Constructor Z14.
yaled_timed(const atermpp::aterm &term)
const data::data_expression & time_stamp() const
\brief The yaled operator for state formulas
yaled()
\brief Default constructor X3.
yaled(const atermpp::aterm &term)
yaled & operator=(const yaled &) noexcept=default
yaled(const yaled &) noexcept=default
Move semantics.
yaled(yaled &&) noexcept=default
yaled & operator=(yaled &&) noexcept=default
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:393
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(or_ &t1, or_ &t2) noexcept
\brief swap overload
std::string pp(const action_formulas::exists &x, bool arg0)
bool is_at(const atermpp::aterm &x)
void swap(forall &t1, forall &t2) noexcept
\brief swap overload
std::string pp(const action_formulas::imp &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const or_ &x)
std::string pp(const action_formulas::at &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const action_formula &x)
std::string pp(const action_formulas::forall &x, bool arg0)
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const action_formulas::or_ &x, bool arg0)
std::string pp(const action_formulas::action_formula &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const true_ &x)
std::ostream & operator<<(std::ostream &out, const exists &x)
std::ostream & operator<<(std::ostream &out, const at &x)
std::string pp(const action_formulas::true_ &x, bool arg0)
std::set< data::variable > find_all_variables(const action_formulas::action_formula &x)
bool is_or(const atermpp::aterm &x)
void swap(action_formula &t1, action_formula &t2) noexcept
\brief swap overload
bool is_true(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
void swap(not_ &t1, not_ &t2) noexcept
\brief swap overload
std::string pp(const action_formulas::not_ &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const and_ &x)
void swap(true_ &t1, true_ &t2) noexcept
\brief swap overload
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const false_ &x)
bool is_false(const atermpp::aterm &x)
bool is_not(const atermpp::aterm &x)
void swap(false_ &t1, false_ &t2) noexcept
\brief swap overload
void swap(and_ &t1, and_ &t2) noexcept
\brief swap overload
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_imp(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(multi_action &t1, multi_action &t2) noexcept
\brief swap overload
void swap(imp &t1, imp &t2) noexcept
\brief swap overload
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const forall &x)
void swap(exists &t1, exists &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const imp &x)
std::ostream & operator<<(std::ostream &out, const multi_action &x)
void make_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_multi_action(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const not_ &x)
std::string pp(const action_formulas::multi_action &x, bool arg0)
void swap(at &t1, at &t2) noexcept
\brief swap overload
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const action_formulas::false_ &x, bool arg0)
bool is_exists(const atermpp::aterm &x)
std::string pp(const action_formulas::and_ &x, bool arg0)
bool is_action_formula(const atermpp::aterm &x)
static data_specification const & default_specification()
Definition parse.h:28
Namespace for system defined sort int_.
application cint(const data_expression &arg0)
Application of function symbol @cInt.
Definition int1.h:101
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:44
Namespace for system defined sort nat.
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:43
application cnat(const data_expression &arg0)
Application of function symbol @cNat.
Definition nat1.h:161
Namespace for system defined sort pos.
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:42
Namespace for system defined sort real_.
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:45
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_untyped_data_parameter(const atermpp::aterm &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
multi_action complete_multi_action(process::untyped_multi_action &x, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Definition lps.cpp:148
void complete_action_rename_specification(action_rename_specification &x, const lps::stochastic_specification &spec)
Definition lps.cpp:166
process::untyped_multi_action parse_multi_action_new(const std::string &text)
Definition lps.cpp:130
multi_action complete_multi_action(process::untyped_multi_action &x, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Definition lps.cpp:140
action_rename_specification parse_action_rename_specification_new(const std::string &text)
Definition lps.cpp:156
The main namespace for the LPS library.
Definition constelm.h:18
specification parse_linear_process_specification(const std::string &text)
Parses a linear process specification from a string.
Definition parse.h:149
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
multi_action parse_multi_action(const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from a string.
Definition parse.h:67
void parse_lps(std::istream &, Specification &)
Definition parse.h:156
process::action parse_action(const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses an action from a string.
Definition parse.h:208
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
multi_action parse_multi_action(std::stringstream &in, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from an input stream.
Definition parse.h:53
action_rename_specification parse_action_rename_specification(std::istream &in, const lps::stochastic_specification &spec)
Parses a process specification from an input stream.
Definition parse.h:91
multi_action parse_multi_action(std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from an input stream.
Definition parse.h:39
action_rename_specification parse_action_rename_specification(const std::string &spec_string, const lps::stochastic_specification &spec)
Parses an action rename specification. Parses an action rename specification. If the action rename sp...
Definition parse.h:107
void parse_lps< specification >(std::istream &from, specification &result)
Definition parse.h:163
void make_state(state &result, ForwardTraversalIterator p, const std::size_t size)
Definition state.h:33
void parse_lps< stochastic_specification >(std::istream &from, stochastic_specification &result)
Parses a stochastic linear process specification from an input stream.
Definition parse.h:180
std::string pp(const lps::state &x)
Definition state.h:44
multi_action parse_multi_action(const std::string &text, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from a string.
Definition parse.h:80
void parse_lps(const std::string &text, Specification &result)
Definition parse.h:194
specification parse_linear_process_specification(std::istream &spec_stream)
Parses a linear process specification from an input stream.
Definition parse.h:125
void make_state(state &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)
Definition state.h:24
bool bisimulation_compare(const LTS_TYPE &l1, const LTS_TYPE &l2, bool branching=false, bool preserve_divergences=false, bool generate_counter_examples=false, const std::string &counter_example_file="", bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
lts_type guess_format(std::string const &s, const bool be_verbose)
Determines the LTS format from a filename by its extension.
Definition liblts.cpp:26
static const std::array< std::string, 5 > extension_strings
Definition liblts.cpp:73
std::string supported_lts_formats_text(lts_type default_format, const std::set< lts_type > &supported)
Gives a textual list describing supported LTS formats.
Definition liblts.cpp:152
std::string supported_lts_formats_text(const std::set< lts_type > &supported)
Gives a textual list describing supported LTS formats.
Definition liblts.cpp:185
std::string string_for_type(const lts_type type)
Gives a string representation of an LTS format.
Definition liblts.cpp:112
void unmark_explicit_divergence_transitions(LTS_TYPE &l, const std::size_t divergent_transition_label)
std::string mime_type_for_type(const lts_type type)
Gives the MIME type associated with an LTS format.
Definition liblts.cpp:122
void get_trans(const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::ptrdiff_t d, std::vector< transition > &d_trans, LTS_TYPE &aut)
lts_type parse_format(std::string const &s)
Determines the LTS format from a format specification string.
Definition liblts.cpp:91
static const std::array< std::string, 5 > type_strings
Definition liblts.cpp:71
std::string extension_for_type(const lts_type type)
Gives the filename extension associated with an LTS format.
Definition liblts.cpp:117
LABEL_TYPE make_divergence_label(const std::string &s)
const std::set< lts_type > & supported_lts_formats()
Gives the set of all supported LTS formats.
Definition liblts.cpp:139
std::string lts_extensions_as_string(const std::set< lts_type > &supported)
Gives a list of extensions for supported LTS formats.
Definition liblts.cpp:221
std::string lts_extensions_as_string(const std::string &sep, const std::set< lts_type > &supported)
Gives a list of extensions for supported LTS formats.
Definition liblts.cpp:190
std::size_t mark_explicit_divergence_transitions(LTS_TYPE &l)
bool destructive_bisimulation_compare(LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergences=false, bool generate_counter_examples=false, const std::string &counter_example_file="", bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
void bisimulation_reduce(LTS_TYPE &l, bool branching=false, bool preserve_divergences=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
bool lts_named_cmp(const std::array< std::string, Size > &N, T a, T b)
Definition liblts.cpp:147
static const std::array< std::string, 5 > type_desc_strings
Definition liblts.cpp:75
static const std::array< std::string, 5 > mime_type_strings
Definition liblts.cpp:84
static const std::set< lts_type > & initialise_supported_lts_formats()
Definition liblts.cpp:127
std::string pp(const state_label_lts &label)
Pretty print a state value of this LTS.
Definition lts_lts.h:106
bool is_deterministic(const LTS_TYPE &l)
Checks whether this LTS is deterministic.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
action_label_lts parse_lts_action(const std::string &multi_action_string, const data::data_specification &data_spec, lps::multi_action_type_checker &typechecker)
Parse a string into an action label.
Definition lts_lts.h:201
void group_transitions_on_label(std::vector< transition > &transitions, std::function< std::size_t(const transition &)> get_label, const std::size_t number_of_labels, const std::size_t tau_label_index)
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label.
void sort_transitions(std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
void determinise(LTS_TYPE &l)
Determinises this LTS.
void reduce(LTS_TYPE &l, lts_equivalence eq)
Applies a reduction algorithm to this LTS.
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, lts_equivalence eq, bool generate_counter_examples=false, const std::string &counter_example_file="", bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector< transition > &trans, const std::set< transition::size_type > &hide_label_set)
Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file=std::string(), const bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
std::string pp(const action_label_lts &l)
Print the action label to string.
Definition lts_lts.h:188
bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, lts_preorder pre, bool generate_counter_example, const std::string &counter_example_file="", bool structured_output=false, lps::exploration_strategy strategy=lps::es_breadth, bool preprocess=true)
Checks whether this LTS is smaller than another LTS according to a preorder.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector< transition > &trans, const std::set< transition::size_type > &hide_label_set)
Provide the transitions as a multimap accessible per from state and label.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
Merge the second lts into the first lts.
bool reachability_check(lts< SL, AL, BASE > &l, bool remove_unreachable=false)
Checks whether all states in this LTS are reachable from the initial state and remove unreachable sta...
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
void group_transitions_on_label(const std::vector< transition >::iterator begin, const std::vector< transition >::iterator end, std::function< std::size_t(const transition &)> get_label, std::vector< std::pair< std::size_t, std::size_t > > &count_sum_transitions_per_action, const std::size_t tau_label_index=0, std::vector< std::size_t > &todo_stack=bogus_todo_stack)
bool reachability_check(probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &l, bool remove_unreachable=false)
Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unre...
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, lts_preorder pre, bool generate_counter_example, const std::string &counter_example_file="", bool structured_output=false, lps::exploration_strategy strategy=lps::es_breadth, bool preprocess=true)
Checks whether this LTS is smaller than another LTS according to a preorder.
The main namespace for the Process library.
bool is_linear(const process_specification &p, bool verbose=false)
Returns true if the process specification is linear.
Definition is_linear.h:344
bool is_untyped_multi_action(const atermpp::aterm &x)
void swap(trans &t1, trans &t2) noexcept
\brief swap overload
bool is_alt(const atermpp::aterm &x)
bool is_untyped_regular_formula(const atermpp::aterm &x)
void make_trans(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const regular_formula &x)
void make_seq(atermpp::aterm &t, const ARGUMENTS &... args)
void make_trans_or_nil(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_trans(const atermpp::aterm &x)
std::string pp(const regular_formulas::trans &x, bool arg0)
void make_alt(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_regular_formula(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const regular_formulas::alt &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const trans &x)
void swap(untyped_regular_formula &t1, untyped_regular_formula &t2) noexcept
\brief swap overload
bool is_trans_or_nil(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const untyped_regular_formula &x)
bool is_regular_formula(const atermpp::aterm &x)
void swap(trans_or_nil &t1, trans_or_nil &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const trans_or_nil &x)
bool is_seq(const atermpp::aterm &x)
std::string pp(const regular_formulas::untyped_regular_formula &x, bool arg0)
std::string pp(const regular_formulas::seq &x, bool arg0)
std::string pp(const regular_formulas::trans_or_nil &x, bool arg0)
void swap(seq &t1, seq &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const seq &x)
void swap(regular_formula &t1, regular_formula &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const alt &x)
std::string pp(const regular_formulas::regular_formula &x, bool arg0)
void swap(alt &t1, alt &t2) noexcept
\brief swap overload
bool is_timed(const state_formula &x)
void swap(variable &t1, variable &t2) noexcept
\brief swap overload
bool is_infimum(const atermpp::aterm &x)
std::string pp(const state_formulas::nu &x, bool arg0)
std::string pp(const state_formulas::exists &x, bool arg0)
std::string pp(const state_formulas::not_ &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const not_ &x)
bool is_and(const atermpp::aterm &x)
void swap(minus &t1, minus &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const sum &x)
std::string pp(const state_formulas::supremum &x, bool arg0)
bool is_delay_timed(const atermpp::aterm &x)
void swap(exists &t1, exists &t2) noexcept
\brief swap overload
bool is_const_multiply(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const exists &x)
std::string pp(const state_formulas::must &x, bool arg0)
void swap(const_multiply_alt &t1, const_multiply_alt &t2) noexcept
\brief swap overload
bool is_minus(const atermpp::aterm &x)
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_exists(const atermpp::aterm &x)
void swap(may &t1, may &t2) noexcept
\brief swap overload
void swap(mu &t1, mu &t2) noexcept
\brief swap overload
bool is_not(const atermpp::aterm &x)
std::string pp(const state_formulas::minus &x, bool arg0)
bool is_state_formula(const atermpp::aterm &x)
void swap(sum &t1, sum &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const const_multiply &x)
std::ostream & operator<<(std::ostream &out, const may &x)
void make_const_multiply(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const nu &x)
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(supremum &t1, supremum &t2) noexcept
\brief swap overload
bool is_supremum(const atermpp::aterm &x)
void swap(true_ &t1, true_ &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const minus &x)
bool is_must(const atermpp::aterm &x)
void swap(const_multiply &t1, const_multiply &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const state_formulas::state_formula &x)
std::ostream & operator<<(std::ostream &out, const imp &x)
bool is_yaled(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const mu &x)
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const must &x)
std::ostream & operator<<(std::ostream &out, const supremum &x)
void swap(not_ &t1, not_ &t2) noexcept
\brief swap overload
std::set< data::variable > find_free_variables(const state_formulas::state_formula &x)
void swap(state_formula &t1, state_formula &t2) noexcept
\brief swap overload
bool is_true(const atermpp::aterm &x)
std::string pp(const state_formulas::true_ &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const true_ &x)
std::string pp(const state_formulas::state_formula &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const variable &x)
std::ostream & operator<<(std::ostream &out, const state_formula &x)
void swap(plus &t1, plus &t2) noexcept
\brief swap overload
std::string pp(const state_formulas::const_multiply &x, bool arg0)
void make_plus(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const and_ &x)
std::string pp(const state_formulas::delay_timed &x, bool arg0)
void swap(yaled &t1, yaled &t2) noexcept
\brief swap overload
void swap(delay &t1, delay &t2) noexcept
\brief swap overload
bool is_variable(const atermpp::aterm &x)
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const forall &x)
void make_infimum(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_may(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const yaled_timed &x)
bool is_yaled_timed(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
void swap(yaled_timed &t1, yaled_timed &t2) noexcept
\brief swap overload
void make_delay_timed(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const state_formulas::imp &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const or_ &x)
std::string pp(const state_formulas::mu &x, bool arg0)
void make_const_multiply_alt(atermpp::aterm &t, const ARGUMENTS &... args)
void make_may(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_sum(const atermpp::aterm &x)
state_formulas::state_formula translate_user_notation(const state_formulas::state_formula &x)
void make_must(atermpp::aterm &t, const ARGUMENTS &... args)
state_formulas::state_formula normalize_sorts(const state_formulas::state_formula &x, const data::sort_specification &sortspec)
void swap(and_ &t1, and_ &t2) noexcept
\brief swap overload
bool is_nu(const atermpp::aterm &x)
void swap(false_ &t1, false_ &t2) noexcept
\brief swap overload
std::string pp(const state_formulas::delay &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const false_ &x)
std::string pp(const state_formulas::forall &x, bool arg0)
void swap(forall &t1, forall &t2) noexcept
\brief swap overload
std::string pp(const state_formulas::sum &x, bool arg0)
void swap(delay_timed &t1, delay_timed &t2) noexcept
\brief swap overload
void swap(infimum &t1, infimum &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const plus &x)
std::string pp(const state_formulas::yaled &x, bool arg0)
bool is_delay(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const infimum &x)
std::string pp(const state_formulas::infimum &x, bool arg0)
std::string pp(const state_formulas::or_ &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const delay &x)
std::string pp(const state_formulas::may &x, bool arg0)
bool is_false(const atermpp::aterm &x)
void make_variable(atermpp::aterm &t, const ARGUMENTS &... args)
void make_nu(atermpp::aterm &t, const ARGUMENTS &... args)
void make_supremum(atermpp::aterm &t, const ARGUMENTS &... args)
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(must &t1, must &t2) noexcept
\brief swap overload
bool is_plus(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const delay_timed &x)
void swap(nu &t1, nu &t2) noexcept
\brief swap overload
std::string pp(const state_formulas::and_ &x, bool arg0)
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const state_formulas::false_ &x, bool arg0)
std::string pp(const state_formulas::const_multiply_alt &x, bool arg0)
bool is_mu(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
void make_minus(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_const_multiply_alt(const atermpp::aterm &x)
void swap(or_ &t1, or_ &t2) noexcept
\brief swap overload
std::string pp(const state_formulas::yaled_timed &x, bool arg0)
std::string pp(const state_formulas::plus &x, bool arg0)
bool is_or(const atermpp::aterm &x)
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
void make_yaled_timed(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const state_formulas::variable &x, bool arg0)
void swap(imp &t1, imp &t2) noexcept
\brief swap overload
std::set< data::sort_expression > find_sort_expressions(const state_formulas::state_formula &x)
bool find_nil(const state_formulas::state_formula &x)
std::ostream & operator<<(std::ostream &out, const const_multiply_alt &x)
std::set< process::action_label > find_action_labels(const state_formulas::state_formula &x)
std::ostream & operator<<(std::ostream &out, const yaled &x)
void make_mu(atermpp::aterm &t, const ARGUMENTS &... args)
std::set< core::identifier_string > find_identifiers(const state_formulas::state_formula &x)
static const atermpp::aterm StateMay
static const atermpp::aterm StateOr
static const atermpp::aterm UntypedRegFrm
static const atermpp::aterm StateFrm
static const atermpp::aterm StateYaled
static const atermpp::aterm RegAlt
static const atermpp::aterm ActNot
static const atermpp::aterm ActImp
static const atermpp::aterm ActTrue
static const atermpp::aterm StateInfimum
static const atermpp::aterm StateAnd
static const atermpp::aterm StateExists
static const atermpp::aterm RegTrans
static const atermpp::aterm ActOr
static const atermpp::aterm StateConstantMultiplyAlt
static const atermpp::aterm ActFrm
static const atermpp::aterm ActForall
static const atermpp::aterm StateYaledTimed
static const atermpp::aterm ActFalse
static const atermpp::aterm StateFalse
static const atermpp::aterm RegFrm
static const atermpp::aterm StateDelay
static const atermpp::aterm StatePlus
static const atermpp::aterm StateMinus
static const atermpp::aterm StateNu
static const atermpp::aterm ActAnd
static const atermpp::aterm StateDelayTimed
static const atermpp::aterm StateSupremum
static const atermpp::aterm StateSum
static const atermpp::aterm ActAt
static const atermpp::aterm ActExists
static const atermpp::aterm StateMu
static const atermpp::aterm RegTransOrNil
static const atermpp::aterm StateVar
static const atermpp::aterm StateImp
static const atermpp::aterm RegSeq
static const atermpp::aterm StateTrue
static const atermpp::aterm StateForall
static const atermpp::aterm StateMust
static const atermpp::aterm StateNot
static const atermpp::aterm ActMultAct
static const atermpp::aterm StateConstantMultiply
std::vector< transition > non_inert_transitions
std::vector< non_bottom_state > non_bottom_states
non_bottom_state(const state_type s, const std::vector< state_type > &it)
Converts a process expression into linear process format. Use the convert member functions for this.
lps::specification convert(const process_specification &p)
Converts a process_specification into a specification. Throws non_linear_process if a non-linear sub-...
Converts a process expression into linear process format. Use the convert member functions for this.
lps::stochastic_specification convert(const process_specification &p)
Converts a process_specification into a stochastic_specification. Throws non_linear_process if a non-...
std::size_t operator()(const mcrl2::lts::action_label_lts &as) const
Definition lts_lts.h:424