diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
index 52a24d0dd..8a43e6cc5 100644
--- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -59,10 +59,6 @@ namespace storm {
std::map<uint_fast64_t, std::list<uint_fast64_t>> relevantChoicesForRelevantStates;
};
- struct GeneratorStats {
-
- };
-
struct VariableInformation {
// The manager responsible for the constraints we are building.
std::shared_ptr<storm::expressions::ExpressionManager> manager;
@@ -271,21 +267,6 @@ namespace storm {
return variableInformation;
}
- /*!
- * Asserts the constraints that are initially needed for the Fu-Malik procedure.
- *
- * @param solver The solver in which to assert the constraints.
- * @param variableInformation A structure with information about the variables for the labels.
- */
- static void assertFuMalikInitialConstraints(z3::solver& solver, VariableInformation const& variableInformation) {
- // Assert that at least one of the labels must be taken.
- z3::expr formula = variableInformation.labelVariables.at(0);
- for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) {
- formula = formula || variableInformation.labelVariables.at(index);
- }
- solver.add(formula);
- }
-
static storm::expressions::Expression getOtherSynchronizationEnabledFormula(boost::container::flat_set<uint_fast64_t> const& labelSet, std::map<uint_fast64_t, std::set<boost::container::flat_set<uint_fast64_t>>> const& synchronizingLabels, boost::container::flat_map<boost::container::flat_set<uint_fast64_t>, storm::expressions::Expression> const& labelSetToFormula, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) {
// Taking all commands of a combination does not necessarily mean that a following label set needs to be taken.
// This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need
@@ -970,22 +951,7 @@ namespace storm {
}
solver.add(disjunction);
}
-
- /*!
- * Asserts that the conjunction of the given formulae holds. If the content of the conjunction is empty,
- * this corresponds to asserting true.
- *
- * @param context The Z3 context in which to build the expressions.
- * @param solver The solver to use for the satisfiability evaluation.
- * @param formulaVector A vector of expressions that shall form the conjunction.
- */
- static void assertConjunction(z3::context& context, z3::solver& solver, std::vector<z3::expr> const& formulaVector) {
- z3::expr conjunction = context.bool_val(true);
- for (auto expr : formulaVector) {
- conjunction = conjunction && expr;
- }
- solver.add(conjunction);
- }
+
/*!
* Creates a full-adder for the two inputs and returns the resulting bit as well as the carry bit.
@@ -1617,6 +1583,13 @@ namespace storm {
uint64_t maximumCounterexamples = 1;
uint64_t multipleCounterexampleSizeCap = 100000000;
};
+
+ struct GeneratorStats {
+ std::chrono::milliseconds setupTime;
+ std::chrono::milliseconds solverTime;
+ std::chrono::milliseconds modelCheckingTime;
+ std::chrono::milliseconds analysisTime;
+ };
/*!
* Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi.
@@ -1630,7 +1603,7 @@ namespace storm {
* @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 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()) {
+ static std::vector<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, GeneratorStats& stats, 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.
@@ -1821,12 +1794,19 @@ namespace storm {
// Compute and emit the time measurements if the corresponding flag was set.
totalTime = std::chrono::high_resolution_clock::now() - totalClock;
+
+ stats.analysisTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalAnalysisTime);
+ stats.setupTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalSetupTime);
+ stats.modelCheckingTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalModelCheckingTime);
+ stats.solverTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalSolverTime);
+
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
boost::container::flat_set<uint64_t> allLabels;
for (auto const& e : labelSets) {
allLabels.insert(e.begin(), e.end());
}
-
+
+
std::cout << "Metrics:" << std::endl;
std::cout << " * all labels: " << allLabels.size() << std::endl;
std::cout << " * known labels: " << relevancyInformation.knownLabels.size() << std::endl;
@@ -1851,7 +1831,7 @@ namespace storm {
#endif
}
- static void extendLabelSetLowerBound(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t>& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) {
+ static void extendLabelSetLowerBound(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t>& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) {
auto startTime = std::chrono::high_resolution_clock::now();
// Create sub-model that only contains the choices allowed by the given command set.
@@ -1935,7 +1915,7 @@ namespace storm {
}
- static std::vector<boost::container::flat_set<uint_fast64_t>> computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options(true)) {
+ static std::vector<boost::container::flat_set<uint_fast64_t>> computeCounterexampleLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options(true)) {
STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models.");
if (!options.silent) {
std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
@@ -2027,7 +2007,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, rewardName, strictBound, dontCareLabels, options);
+ auto labelSets = getMinimalLabelSet(env, stats, 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) {
@@ -2049,7 +2029,8 @@ namespace storm {
static std::shared_ptr<HighLevelCounterexample> computeCounterexample(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
#ifdef STORM_HAVE_Z3
- auto labelSets = computeCounterexampleLabelSet(env, symbolicModel, model, formula);
+ GeneratorStats stats;
+ auto labelSets = computeCounterexampleLabelSet(env, stats, symbolicModel, model, formula);
if (symbolicModel.isPrismProgram()) {
diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
index 9fe9d3d36..5b2142ee3 100644
--- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -1,4 +1,4 @@
-#include "CounterexampleGeneratorSettings.h"
+#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/exceptions/InvalidSettingsException.h"
diff --git a/src/storm/api/export.cpp b/src/storm/api/export.cpp
index 193ec0668..e1acf9b8d 100644
--- a/src/storm/api/export.cpp
+++ b/src/storm/api/export.cpp
@@ -5,13 +5,18 @@ namespace storm {
void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
auto janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
-
+
+ storm::jani::Model modelForExport = model;
+ if (janiSettings.isExportFlattenedSet()) {
+ modelForExport = modelForExport.flattenComposition();
+ }
+
if (janiSettings.isExportAsStandardJaniSet()) {
- storm::jani::Model normalisedModel = model;
+ storm::jani::Model normalisedModel = modelForExport;
normalisedModel.makeStandardJaniCompliant();
storm::jani::JsonExporter::toFile(normalisedModel, properties, filename);
} else {
- storm::jani::JsonExporter::toFile(model, properties, filename);
+ storm::jani::JsonExporter::toFile(modelForExport, properties, filename);
}
}