Formula.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <map>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/prism/LocatedInformation.h"
 
namespace storm {
namespace prism {
class Formula : public LocatedInformation {
   public:
    Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename = "",
            uint_fast64_t lineNumber = 0);

    Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);

    Formula(std::string const& name, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    Formula() = default;
    Formula(Formula const& other) = default;
    Formula& operator=(Formula const& other) = default;
    Formula(Formula&& other) = default;
    Formula& operator=(Formula&& other) = default;

    std::string const& getName() const;

    bool hasExpressionVariable() const;

    storm::expressions::Variable const& getExpressionVariable() const;

    storm::expressions::Expression const& getExpression() const;

    storm::expressions::Type const& getType() const;

    Formula substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
    Formula substituteNonStandardPredicates() const;
 
    friend std::ostream& operator<<(std::ostream& stream, Formula const& formula);
 
   private:
    // The name of the formula.
    std::string name;
 
    // Expression variable that is used as a placeholder for this formula
    boost::optional<storm::expressions::Variable> variable;
 
    // A predicate that needs to be satisfied by states for the label to be attached.
    storm::expressions::Expression expression;
};
}  // namespace prism
}  // namespace storm