Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Formula.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_FORMULA_H_
2#define STORM_STORAGE_PRISM_FORMULA_H_
3
4#include <boost/optional.hpp>
5#include <map>
6
10
11namespace storm {
12namespace prism {
14 public:
23 Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename = "",
24 uint_fast64_t lineNumber = 0);
25
34 Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
35
43 Formula(std::string const& name, std::string const& filename = "", uint_fast64_t lineNumber = 0);
44
45 // Create default implementations of constructors/assignment.
46 Formula() = default;
47 Formula(Formula const& other) = default;
48 Formula& operator=(Formula const& other) = default;
49 Formula(Formula&& other) = default;
50 Formula& operator=(Formula&& other) = default;
51
57 std::string const& getName() const;
58
63 bool hasExpressionVariable() const;
64
71
78
84 storm::expressions::Type const& getType() const;
85
93 Formula substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
95
96 friend std::ostream& operator<<(std::ostream& stream, Formula const& formula);
97
98 private:
99 // The name of the formula.
100 std::string name;
101
102 // Expression variable that is used as a placeholder for this formula
103 boost::optional<storm::expressions::Variable> variable;
104
105 // A predicate that needs to be satisfied by states for the label to be attached.
107};
108} // namespace prism
109} // namespace storm
110
111#endif /* STORM_STORAGE_PRISM_FORMULA_H_ */
Formula(Formula const &other)=default
Formula substituteNonStandardPredicates() const
Definition Formula.cpp:51
Formula & operator=(Formula &&other)=default
friend std::ostream & operator<<(std::ostream &stream, Formula const &formula)
Definition Formula.cpp:60
storm::expressions::Expression const & getExpression() const
Retrieves the expression that is associated with this formula.
Definition Formula.cpp:32
bool hasExpressionVariable() const
Retrieves wheter a placeholder variable is used in expressions to represent this formula.
Definition Formula.cpp:24
Formula substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all variables in the expression of the formula according to the given map.
Definition Formula.cpp:42
Formula(Formula &&other)=default
std::string const & getName() const
Retrieves the name that is associated with this formula.
Definition Formula.cpp:20
Formula & operator=(Formula const &other)=default
storm::expressions::Type const & getType() const
Retrieves the return type of the formula, i.e., the return-type of the defining expression.
Definition Formula.cpp:36
storm::expressions::Variable const & getExpressionVariable() const
Retrieves the placeholder variable that is used in expressions to represent this formula.
Definition Formula.cpp:28
LabParser.cpp.