TerminalStatesGetter.h

Go to the documentation of this file.

#pragma once
 
#include <functional>
#include <string>
#include <vector>
 
namespace storm {
 
namespace expressions {
class Expression;
}
namespace logic {
class Formula;
}
 
namespace builder {
 
void getTerminalStatesFromFormula(storm::logic::Formula const& formula,
                                  std::function<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback,
                                  std::function<void(std::string const&, bool)> const& terminalLabelCallback);
 
struct TerminalStates {
    std::vector<storm::expressions::Expression> terminalExpressions;         // if one of these is true, we can stop exploration
    std::vector<storm::expressions::Expression> negatedTerminalExpressions;  // if one of these is false, we can stop exploration
    std::vector<std::string> terminalLabels;                                 // if a state has one of these labels, we can stop exploration
    std::vector<std::string> negatedTerminalLabels;                          // if a state does not have all of these labels, we can stop exploration
 
    void clear();
 
    bool empty() const;
 
    storm::expressions::Expression asExpression(std::function<storm::expressions::Expression(std::string const&)> const& labelToExpressionMap) const;
};
 
TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula);
 
}  // namespace builder
}  // namespace storm