sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added two tests for exploration engine 

Former-commit-id: 960393b229
tempestpy_adaptions
dehnert 9 years ago
parent
d2b3f90a76
commit
60bbce0ba1
12 changed files with 190 additions and 86 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/cli/entrypoints.h
  2. 1
      src/logic/FragmentSpecification.cpp
  3. 2
      src/modelchecker/CheckTask.h
  4. 92
      src/modelchecker/exploration/SparseExplorationModelChecker.cpp
  5. 13
      src/modelchecker/exploration/SparseExplorationModelChecker.h
  6. 9
      src/settings/modules/ExplorationSettings.cpp
  7. 9
      src/settings/modules/ExplorationSettings.h
  8. 2
      src/utility/storm.h
  9. 8
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  10. 16
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  11. 36
      test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  12. 86
      test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp

2
src/cli/entrypoints.h
View File

@ -61,7 +61,7 @@ namespace storm {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs."); STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::cout << std::endl << "Model checking property: " << *formula << " ...";
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
storm::modelchecker::SparseMdpExplorationModelChecker<ValueType> checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::generalSettings().getConstantDefinitionString()));
storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::generalSettings().getConstantDefinitionString()));
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (checker.canHandle(task)) { if (checker.canHandle(task)) {
result = checker.check(task); result = checker.check(task);

1
src/logic/FragmentSpecification.cpp
View File

@ -414,6 +414,7 @@ namespace storm {
FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) { FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) {
operatorAtTopLevelRequired = newValue; operatorAtTopLevelRequired = newValue;
return *this;
} }
} }

2
src/modelchecker/CheckTask.h
View File

@ -23,7 +23,7 @@ namespace storm {
/* /*
* This class is used to customize the checking process of a formula. * This class is used to customize the checking process of a formula.
*/ */
template<typename FormulaType, typename ValueType = double>
template<typename FormulaType = storm::logic::Formula, typename ValueType = double>
class CheckTask { class CheckTask {
public: public:
template<typename OtherFormulaType, typename OtherValueType> template<typename OtherFormulaType, typename OtherValueType>

92
src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp → src/modelchecker/exploration/SparseExplorationModelChecker.cpp
View File

@ -1,4 +1,4 @@
#include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.h"
#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "src/modelchecker/exploration/ExplorationInformation.h" #include "src/modelchecker/exploration/ExplorationInformation.h"
#include "src/modelchecker/exploration/StateGeneration.h" #include "src/modelchecker/exploration/StateGeneration.h"
@ -33,20 +33,20 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
template<typename ValueType>
SparseMdpExplorationModelChecker<ValueType>::SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram<ValueType>(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator() {
template<typename ValueType, typename StateType>
SparseExplorationModelChecker<ValueType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram<ValueType>(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::explorationSettings().getPrecision()) {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
template<typename ValueType, typename StateType>
bool SparseExplorationModelChecker<ValueType, StateType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::Formula const& formula = checkTask.getFormula();
storm::logic::FragmentSpecification fragment = storm::logic::reachability(); storm::logic::FragmentSpecification fragment = storm::logic::reachability();
return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
} }
template<typename ValueType>
std::unique_ptr<CheckResult> SparseMdpExplorationModelChecker<ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
template<typename ValueType, typename StateType>
std::unique_ptr<CheckResult> SparseExplorationModelChecker<ValueType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
storm::logic::UntilFormula const& untilFormula = checkTask.getFormula(); storm::logic::UntilFormula const& untilFormula = checkTask.getFormula();
storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula(); storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula();
storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula(); storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula();
@ -66,8 +66,8 @@ namespace storm {
return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
} }
template<typename ValueType>
std::tuple<typename SparseMdpExplorationModelChecker<ValueType>::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const {
template<typename ValueType, typename StateType>
std::tuple<StateType, ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const {
// Generate the initial state so we know where to start the simulation. // Generate the initial state so we know where to start the simulation.
stateGeneration.computeInitialStates(); stateGeneration.computeInitialStates();
STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine.");
@ -119,8 +119,8 @@ namespace storm {
return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation)); return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation));
} }
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
template<typename ValueType, typename StateType>
bool SparseExplorationModelChecker<ValueType, StateType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
// Start the search from the initial state. // Start the search from the initial state.
stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0)); stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0));
@ -181,8 +181,8 @@ namespace storm {
return foundTerminalState; return foundTerminalState;
} }
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
template<typename ValueType, typename StateType>
bool SparseExplorationModelChecker<ValueType, StateType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
bool isTerminalState = false; bool isTerminalState = false;
bool isTargetState = false; bool isTargetState = false;
@ -283,8 +283,8 @@ namespace storm {
return isTerminalState; return isTerminalState;
} }
template<typename ValueType>
typename SparseMdpExplorationModelChecker<ValueType>::ActionType SparseMdpExplorationModelChecker<ValueType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
template<typename ValueType, typename StateType>
typename SparseExplorationModelChecker<ValueType, StateType>::ActionType SparseExplorationModelChecker<ValueType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
// Determine the values of all available actions. // Determine the values of all available actions.
std::vector<std::pair<ActionType, ValueType>> actionValues; std::vector<std::pair<ActionType, ValueType>> actionValues;
StateType rowGroup = explorationInformation.getRowGroup(currentStateId); StateType rowGroup = explorationInformation.getRowGroup(currentStateId);
@ -321,14 +321,13 @@ namespace storm {
return actionValues[distribution(randomGenerator)].first; return actionValues[distribution(randomGenerator)].first;
} }
template<typename ValueType>
typename SparseMdpExplorationModelChecker<ValueType>::StateType SparseMdpExplorationModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
template<typename ValueType, typename StateType>
StateType SparseExplorationModelChecker<ValueType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction); std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
if (row.size() == 1) { if (row.size() == 1) {
return row.front().getColumn(); return row.front().getColumn();
} }
// Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen. // Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen.
if (explorationInformation.useDifferenceProbabilitySumHeuristic() || explorationInformation.useProbabilityHeuristic()) { if (explorationInformation.useDifferenceProbabilitySumHeuristic() || explorationInformation.useProbabilityHeuristic()) {
std::vector<ValueType> probabilities(row.size()); std::vector<ValueType> probabilities(row.size());
@ -347,14 +346,15 @@ namespace storm {
// Now sample according to the probabilities. // Now sample according to the probabilities.
std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end()); std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end());
return row[distribution(randomGenerator)].getColumn(); return row[distribution(randomGenerator)].getColumn();
} else if (explorationInformation.useUniformHeuristic()) {
} else {
STORM_LOG_ASSERT(explorationInformation.useUniformHeuristic(), "Illegal next-state heuristic.");
std::uniform_int_distribution<ActionType> distribution(0, row.size() - 1); std::uniform_int_distribution<ActionType> distribution(0, row.size() - 1);
return row[distribution(randomGenerator)].getColumn(); return row[distribution(randomGenerator)].getColumn();
} }
} }
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
template<typename ValueType, typename StateType>
bool SparseExplorationModelChecker<ValueType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
++stats.numberOfPrecomputations; ++stats.numberOfPrecomputations;
// Outline: // Outline:
@ -370,7 +370,7 @@ namespace storm {
std::vector<StateType> relevantStates; std::vector<StateType> relevantStates;
if (explorationInformation.useLocalPrecomputation()) { if (explorationInformation.useLocalPrecomputation()) {
for (auto const& stateActionPair : stack) { for (auto const& stateActionPair : stack) {
if (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
if (explorationInformation.maximize() || !storm::utility::isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
relevantStates.push_back(stateActionPair.first); relevantStates.push_back(stateActionPair.first);
} }
} }
@ -486,8 +486,8 @@ namespace storm {
return true; return true;
} }
template<typename ValueType>
void SparseMdpExplorationModelChecker<ValueType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
template<typename ValueType, typename StateType>
void SparseExplorationModelChecker<ValueType, StateType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
bool containsTargetState = false; bool containsTargetState = false;
// Now we record all actions leaving the EC. // Now we record all actions leaving the EC.
@ -498,7 +498,7 @@ namespace storm {
StateType originalRowGroup = explorationInformation.getRowGroup(originalState); StateType originalRowGroup = explorationInformation.getRowGroup(originalState);
// Check whether a target state is contained in the MEC. // Check whether a target state is contained in the MEC.
if (!containsTargetState && comparator.isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) {
if (!containsTargetState && storm::utility::isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) {
containsTargetState = true; containsTargetState = true;
} }
@ -555,8 +555,8 @@ namespace storm {
} }
} }
template<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
template<typename ValueType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType result = storm::utility::zero<ValueType>(); ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
@ -564,8 +564,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
template<typename ValueType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType result = storm::utility::zero<ValueType>(); ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
@ -573,8 +573,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType>
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
template<typename ValueType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
// TODO: take into account self-loops? // TODO: take into account self-loops?
std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()); std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
@ -584,8 +584,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType>
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
template<typename ValueType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
StateType group = explorationInformation.getRowGroup(currentStateId); StateType group = explorationInformation.getRowGroup(currentStateId);
std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection()); std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection());
for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) { for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) {
@ -595,8 +595,8 @@ namespace storm {
return result; return result;
} }
template<typename ValueType>
void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
template<typename ValueType, typename StateType>
void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
stack.pop_back(); stack.pop_back();
while (!stack.empty()) { while (!stack.empty()) {
updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds);
@ -604,8 +604,8 @@ namespace storm {
} }
} }
template<typename ValueType>
void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
template<typename ValueType, typename StateType>
void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
// Compute the new lower/upper values of the action. // Compute the new lower/upper values of the action.
std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds);
@ -639,8 +639,8 @@ namespace storm {
} }
} }
template<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
template<typename ValueType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection()); ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection());
ActionType group = explorationInformation.getRowGroup(state); ActionType group = explorationInformation.getRowGroup(state);
@ -658,14 +658,14 @@ namespace storm {
return bound; return bound;
} }
template<typename ValueType>
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::getLowestBounds(storm::OptimizationDirection const& direction) const {
template<typename ValueType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const {
ValueType val = getLowestBound(direction); ValueType val = getLowestBound(direction);
return std::make_pair(val, val); return std::make_pair(val, val);
} }
template<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::getLowestBound(storm::OptimizationDirection const& direction) const {
template<typename ValueType, typename StateType>
ValueType SparseExplorationModelChecker<ValueType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const {
if (direction == storm::OptimizationDirection::Maximize) { if (direction == storm::OptimizationDirection::Maximize) {
return storm::utility::zero<ValueType>(); return storm::utility::zero<ValueType>();
} else { } else {
@ -673,8 +673,8 @@ namespace storm {
} }
} }
template<typename ValueType>
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const {
template<typename ValueType, typename StateType>
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const {
if (direction == storm::OptimizationDirection::Maximize) { if (direction == storm::OptimizationDirection::Maximize) {
return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second)); return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second));
} else { } else {
@ -682,6 +682,6 @@ namespace storm {
} }
} }
template class SparseMdpExplorationModelChecker<double>;
template class SparseExplorationModelChecker<double, uint32_t>;
} }
} }

13
src/modelchecker/exploration/SparseMdpExplorationModelChecker.h → src/modelchecker/exploration/SparseExplorationModelChecker.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_
#define STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_
#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_
#define STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_
#include <random> #include <random>
@ -30,14 +30,13 @@ namespace storm {
using namespace exploration_detail; using namespace exploration_detail;
template<typename ValueType>
class SparseMdpExplorationModelChecker : public AbstractModelChecker {
template<typename ValueType, typename StateType = uint32_t>
class SparseExplorationModelChecker : public AbstractModelChecker {
public: public:
typedef uint32_t StateType;
typedef StateType ActionType; typedef StateType ActionType;
typedef std::vector<std::pair<StateType, ActionType>> StateActionStack; typedef std::vector<std::pair<StateType, ActionType>> StateActionStack;
SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions);
SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions = boost::none);
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override; virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
@ -87,4 +86,4 @@ namespace storm {
} }
} }
#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ */
#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_ */

9
src/settings/modules/ExplorationSettings.cpp
View File

@ -15,6 +15,8 @@ namespace storm {
const std::string ExplorationSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp"; const std::string ExplorationSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp";
const std::string ExplorationSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp"; const std::string ExplorationSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp";
const std::string ExplorationSettings::nextStateHeuristicOptionName = "nextstate"; const std::string ExplorationSettings::nextStateHeuristicOptionName = "nextstate";
const std::string ExplorationSettings::precisionOptionName = "precision";
const std::string ExplorationSettings::precisionOptionShortName = "eps";
ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> types = { "local", "global" }; std::vector<std::string> types = { "local", "global" };
@ -24,6 +26,9 @@ namespace storm {
std::vector<std::string> nextStateHeuristics = { "probdiffs", "prob", "unif" }; std::vector<std::string> nextStateHeuristics = { "probdiffs", "prob", "unif" };
this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
} }
bool ExplorationSettings::isLocalPrecomputationSet() const { bool ExplorationSettings::isLocalPrecomputationSet() const {
@ -74,6 +79,10 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'."); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'.");
} }
double ExplorationSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
bool ExplorationSettings::check() const { bool ExplorationSettings::check() const {
bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() || bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() ||
this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() ||

9
src/settings/modules/ExplorationSettings.h
View File

@ -74,6 +74,13 @@ namespace storm {
*/ */
NextStateHeuristic getNextStateHeuristic() const; NextStateHeuristic getNextStateHeuristic() const;
/*!
* Retrieves the precision to use for numerical operations.
*
* @return The precision to use for numerical operations.
*/
double getPrecision() const;
virtual bool check() const override; virtual bool check() const override;
// The name of the module. // The name of the module.
@ -85,6 +92,8 @@ namespace storm {
static const std::string numberOfExplorationStepsUntilPrecomputationOptionName; static const std::string numberOfExplorationStepsUntilPrecomputationOptionName;
static const std::string numberOfSampledPathsUntilPrecomputationOptionName; static const std::string numberOfSampledPathsUntilPrecomputationOptionName;
static const std::string nextStateHeuristicOptionName; static const std::string nextStateHeuristicOptionName;
static const std::string precisionOptionName;
static const std::string precisionOptionShortName;
}; };
} // namespace modules } // namespace modules
} // namespace settings } // namespace settings

2
src/utility/storm.h
View File

@ -57,7 +57,7 @@
#include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.h"
#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"

8
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -157,7 +157,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -181,7 +181,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -205,7 +205,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -268,7 +268,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());

16
test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -157,8 +157,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -181,8 +181,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -205,8 +205,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -268,8 +268,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::nativeEquationSolverSettings().getPrecision());

36
test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -211,7 +211,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -219,7 +219,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -243,7 +243,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -251,7 +251,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -284,7 +284,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -293,7 +293,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -302,7 +302,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -311,7 +311,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -320,7 +320,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2. / 3., quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(2. / 3., quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -329,7 +329,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -370,7 +370,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -379,7 +379,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -388,7 +388,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -397,7 +397,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -406,7 +406,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -415,7 +415,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -492,7 +492,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(37. / 60., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(37. / 60., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@ -505,7 +505,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());

86
test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp
View File

@ -0,0 +1,86 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/logic/Formulas.h"
#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/ExplorationSettings.h"
TEST(SparseExplorationModelCheckerTest, Dice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
storm::modelchecker::SparseExplorationModelChecker<double, uint32_t> checker(program);
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::explorationSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::explorationSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::explorationSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::explorationSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::explorationSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::explorationSettings().getPrecision());
}
TEST(SparseExplorationModelCheckerTest, AsynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
storm::modelchecker::SparseExplorationModelChecker<double, uint32_t> checker(program);
std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::explorationSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::explorationSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save