Command.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_PRISM_COMMAND_H_
#define STORM_STORAGE_PRISM_COMMAND_H_
 
#include <map>
#include <string>
#include <vector>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/prism/Update.h"
 
namespace storm {
namespace prism {
class Command : public LocatedInformation {
   public:
    Command(uint_fast64_t globalIndex, bool markovian, uint_fast64_t actionIndex, std::string const& actionName,
            storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename = "",
            uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    Command() = default;
    Command(Command const& other) = default;
    Command& operator=(Command const& other) = default;
    Command(Command&& other) = default;
    Command& operator=(Command&& other) = default;
 
    std::string const& getActionName() const;
 
    uint_fast64_t getActionIndex() const;
 
    bool isMarkovian() const;
 
    void setMarkovian(bool value);
 
    storm::expressions::Expression const& getGuardExpression() const;
 
    std::size_t getNumberOfUpdates() const;
 
    storm::prism::Update const& getUpdate(uint_fast64_t index) const;
 
    std::vector<storm::prism::Update> const& getUpdates() const;
 
    std::vector<storm::prism::Update>& getUpdates();
 
    uint_fast64_t getGlobalIndex() const;
 
    Command substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
 
    Command substituteNonStandardPredicates() const;
    bool isLabeled() const;
 
    bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
 
    friend std::ostream& operator<<(std::ostream& stream, Command const& command);
 
    Command simplify() const;
 
   private:
    //  The index of the action associated with this command.
    uint_fast64_t actionIndex;
 
    // A flag indicating whether the likelihoods attached to the updates are to be interpreted as rates rather
    // than probabilities.
    bool markovian;
 
    // The name of the command.
    std::string actionName;
 
    // The expression that defines the guard of the command.
    storm::expressions::Expression guardExpression;
 
    // The list of updates of the command.
    std::vector<storm::prism::Update> updates;
 
    // The global index of the command.
    uint_fast64_t globalIndex;
 
    // A flag indicating whether the command is labeled.
    bool labeled;
 
    Command copyWithNewUpdates(std::vector<Update>&& newUpdates) const;
};
 
}  // namespace prism
}  // namespace storm
 
#endif /* STORM_STORAGE_PRISM_COMMAND_H_ */