From 6dfce6a405fdd52e3f24f422893a29a77a3043da Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Sun, 10 Jun 2018 18:50:56 +0200
Subject: [PATCH] extended counterexamples towards expected rewards, and moved
counterexamples to a seperate lib (still in main cli) to slightly accelarate
building times
---
src/CMakeLists.txt | 1 +
src/storm-cli-utilities/CMakeLists.txt | 2 +-
src/storm-cli-utilities/cli.cpp | 2 +
src/storm-cli-utilities/model-handling.h | 2 +
src/storm-counterexamples/CMakeLists.txt | 40 ++++++++
.../api/counterexamples.cpp | 2 +-
.../api/counterexamples.h | 4 +-
.../counterexamples/Counterexample.cpp | 2 +-
.../counterexamples/Counterexample.h | 0
.../HighLevelCounterexample.cpp | 2 +-
.../counterexamples/HighLevelCounterexample.h | 2 +-
.../MILPMinimalLabelSetGenerator.h | 4 +-
.../SMTMinimalLabelSetGenerator.h | 91 +++++++++++++------
.../CounterexampleGeneratorSettings.cpp | 2 +-
.../modules/CounterexampleGeneratorSettings.h | 0
src/storm-pars/settings/ParsSettings.cpp | 2 -
src/storm/api/storm.h | 1 -
src/storm/settings/SettingsManager.cpp | 2 -
.../utility/ModelInstantiatorTest.cpp | 1 +
19 files changed, 118 insertions(+), 44 deletions(-)
create mode 100644 src/storm-counterexamples/CMakeLists.txt
rename src/{storm => storm-counterexamples}/api/counterexamples.cpp (95%)
rename src/{storm => storm-counterexamples}/api/counterexamples.h (80%)
rename src/{storm => storm-counterexamples}/counterexamples/Counterexample.cpp (79%)
rename src/{storm => storm-counterexamples}/counterexamples/Counterexample.h (100%)
rename src/{storm => storm-counterexamples}/counterexamples/HighLevelCounterexample.cpp (92%)
rename src/{storm => storm-counterexamples}/counterexamples/HighLevelCounterexample.h (93%)
rename src/{storm => storm-counterexamples}/counterexamples/MILPMinimalLabelSetGenerator.h (99%)
rename src/{storm => storm-counterexamples}/counterexamples/SMTMinimalLabelSetGenerator.h (95%)
rename src/{storm => storm-counterexamples}/settings/modules/CounterexampleGeneratorSettings.cpp (98%)
rename src/{storm => storm-counterexamples}/settings/modules/CounterexampleGeneratorSettings.h (100%)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index acf819119..0f277386d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -5,6 +5,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
add_custom_target(binaries)
add_subdirectory(storm)
+add_subdirectory(storm-counterexamples)
add_subdirectory(storm-cli-utilities)
add_subdirectory(storm-pgcl)
add_subdirectory(storm-pgcl-cli)
diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt
index 84819b72b..5e37b5db4 100644
--- a/src/storm-cli-utilities/CMakeLists.txt
+++ b/src/storm-cli-utilities/CMakeLists.txt
@@ -17,7 +17,7 @@ set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "")
list(APPEND STORM_TARGETS storm-cli-utilities)
set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
-target_link_libraries(storm-cli-utilities PUBLIC storm)
+target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples)
# Install storm headers to include directory.
foreach(HEADER ${STORM_CLI_UTIL_HEADERS})
diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp
index 4d44454c8..e79971cbc 100644
--- a/src/storm-cli-utilities/cli.cpp
+++ b/src/storm-cli-utilities/cli.cpp
@@ -49,6 +49,8 @@ namespace storm {
storm::cli::printHeader("Storm", argc, argv);
storm::settings::initializeAll("Storm", "storm");
+ storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+
storm::utility::Stopwatch totalTimer(true);
if (!storm::cli::parseOptions(argc, argv)) {
return -1;
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index d03cfe630..b57818c08 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -2,6 +2,8 @@
#include "storm/api/storm.h"
+#include "storm-counterexamples/api/counterexamples.h"
+
#include "storm/utility/resources.h"
#include "storm/utility/file.h"
#include "storm/utility/storm-version.h"
diff --git a/src/storm-counterexamples/CMakeLists.txt b/src/storm-counterexamples/CMakeLists.txt
new file mode 100644
index 000000000..d01c4ceb7
--- /dev/null
+++ b/src/storm-counterexamples/CMakeLists.txt
@@ -0,0 +1,40 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-counterexamples)
+
+
+
+file(GLOB_RECURSE STORM_CEX_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.cpp)
+file(GLOB_RECURSE STORM_CEX_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h)
+
+
+# Create storm-dft.
+add_library(storm-counterexamples SHARED ${STORM_CEX_SOURCES} ${STORM_CEX_HEADERS})
+
+# Remove define symbol for shared libstorm.
+set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "")
+#add_dependencies(storm resources)
+list(APPEND STORM_TARGETS storm-counterexamples)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+
+target_link_libraries(storm-counterexamples PUBLIC storm)
+
+# Install storm headers to include directory.
+foreach(HEADER ${STORM_DFT_HEADERS})
+ string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
+ string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
+ string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
+ add_custom_command(
+ OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+ COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
+ COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+ DEPENDS ${HEADER}
+ )
+ list(APPEND STORM_CEX_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
+endforeach()
+add_custom_target(copy_storm_cex_headers DEPENDS ${STORM_CEX_OUTPUT_HEADERS} ${STORM_CEX_HEADERS})
+add_dependencies(storm-counterexamples copy_storm_cex_headers)
+
+# installation
+install(TARGETS storm-counterexamples EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+
diff --git a/src/storm/api/counterexamples.cpp b/src/storm-counterexamples/api/counterexamples.cpp
similarity index 95%
rename from src/storm/api/counterexamples.cpp
rename to src/storm-counterexamples/api/counterexamples.cpp
index c57724ad5..5652beba6 100644
--- a/src/storm/api/counterexamples.cpp
+++ b/src/storm-counterexamples/api/counterexamples.cpp
@@ -1,4 +1,4 @@
-#include "storm/api/counterexamples.h"
+#include "storm-counterexamples/api/counterexamples.h"
#include "storm/environment/Environment.h"
diff --git a/src/storm/api/counterexamples.h b/src/storm-counterexamples/api/counterexamples.h
similarity index 80%
rename from src/storm/api/counterexamples.h
rename to src/storm-counterexamples/api/counterexamples.h
index 672ddc4df..6a5984991 100644
--- a/src/storm/api/counterexamples.h
+++ b/src/storm-counterexamples/api/counterexamples.h
@@ -1,7 +1,7 @@
#pragma once
-#include "storm/counterexamples/MILPMinimalLabelSetGenerator.h"
-#include "storm/counterexamples/SMTMinimalLabelSetGenerator.h"
+#include "storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h"
+#include "storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h"
namespace storm {
namespace api {
diff --git a/src/storm/counterexamples/Counterexample.cpp b/src/storm-counterexamples/counterexamples/Counterexample.cpp
similarity index 79%
rename from src/storm/counterexamples/Counterexample.cpp
rename to src/storm-counterexamples/counterexamples/Counterexample.cpp
index 4aba71b9c..9975f54ba 100644
--- a/src/storm/counterexamples/Counterexample.cpp
+++ b/src/storm-counterexamples/counterexamples/Counterexample.cpp
@@ -1,4 +1,4 @@
-#include "storm/counterexamples/Counterexample.h"
+#include "storm-counterexamples/counterexamples/Counterexample.h"
namespace storm {
namespace counterexamples {
diff --git a/src/storm/counterexamples/Counterexample.h b/src/storm-counterexamples/counterexamples/Counterexample.h
similarity index 100%
rename from src/storm/counterexamples/Counterexample.h
rename to src/storm-counterexamples/counterexamples/Counterexample.h
diff --git a/src/storm/counterexamples/HighLevelCounterexample.cpp b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp
similarity index 92%
rename from src/storm/counterexamples/HighLevelCounterexample.cpp
rename to src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp
index 707ed6d39..11279a220 100644
--- a/src/storm/counterexamples/HighLevelCounterexample.cpp
+++ b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp
@@ -1,4 +1,4 @@
-#include "storm/counterexamples/HighLevelCounterexample.h"
+#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
namespace storm {
namespace counterexamples {
diff --git a/src/storm/counterexamples/HighLevelCounterexample.h b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h
similarity index 93%
rename from src/storm/counterexamples/HighLevelCounterexample.h
rename to src/storm-counterexamples/counterexamples/HighLevelCounterexample.h
index 92310a5ba..27fe981c0 100644
--- a/src/storm/counterexamples/HighLevelCounterexample.h
+++ b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h
@@ -1,6 +1,6 @@
#pragma once
-#include "storm/counterexamples/Counterexample.h"
+#include "Counterexample.h"
#include "storm/storage/SymbolicModelDescription.h"
diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h
similarity index 99%
rename from src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
rename to src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h
index 861f86f83..52ed50778 100644
--- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -17,7 +17,7 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
-#include "storm/counterexamples/HighLevelCounterexample.h"
+#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
#include "storm/utility/graph.h"
#include "storm/utility/counterexamples.h"
@@ -29,7 +29,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
-#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
+#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h"
namespace storm {
diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
similarity index 95%
rename from src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
rename to src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
index 0313fe655..4de23e767 100644
--- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -5,7 +5,7 @@
#include "storm/solver/Z3SmtSolver.h"
-#include "storm/counterexamples/HighLevelCounterexample.h"
+#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h"
#include "storm/storage/prism/Program.h"
#include "storm/storage/expressions/Expression.h"
@@ -1510,7 +1510,7 @@ namespace storm {
* Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet.
* Also returns the Labelsets of the sub-model.
*/
- static std::pair<std::shared_ptr<storm::models::sparse::Model<T>>, std::vector<boost::container::flat_set<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t> const& filterLabelSet) {
+ static std::pair<std::shared_ptr<storm::models::sparse::Model<T>>, std::vector<boost::container::flat_set<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t> const& filterLabelSet, boost::optional<uint64_t> absorbState = boost::none) {
bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp);
@@ -1544,7 +1544,8 @@ namespace storm {
if (customRowGrouping) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
- transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one<T>());
+ uint64_t targetState = absorbState == boost::none ? state : absorbState.get();
+ transitionMatrixBuilder.addNextValue(currentRow, targetState, storm::utility::one<T>());
// Insert an empty label set for this choice
resultLabelSet.emplace_back();
++currentRow;
@@ -1561,17 +1562,25 @@ namespace storm {
return std::make_pair(resultModel, std::move(resultLabelSet));
}
- static T computeMaximalReachabilityProbability(Environment const& env, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ static T computeMaximalReachabilityProbability(Environment const& env, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::string> const& rewardName) {
T result = storm::utility::zero<T>();
std::vector<T> allStatesResult;
STORM_LOG_DEBUG("Invoking model checker.");
if (model.isOfType(storm::models::ModelType::Dtmc)) {
- allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<T>::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false);
+ if (rewardName == boost::none) {
+ allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<T>::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false);
+ } else {
+ allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<T>::computeReachabilityRewards(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), model.getRewardModel(rewardName.get()), psiStates, false);
+ }
} else {
- storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
- allStatesResult = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, false).values);
+ if (rewardName == boost::none) {
+ storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
+ allStatesResult = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, model.getTransitionMatrix(),model.getBackwardTransitions(), phiStates,psiStates, false, false).values);
+ } else {
+ STORM_LOG_THROW(rewardName != boost::none, storm::exceptions::NotSupportedException, "Reward property counterexample generation is currently only supported for DTMCs.");
+ }
}
for (auto state : model.getInitialStates()) {
result = std::max(result, allStatesResult[state]);
@@ -1604,11 +1613,12 @@ namespace storm {
* @param model The sparse model in which to find the minimal command set.
* @param phiStates A bit vector characterizing all phi states in the model.
* @param psiStates A bit vector characterizing all psi states in the model.
- * @param probabilityThreshold The threshold that is to be achieved or exceeded.
+ * @param propertyThreshold The threshold that is to be achieved or exceeded.
+ * @param rewardName The name of the reward structure to use, or boost::none if probabilities are considerd.
* @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false).
* @param options A set of options for customization.
*/
- static std::vector<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options()) {
+ static std::vector<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional<std::string> const& rewardName, bool strictBound, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options()) {
#ifdef STORM_HAVE_Z3
std::vector<boost::container::flat_set<uint_fast64_t>> result;
// Set up all clocks used for time measurement.
@@ -1650,10 +1660,10 @@ namespace storm {
// (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
double maximalReachabilityProbability = 0;
if (options.checkThresholdFeasible) {
- maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates);
+ maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates, rewardName);
- STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".");
- std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl;
+ STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= propertyThreshold) || (!strictBound && maximalReachabilityProbability > propertyThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << propertyThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << ".");
+ std::cout << std::endl << "Maximal property value in model is " << maximalReachabilityProbability << "." << std::endl << std::endl;
}
// (2) Identify all states and commands that are relevant, because only these need to be considered later.
@@ -1705,7 +1715,7 @@ namespace storm {
uint_fast64_t lastSize = 0;
uint_fast64_t iterations = 0;
uint_fast64_t currentBound = 0;
- maximalReachabilityProbability = 0;
+ double maximalPropertyValue = 0;
uint_fast64_t zeroProbabilityCount = 0;
uint64_t smallestCounterexampleSize = model.getNumberOfChoices(); // Definitive u
uint64_t progressDelay = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getShowProgressDelay();
@@ -1732,18 +1742,18 @@ namespace storm {
}
- auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet);
+ auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0));
std::shared_ptr<storm::models::sparse::Model<T>> const& subModel = subChoiceOrigins.first;
std::vector<boost::container::flat_set<uint_fast64_t>> const& subLabelSets = subChoiceOrigins.second;
// Now determine the maximal reachability probability in the sub-model.
- maximalReachabilityProbability = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates);
+ maximalPropertyValue = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates, rewardName);
totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock;
// Depending on whether the threshold was successfully achieved or not, we proceed by either analyzing the bad solution or stopping the iteration process.
analysisClock = std::chrono::high_resolution_clock::now();
- if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) {
- if (maximalReachabilityProbability == storm::utility::zero<T>()) {
+ if ((strictBound && maximalPropertyValue < propertyThreshold) || (!strictBound && maximalPropertyValue <= propertyThreshold)) {
+ if (maximalPropertyValue == storm::utility::zero<T>()) {
++zeroProbabilityCount;
}
@@ -1759,6 +1769,10 @@ namespace storm {
// the given threshold, we analyze the solution and try to guide the solver into the right direction.
analyzeInsufficientProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation);
}
+
+ if (relevancyInformation.dontCareLabels.size() > 0) {
+ ruleOutSingleSolution(*solver, commandSet, variableInformation, relevancyInformation);
+ }
} else {
// Do not guide solver, just rule out current solution.
ruleOutSingleSolution(*solver, commandSet, variableInformation, relevancyInformation);
@@ -1915,22 +1929,41 @@ namespace storm {
std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
}
- STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
- storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula();
- STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas.");
- STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
+ storm::logic::ComparisonType comparisonType;
+ double threshold;
+ boost::optional<std::string> rewardName = boost::none;
+
+ STORM_LOG_THROW(formula->isProbabilityOperatorFormula() || formula->isRewardOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
+ if (formula->isProbabilityOperatorFormula()) {
+ storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula();
+ STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas.");
+ STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
+
+ comparisonType = probabilityOperator.getComparisonType();
+ threshold = probabilityOperator.getThresholdAs<T>();
+ } else {
+ assert(formula->isRewardOperatorFormula());
+ storm::logic::RewardOperatorFormula const& rewardOperator = formula->asRewardOperatorFormula();
+ STORM_LOG_THROW(rewardOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas.");
+ STORM_LOG_THROW( rewardOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'F phi' for counterexample generation.");
+
+ comparisonType = rewardOperator.getComparisonType();
+ threshold = rewardOperator.getThresholdAs<T>();
+ rewardName = rewardOperator.getRewardModelName();
- storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType();
- bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
- double threshold = probabilityOperator.getThresholdAs<T>();
+ STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for probability formulas.");
+ }
+ bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
+ storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula();
+
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<T>> modelchecker(model);
- if (probabilityOperator.getSubformula().isUntilFormula()) {
+ if (subformula.isUntilFormula()) {
STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for eventually formulas.");
- storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula();
+ storm::logic::UntilFormula const& untilFormula = subformula.asUntilFormula();
std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(env, untilFormula.getLeftSubformula());
std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(env, untilFormula.getRightSubformula());
@@ -1940,8 +1973,8 @@ namespace storm {
phiStates = leftQualitativeResult.getTruthValuesVector();
psiStates = rightQualitativeResult.getTruthValuesVector();
- } else if (probabilityOperator.getSubformula().isEventuallyFormula()) {
- storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula();
+ } else if (subformula.isEventuallyFormula()) {
+ storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula();
std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
@@ -1981,7 +2014,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
- auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, dontCareLabels, options);
+ auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, rewardName, strictBound, dontCareLabels, options);
auto endTime = std::chrono::high_resolution_clock::now();
if (!options.silent) {
for (auto const& labelSet : labelSets) {
diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
similarity index 98%
rename from src/storm/settings/modules/CounterexampleGeneratorSettings.cpp
rename to src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
index 0eaf656bb..9fe9d3d36 100644
--- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -1,4 +1,4 @@
-#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
+#include "CounterexampleGeneratorSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/exceptions/InvalidSettingsException.h"
diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.h b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h
similarity index 100%
rename from src/storm/settings/modules/CounterexampleGeneratorSettings.h
rename to src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h
diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp
index a0e9d8073..bf6065d62 100644
--- a/src/storm-pars/settings/ParsSettings.cpp
+++ b/src/storm-pars/settings/ParsSettings.cpp
@@ -1,4 +1,3 @@
-#include <storm/settings/modules/CounterexampleGeneratorSettings.h>
#include "storm-pars/settings/ParsSettings.h"
#include "storm-pars/settings/modules/ParametricSettings.h"
@@ -38,7 +37,6 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::ParametricSettings>();
storm::settings::addModule<storm::settings::modules::RegionSettings>();
storm::settings::addModule<storm::settings::modules::BuildSettings>();
- storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::SylvanSettings>();
diff --git a/src/storm/api/storm.h b/src/storm/api/storm.h
index ffc4c75a6..d8f6aed82 100644
--- a/src/storm/api/storm.h
+++ b/src/storm/api/storm.h
@@ -6,5 +6,4 @@
#include "storm/api/bisimulation.h"
#include "storm/api/transformation.h"
#include "storm/api/verification.h"
-#include "storm/api/counterexamples.h"
#include "storm/api/export.h"
diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index fc2b80b35..f18f76bb1 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -17,7 +17,6 @@
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/settings/modules/DebugSettings.h"
-#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
#include "storm/settings/modules/CuddSettings.h"
#include "storm/settings/modules/BuildSettings.h"
#include "storm/settings/modules/SylvanSettings.h"
@@ -531,7 +530,6 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
- storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
storm::settings::addModule<storm::settings::modules::CuddSettings>();
storm::settings::addModule<storm::settings::modules::SylvanSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
diff --git a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp
index e66a912d5..1873a4436 100644
--- a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp
+++ b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp
@@ -16,6 +16,7 @@
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
TEST(ModelInstantiatorTest, BrpProb) {
carl::VariablePool::getInstance().clear();