Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
PathCounterexample.cpp
Go to the documentation of this file.
2
3#include "storm/io/export.h"
4
5namespace storm {
6namespace counterexamples {
7
8template<typename ValueType>
10 // Intentionally left empty.
11}
12
13template<typename ValueType>
14void PathCounterexample<ValueType>::addPath(std::vector<storage::sparse::state_type> path, size_t k) {
15 if (k >= shortestPaths.size()) {
16 shortestPaths.resize(k);
17 }
18 shortestPaths[k - 1] = path;
19}
20
21template<typename ValueType>
22void PathCounterexample<ValueType>::writeToStream(std::ostream& out) const {
23 out << "Shortest path counterexample with k = " << shortestPaths.size() << " paths: \n";
24 for (size_t i = 0; i < shortestPaths.size(); ++i) {
25 out << i + 1 << "-shortest path: \n";
26 for (auto it = shortestPaths[i].rbegin(); it != shortestPaths[i].rend(); ++it) {
27 out << "\tstate " << *it;
28 if (model->hasStateValuations()) {
29 out << ": " << model->getStateValuations().getStateInfo(*it);
30 }
31 out << ": {";
32 storm::io::outputFixedWidth(out, model->getLabelsOfState(*it), 0);
33 out << "}\n";
34 }
35 }
36}
37
38template class PathCounterexample<double>;
39} // namespace counterexamples
40} // namespace storm
void addPath(std::vector< storage::sparse::state_type > path, size_t k)
void writeToStream(std::ostream &out) const override
PathCounterexample(std::shared_ptr< storm::models::sparse::Model< ValueType > > model)
Base class for all sparse models.
Definition Model.h:33
void outputFixedWidth(std::ostream &stream, Container const &output, size_t maxWidth=30)
Output list of strings with linebreaks according to fixed width.
Definition export.h:60
LabParser.cpp.
Definition cli.cpp:18