algorithms.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// 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_MODAL_FORMULA_ALGORITHMS_H
#define MCRL2_MODAL_FORMULA_ALGORITHMS_H
 
#include "mcrl2/lps/stochastic_specification.h"
#include "mcrl2/modal_formula/state_formula_specification.h"
 
namespace mcrl2 {
 
namespace state_formulas {
 
namespace algorithms {
 
// spec may be updated as the data implementation of the state formula
// may cause internal names to change.
state_formula parse_state_formula(std::istream& in, lps::stochastic_specification& spec, const bool formula_is_quantitative);
 
// spec may be updated as the data implementation of the state formula
// may cause internal names to change.
state_formula parse_state_formula(const std::string& formula_text, lps::stochastic_specification& spec, const bool formula_is_quantitative);
 
state_formula_specification parse_state_formula_specification(std::istream& in, const bool formula_is_quantitative);
 
state_formula_specification parse_state_formula_specification(const std::string& text, const bool formula_is_quantitative);
 
state_formula_specification parse_state_formula_specification(std::istream& in, lps::stochastic_specification& lpsspec, const bool formula_is_quantitative);
 
state_formula_specification parse_state_formula_specification(const std::string& text, lps::stochastic_specification& lpsspec, const bool formula_is_quantitative);
 
bool is_monotonous(const state_formula& f);
 
state_formula normalize(const state_formula& x);
 
bool is_normalized(const state_formula& x);
 
std::set<core::identifier_string> find_state_variable_names(const state_formula& x);
 
} // namespace algorithms
 
} // namespace state_formulas
 
} // namespace mcrl2
 
#endif // MCRL2_MODAL_FORMULA_ALGORITHMS_H