RefinementCommand.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <vector>
 
#include <boost/optional.hpp>
 
#include "storm/storage/expressions/Expression.h"
 
namespace storm::gbar {
namespace abstraction {
 
class RefinementCommand {
   public:
    RefinementCommand(uint64_t referencedPlayer1Choice, std::vector<storm::expressions::Expression> const& predicates);
 
    RefinementCommand(std::vector<storm::expressions::Expression> const& predicates);
 
    bool refersToPlayer1Choice() const;
    uint64_t getReferencedPlayer1Choice() const;
    std::vector<storm::expressions::Expression> const& getPredicates() const;
 
   private:
    boost::optional<uint64_t> referencedPlayer1Choice;
    std::vector<storm::expressions::Expression> predicates;
};
 
}  // namespace abstraction
}  // namespace storm::gbar