Update.h

Go to the documentation of this file.

#pragma once
 
#include <vector>
 
#include "storm/storage/prism/Assignment.h"
#include "storm/storage/prism/LocatedInformation.h"
 
namespace storm {
namespace prism {
class Update : public LocatedInformation {
   public:
    using ExpressionPair = std::pair<storm::expressions::Expression, storm::expressions::Expression>;

    Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments,
           std::string const& filename = "", uint_fast64_t lineNumber = 0);
    Update(uint_fast64_t globalIndex, ExpressionPair const& likelihoodExpressionInterval, std::vector<storm::prism::Assignment> const& assignments,
           std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    Update() = default;
    Update(Update const& other) = default;
    Update& operator=(Update const& other) = default;
    Update(Update&& other) = default;
    Update& operator=(Update&& other) = default;
 
    bool isLikelihoodInterval() const;

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

    ExpressionPair const& getLikelihoodExpressionInterval() const;

    std::size_t getNumberOfAssignments() const;

    std::vector<storm::prism::Assignment> const& getAssignments() const;

    std::vector<storm::prism::Assignment>& getAssignments();

    storm::prism::Assignment const& getAssignment(std::string const& variableName) const;

    std::map<storm::expressions::Variable, storm::expressions::Expression> getAsVariableToExpressionMap() const;

    uint_fast64_t getGlobalIndex() const;

    Update substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;

    Update removeIdentityAssignments() const;
 
    Update substituteNonStandardPredicates() const;

    Update simplify() const;
 
    friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);
 
   private:
    void createAssignmentMapping();
 
    // Expressions specifying the likelihood of taking this update.
    // Either both expressions are initialized (representing an interval likelihood [first, second] for interval models)
    // or only the first one is initialized (standard, non-interval interpretation)
    ExpressionPair likelihoodExpressions;
 
    // The assignments of this update.
    std::vector<storm::prism::Assignment> assignments;
 
    // A mapping from variable names to their assignments.
    std::map<std::string, uint_fast64_t> variableToAssignmentIndexMap;
 
    // The global index of the update.
    uint_fast64_t globalIndex;
};
}  // namespace prism
}  // namespace storm