Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm-pars.cpp
Go to the documentation of this file.
9
13
18
20
29
33
35
37#include "storm/api/storm.h"
38
42
44
46
48
51
52#include "storm/io/file.h"
57
63
64namespace storm {
65namespace pars {
67 PreprocessResult(std::shared_ptr<storm::models::ModelBase> const& model, bool changed) : changed(changed), model(model) {
68 // Intentionally left empty.
69 }
70
71 bool changed;
72 std::shared_ptr<storm::models::ModelBase> model;
73 boost::optional<std::vector<std::shared_ptr<storm::logic::Formula const>>> formulas;
74};
75
76template<typename ValueType>
77std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) {
78 std::vector<storm::storage::ParameterRegion<ValueType>> result;
79 auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
80 if (regionSettings.isRegionSet()) {
81 result = storm::api::parseRegions<ValueType>(regionSettings.getRegionString(), *model);
82 } else if (regionSettings.isRegionBoundSet()) {
83 result = storm::api::createRegion<ValueType>(regionSettings.getRegionBoundString(), *model);
84 }
85 return result;
86}
87
88template<typename ValueType>
89std::shared_ptr<storm::models::ModelBase> eliminateScc(std::shared_ptr<storm::models::ModelBase> const& model) {
90 storm::utility::Stopwatch eliminationWatch(true);
91 std::shared_ptr<storm::models::ModelBase> result;
92 if (model->isOfType(storm::models::ModelType::Dtmc)) {
93 STORM_PRINT("Applying scc elimination\n");
94 auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
95 auto matrix = sparseModel->getTransitionMatrix();
96 auto backwardsTransitionMatrix = matrix.transpose();
97
100
101 storm::storage::BitVector selectedStates(matrix.getRowCount());
102 storm::storage::BitVector selfLoopStates(matrix.getRowCount());
103 for (size_t i = 0; i < decomposition.size(); ++i) {
104 auto scc = decomposition.getBlock(i);
105 if (scc.size() > 1) {
106 auto statesScc = scc.getStates();
107 std::vector<uint_fast64_t> entryStates;
108 for (auto state : statesScc) {
109 auto row = backwardsTransitionMatrix.getRow(state);
110 bool found = false;
111 for (auto backState : row) {
112 if (!scc.containsState(backState.getColumn())) {
113 found = true;
114 }
115 }
116 if (found) {
117 entryStates.push_back(state);
118 selfLoopStates.set(state);
119 } else {
120 selectedStates.set(state);
121 }
122 }
123
124 if (entryStates.size() != 1) {
125 STORM_LOG_THROW(entryStates.size() > 1, storm::exceptions::NotImplementedException,
126 "state elimination not implemented for scc with more than 1 entry points");
127 }
128 }
129 }
130
132 storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardsTransitionMatrix, true);
133 auto actionRewards = std::vector<ValueType>(matrix.getRowCount(), storm::utility::zero<ValueType>());
134 storm::solver::stateelimination::NondeterministicModelStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions,
135 actionRewards);
136 for (auto state : selectedStates) {
137 stateEliminator.eliminateState(state, true);
138 }
139 for (auto state : selfLoopStates) {
140 auto row = flexibleMatrix.getRow(state);
141 stateEliminator.eliminateLoop(state);
142 }
143 selectedStates.complement();
144 auto keptRows = matrix.getRowFilter(selectedStates);
145 storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
146 // TODO @Jip: note that rewards get lost
147 result = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(newTransitionMatrix),
148 sparseModel->getStateLabeling().getSubLabeling(selectedStates));
149
150 eliminationWatch.stop();
151 STORM_PRINT("\nTime for scc elimination: " << eliminationWatch << ".\n\n");
152 result->printModelInformationToStream(std::cout);
153 } else if (model->isOfType(storm::models::ModelType::Mdp)) {
154 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
155 "Unable to perform SCC elimination for monotonicity analysis on MDP: Not mplemented");
156 } else {
157 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
158 }
159 return result;
160}
161
162template<typename ValueType>
163std::shared_ptr<storm::models::ModelBase> simplifyModel(std::shared_ptr<storm::models::ModelBase> const& model, cli::SymbolicInput const& input) {
164 storm::utility::Stopwatch simplifyingWatch(true);
165 std::shared_ptr<storm::models::ModelBase> result;
166 if (model->isOfType(storm::models::ModelType::Dtmc)) {
168 *(model->template as<storm::models::sparse::Dtmc<ValueType>>()));
169
170 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
171 STORM_LOG_THROW(formulas.begin() != formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported");
172
173 if (!simplifier.simplify(*(formulas[0]))) {
174 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
175 }
176 result = simplifier.getSimplifiedModel();
177 } else if (model->isOfType(storm::models::ModelType::Mdp)) {
179 *(model->template as<storm::models::sparse::Mdp<ValueType>>()));
180
181 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
182 STORM_LOG_THROW(formulas.begin() != formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported");
183
184 if (!simplifier.simplify(*(formulas[0]))) {
185 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
186 }
187 result = simplifier.getSimplifiedModel();
188 } else {
189 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
190 }
191
192 simplifyingWatch.stop();
193 STORM_PRINT("\nTime for model simplification: " << simplifyingWatch << ".\n\n");
194 result->printModelInformationToStream(std::cout);
195 return result;
196}
197
198template<typename ValueType>
201 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
202 auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
203 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
204 auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
205
206 PreprocessResult result(model, false);
207 // TODO: why only simplify in these modes
208 if (parametricSettings.getOperationMode() == storm::pars::utility::ParametricMode::Monotonicity ||
209 parametricSettings.getOperationMode() == storm::pars::utility::ParametricMode::Feasibility) {
210 STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidSettingsException, "Simplification requires property to be specified");
211 result.model = storm::pars::simplifyModel<ValueType>(result.model, input);
212 result.changed = true;
213 }
214
215 if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
217 result.changed = true;
218 }
219
220 if (mpi.applyBisimulation) {
221 result.model =
222 storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
223 result.changed = true;
224 }
225
226 if (parametricSettings.isLinearToSimpleEnabled()) {
227 STORM_LOG_INFO("Transforming linear to simple...");
229 result.model = transformer.transform(*result.model->template as<storm::models::sparse::Dtmc<RationalFunction>>(), true);
230 result.changed = true;
231 }
232
233 if (parametricSettings.isTimeTravellingEnabled()) {
237 result.model = std::make_shared<storm::models::sparse::Dtmc<RationalFunction>>(
238 tt.timeTravel(*result.model->template as<storm::models::sparse::Dtmc<RationalFunction>>(), checkTask));
239 result.changed = true;
240 }
241
242 if (transformationSettings.isChainEliminationSet() && model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
243 // TODO: Why only on MAs?
244 auto eliminationResult =
246 storm::api::extractFormulasFromProperties(input.properties), transformationSettings.getLabelBehavior());
247 result.model = eliminationResult.first;
248 // Set transformed properties as new properties in input
249 result.formulas = eliminationResult.second;
250 result.changed = true;
251 }
252
253 if (parametricSettings.transformContinuousModel() &&
254 (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) {
257 result.model = transformResult.first;
258 // Set transformed properties as new properties in input
259 result.formulas = transformResult.second;
260 result.changed = true;
261 }
262
263 if (monSettings.isSccEliminationSet()) {
264 // TODO move this into the API?
265 result.model = storm::pars::eliminateScc<ValueType>(result.model);
266 result.changed = true;
267 }
268
269 return result;
270}
271
272template<storm::dd::DdType DdType, typename ValueType>
275 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
276
277 PreprocessResult result(model, false);
278
280 // Currently, hybrid engine for parametric models just refers to building the model symbolically.
281 STORM_LOG_INFO("Translating symbolic model to sparse model...");
283 result.changed = true;
284 // Invoke preprocessing on the sparse model
285 PreprocessResult sparsePreprocessingResult =
286 storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input, mpi);
287 if (sparsePreprocessingResult.changed) {
288 result.model = sparsePreprocessingResult.model;
289 result.formulas = sparsePreprocessingResult.formulas;
290 }
291 } else {
292 STORM_LOG_ASSERT(mpi.engine == storm::utility::Engine::Dd, "Expected Dd engine.");
293 if (mpi.applyBisimulation) {
295 bisimulationSettings, mpi);
296 result.changed = true;
297 }
298 }
299 return result;
300}
301
302template<storm::dd::DdType DdType, typename ValueType>
303PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, cli::SymbolicInput const& input,
305 storm::utility::Stopwatch preprocessingWatch(true);
306
307 PreprocessResult result(model, false);
308 if (model->isSparseModel()) {
309 result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input, mpi);
310 } else {
311 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
312 result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, mpi);
313 }
314
315 if (result.changed) {
316 STORM_PRINT_AND_LOG("\nTime for model preprocessing: " << preprocessingWatch << ".\n\n");
317 }
318 return result;
319}
320
321template<typename ValueType>
323 std::vector<storm::storage::ParameterRegion<ValueType>> const& regions,
325 STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region verification is supported for a (single) region only.");
326 storm::storage::ParameterRegion<ValueType> const& region = regions.front();
327 STORM_LOG_THROW(input.properties.size() == 1, storm::exceptions::NotSupportedException, "Region verification is supported for a (single) property only.");
328 auto const& property = input.properties.front();
329
330 auto const& rvs = storm::settings::getModule<storm::settings::modules::RegionVerificationSettings>();
331 auto engine = rvs.getRegionCheckEngine();
332 bool generateSplitEstimates = rvs.isSplittingThresholdSet();
333 std::optional<uint64_t> maxSplitsPerStep = generateSplitEstimates ? std::make_optional(rvs.getSplittingThreshold()) : std::nullopt;
334 storm::utility::Stopwatch watch(true);
335 if (storm::api::verifyRegion<ValueType>(model, *(property.getRawFormula()), region, engine, monotonicitySettings, generateSplitEstimates,
336 maxSplitsPerStep)) {
337 STORM_PRINT_AND_LOG("Formula is satisfied by all parameter instantiations.\n");
338 } else {
339 STORM_PRINT_AND_LOG("Formula is not satisfied by all parameter instantiations.\n");
340 }
341 STORM_PRINT_AND_LOG("Time for model checking: " << watch << ".\n");
342}
343
344template<typename ValueType>
346 std::vector<storm::storage::ParameterRegion<ValueType>> const& regions,
348 uint64_t monThresh = 0) {
349 STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions.");
350 STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions.");
351 STORM_LOG_THROW(input.properties.size() == 1, storm::exceptions::NotSupportedException, "Region verification is supported for a (single) property only.");
352 auto const& property = input.properties.front();
353
354 auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
355 auto rvs = storm::settings::getModule<storm::settings::modules::RegionVerificationSettings>();
356 auto partitionSettings = storm::settings::getModule<storm::settings::modules::PartitionSettings>();
357
358 ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(partitionSettings.getCoverageThreshold());
359 boost::optional<uint64_t> optionalDepthLimit;
360 if (partitionSettings.isDepthLimitSet()) {
361 optionalDepthLimit = partitionSettings.getDepthLimit();
362 }
363
365 STORM_PRINT_AND_LOG("Analyzing parameter region " << regions.front());
366
367 auto engine = rvs.getRegionCheckEngine();
368 STORM_PRINT_AND_LOG(" using " << engine);
369 if (monotonicitySettings.useMonotonicity) {
370 STORM_PRINT_AND_LOG(" with local monotonicity and");
371 }
372
373 STORM_PRINT_AND_LOG(" with iterative refinement until "
374 << (1.0 - partitionSettings.getCoverageThreshold()) * 100.0 << "% is covered."
375 << (partitionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(partitionSettings.getDepthLimit()) + "." : "") << '\n');
376
378 storm::utility::Stopwatch watch(true);
379 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(
380 model, storm::api::createTask<ValueType>((property.getRawFormula()), true), regions.front(), engine, refinementThreshold, optionalDepthLimit,
381 storm::modelchecker::RegionResultHypothesis::Unknown, false, monotonicitySettings, monThresh);
382 watch.stop();
383 printInitialStatesResult<ValueType>(result, &watch);
384
385 if (parametricSettings.exportResultToFile()) {
386 storm::api::exportRegionCheckResultToFile<ValueType>(result, parametricSettings.exportResultPath());
387 }
388}
389
391 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
392 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
393 auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
394 auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
395 auto sampleSettings = storm::settings::getModule<storm::settings::modules::SamplingSettings>();
396
398 storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
399 STORM_LOG_THROW(parSettings.hasOperationModeBeenSet(), storm::exceptions::InvalidSettingsException, "An operation mode must be selected with --mode");
400 std::shared_ptr<storm::models::ModelBase> model;
401 if (!buildSettings.isNoBuildModelSet()) {
402 model = storm::cli::buildModel(input, ioSettings, mpi);
403 }
404
405 STORM_LOG_THROW(model, storm::exceptions::InvalidSettingsException, "No input model.");
406 if (model) {
407 model->printModelInformationToStream(std::cout);
408 }
409
410 using ValueType = storm::RationalFunction;
411 auto const DdType = storm::dd::DdType::Sylvan;
412 STORM_LOG_THROW(model->supportsParameters(), storm::exceptions::UnexpectedException, "Expected a parametric model.");
413 STORM_LOG_THROW(model->isSparseModel() || model->getDdType().value() == DdType, storm::exceptions::UnexpectedException,
414 "Expected type of model representation.");
415
416 // If minimization is active and the model is parametric, parameters might be minimized away because they are inconsequential.
417 // This is the set of all such inconsequential parameters.
418 std::set<RationalFunctionVariable> omittedParameters;
419
420 if (model) {
421 auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, mpi);
422 if (preprocessingResult.changed) {
423 if (model->isOfType(models::ModelType::Dtmc) || model->isOfType(models::ModelType::Mdp)) {
424 auto const previousParams = storm::models::sparse::getAllParameters(*model->template as<storm::models::sparse::Model<ValueType>>());
425 auto const currentParams =
426 storm::models::sparse::getAllParameters(*(preprocessingResult.model)->template as<storm::models::sparse::Model<ValueType>>());
427 for (auto const& variable : previousParams) {
428 if (!currentParams.count(variable)) {
429 omittedParameters.insert(variable);
430 }
431 }
432 }
433 model = preprocessingResult.model;
434
435 if (preprocessingResult.formulas) {
436 std::vector<storm::jani::Property> newProperties;
437 for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) {
438 auto formula = preprocessingResult.formulas.get().at(i);
439 STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties.");
440 storm::jani::Property property = input.properties.at(i);
441 newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment()));
442 }
443 input.properties = newProperties;
444 }
445 model->printModelInformationToStream(std::cout);
446 }
447 }
448
449 std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
450 if (!model) {
451 return;
452 } else {
453 storm::cli::castAndApply(model, [&input](auto const& m) { storm::cli::exportModel(m, input); });
454 }
455
456 // TODO move this.
457 storm::api::MonotonicitySetting monotonicitySettings(parSettings.isUseMonotonicitySet(), false, monSettings.isUsePLABoundsSet());
458 uint64_t monThresh = monSettings.getMonotonicityThreshold();
459
460 auto mode = parSettings.getOperationMode();
462 STORM_LOG_INFO("Solution function mode started.");
463 STORM_LOG_THROW(regions.empty(), storm::exceptions::InvalidSettingsException,
464 "Solution function computations cannot be restricted to specific regions");
465
466 if (model->isSparseModel()) {
468 } else {
470 }
472 STORM_LOG_INFO("Monotonicity mode started.");
473 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Monotonicity analysis is only supported on sparse models.");
476 STORM_LOG_INFO("Feasibility mode started.");
477 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Feasibility analysis is only supported on sparse models.");
478 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
479 STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::InvalidSettingsException,
480 "Feasibility analysis is only supported for single-objective properties.");
481 auto formula = formulas[0];
482 storm::pars::performFeasibility<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(),
483 createFeasibilitySynthesisTaskFromSettings(formula, regions), omittedParameters, monotonicitySettings);
485 STORM_LOG_INFO("Verification mode started.");
486 STORM_LOG_THROW(input.properties.size() == 1, storm::exceptions::InvalidSettingsException,
487 "Verification analysis is only supported for single-objective properties.");
488 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Verification analysis is only supported on sparse models.");
489 verifyRegionWithSparseEngine(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, monotonicitySettings);
490
492 STORM_LOG_INFO("Partition mode started.");
493 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException,
494 "Parameter space partitioning is only supported on sparse models.");
495 STORM_LOG_THROW(regions.size() == 1, storm::exceptions::InvalidSettingsException, "Partitioning requires a (single) initial region.");
496
497 // TODO Partition mode does not support monotonicity. This should generally be possible.
498 // TODO here setting monotone parameters from the outside may actually be useful
499
500 assert(!monotonicitySettings.useOnlyGlobalMonotonicity);
501 assert(!monotonicitySettings.useBoundsFromPLA);
503 monThresh);
505 STORM_LOG_INFO("Sampling mode started.");
506 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Sampling analysis is currently only supported on sparse models.");
507 // TODO unclear why this only works for sparse models?
508
509 std::string samplesAsString = sampleSettings.getSamples();
511 if (!samplesAsString.empty()) {
512 samples = parseSamples<ValueType>(model, samplesAsString, sampleSettings.isSamplesAreGraphPreservingSet());
513 samples.exact = sampleSettings.isSampleExactSet();
514 }
515 if (!samples.empty()) {
516 STORM_LOG_TRACE("Sampling the model at given points.");
517
518 if (samples.exact) {
519 verifyPropertiesAtSamplePointsWithSparseEngine<ValueType, storm::RationalNumber>(model->as<storm::models::sparse::Model<ValueType>>(), input,
520 samples);
521 } else {
522 verifyPropertiesAtSamplePointsWithSparseEngine<ValueType, double>(model->as<storm::models::sparse::Model<ValueType>>(), input, samples);
523 }
524 }
525 } else {
526 STORM_LOG_ASSERT(false, "Unknown operation mode.");
527 }
528}
529
531 auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
532 auto engine = coreSettings.getEngine();
534 engine != storm::utility::Engine::Dd || engine != storm::utility::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan,
535 "The selected DD library does not support parametric models. Switching to Sylvan...");
536
537 // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
538 auto symbolicInput = storm::cli::parseSymbolicInput();
540 std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput);
544 processInput(std::move(symbolicInput), mpi);
545}
546} // namespace pars
547} // namespace storm
548
552int main(const int argc, const char** argv) {
553 try {
554 return storm::cli::process("Storm-pars", "storm-pars", storm::settings::initializeParsSettings, storm::pars::processOptions, argc, argv);
555 } catch (storm::exceptions::BaseException const& exception) {
556 STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what());
557 return 1;
558 } catch (std::exception const& exception) {
559 STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pars to terminate. The message of this exception is: " << exception.what());
560 return 2;
561 }
562}
This class represents the base class of all exception classes.
virtual const char * what() const noexcept override
Retrieves the message associated with this exception.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
This class represents a Markov automaton.
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
Base class for all sparse models.
Definition Model.h:32
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:197
Base class for all symbolic models.
Definition Model.h:45
void eliminateState(storm::storage::sparse::state_type state, bool removeForwardTransitions)
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
void complement()
Negates all bits in the bit vector.
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
The flexible sparse matrix is used during state elimination.
storm::storage::SparseMatrix< ValueType > createSparseMatrix()
Creates a sparse matrix from the flexible sparse matrix.
row_type & getRow(index_type)
Returns an object representing the given row.
A class that holds a possibly non-square matrix in the compressed row storage format.
This class represents the decomposition of a graph-like structure into its strongly connected compone...
std::shared_ptr< storm::models::sparse::Dtmc< RationalFunction > > transform(storm::models::sparse::Dtmc< RationalFunction > const &dtmc, bool keepStateValuations=false) const
Transforms a pDTMC that has linear transitions (e.g.
This class performs different steps to simplify the given (parametric) model.
This class performs different steps to simplify the given (parametric) model.
models::sparse::Dtmc< RationalFunction > timeTravel(models::sparse::Dtmc< RationalFunction > const &model, modelchecker::CheckTask< logic::Formula, RationalFunction > const &checkTask)
Perform time-travelling on the given model and the given checkTask.
A class that provides convenience operations to display run times.
Definition Stopwatch.h:14
void stop()
Stop stopwatch and add measured time to total time.
Definition Stopwatch.cpp:42
#define STORM_LOG_INFO(message)
Definition logging.h:24
#define STORM_LOG_TRACE(message)
Definition logging.h:12
#define STORM_LOG_ERROR(message)
Definition logging.h:26
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
#define STORM_PRINT_AND_LOG(message)
Definition macros.h:68
#define STORM_PRINT(message)
Define the macros that print information and optionally also log it.
Definition macros.h:62
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > eliminateNonMarkovianChains(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior)
Eliminates chains of non-Markovian states from a given Markov Automaton.
std::shared_ptr< storm::models::sparse::Model< ValueType > > transformSymbolicToSparseModel(std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &symbolicModel, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas=std::vector< std::shared_ptr< storm::logic::Formula const > >())
Transforms the given symbolic model to a sparse model.
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > transformContinuousToDiscreteTimeSparseModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
Transforms the given continuous model to a discrete time model.
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
void exportModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)
auto castAndApply(std::shared_ptr< storm::models::ModelBase > const &model, auto const &callback)
SymbolicInput parseSymbolicInput()
int process(std::string const &name, std::string const &executableName, std::function< void(std::string const &, std::string const &)> initSettingsFunc, std::function< void(void)> processOptionsFunc, const int argc, const char **argv)
Processes the options and returns the exit code.
Definition cli.cpp:84
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseMarkovAutomaton(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &model)
std::pair< SymbolicInput, ModelProcessingInformation > preprocessSymbolicInput(SymbolicInput const &input)
std::shared_ptr< storm::models::ModelBase > buildModel(SymbolicInput const &input, storm::settings::modules::IOSettings const &ioSettings, ModelProcessingInformation const &mpi)
void printModelCheckingProperty(storm::jani::Property const &property)
std::shared_ptr< storm::models::Model< ExportValueType > > preprocessDdModelBisimulation(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseModelBisimulation(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings)
std::set< storm::RationalFunctionVariable > getAllParameters(Model< storm::RationalFunction > const &model)
Get all parameters (probability, rewards, and rates) occurring in the model.
Definition Model.cpp:728
std::shared_ptr< storm::models::ModelBase > simplifyModel(std::shared_ptr< storm::models::ModelBase > const &model, cli::SymbolicInput const &input)
void parameterSpacePartitioningWithSparseEngine(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, storm::api::MonotonicitySetting monotonicitySettings=storm::api::MonotonicitySetting(), uint64_t monThresh=0)
void analyzeMonotonicity(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions)
void processOptions()
PreprocessResult preprocessSparseModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, storm::cli::ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase > eliminateScc(std::shared_ptr< storm::models::ModelBase > const &model)
void computeSolutionFunctionsWithSymbolicEngine(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, cli::SymbolicInput const &input)
PreprocessResult preprocessDdModel(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, cli::SymbolicInput const &input, storm::cli::ModelProcessingInformation const &mpi)
void processInput(cli::SymbolicInput &&input, storm::cli::ModelProcessingInformation const &mpi)
PreprocessResult preprocessModel(std::shared_ptr< storm::models::ModelBase > const &model, cli::SymbolicInput const &input, storm::cli::ModelProcessingInformation const &mpi)
void verifyRegionWithSparseEngine(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, storm::api::MonotonicitySetting monotonicitySettings=storm::api::MonotonicitySetting())
std::vector< storm::storage::ParameterRegion< ValueType > > parseRegions(std::shared_ptr< storm::models::ModelBase > const &model)
std::shared_ptr< FeasibilitySynthesisTask const > createFeasibilitySynthesisTaskFromSettings(std::shared_ptr< storm::logic::Formula const > const &formula, std::vector< storm::storage::ParameterRegion< storm::RationalFunction > > const &regions)
void computeSolutionFunctionsWithSparseEngine(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input)
void initializeParsSettings(std::string const &name, std::string const &executableName)
LabParser.cpp.
carl::RationalFunction< Polynomial, true > RationalFunction
int main(const int argc, const char **argv)
Main entry point of the executable storm-pars.
std::vector< storm::jani::Property > properties
boost::optional< std::vector< std::shared_ptr< storm::logic::Formula const > > > formulas
PreprocessResult(std::shared_ptr< storm::models::ModelBase > const &model, bool changed)
std::shared_ptr< storm::models::ModelBase > model