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

Output uses logger now 

Former-commit-id: bb5061ccd4
main
Mavo 9 years ago
parent
0c37f078fb
commit
4ae86c76f9
10 changed files with 90 additions and 101 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. 19
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 15
      src/parser/DFTGalileoParser.cpp
  3. 53
      src/storage/dft/DFT.cpp
  4. 27
      src/storage/dft/DFT.h
  5. 6
      src/storage/dft/DFTBuilder.cpp
  6. 40
      src/storage/dft/DFTElements.h
  7. 3
      src/storage/dft/DFTState.cpp
  8. 14
      src/storage/dft/DFTState.h
  9. 2
      src/storage/dft/DFTStateSpaceGenerationQueues.h
  10. 12
      src/storm-dyftee.cpp

19
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -17,12 +17,11 @@ namespace storm {
// Begin model generation
exploreStates(stateQueue, transitionMatrixBuilder);
//std::cout << "Generated " << mStates.size() << " states" << std::endl;
STORM_LOG_DEBUG("Generated " << mStates.size() << " states");
// Build CTMC
transitionMatrix = transitionMatrixBuilder.build();
//std::cout << "TransitionMatrix: " << std::endl;
//std::cout << transitionMatrix << std::endl;
STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << transitionMatrix);
// TODO Matthias: build CTMC
}
@ -44,7 +43,7 @@ namespace storm {
// Let BE fail
while (smallest < state.nrFailableBEs()) {
//std::cout << "exploring from: " << mDft.getStateString(state) << std::endl;
STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state));
storm::storage::DFTState newState(state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBE = newState.letNextBEFail(smallest++);
@ -53,7 +52,7 @@ namespace storm {
break;
}
//std::cout << "with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]" << std::endl;
STORM_LOG_TRACE("with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]");
storm::storage::DFTStateSpaceGenerationQueues queues;
@ -85,22 +84,22 @@ namespace storm {
auto itInsert = mStates.insert(newState);
assert(itInsert.second);
it = itInsert.first;
//std::cout << "New state " << mDft.getStateString(newState) << std::endl;
STORM_LOG_TRACE("New state " << mDft.getStateString(newState));
// Recursive call
if (!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) {
stateQueue.push(newState);
} else {
if (mDft.hasFailed(newState)) {
//std::cout << "Failed " << mDft.getStateString(newState) << std::endl;
STORM_LOG_TRACE("Failed " << mDft.getStateString(newState));
} else {
assert(mDft.isFailsafe(newState));
//std::cout << "Failsafe" << mDft.getStateString(newState) << std::endl;
STORM_LOG_TRACE("Failsafe" << mDft.getStateString(newState));
}
}
} else {
// State already exists
//std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl;
STORM_LOG_TRACE("State " << mDft.getStateString(*it) << " already exists");
}
// Set transition
@ -114,7 +113,7 @@ namespace storm {
{
ValueType rate = it->second / sum;
transitionMatrixBuilder.addNextValue(state.getId(), it->first, rate);
//std::cout << "Added transition from " << state.getId() << " to " << it->first << " with " << rate << std::endl;
STORM_LOG_TRACE("Added transition from " << state.getId() << " to " << it->first << " with " << rate);
}
} // end while queue

15
src/parser/DFTGalileoParser.cpp
View File

@ -12,7 +12,10 @@ namespace storm {
namespace parser {
storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) {
if(readFile(filename)) {
return mBuilder.build();
storm::storage::DFT dft = mBuilder.build();
STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString());
STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString());
return dft;
} else {
throw storm::exceptions::FileIoException();
}
@ -24,9 +27,8 @@ namespace storm {
if(firstQuots == std::string::npos) {
return name;
} else if (secondQuots ==std::string::npos) {
std::cerr << "No ending quotation mark found in " << name <<std::endl;
throw storm::exceptions::FileIoException();
} else if (secondQuots == std::string::npos) {
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "No ending quotation mark found in " << name);
} else {
return name.substr(firstQuots+1,secondQuots-1);
}
@ -43,7 +45,7 @@ namespace storm {
file.open(filename);
}
catch (std::ifstream::failure e) {
std::cerr << "Exception during file opening on " << filename << "." << std::endl;
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << ".");
return false;
}
file.exceptions( 0 );
@ -53,7 +55,7 @@ namespace storm {
while(std::getline(file, line))
{
bool success = true;
std::cout << line << std::endl;
STORM_LOG_TRACE("Parsing: " << line);
size_t commentstarts = line.find("//");
line = line.substr(0, commentstarts);
size_t firstsemicolon = line.find(";");
@ -89,6 +91,7 @@ namespace storm {
} else if(tokens[1] == "wsp" || tokens[1] == "csp") {
success = mBuilder.addSpareElement(name, childNames);
} else if(boost::starts_with(tokens[1], "lambda=")) {
//TODO Matthias: Use ValueType instead of fixed double
success = mBuilder.addBasicElement(name, boost::lexical_cast<double>(tokens[1].substr(7)), boost::lexical_cast<double>(tokens[2].substr(5)));
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " + tokens[1] + " not recognized.");

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

@ -61,60 +61,63 @@ namespace storm {
}
void DFT::printElements(std::ostream& os) const {
std::string DFT::getElementsString() const {
std::stringstream stream;
for (auto const& elem : mElements) {
elem->print(os);
os << std::endl;
stream << "[" << elem->id() << "]" << elem->toString() << std::endl;
}
return stream.str();
}
void DFT::printInfo(std::ostream& os) const {
os << "Top level index: " << mTopLevelIndex << std::endl << "Nr BEs" << mNrOfBEs << std::endl;
std::string DFT::getInfoString() const {
std::stringstream stream;
stream << "Top level index: " << mTopLevelIndex << ", Nr BEs" << mNrOfBEs;
return stream.str();
}
void DFT::printSpareModules(std::ostream& os) const {
std::cout << "[" << mElements[mTopLevelIndex]->id() << "] {";
std::string DFT::getSpareModulesString() const {
std::stringstream stream;
stream << "[" << mElements[mTopLevelIndex]->id() << "] {";
std::vector<size_t>::const_iterator it = mTopModule.begin();
assert(it != mTopModule.end());
os << mElements[(*it)]->name();
stream << mElements[(*it)]->name();
++it;
while(it != mTopModule.end()) {
os << ", " << mElements[(*it)]->name();
stream << ", " << mElements[(*it)]->name();
++it;
}
os << "}" << std::endl;
stream << "}" << std::endl;
for(auto const& spareModule : mSpareModules) {
std::cout << "[" << mElements[spareModule.first]->name() << "] = {";
os.flush();
stream << "[" << mElements[spareModule.first]->name() << "] = {";
std::vector<size_t>::const_iterator it = spareModule.second.begin();
assert(it != spareModule.second.end());
os << mElements[(*it)]->name();
stream << mElements[(*it)]->name();
++it;
while(it != spareModule.second.end()) {
os << ", " << mElements[(*it)]->name();
os.flush();
stream << ", " << mElements[(*it)]->name();
++it;
}
os << "}" << std::endl;
stream << "}" << std::endl;
}
return stream.str();
}
void DFT::printElementsWithState(DFTState const& state, std::ostream& os) const{
std::string DFT::getElementsWithStateString(DFTState const& state) const{
std::stringstream stream;
for (auto const& elem : mElements) {
os << "[" << elem->id() << "]";
elem->print(os);
os << "\t** " << state.getElementState(elem->id());
stream << "[" << elem->id() << "]";
stream << elem->toString();
stream << "\t** " << state.getElementState(elem->id());
if(elem->isSpareGate()) {
if(state.isActiveSpare(elem->id())) {
os << " actively";
stream << " actively";
}
os << " using " << state.uses(elem->id());
stream << " using " << state.uses(elem->id());
}
std::cout << std::endl;
stream << std::endl;
}
return stream.str();
}
std::string DFT::getStateString(DFTState const& state) const{

27
src/storage/dft/DFT.h
View File

@ -11,6 +11,7 @@
#include <map>
#include "../../utility/math.h"
#include "src/utility/macros.h"
#include <boost/iterator/counting_iterator.hpp>
namespace storm {
@ -143,15 +144,14 @@ namespace storm {
bool isFailsafe(DFTState const& state) const {
return state.isFailsafe(mTopLevelIndex);
}
void printElements(std::ostream& os = std::cout) const;
void printInfo(std::ostream& os = std::cout) const;
void printSpareModules(std::ostream& os = std::cout) const;
void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const;
std::string getElementsString() const;
std::string getInfoString() const;
std::string getSpareModulesString() const;
std::string getElementsWithStateString(DFTState const& state) const;
std::string getStateString(DFTState const& state) const;
@ -163,18 +163,7 @@ namespace storm {
return true;
}
};
}
}

6
src/storage/dft/DFTBuilder.cpp
View File

@ -34,13 +34,7 @@ namespace storm {
for(std::shared_ptr<DFTElement> e : elems) {
e->setId(id++);
}
for(auto& e : elems) {
std::cout << "[" << e->id() << "] ";
e->print();
std::cout << std::endl;
}
return DFT(elems, mElements[topLevelIdentifier]);
}
unsigned DFTBuilder::computeRank(std::shared_ptr<DFTElement> const& elem) {

40
src/storage/dft/DFTElements.h
View File

@ -96,8 +96,8 @@ namespace storm {
virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
virtual size_t nrChildren() const = 0;
virtual void print(std::ostream& = std::cout) const = 0;
virtual std::string toString() const = 0;
virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
virtual std::vector<size_t> independentUnit() const = 0;
@ -187,16 +187,18 @@ namespace storm {
virtual void print(std::ostream& os = std::cout) const override {
os << "{" << name() << "} " << typestring() << "( ";
virtual std::string toString() const override {
std::stringstream stream;
stream << "{" << name() << "} " << typestring() << "( ";
std::vector<std::shared_ptr<DFTElement>>::const_iterator it = mChildren.begin();
os << (*it)->name();
stream << (*it)->name();
++it;
while(it != mChildren.end()) {
os << ", " << (*it)->name();
stream << ", " << (*it)->name();
++it;
}
os << ")";
stream << ")";
return stream.str();
}
virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override {
@ -287,8 +289,10 @@ namespace storm {
return mPassiveFailureRate;
}
void print(std::ostream& os = std::cout) const {
os << *this;
std::string toString() const {
std::stringstream stream;
stream << *this;
return stream.str();
}
bool isBasicElement() const {
@ -372,8 +376,7 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) {
gate.print(os);
return os;
return os << gate.toString();
}
@ -411,8 +414,7 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) {
gate.print(os);
return os;
return os << gate.toString();
}
class DFTSeqAnd : public DFTGate {
@ -463,8 +465,7 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) {
gate.print(os);
return os;
return os << gate.toString();
}
class DFTPand : public DFTGate {
@ -510,8 +511,7 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) {
gate.print(os);
return os;
return os << gate.toString();
}
class DFTPor : public DFTGate {
@ -534,8 +534,7 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) {
gate.print(os);
return os;
return os << gate.toString();
}
class DFTVot : public DFTGate {
@ -594,8 +593,7 @@ namespace storm {
};
inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) {
gate.print(os);
return os;
return os << gate.toString();
}
class DFTSpare : public DFTGate {

3
src/storage/dft/DFTState.cpp
View File

@ -69,8 +69,7 @@ namespace storm {
std::pair<std::shared_ptr<DFTBE<double>>, bool> DFTState::letNextBEFail(size_t index)
{
assert(index < mIsCurrentlyFailableBE.size());
//std::cout << "currently failable: ";
//printCurrentlyFailable();
STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
std::pair<std::shared_ptr<DFTBE<double>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
setFailed(res.first->id());

14
src/storage/dft/DFTState.h
View File

@ -4,7 +4,7 @@
#include "../BitVector.h"
#include "DFTElementState.h"
#include <iostream>
#include <sstream>
namespace storm {
namespace storage {
@ -111,18 +111,20 @@ namespace storm {
std::pair<std::shared_ptr<DFTBE<double>>, bool> letNextBEFail(size_t smallestIndex = 0);
void printCurrentlyFailable(std::ostream& os = std::cout) {
std::string getCurrentlyFailableString() {
std::stringstream stream;
auto it = mIsCurrentlyFailableBE.begin();
os << "{";
stream << "{";
if(it != mIsCurrentlyFailableBE.end()) {
os << *it;
stream << *it;
}
++it;
while(it != mIsCurrentlyFailableBE.end()) {
os << ", " << *it;
stream << ", " << *it;
++it;
}
os << "}" << std::endl;
stream << "}";
return stream.str();
}
friend bool operator==(DFTState const& a, DFTState const& b) {

2
src/storage/dft/DFTStateSpaceGenerationQueues.h
View File

@ -31,7 +31,7 @@ namespace storm {
}
std::shared_ptr<DFTGate> nextFailurePropagation() {
std::shared_ptr<DFTGate> next= failurePropagation.top();
std::shared_ptr<DFTGate> next = failurePropagation.top();
failurePropagation.pop();
return next;
}

12
src/storm-dyftee.cpp
View File

@ -10,22 +10,24 @@ int main(int argc, char** argv) {
if(argc != 2) {
std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl;
}
storm::utility::setUp();
log4cplus::LogLevel level = log4cplus::TRACE_LOG_LEVEL;
logger.setLogLevel(level);
logger.getAppender("mainConsoleAppender")->setThreshold(level);
std::cout << "Parsing DFT file..." << std::endl;
storm::parser::DFTGalileoParser parser;
storm::storage::DFT dft = parser.parseDFT(argv[1]);
std::cout << "Built data structure" << std::endl;
dft.printElements();
dft.printSpareModules();
std::cout << "Building CTMC..." << std::endl;
storm::builder::ExplicitDFTModelBuilder<double> builder(dft);
builder.buildCTMC();
std::cout << "Built CTMC" << std::endl;
//std::cout << "Model checking..." << std::endl;
//TODO check CTMC
//std::cout << "Checked model" << std::endl;
std::cout << "Model checking..." << std::endl;
//TODO Matthias: check CTMC
std::cout << "Checked model" << std::endl;
}
Write Preview
Loading…
Cancel
Save