Label.h

Go to the documentation of this file.

#pragma once
 
#include <map>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/prism/LocatedInformation.h"
 
namespace storm {
namespace storage {
namespace expressions {
class Variable;
}
}  // namespace storage
}  // namespace storm
 
namespace storm {
namespace prism {
class Label : public LocatedInformation {
   public:
    Label(std::string const& name, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "",
          uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    Label() = default;
    Label(Label const& other) = default;
    Label& operator=(Label const& other) = default;
    Label(Label&& other) = default;
    Label& operator=(Label&& other) = default;

    std::string const& getName() const;

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

    Label substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
    Label substituteNonStandardPredicates() const;
 
    friend std::ostream& operator<<(std::ostream& stream, Label const& label);
 
   private:
    // The name of the label.
    std::string name;
 
    // A predicate that needs to be satisfied by states for the label to be attached.
    storm::expressions::Expression statePredicateExpression;
};
 
class ObservationLabel : public Label {
   public:
    ObservationLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "",
                     uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    ObservationLabel() = default;
    ObservationLabel(ObservationLabel const& other) = default;
    ObservationLabel& operator=(ObservationLabel const& other) = default;
    ObservationLabel(ObservationLabel&& other) = default;
    ObservationLabel& operator=(ObservationLabel&& other) = default;

    ObservationLabel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
    ObservationLabel substituteNonStandardPredicates() const;
};
 
}  // namespace prism
}  // namespace storm