diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7587a3f22..345efa36c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -21,6 +21,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_HELPER_FILES ${PROJECT_SOURCE_DIR}/sr file(GLOB STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp) +file(GLOB_RECURSE STORM_MODELCHECKER_EXPLORATION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp) file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) @@ -68,6 +69,7 @@ source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES}) source_group(modelchecker\\prctl\\helper FILES ${STORM_MODELCHECKER_PRCTL_HELPER_FILES}) source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES}) source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FILES}) +source_group(modelchecker\\exploration FILES ${STORM_MODELCHECKER_EXPLORATION_FILES}) source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES}) source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES}) source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES}) diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 505ec0cd3..17291f750 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -55,33 +55,33 @@ namespace storm { } template - void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { - STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently learning-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 << " ..."; storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - storm::modelchecker::SparseMdpLearningModelChecker checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::generalSettings().getConstantDefinitionString())); + storm::modelchecker::SparseMdpExplorationModelChecker checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::generalSettings().getConstantDefinitionString())); std::unique_ptr result; if (checker.canHandle(task)) { result = checker.check(task); + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } } else { std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl; } - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } } } #ifdef STORM_HAVE_CARL template<> - void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Learning-based verification does currently not support parametric models."); + void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif @@ -151,8 +151,8 @@ namespace storm { if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) { verifySymbolicModelWithAbstractionRefinementEngine(program, formulas, onlyInitialStatesRelevant); - } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning) { - verifySymbolicModelWithLearningEngine(program, formulas, onlyInitialStatesRelevant); + } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Exploration) { + verifySymbolicModelWithExplorationEngine(program, formulas, onlyInitialStatesRelevant); } else { storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel(program, formulas); STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException, diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 0064636b6..3ba8b89f7 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -59,6 +59,9 @@ namespace storm { template bool PrismNextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { + if (expression.isTrue()) { + return true; + } return evaluator.asBool(expression); } diff --git a/src/logic/CopyVisitor.cpp b/src/logic/CloneVisitor.cpp similarity index 100% rename from src/logic/CopyVisitor.cpp rename to src/logic/CloneVisitor.cpp diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 492230a33..de915eaa1 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -419,9 +419,13 @@ namespace storm { return visitor.substitute(*this); } - storm::expressions::Expression Formula::toExpression() const { + storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map const& labelToExpressionMapping) const { ToExpressionVisitor visitor; - return visitor.toExpression(*this); + if (labelToExpressionMapping.empty()) { + return visitor.toExpression(*this, manager); + } else { + return visitor.toExpression(*this->substitute(labelToExpressionMapping), manager); + } } std::shared_ptr Formula::asSharedPointer() { diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 11865b950..d5625a296 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -190,12 +190,15 @@ namespace storm { std::shared_ptr substitute(std::map const& labelSubstitution) const; /*! - * Takes the formula and converts it to an equivalent expression assuming that only atomic expression formulas - * and boolean connectives appear in the formula. + * Takes the formula and converts it to an equivalent expression. The formula may contain atomic labels, but + * then the given mapping must provide a corresponding expression. Other than that, only atomic expression + * formulas and boolean connectives may appear in the formula. * + * @param manager The manager responsible for the expressions in the formula and the resulting expression. + * @param A mapping from labels to the expressions that define them. * @return An equivalent expression. */ - storm::expressions::Expression toExpression() const; + storm::expressions::Expression toExpression(storm::expressions::ExpressionManager const& manager, std::map const& labelToExpressionMapping = {}) const; std::string toString() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 09bfc31dd..b86a96693 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -19,8 +19,13 @@ namespace storm { }; bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const { - boost::any result = f.accept(*this, InheritedInformation(specification)); - return boost::any_cast(result); + bool result = boost::any_cast(f.accept(*this, InheritedInformation(specification))); + + if (specification.isOperatorAtTopLevelRequired()) { + result &= f.isOperatorFormula(); + } + + return result; } boost::any FragmentChecker::visit(AtomicExpressionFormula const& f, boost::any const& data) const { diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index 31f2eeee2..6877496d2 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -17,6 +17,18 @@ namespace storm { return propositional; } + FragmentSpecification reachability() { + FragmentSpecification reachability = propositional(); + + reachability.setProbabilityOperatorsAllowed(true); + reachability.setUntilFormulasAllowed(true); + reachability.setReachabilityProbabilityFormulasAllowed(true); + reachability.setOperatorAtTopLevelRequired(true); + reachability.setNestedOperatorsAllowed(false); + + return reachability; + } + FragmentSpecification pctl() { FragmentSpecification pctl = propositional(); @@ -31,6 +43,14 @@ namespace storm { return pctl; } + FragmentSpecification flatPctl() { + FragmentSpecification flatPctl = pctl(); + + flatPctl.setNestedOperatorsAllowed(false); + + return flatPctl; + } + FragmentSpecification prctl() { FragmentSpecification prctl = pctl(); @@ -100,6 +120,8 @@ namespace storm { qualitativeOperatorResults = true; quantitativeOperatorResults = true; + + operatorAtTopLevelRequired = false; } FragmentSpecification FragmentSpecification::copy() const { @@ -386,6 +408,13 @@ namespace storm { return *this; } + bool FragmentSpecification::isOperatorAtTopLevelRequired() const { + return operatorAtTopLevelRequired; + } + + FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) { + operatorAtTopLevelRequired = newValue; + } } } \ No newline at end of file diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index 5074187b8..6637d0750 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -100,6 +100,9 @@ namespace storm { bool areQualitativeOperatorResultsAllowed() const; FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue); + bool isOperatorAtTopLevelRequired() const; + FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue); + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -142,13 +145,20 @@ namespace storm { bool varianceAsMeasureType; bool quantitativeOperatorResults; bool qualitativeOperatorResults; + bool operatorAtTopLevelRequired; }; // Propositional. FragmentSpecification propositional(); + // Just reachability properties. + FragmentSpecification reachability(); + // Regular PCTL. FragmentSpecification pctl(); + + // Flat PCTL. + FragmentSpecification flatPctl(); // PCTL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification prctl(); diff --git a/src/logic/ToExpressionVisitor.cpp b/src/logic/ToExpressionVisitor.cpp index 887f9d405..53dfedeca 100644 --- a/src/logic/ToExpressionVisitor.cpp +++ b/src/logic/ToExpressionVisitor.cpp @@ -2,14 +2,16 @@ #include "src/logic/Formulas.h" +#include "src/storage/expressions/ExpressionManager.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" namespace storm { namespace logic { - storm::expressions::Expression ToExpressionVisitor::toExpression(Formula const& f) const { - boost::any result = f.accept(*this, boost::any()); + storm::expressions::Expression ToExpressionVisitor::toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const { + boost::any result = f.accept(*this, std::ref(manager)); return boost::any_cast(result); } @@ -18,7 +20,7 @@ namespace storm { } boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression, because the undefined atomic label '" << f.getLabel() << "' appears in the formula."); } boost::any ToExpressionVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { @@ -35,7 +37,13 @@ namespace storm { } boost::any ToExpressionVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { - return std::static_pointer_cast(std::make_shared(f)); + storm::expressions::Expression result; + if (f.isTrueFormula()) { + result = boost::any_cast>(data).get().boolean(true); + } else { + result = boost::any_cast>(data).get().boolean(false); + } + return result; } boost::any ToExpressionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { diff --git a/src/logic/ToExpressionVisitor.h b/src/logic/ToExpressionVisitor.h index a42258a46..ee4a81d8f 100644 --- a/src/logic/ToExpressionVisitor.h +++ b/src/logic/ToExpressionVisitor.h @@ -10,7 +10,7 @@ namespace storm { class ToExpressionVisitor : public FormulaVisitor { public: - storm::expressions::Expression toExpression(Formula const& f) const; + storm::expressions::Expression toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const; virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; diff --git a/src/modelchecker/exploration/BoundValues.cpp b/src/modelchecker/exploration/BoundValues.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/modelchecker/exploration/BoundValues.h b/src/modelchecker/exploration/BoundValues.h new file mode 100644 index 000000000..3640fa9c6 --- /dev/null +++ b/src/modelchecker/exploration/BoundValues.h @@ -0,0 +1,137 @@ +#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ +#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPEXPLORATIONMODELCHECKER_H_ + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + // A struct containg the lower and upper bounds per state and action. + struct BoundValues { + std::vector lowerBoundsPerState; + std::vector upperBoundsPerState; + std::vector lowerBoundsPerAction; + std::vector upperBoundsPerAction; + + std::pair getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + if (index == explorationInformation.getUnexploredMarker()) { + return std::make_pair(storm::utility::zero(), storm::utility::one()); + } else { + return std::make_pair(lowerBoundsPerState[index], upperBoundsPerState[index]); + } + } + + ValueType getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + if (index == explorationInformation.getUnexploredMarker()) { + return storm::utility::zero(); + } else { + return getLowerBoundForRowGroup(index); + } + } + + ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const { + return lowerBoundsPerState[rowGroup]; + } + + ValueType getUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + if (index == explorationInformation.getUnexploredMarker()) { + return storm::utility::one(); + } else { + return getUpperBoundForRowGroup(index); + } + } + + ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const { + return upperBoundsPerState[rowGroup]; + } + + std::pair getBoundsForAction(ActionType const& action) const { + return std::make_pair(lowerBoundsPerAction[action], upperBoundsPerAction[action]); + } + + ValueType const& getLowerBoundForAction(ActionType const& action) const { + return lowerBoundsPerAction[action]; + } + + ValueType const& getUpperBoundForAction(ActionType const& action) const { + return upperBoundsPerAction[action]; + } + + ValueType const& getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const { + if (direction == storm::OptimizationDirection::Maximize) { + return getUpperBoundForAction(action); + } else { + return getLowerBoundForAction(action); + } + } + + ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const { + std::pair bounds = getBoundsForState(state, explorationInformation); + return bounds.second - bounds.first; + } + + void initializeBoundsForNextState(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())) { + lowerBoundsPerState.push_back(vals.first); + upperBoundsPerState.push_back(vals.second); + } + + void initializeBoundsForNextAction(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())) { + lowerBoundsPerAction.push_back(vals.first); + upperBoundsPerAction.push_back(vals.second); + } + + void setLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { + setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value); + } + + void setLowerBoundForRowGroup(StateType const& group, ValueType const& value) { + lowerBoundsPerState[group] = value; + } + + void setUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { + setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value); + } + + void setUpperBoundForRowGroup(StateType const& group, ValueType const& value) { + upperBoundsPerState[group] = value; + } + + void setBoundsForAction(ActionType const& action, std::pair const& values) { + lowerBoundsPerAction[action] = values.first; + upperBoundsPerAction[action] = values.second; + } + + void setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair const& values) { + StateType const& rowGroup = explorationInformation.getRowGroup(state); + setBoundsForRowGroup(rowGroup, values); + } + + void setBoundsForRowGroup(StateType const& rowGroup, std::pair const& values) { + lowerBoundsPerState[rowGroup] = values.first; + upperBoundsPerState[rowGroup] = values.second; + } + + bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newLowerValue) { + StateType const& rowGroup = explorationInformation.getRowGroup(state); + if (lowerBoundsPerState[rowGroup] < newLowerValue) { + lowerBoundsPerState[rowGroup] = newLowerValue; + return true; + } + return false; + } + + bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newUpperValue) { + StateType const& rowGroup = explorationInformation.getRowGroup(state); + if (newUpperValue < upperBoundsPerState[rowGroup]) { + upperBoundsPerState[rowGroup] = newUpperValue; + return true; + } + return false; + } + }; + + } + } +} \ No newline at end of file diff --git a/src/modelchecker/exploration/ExplorationInformation.cpp b/src/modelchecker/exploration/ExplorationInformation.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/modelchecker/exploration/ExplorationInformation.h b/src/modelchecker/exploration/ExplorationInformation.h new file mode 100644 index 000000000..e69de29bb diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp similarity index 86% rename from src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp rename to src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp index b0f6cc4da..037d97800 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp @@ -1,4 +1,4 @@ -#include "src/modelchecker/reachability/SparseMdpLearningModelChecker.h" +#include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.h" #include "src/storage/SparseMatrix.h" #include "src/storage/MaximalEndComponentDecomposition.h" @@ -22,27 +22,30 @@ namespace storm { namespace modelchecker { + template - SparseMdpLearningModelChecker::SparseMdpLearningModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator() { + SparseMdpExplorationModelChecker::SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator() { // Intentionally left empty. } template - bool SparseMdpLearningModelChecker::canHandle(CheckTask const& checkTask) const { + bool SparseMdpExplorationModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true).setNestedOperatorsAllowed(false); + storm::logic::FragmentSpecification fragment = storm::logic::reachability(); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); } template - std::unique_ptr SparseMdpLearningModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { - storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); - storm::logic::Formula const& subformula = eventuallyFormula.getSubformula(); + std::unique_ptr SparseMdpExplorationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& untilFormula = checkTask.getFormula(); + storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula(); + storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula(); STORM_LOG_THROW(program.isDeterministicModel() || checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "For nondeterministic systems, an optimization direction (min/max) must be given in the property."); - StateGeneration stateGeneration(program, variableInformation, getTargetStateExpression(subformula)); + std::map labelToExpressionMapping = program.getLabelToExpressionMapping(); + StateGeneration stateGeneration(program, variableInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); - ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().getNumberOfExplorationStepsUntilPrecomputation()); + ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::explorationSettings().getNumberOfExplorationStepsUntilPrecomputation()); explorationInformation.optimizationDirection = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; // The first row group starts at action 0. @@ -52,24 +55,12 @@ namespace storm { stateGeneration.stateToIdCallback = createStateToIdCallback(explorationInformation); // Compute and return result. - std::tuple boundsForInitialState = performLearningProcedure(stateGeneration, explorationInformation); + std::tuple boundsForInitialState = performExploration(stateGeneration, explorationInformation); return std::make_unique>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); } template - storm::expressions::Expression SparseMdpLearningModelChecker::getTargetStateExpression(storm::logic::Formula const& subformula) const { - std::shared_ptr preparedSubformula = subformula.substitute(program.getLabelToExpressionMapping()); - storm::expressions::Expression result; - try { - result = preparedSubformula->toExpression(); - } catch(storm::exceptions::InvalidOperationException const& e) { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The property refers to unknown labels."); - } - return result; - } - - template - std::function::StateType (storm::generator::CompressedState const&)> SparseMdpLearningModelChecker::createStateToIdCallback(ExplorationInformation& explorationInformation) const { + std::function::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker::createStateToIdCallback(ExplorationInformation& explorationInformation) const { return [&explorationInformation,this] (storm::generator::CompressedState const& state) -> StateType { StateType newIndex = explorationInformation.stateStorage.numberOfStates; @@ -85,11 +76,11 @@ namespace storm { } template - std::tuple::StateType, ValueType, ValueType> SparseMdpLearningModelChecker::performLearningProcedure(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { + std::tuple::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { // Generate the initial state so we know where to start the simulation. explorationInformation.setInitialStates(stateGeneration.getInitialStates()); - STORM_LOG_THROW(explorationInformation.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the learning engine."); + STORM_LOG_THROW(explorationInformation.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); StateType initialStateIndex = explorationInformation.getFirstInitialState(); // Create a structure that holds the bounds for the states and actions. @@ -139,7 +130,7 @@ namespace storm { } template - bool SparseMdpLearningModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const { + bool SparseMdpExplorationModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const { // Start the search from the initial state. stack.push_back(std::make_pair(explorationInformation.getFirstInitialState(), 0)); @@ -201,7 +192,7 @@ namespace storm { } template - bool SparseMdpLearningModelChecker::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { + bool SparseMdpExplorationModelChecker::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { bool isTerminalState = false; bool isTargetState = false; @@ -217,12 +208,12 @@ namespace storm { // Before generating the behavior of the state, we need to determine whether it's a target state that // does not need to be expanded. - stateGeneration.generator.load(currentState); + stateGeneration.load(currentState); if (stateGeneration.isTargetState()) { ++stats.numberOfTargetStates; isTargetState = true; isTerminalState = true; - } else { + } else if (stateGeneration.isConditionState()) { STORM_LOG_TRACE("Exploring state."); // If it needs to be expanded, we use the generator to retrieve the behavior of the new state. @@ -273,6 +264,10 @@ namespace storm { bounds.setBoundsForState(currentStateId, explorationInformation, stateBounds); STORM_LOG_TRACE("Initializing bounds of state " << currentStateId << " to " << bounds.getLowerBoundForState(currentStateId, explorationInformation) << " and " << bounds.getUpperBoundForState(currentStateId, explorationInformation) << "."); } + } else { + // In this case, the state is neither a target state nor a condition state and therefore a rejecting + // terminal state. + isTerminalState = true; } if (isTerminalState) { @@ -298,7 +293,7 @@ namespace storm { } template - typename SparseMdpLearningModelChecker::ActionType SparseMdpLearningModelChecker::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { + typename SparseMdpExplorationModelChecker::ActionType SparseMdpExplorationModelChecker::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { // Determine the values of all available actions. std::vector> actionValues; StateType rowGroup = explorationInformation.getRowGroup(currentStateId); @@ -336,7 +331,7 @@ namespace storm { } template - typename SparseMdpLearningModelChecker::StateType SparseMdpLearningModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + typename SparseMdpExplorationModelChecker::StateType SparseMdpExplorationModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { std::vector> const& row = explorationInformation.getRowOfMatrix(chosenAction); // if (row.size() == 1) { // return row.front().getColumn(); @@ -364,7 +359,7 @@ namespace storm { } template - bool SparseMdpLearningModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { + bool SparseMdpExplorationModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { ++stats.numberOfPrecomputations; // Outline: @@ -498,7 +493,7 @@ namespace storm { } template - void SparseMdpLearningModelChecker::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const { + void SparseMdpExplorationModelChecker::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const { bool containsTargetState = false; // Now we record all actions leaving the EC. @@ -567,7 +562,7 @@ namespace storm { } template - ValueType SparseMdpLearningModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + ValueType SparseMdpExplorationModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { ValueType result = storm::utility::zero(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); @@ -576,7 +571,7 @@ namespace storm { } template - ValueType SparseMdpLearningModelChecker::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + ValueType SparseMdpExplorationModelChecker::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { ValueType result = storm::utility::zero(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); @@ -585,7 +580,7 @@ namespace storm { } template - std::pair SparseMdpLearningModelChecker::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + std::pair SparseMdpExplorationModelChecker::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { // TODO: take into account self-loops? std::pair result = std::make_pair(storm::utility::zero(), storm::utility::zero()); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { @@ -596,7 +591,7 @@ namespace storm { } template - std::pair SparseMdpLearningModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + std::pair SparseMdpExplorationModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { StateType group = explorationInformation.getRowGroup(currentStateId); std::pair result = getLowestBounds(explorationInformation.optimizationDirection); for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) { @@ -607,7 +602,7 @@ namespace storm { } template - void SparseMdpLearningModelChecker::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { + void SparseMdpExplorationModelChecker::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { stack.pop_back(); while (!stack.empty()) { updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); @@ -616,7 +611,7 @@ namespace storm { } template - void SparseMdpLearningModelChecker::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { + void SparseMdpExplorationModelChecker::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { // Compute the new lower/upper values of the action. std::pair newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); @@ -651,7 +646,7 @@ namespace storm { } template - ValueType SparseMdpLearningModelChecker::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + ValueType SparseMdpExplorationModelChecker::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { ValueType bound = getLowestBound(explorationInformation.optimizationDirection); ActionType group = explorationInformation.getRowGroup(state); @@ -670,13 +665,13 @@ namespace storm { } template - std::pair SparseMdpLearningModelChecker::getLowestBounds(storm::OptimizationDirection const& direction) const { + std::pair SparseMdpExplorationModelChecker::getLowestBounds(storm::OptimizationDirection const& direction) const { ValueType val = getLowestBound(direction); return std::make_pair(val, val); } template - ValueType SparseMdpLearningModelChecker::getLowestBound(storm::OptimizationDirection const& direction) const { + ValueType SparseMdpExplorationModelChecker::getLowestBound(storm::OptimizationDirection const& direction) const { if (direction == storm::OptimizationDirection::Maximize) { return storm::utility::zero(); } else { @@ -685,7 +680,7 @@ namespace storm { } template - std::pair SparseMdpLearningModelChecker::combineBounds(storm::OptimizationDirection const& direction, std::pair const& bounds1, std::pair const& bounds2) const { + std::pair SparseMdpExplorationModelChecker::combineBounds(storm::OptimizationDirection const& direction, std::pair const& bounds1, std::pair const& bounds2) const { if (direction == storm::OptimizationDirection::Maximize) { return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second)); } else { @@ -693,6 +688,6 @@ namespace storm { } } - template class SparseMdpLearningModelChecker; + template class SparseMdpExplorationModelChecker; } } \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h similarity index 64% rename from src/modelchecker/reachability/SparseMdpLearningModelChecker.h rename to src/modelchecker/exploration/SparseMdpExplorationModelChecker.h index 2e43ad582..f73f7b39f 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h @@ -1,5 +1,5 @@ -#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ -#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ +#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ +#define STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ #include @@ -13,7 +13,7 @@ #include "src/generator/VariableInformation.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/LearningSettings.h" +#include "src/settings/modules/ExplorationSettings.h" #include "src/utility/macros.h" #include "src/utility/ConstantsComparator.h" @@ -37,7 +37,7 @@ namespace storm { namespace modelchecker { template - class SparseMdpLearningModelChecker : public AbstractModelChecker { + class SparseMdpExplorationModelChecker : public AbstractModelChecker { public: typedef uint32_t StateType; typedef uint32_t ActionType; @@ -46,18 +46,18 @@ namespace storm { typedef std::shared_ptr ActionSetPointer; typedef std::vector> StateActionStack; - SparseMdpLearningModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions); + SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions); virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; private: // A structure containing the data assembled during exploration. struct ExplorationInformation { - ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::LearningSettings::NextStateHeuristic::DifferenceWeightedProbability) { + ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) { - storm::settings::modules::LearningSettings const& settings = storm::settings::learningSettings(); + storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings(); localPrecomputation = settings.isLocalPrecomputationSet(); if (settings.isNumberOfSampledPathsUntilPrecomputationSet()) { numberOfSampledPathsUntilPrecomputation = settings.getNumberOfSampledPathsUntilPrecomputation(); @@ -83,7 +83,7 @@ namespace storm { uint_fast64_t numberOfExplorationStepsUntilPrecomputation; boost::optional numberOfSampledPathsUntilPrecomputation; - storm::settings::modules::LearningSettings::NextStateHeuristic nextStateHeuristic; + storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic; void setInitialStates(std::vector const& initialStates) { stateStorage.initialStateIndices = initialStates; @@ -212,16 +212,16 @@ namespace storm { return !useLocalPrecomputation(); } - storm::settings::modules::LearningSettings::NextStateHeuristic const& getNextStateHeuristic() const { + storm::settings::modules::ExplorationSettings::NextStateHeuristic const& getNextStateHeuristic() const { return nextStateHeuristic; } bool useDifferenceWeightedProbabilityHeuristic() const { - return nextStateHeuristic == storm::settings::modules::LearningSettings::NextStateHeuristic::DifferenceWeightedProbability; + return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability; } bool useProbabilityHeuristic() const { - return nextStateHeuristic == storm::settings::modules::LearningSettings::NextStateHeuristic::Probability; + return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability; } }; @@ -258,7 +258,7 @@ namespace storm { std::size_t totalNumberOfEcDetected; void printToStream(std::ostream& out, ExplorationInformation const& explorationInformation) const { - out << std::endl << "Learning statistics:" << std::endl; + out << std::endl << "Exploration statistics:" << std::endl; out << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << numberOfTargetStates << " target)" << std::endl; out << "Exploration steps: " << explorationSteps << std::endl; out << "Sampled paths: " << pathsSampled << std::endl; @@ -270,10 +270,14 @@ namespace storm { // A struct containing the data required for state exploration. struct StateGeneration { - StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), targetStateExpression(targetStateExpression) { + StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { // Intentionally left empty. } + void load(storm::generator::CompressedState const& state) { + generator.load(state); + } + std::vector getInitialStates() { return generator.getInitialStates(stateToIdCallback); } @@ -282,147 +286,23 @@ namespace storm { return generator.expand(stateToIdCallback); } + bool isConditionState() const { + return generator.satisfies(conditionStateExpression); + } + bool isTargetState() const { return generator.satisfies(targetStateExpression); } storm::generator::PrismNextStateGenerator generator; std::function stateToIdCallback; + storm::expressions::Expression conditionStateExpression; storm::expressions::Expression targetStateExpression; }; - // A struct containg the lower and upper bounds per state and action. - struct BoundValues { - std::vector lowerBoundsPerState; - std::vector upperBoundsPerState; - std::vector lowerBoundsPerAction; - std::vector upperBoundsPerAction; - - std::pair getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - if (index == explorationInformation.getUnexploredMarker()) { - return std::make_pair(storm::utility::zero(), storm::utility::one()); - } else { - return std::make_pair(lowerBoundsPerState[index], upperBoundsPerState[index]); - } - } - - ValueType getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - if (index == explorationInformation.getUnexploredMarker()) { - return storm::utility::zero(); - } else { - return getLowerBoundForRowGroup(index); - } - } - - ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const { - return lowerBoundsPerState[rowGroup]; - } - - ValueType getUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - if (index == explorationInformation.getUnexploredMarker()) { - return storm::utility::one(); - } else { - return getUpperBoundForRowGroup(index); - } - } - - ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const { - return upperBoundsPerState[rowGroup]; - } - - std::pair getBoundsForAction(ActionType const& action) const { - return std::make_pair(lowerBoundsPerAction[action], upperBoundsPerAction[action]); - } - - ValueType const& getLowerBoundForAction(ActionType const& action) const { - return lowerBoundsPerAction[action]; - } - - ValueType const& getUpperBoundForAction(ActionType const& action) const { - return upperBoundsPerAction[action]; - } - - ValueType const& getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const { - if (direction == storm::OptimizationDirection::Maximize) { - return getUpperBoundForAction(action); - } else { - return getLowerBoundForAction(action); - } - } - - ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const { - std::pair bounds = getBoundsForState(state, explorationInformation); - return bounds.second - bounds.first; - } - - void initializeBoundsForNextState(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())) { - lowerBoundsPerState.push_back(vals.first); - upperBoundsPerState.push_back(vals.second); - } - - void initializeBoundsForNextAction(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())) { - lowerBoundsPerAction.push_back(vals.first); - upperBoundsPerAction.push_back(vals.second); - } - - void setLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { - setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value); - } - - void setLowerBoundForRowGroup(StateType const& group, ValueType const& value) { - lowerBoundsPerState[group] = value; - } - - void setUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { - setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value); - } - - void setUpperBoundForRowGroup(StateType const& group, ValueType const& value) { - upperBoundsPerState[group] = value; - } - - void setBoundsForAction(ActionType const& action, std::pair const& values) { - lowerBoundsPerAction[action] = values.first; - upperBoundsPerAction[action] = values.second; - } - - void setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair const& values) { - StateType const& rowGroup = explorationInformation.getRowGroup(state); - setBoundsForRowGroup(rowGroup, values); - } - - void setBoundsForRowGroup(StateType const& rowGroup, std::pair const& values) { - lowerBoundsPerState[rowGroup] = values.first; - upperBoundsPerState[rowGroup] = values.second; - } - - bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newLowerValue) { - StateType const& rowGroup = explorationInformation.getRowGroup(state); - if (lowerBoundsPerState[rowGroup] < newLowerValue) { - lowerBoundsPerState[rowGroup] = newLowerValue; - return true; - } - return false; - } - - bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newUpperValue) { - StateType const& rowGroup = explorationInformation.getRowGroup(state); - if (newUpperValue < upperBoundsPerState[rowGroup]) { - upperBoundsPerState[rowGroup] = newUpperValue; - return true; - } - return false; - } - }; - - storm::expressions::Expression getTargetStateExpression(storm::logic::Formula const& subformula) const; - std::function createStateToIdCallback(ExplorationInformation& explorationInformation) const; - std::tuple performLearningProcedure(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const; + std::tuple performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const; bool samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const; @@ -465,4 +345,4 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ */ \ No newline at end of file diff --git a/src/modelchecker/exploration/StateGeneration.cpp b/src/modelchecker/exploration/StateGeneration.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/modelchecker/exploration/StateGeneration.h b/src/modelchecker/exploration/StateGeneration.h new file mode 100644 index 000000000..e69de29bb diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index effeaa658..a8ce73080 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -26,7 +26,7 @@ #include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" -#include "src/settings/modules/LearningSettings.h" +#include "src/settings/modules/ExplorationSettings.h" #include "src/utility/macros.h" #include "src/settings/Option.h" @@ -49,7 +49,7 @@ namespace storm { this->addModule(std::unique_ptr(new modules::TopologicalValueIterationEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::ParametricSettings(*this))); this->addModule(std::unique_ptr(new modules::SparseDtmcEliminationModelCheckerSettings(*this))); - this->addModule(std::unique_ptr(new modules::LearningSettings(*this))); + this->addModule(std::unique_ptr(new modules::ExplorationSettings(*this))); } SettingsManager::~SettingsManager() { @@ -550,8 +550,8 @@ namespace storm { return dynamic_cast(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName)); } - storm::settings::modules::LearningSettings const& learningSettings() { - return dynamic_cast(manager().getModule(storm::settings::modules::LearningSettings::moduleName)); + storm::settings::modules::ExplorationSettings const& explorationSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::ExplorationSettings::moduleName)); } } } \ No newline at end of file diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 52bc470d3..f6a1779d1 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -25,7 +25,7 @@ namespace storm { class TopologicalValueIterationEquationSolverSettings; class ParametricSettings; class SparseDtmcEliminationModelCheckerSettings; - class LearningSettings; + class ExplorationSettings; class ModuleSettings; } class Option; @@ -332,11 +332,11 @@ namespace storm { */ storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings(); - /* Retrieves the settings of the learning engine. + /* Retrieves the settings of the exploration engine. * - * @return An object that allows accessing the settings of the learning engine. + * @return An object that allows accessing the settings of the exploration engine. */ - storm::settings::modules::LearningSettings const& learningSettings(); + storm::settings::modules::ExplorationSettings const& explorationSettings(); } // namespace settings } // namespace storm diff --git a/src/settings/modules/LearningSettings.cpp b/src/settings/modules/ExplorationSettings.cpp similarity index 72% rename from src/settings/modules/LearningSettings.cpp rename to src/settings/modules/ExplorationSettings.cpp index 0ce44a8e4..a890a1f9e 100644 --- a/src/settings/modules/LearningSettings.cpp +++ b/src/settings/modules/ExplorationSettings.cpp @@ -1,4 +1,4 @@ -#include "src/settings/modules/LearningSettings.h" +#include "src/settings/modules/ExplorationSettings.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/Option.h" #include "src/settings/OptionBuilder.h" @@ -10,13 +10,13 @@ namespace storm { namespace settings { namespace modules { - const std::string LearningSettings::moduleName = "learning"; - const std::string LearningSettings::precomputationTypeOptionName = "precomp"; - const std::string LearningSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp"; - const std::string LearningSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp"; - const std::string LearningSettings::nextStateHeuristicOptionName = "nextstate"; + const std::string ExplorationSettings::moduleName = "exploration"; + const std::string ExplorationSettings::precomputationTypeOptionName = "precomp"; + const std::string ExplorationSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp"; + const std::string ExplorationSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp"; + const std::string ExplorationSettings::nextStateHeuristicOptionName = "nextstate"; - LearningSettings::LearningSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector types = { "local", "global" }; this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("global").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, false, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); @@ -26,58 +26,58 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiff, prob } where 'prob' samples according to the probabilities in the system and 'probdiff' weights the probabilities with the differences between the current bounds.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiff").build()).build()); } - bool LearningSettings::isLocalPrecomputationSet() const { + bool ExplorationSettings::isLocalPrecomputationSet() const { if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "local") { return true; } return false; } - bool LearningSettings::isGlobalPrecomputationSet() const { + bool ExplorationSettings::isGlobalPrecomputationSet() const { if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "global") { return true; } return false; } - LearningSettings::PrecomputationType LearningSettings::getPrecomputationType() const { + ExplorationSettings::PrecomputationType ExplorationSettings::getPrecomputationType() const { std::string typeAsString = this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString(); if (typeAsString == "local") { - return LearningSettings::PrecomputationType::Local; + return ExplorationSettings::PrecomputationType::Local; } else if (typeAsString == "global") { - return LearningSettings::PrecomputationType::Global; + return ExplorationSettings::PrecomputationType::Global; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown precomputation type '" << typeAsString << "'."); } - uint_fast64_t LearningSettings::getNumberOfExplorationStepsUntilPrecomputation() const { + uint_fast64_t ExplorationSettings::getNumberOfExplorationStepsUntilPrecomputation() const { return this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); } - bool LearningSettings::isNumberOfSampledPathsUntilPrecomputationSet() const { + bool ExplorationSettings::isNumberOfSampledPathsUntilPrecomputationSet() const { return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet(); } - uint_fast64_t LearningSettings::getNumberOfSampledPathsUntilPrecomputation() const { + uint_fast64_t ExplorationSettings::getNumberOfSampledPathsUntilPrecomputation() const { return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); } - LearningSettings::NextStateHeuristic LearningSettings::getNextStateHeuristic() const { + ExplorationSettings::NextStateHeuristic ExplorationSettings::getNextStateHeuristic() const { std::string nextStateHeuristicAsString = this->getOption(nextStateHeuristicOptionName).getArgumentByName("name").getValueAsString(); if (nextStateHeuristicAsString == "probdiff") { - return LearningSettings::NextStateHeuristic::DifferenceWeightedProbability; + return ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability; } else if (nextStateHeuristicAsString == "prob") { - return LearningSettings::NextStateHeuristic::Probability; + return ExplorationSettings::NextStateHeuristic::Probability; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'."); } - bool LearningSettings::check() const { + bool ExplorationSettings::check() const { bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() || this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning || !optionsSet, "Learning engine is not selected, so setting options for it has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect."); return true; } } // namespace modules diff --git a/src/settings/modules/LearningSettings.h b/src/settings/modules/ExplorationSettings.h similarity index 88% rename from src/settings/modules/LearningSettings.h rename to src/settings/modules/ExplorationSettings.h index 2aa0d61a7..10dcaf080 100644 --- a/src/settings/modules/LearningSettings.h +++ b/src/settings/modules/ExplorationSettings.h @@ -1,5 +1,5 @@ -#ifndef STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ -#define STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ +#ifndef STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ +#define STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ #include "src/settings/modules/ModuleSettings.h" @@ -8,9 +8,9 @@ namespace storm { namespace modules { /*! - * This class represents the learning settings. + * This class represents the exploration settings. */ - class LearningSettings : public ModuleSettings { + class ExplorationSettings : public ModuleSettings { public: // An enumeration of all available precomputation types. enum class PrecomputationType { Local, Global }; @@ -19,11 +19,11 @@ namespace storm { enum class NextStateHeuristic { DifferenceWeightedProbability, Probability }; /*! - * Creates a new set of learning settings that is managed by the given manager. + * Creates a new set of exploration settings that is managed by the given manager. * * @param settingsManager The responsible manager. */ - LearningSettings(storm::settings::SettingsManager& settingsManager); + ExplorationSettings(storm::settings::SettingsManager& settingsManager); /*! * Retrieves whether local precomputation is to be used. @@ -90,4 +90,4 @@ namespace storm { } // namespace settings } // namespace storm -#endif /* STORM_SETTINGS_MODULES_LEARNINGSETTINGS_H_ */ +#endif /* STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ */ diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 85dc49c2d..a5e878f0b 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -103,9 +103,9 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); - std::vector engines = {"sparse", "hybrid", "dd", "learn", "abs"}; + std::vector engines = {"sparse", "hybrid", "dd", "expl", "abs"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, learn, abs}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, expl, abs}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); std::vector linearEquationSolver = {"gmm++", "native"}; this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") @@ -367,8 +367,8 @@ namespace storm { engine = GeneralSettings::Engine::Hybrid; } else if (engineStr == "dd") { engine = GeneralSettings::Engine::Dd; - } else if (engineStr == "learn") { - engine = GeneralSettings::Engine::Learning; + } else if (engineStr == "expl") { + engine = GeneralSettings::Engine::Exploration; } else if (engineStr == "abs") { engine = GeneralSettings::Engine::AbstractionRefinement; } else { diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 4eb493e4d..522d169af 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -28,7 +28,7 @@ namespace storm { public: // An enumeration of all engines. enum class Engine { - Sparse, Hybrid, Dd, Learning, AbstractionRefinement + Sparse, Hybrid, Dd, Exploration, AbstractionRefinement }; /*! diff --git a/src/utility/storm.h b/src/utility/storm.h index aca1a1cac..d5713a142 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -57,7 +57,7 @@ #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" -#include "src/modelchecker/reachability/SparseMdpLearningModelChecker.h" +#include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" diff --git a/src/utility/vector.h b/src/utility/vector.h index 31b1a5493..731cc4a0d 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -22,8 +22,6 @@ namespace storm { namespace utility { namespace vector { - - /*! * Sets the provided values at the provided positions in the given vector. *