sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Cleaned up debug output 

Former-commit-id: daabe84596
main
Mavo 10 years ago
parent
28a49659db
commit
3f41aa55f8
6 changed files with 60 additions and 37 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 23
      src/storage/dft/DFT.cpp
  3. 4
      src/storage/dft/DFTIsomorphism.h
  4. 8
      src/storage/dft/SymmetricUnits.h
  5. 40
      src/storm-dyftee.cpp
  6. 20
      src/utility/vector.h

2
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -1233,6 +1233,8 @@ namespace storm {
template class StatePriorityQueue<double>;
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>>;
template uint_fast64_t estimateComplexity(double const& value);
#ifdef STORM_HAVE_CARL
template class StatePriorityQueue<storm::RationalFunction>;

23
src/storage/dft/DFT.cpp
View File

@ -7,6 +7,7 @@
#include "DFTIsomorphism.h"
#include "utility/iota_n.h"
#include "utility/vector.h"
namespace storm {
namespace storage {
@ -233,12 +234,8 @@ namespace storm {
template<typename ValueType>
DFT<ValueType> DFT<ValueType>::optimize() const {
std::vector<size_t> modIdea = findModularisationRewrite();
std::cout << "Modularisation idea: " << std::endl;
for( auto const& i : modIdea ) {
std::cout << i << ", ";
}
STORM_LOG_DEBUG("Modularisation idea: " << storm::utility::vector::toString(modIdea));
if (modIdea.empty()) {
// No rewrite needed
return *this;
@ -316,6 +313,7 @@ namespace storm {
builder.setTopLevel(mElements[mTopLevelIndex]->name());
// TODO use reference?
DFT<ValueType> newDft = builder.build();
STORM_LOG_TRACE(newDft.getElementsString());
return newDft.optimize();
}
@ -487,20 +485,20 @@ namespace storm {
std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end());
if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) {
std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
STORM_LOG_TRACE("Considering ids " << *it1 << ", " << *it2 << " for isomorphism.");
bool isSymmetry = false;
std::vector<size_t> isubdft1 = getGate(*it1)->independentSubDft(false);
std::vector<size_t> isubdft2 = getGate(*it2)->independentSubDft(false);
if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
continue;
}
std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
STORM_LOG_TRACE("Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism.");
auto LHS = colouring.colourSubdft(isubdft1);
auto RHS = colouring.colourSubdft(isubdft2);
auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
isSymmetry = IsoCheck.findIsomorphism();
if(isSymmetry) {
std::cout << "subdfts are symmetric" << std::endl;
STORM_LOG_TRACE("Subdfts are symmetric");
foundEqClassFor.insert(*it2);
if(symClass.empty()) {
for(auto const& i : isubdft1) {
@ -534,20 +532,13 @@ namespace storm {
// suitable parent gate! - Lets check the independent submodules of the children
auto const& children = std::static_pointer_cast<DFTGate<ValueType>>(e)->children();
for(auto const& child : children) {
//std::cout << "check idea for: " << child->id() << std::endl;;
auto ISD = std::static_pointer_cast<DFTGate<ValueType>>(child)->independentSubDft(true);
// In the ISD, check for other children:
//std::cout << "** subdft = ";
for(auto const& isdelemid : ISD) {
std::cout << isdelemid << " ";
}
std::cout << std::endl;
std::vector<size_t> rewrite = {e->id(), child->id()};
for(size_t isdElemId : ISD) {
if(isdElemId == child->id()) continue;
if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr<DFTElement<ValueType>> const& e) { return e->id() == isdElemId; } ) != children.end()) {
//std::cout << "** found child in subdft: " << isdElemId << std::endl;
rewrite.push_back(isdElemId);
}
}

4
src/storage/dft/DFTIsomorphism.h
View File

@ -249,7 +249,7 @@ namespace storage {
}
void colourize(std::shared_ptr<const DFTGate<ValueType>> const& gate) {
std::cout << "Colour " << gate->id() << ": " << gate->type() << " " << gate->nrChildren() << " " << gate->rank() << "." << std::endl;
STORM_LOG_TRACE("Colour " << gate->id() << ": " << gate->type() << " " << gate->nrChildren() << " " << gate->rank() << ".");
gateColour[gate->id()] = gateColourizer(gate->type(), gate->nrChildren(), gate->nrParents(), 0, gate->rank());
}
@ -336,7 +336,7 @@ namespace storage {
initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.restrictionCandidates, bright.restrictionCandidates, currentPermutations.restrictionCandidates);
std::cout << bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size() << std::endl;
STORM_LOG_TRACE(bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size());
assert(bijection.size() == bleft.size());
}

8
src/storage/dft/SymmetricUnits.h
View File

@ -12,16 +12,14 @@ namespace storm {
inline std::ostream& operator<<(std::ostream& os, DFTIndependentSymmetries const& s) {
for(auto const& cl : s.groups) {
std::cout << "SYM GROUP FOR " << cl.first << std::endl;
os << "Symmetry group for " << cl.first << std::endl;
for(auto const& eqClass : cl.second) {
for(auto const& i : eqClass) {
std::cout << i << " ";
os << i << " ";
}
std::cout << std::endl;
os << std::endl;
}
}
return os;
}
}

40
src/storm-dyftee.cpp
View File

@ -20,53 +20,65 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
manager.setFromString("");
// Parsing DFT
std::cout << "Parsing DFT file..." << std::endl;
std::chrono::high_resolution_clock::time_point parsingStart = std::chrono::high_resolution_clock::now();
storm::parser::DFTGalileoParser<ValueType> parser;
storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
std::cout << "Built data structure" << std::endl;
std::cout << "Parse formula..." << std::endl;
std::vector<std::shared_ptr<storm::logic::Formula>> parsedFormulas = storm::parseFormulasForExplicit(property);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
assert(formulas.size() == 1);
std::cout << "Parsed formula." << std::endl;
// Optimize DFT
dft = dft.optimize();
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = dft.colourDFT();
symmetries = dft.findSymmetries(colouring);
std::cout << "Symmetries: " << symmetries << std::endl;
std::cout << "Found " << symmetries.groups.size() << " symmetries." << std::endl;
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
std::chrono::high_resolution_clock::time_point parsingEnd = std::chrono::high_resolution_clock::now();
// Building Markov Automaton
std::cout << "Building Model..." << std::endl;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions);
std::cout << "Built Model" << std::endl;
model->printModelInformationToStream(std::cout);
//model->printModelInformationToStream(std::cout);
std::cout << "No. states (Explored): " << model->getNumberOfStates() << std::endl;
std::cout << "No. transitions (Explored): " << model->getNumberOfTransitions() << std::endl;
std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now();
// Bisimulation
if (model->isOfType(storm::models::ModelType::Ctmc)) {
std::cout << "Bisimulation..." << std::endl;
model = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
model->printModelInformationToStream(std::cout);
//model->printModelInformationToStream(std::cout);
}
std::cout << "No. states (Bisimulation): " << model->getNumberOfStates() << std::endl;
std::cout << "No. transitions (Bisimulation): " << model->getNumberOfTransitions() << std::endl;
std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now();
// Model checking
std::cout << "Model checking..." << std::endl;
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formulas[0]));
assert(result);
std::cout << "Result: ";
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
// Times
std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now();
std::chrono::duration<double> parsingTime = parsingEnd - parsingStart;
std::chrono::duration<double> explorationTime = explorationEnd - parsingEnd;
std::chrono::duration<double> bisimulationTime = bisimulationEnd - explorationEnd;
std::chrono::duration<double> modelCheckingTime = modelCheckingEnd - bisimulationEnd;
std::chrono::duration<double> totalTime = modelCheckingEnd - parsingStart;
std::cout << "Times:" << std::endl;
std::cout << "Parsing:\t" << parsingTime.count() << std::endl;
std::cout << "Exploration:\t" << explorationTime.count() << std::endl;
std::cout << "Bisimulaton:\t" << bisimulationTime.count() << std::endl;
std::cout << "Modelchecking:\t" << modelCheckingTime.count() << std::endl;
std::cout << "Total:\t\t" << totalTime.count() << std::endl;
std::cout << "Result: ";
std::cout << *result << std::endl;
}

20
src/utility/vector.h
View File

@ -705,6 +705,26 @@ namespace storm {
assert(result.size() == filter.getNumberOfSetBits());
return result;
}
/*!
* Output vector as string.
*
* @param vector Vector to output.
* @return String containing the representation of the vector.
*/
template<typename ValueType>
std::string toString(std::vector<ValueType> vector) {
std::stringstream stream;
stream << "vector (" << vector.size() << ") [ ";
for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
stream << vector[i] << ", ";
}
if (!vector.empty()) {
stream << vector.back();
}
stream << " ]";
return stream.str();
}
} // namespace vector
} // namespace utility
} // namespace storm

Write Preview
Loading…
Cancel
Save