From d88bc115c46884277d66eb10454ffe494d7dd13b Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 4 Feb 2016 14:23:57 +0100 Subject: [PATCH 01/17] Use keywords for pctl properties Former-commit-id: c0217aacb6b8a5fcafc409b4050cc8280ff208ed --- src/storm-dyftee.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index fc113e438..fd9d67c12 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -54,19 +54,27 @@ int main(int argc, char** argv) { bool parametric = false; log4cplus::LogLevel level = log4cplus::WARN_LOG_LEVEL; std::string filename = argv[1]; - std::string pctlFormula = "Pmax=?[true U \"failed\"]"; + std::string pctlFormula = ""; for (int i = 2; i < argc; ++i) { std::string option = argv[i]; if (option == "--parametric") { parametric = true; + } else if (option == "--expectedtime") { + assert(pctlFormula.empty()); + pctlFormula = "ET=?[F \"failed\"]"; + } else if (option == "--probability") { + assert(pctlFormula.empty()); + pctlFormula = "P=? [F \"failed\"]"; } else if (option == "--trace") { level = log4cplus::TRACE_LOG_LEVEL; } else if (option == "--debug") { level = log4cplus::DEBUG_LOG_LEVEL; } else { + assert(pctlFormula.empty()); pctlFormula = option; } } + assert(!pctlFormula.empty()); storm::utility::setUp(); logger.setLogLevel(level); From 50e37217de2dfc9b09b6e55f4e762817d3a16f63 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 5 Feb 2016 13:59:21 +0100 Subject: [PATCH 02/17] Fixed compile problem Former-commit-id: 718456a293ed121ad644718453505dfa01c6233c --- src/parser/DFTGalileoParser.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 163bc1488..8bc96ed78 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -54,7 +54,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); return false; } - file.exceptions( 0 ); + file.exceptions( std::ifstream::goodbit ); std::string line; bool generalSuccess = true; @@ -156,4 +156,4 @@ namespace storm { #endif } -} \ No newline at end of file +} From 3b1c695b5d2c4b7f9b4c3b05249addcd24e76dae Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 5 Feb 2016 16:33:57 +0100 Subject: [PATCH 03/17] Another compile fix Former-commit-id: 6bb97a0505e07d4952fad582c75e9d04d2f16481 --- src/storage/dft/DFTState.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 7cb5eaf4a..fed33eee3 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -5,6 +5,7 @@ #include "DFTElementState.h" #include +#include namespace storm { namespace storage { From da90b5fcd077ff78082b0d50375b54d812e681bc Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 5 Feb 2016 20:31:43 +0100 Subject: [PATCH 04/17] Fixed benchmark script for new command line options Former-commit-id: d2df6bd5a4c70914b44bbb23bc96e2edbedd9c92 --- benchmark_dft.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/benchmark_dft.py b/benchmark_dft.py index b12d4f185..1b8e29972 100644 --- a/benchmark_dft.py +++ b/benchmark_dft.py @@ -51,7 +51,7 @@ def run_storm_dft(filename, prop, parametric, quiet): dft_file = os.path.join(EXAMPLE_DIR, filename + ".dft") args = [STORM_PATH, dft_file, - '--prop', prop] + prop] if parametric: args.append('--parametric') @@ -88,7 +88,7 @@ if __name__ == "__main__": args = parser.parse_args() count = 0 correct = 0 - properties = ["ET=? [F \"failed\"]", "P=? [F \"failed\"]"] + properties = ['--expectedtime', '--probability'] start = time.time() for index, prop in enumerate(properties): for (benchmark, parametric, result_original) in benchmarks: From e38648f6a7331fe31475a789b1503d15c90d04e2 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 8 Feb 2016 16:26:07 +0100 Subject: [PATCH 05/17] FDeps are parsed and constructed but not used yet Former-commit-id: fbd2a95f9c8e4236841f137bc63c58c53221517f --- src/parser/DFTGalileoParser.cpp | 2 +- src/storage/dft/DFTBuilder.cpp | 25 +++++++++-- src/storage/dft/DFTBuilder.h | 25 +++++++++++ src/storage/dft/DFTElements.h | 79 ++++++++++++++++++++++++++++++++- 4 files changed, 126 insertions(+), 5 deletions(-) diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 163bc1488..d623821e6 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -107,7 +107,7 @@ namespace storm { } else if (tokens[1] == "wsp" || tokens[1] == "csp") { success = builder.addSpareElement(name, childNames); } else if (boost::starts_with(tokens[1], "fdep")) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Functional dependencies currently not supported"); + success = builder.addFDepElement(name, childNames); } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index d49bfd067..4ee258dd1 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -18,11 +18,30 @@ namespace storm { for(auto& elem : mChildNames) { DFTGatePointer gate = std::static_pointer_cast>(elem.first); for(auto const& child : elem.second) { - gate->pushBackChild(mElements[child]); - mElements[child]->addParent(gate); + auto itFind = mElements.find(child); + if (itFind != mElements.end()) { + // Child found + DFTElementPointer childElement = itFind->second; + assert(!childElement->isDependency()); + gate->pushBackChild(childElement); + childElement->addParent(gate); + } else { + // Child not found -> find first dependent event to assure that child is dependency + auto itFind = mElements.find(child + "_1"); + assert(itFind != mElements.end()); + assert(itFind->second->isDependency()); + STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name()); + } } } + // Initialize dependencies + for (auto& dependency : mDependencies) { + DFTGatePointer triggerEvent = std::static_pointer_cast>(mElements[dependency->nameTrigger()]); + std::shared_ptr> dependentEvent = std::static_pointer_cast>(mElements[dependency->nameDependent()]); + dependency->initialize(triggerEvent, dependentEvent); + } + // Sort elements topologically // compute rank for (auto& elem : mElements) { @@ -40,7 +59,7 @@ namespace storm { template unsigned DFTBuilder::computeRank(DFTElementPointer const& elem) { if(elem->rank() == -1) { - if(elem->nrChildren() == 0) { + if(elem->nrChildren() == 0 || elem->isDependency()) { elem->setRank(0); } else { DFTGatePointer gate = std::static_pointer_cast>(elem); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 12d5e88c3..9dfb80ac2 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -19,12 +19,14 @@ namespace storm { using DFTElementVector = std::vector; using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; + using DFTDependencyPointer = std::shared_ptr>; private: std::size_t mNextId = 0; std::string topLevelIdentifier; std::unordered_map mElements; std::unordered_map> mChildNames; + std::vector mDependencies; public: DFTBuilder() { @@ -51,6 +53,29 @@ namespace storm { return addStandardGate(name, children, DFTElementTypes::SPARE); } + bool addFDepElement(std::string const& name, std::vector const& children) { + assert(children.size() > 1); + if(mElements.count(name) != 0) { + // Element with that name already exists. + return false; + } + std::string trigger = children[0]; + for (size_t i = 1; i < children.size(); ++i) { + // TODO Matthias: better code + std::stringstream stream; + stream << name << "_" << i; + std::string s = stream.str(); + if(mElements.count(s) != 0) { + // Element with that name already exists. + return false; + } + DFTDependencyPointer element = std::make_shared>(mNextId++, s, trigger, children[i]); + mElements[element->name()] = element; + mDependencies.push_back(element); + } + return true; + } + bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { assert(children.size() > 0); if(mElements.count(name) != 0) { diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 7f92ebb19..d8f9e19b1 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -74,7 +74,11 @@ namespace storm { virtual bool isSpareGate() const { return false; } - + + virtual bool isDependency() const { + return false; + } + virtual void setId(size_t newId) { mId = newId; } @@ -357,6 +361,79 @@ namespace storm { }; + template + class DFTDependency : public DFTElement { + + using DFTGatePointer = std::shared_ptr>; + using DFTBEPointer = std::shared_ptr>; + using DFTBEVector = std::vector; + + protected: + std::string mNameTrigger; + std::string mNameDependent; + DFTGatePointer mTriggerEvent; + DFTBEPointer mDependentEvent; + + public: + DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent) : + DFTElement(id, name), mNameTrigger(trigger), mNameDependent(dependent) + { + } + + virtual ~DFTDependency() {} + + void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) { + assert(triggerEvent->name() == mNameTrigger); + assert(dependentEvent->name() == mNameDependent); + mTriggerEvent = triggerEvent; + mDependentEvent = dependentEvent; + } + + std::string nameTrigger() { + return mNameTrigger; + } + + std::string nameDependent() { + return mNameDependent; + } + + DFTGatePointer const& triggerEvent() const { + assert(mTriggerEvent); + return mTriggerEvent; + } + + DFTBEPointer const& dependentEvent() const { + assert(mDependentEvent); + return mDependentEvent; + } + + virtual size_t nrChildren() const override { + return 1; + } + + virtual bool isDependency() const override { + return true; + } + + virtual std::vector independentUnit() const override { + std::set unit = {this->mId}; + mDependentEvent->extendUnit(unit); + if(unit.count(mTriggerEvent->id()) != 0) { + return {}; + } + return std::vector(unit.begin(), unit.end()); + } + + virtual std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} FDEP(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")"; + return stream.str(); + } + + protected: + + }; + template class DFTAnd : public DFTGate { From d45ea9cbdeb17fc199a7608f07d8056c4d8ff9ff Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 8 Feb 2016 16:27:08 +0100 Subject: [PATCH 06/17] Improved cmdl options Former-commit-id: b2ecba9ea10e8123683b3860d7bad6bac02a46ae --- src/storm-dyftee.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index fd9d67c12..4986469e7 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -46,7 +46,7 @@ void analyzeDFT(std::string filename, std::string property) { int main(int argc, char** argv) { if(argc < 2) { std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl; - std::cout << "./storm-dft " << std::endl; + std::cout << "./storm-dft <--prop pctl-formula> <--parametric>" << std::endl; return 1; } @@ -69,9 +69,14 @@ int main(int argc, char** argv) { level = log4cplus::TRACE_LOG_LEVEL; } else if (option == "--debug") { level = log4cplus::DEBUG_LOG_LEVEL; - } else { + } else if (option == "--prop") { assert(pctlFormula.empty()); - pctlFormula = option; + ++i; + assert(i < argc); + pctlFormula = argv[i]; + } else { + std::cout << "Option '" << option << "' not recognized." << std::endl; + return 1; } } assert(!pctlFormula.empty()); From c6663ba74a66e34ae008f2e264793c9e86a5d5a8 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 8 Feb 2016 17:11:47 +0100 Subject: [PATCH 07/17] Added FDep bechmarks Former-commit-id: 885b7a9531aa0146b52708ff0ffb0067486e9011 --- examples/dft/cardiac.dft | 21 ++++++ examples/dft/cas.dft | 24 ++++++ examples/dft/deathegg.dft | 16 ++++ examples/dft/fdep.dft | 8 ++ examples/dft/ftpp_complex.dft | 129 +++++++++++++++++++++++++++++++++ examples/dft/ftpp_large.dft | 63 ++++++++++++++++ examples/dft/ftpp_standard.dft | 53 ++++++++++++++ 7 files changed, 314 insertions(+) create mode 100644 examples/dft/cardiac.dft create mode 100644 examples/dft/cas.dft create mode 100644 examples/dft/deathegg.dft create mode 100644 examples/dft/fdep.dft create mode 100644 examples/dft/ftpp_complex.dft create mode 100644 examples/dft/ftpp_large.dft create mode 100644 examples/dft/ftpp_standard.dft diff --git a/examples/dft/cardiac.dft b/examples/dft/cardiac.dft new file mode 100644 index 000000000..505f002b1 --- /dev/null +++ b/examples/dft/cardiac.dft @@ -0,0 +1,21 @@ +toplevel "SYSTEM"; +"SYSTEM" or "FDEP" "CPU" "MOTOR" "PUMPS"; +"FDEP" fdep "TRIGGER" "P" "B"; +"TRIGGER" or "CS" "SS"; +"CPU" wsp "P" "B"; +"MOTOR" or "SWITCH" "MOTORS"; +"SWITCH" pand "MS" "MA"; +"MOTORS" csp "MA" "MB"; +"PUMPS" and "PUMP1" "PUMP2"; +"PUMP1" csp "PA" "PS"; +"PUMP2" csp "PB" "PS"; +"P" lambda=5.0e-5 dorm=0; +"B" lambda=5.0e-5 dorm=0.5; +"CS" lambda=2.0e-5 dorm=0; +"SS" lambda=2.0e-5 dorm=0; +"MS" lambda=1.0e-6 dorm=0; +"MA" lambda=1.0e-4 dorm=0; +"MB" lambda=1.0e-4 dorm=0; +"PA" lambda=1.0e-4 dorm=0; +"PB" lambda=1.0e-4 dorm=0; +"PS" lambda=1.0e-4 dorm=0; diff --git a/examples/dft/cas.dft b/examples/dft/cas.dft new file mode 100644 index 000000000..812a3f30a --- /dev/null +++ b/examples/dft/cas.dft @@ -0,0 +1,24 @@ +toplevel "System"; +"System" or "CPUfdep" "CPUunit" "Motorunit" "Pumpunit"; + +"CPUfdep" fdep "trigger" "P" "B"; +"trigger" or "CS" "SS"; +"CS" lambda=0.2 dorm=0; +"SS" lambda=0.2 dorm=0; +"CPUunit" wsp "P" "B"; +"P" lambda=0.5 dorm=0; +"B" lambda=0.5 dorm=0.5; + +"Motorunit" or "MP" "Motors"; +"MP" pand "MS" "MA"; +"Motors" csp "MA" "MB"; +"MS" lambda=0.01 dorm=0; +"MA" lambda=1 dorm=0; +"MB" lambda=1 dorm=0; + +"Pumpunit" and "PumpA" "PumpB"; +"PumpA" csp "PA" "PS"; +"PumpB" csp "PB" "PS"; +"PA" lambda=1 dorm=0; +"PB" lambda=1 dorm=0; +"PS" lambda=1 dorm=0; diff --git a/examples/dft/deathegg.dft b/examples/dft/deathegg.dft new file mode 100644 index 000000000..618684c4e --- /dev/null +++ b/examples/dft/deathegg.dft @@ -0,0 +1,16 @@ +toplevel "DeathEgg"; +"DeathEgg" or "DeathEggProxy" "DeathEggServer" "CampusPowerDependency" "ProxyPowerDependency"; +"DeathEggServer" or "CampusNET" "DES_Disks"; +"DES_Disks" and "DES_Disks_RAID1" "DES_Disks_RAID2"; +"DES_Disks_RAID1" and "DES_Disk_1" "DES_Disk_2"; +"DES_Disks_RAID2" and "DES_Disk_3" "DES_Disk_4"; +"DeathEggProxy" lambda=0.01 dorm=0; +"DES_Disk_1" lambda=0.01 dorm=0; +"DES_Disk_2" lambda=0.01 dorm=0; +"DES_Disk_3" lambda=0.01 dorm=0; +"DES_Disk_4" lambda=0.01 dorm=0; +"CampusPowerDependency" fdep "CampusPower" "DeathEggServer"; +"ProxyPowerDependency" fdep "ProxyPower" "DeathEggProxy"; +"CampusPower" lambda=0.01 dorm=0; +"CampusNET" lambda=0.01 dorm=0; +"ProxyPower" lambda=0.01 dorm=0; \ No newline at end of file diff --git a/examples/dft/fdep.dft b/examples/dft/fdep.dft new file mode 100644 index 000000000..e597c46ce --- /dev/null +++ b/examples/dft/fdep.dft @@ -0,0 +1,8 @@ +toplevel "System"; +"System" or "Power" "Machine"; +"Power" fdep "B_Power" "P" "B"; +"Machine" or "P" "B"; + +"B_Power" lambda=0.5 dorm=0; +"P" lambda=0.5 dorm=0; +"B" lambda=0.5 dorm=0.5; diff --git a/examples/dft/ftpp_complex.dft b/examples/dft/ftpp_complex.dft new file mode 100644 index 000000000..1b836ee6b --- /dev/null +++ b/examples/dft/ftpp_complex.dft @@ -0,0 +1,129 @@ +toplevel "System"; +"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; + +"triadA" 2of3 "aA" "bA" "cA"; +"aA" csp "TAA" "TAS"; +"bA" csp "TAB" "TAS"; +"cA" csp "TAC" "TAS"; + +"triadB" 2of3 "aB" "bB" "cB"; +"aB" csp "TBA" "TBS"; +"bB" csp "TBB" "TBS"; +"cB" csp "TBC" "TBS"; + +"triadC" 2of3 "aC" "bC" "cC"; +"aC" csp "TCA" "TCS"; +"bC" csp "TCB" "TCS"; +"cC" csp "TCC" "TCS"; + +"triadD" 2of3 "aD" "bD" "cD"; +"aD" csp "TDA" "TDS"; +"bD" csp "TDB" "TDS"; +"cD" csp "TDC" "TDS"; + +"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; +"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; +"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; +"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; + + +"NEA" lambda=0.017 dorm=1; +"NEB" lambda=0.017 dorm=1; +"NEC" lambda=0.017 dorm=1; +"NED" lambda=0.017 dorm=1; + +"TAA" or "cpuAA" "memAA"; +"memAA" csp "memAA1" "memAA2"; +"cpuAA" lambda=0.11 dorm=0; +"memAA1" lambda=0.11 dorm=0; +"memAA2" lambda=0.11 dorm=0; + +"TAB" or "cpuAB" "memAB"; +"memAB" csp "memAB1" "memAB2"; +"cpuAB" lambda=0.11 dorm=0; +"memAB1" lambda=0.11 dorm=0; +"memAB2" lambda=0.11 dorm=0; + +"TAC" or "cpuAC" "memAC"; +"memAC" csp "memAC1" "memAC2"; +"cpuAC" lambda=0.11 dorm=0; +"memAC1" lambda=0.11 dorm=0; +"memAC2" lambda=0.11 dorm=0; + +"TAS" or "cpuAS" "memAS"; +"memAS" csp "memAS1" "memAS2"; +"cpuAS" lambda=0.11 dorm=0; +"memAS1" lambda=0.11 dorm=0; +"memAS2" lambda=0.11 dorm=0; + +"TBA" or "cpuBA" "memBA"; +"memBA" csp "memBA1" "memBA2"; +"cpuBA" lambda=0.11 dorm=0; +"memBA1" lambda=0.11 dorm=0; +"memBA2" lambda=0.11 dorm=0; + +"TBB" or "cpuBB" "memBB"; +"memBB" csp "memBB1" "memBB2"; +"cpuBB" lambda=0.11 dorm=0; +"memBB1" lambda=0.11 dorm=0; +"memBB2" lambda=0.11 dorm=0; + +"TBC" or "cpuBC" "memBC"; +"memBC" csp "memBC1" "memBC2"; +"cpuBC" lambda=0.11 dorm=0; +"memBC1" lambda=0.11 dorm=0; +"memBC2" lambda=0.11 dorm=0; + +"TBS" or "cpuBS" "memBS"; +"memBS" csp "memBS1" "memBS2"; +"cpuBS" lambda=0.11 dorm=0; +"memBS1" lambda=0.11 dorm=0; +"memBS2" lambda=0.11 dorm=0; + +"TCA" or "cpuCA" "memCA"; +"memCA" csp "memCA1" "memCA2"; +"cpuCA" lambda=0.11 dorm=0; +"memCA1" lambda=0.11 dorm=0; +"memCA2" lambda=0.11 dorm=0; + +"TCB" or "cpuCB" "memCB"; +"memCB" csp "memCB1" "memCB2"; +"cpuCB" lambda=0.11 dorm=0; +"memCB1" lambda=0.11 dorm=0; +"memCB2" lambda=0.11 dorm=0; + +"TCC" or "cpuCC" "memCC"; +"memCC" csp "memCC1" "memCC2"; +"cpuCC" lambda=0.11 dorm=0; +"memCC1" lambda=0.11 dorm=0; +"memCC2" lambda=0.11 dorm=0; + +"TCS" or "cpuCS" "memCS"; +"memCS" csp "memCS1" "memCS2"; +"cpuCS" lambda=0.11 dorm=0; +"memCS1" lambda=0.11 dorm=0; +"memCS2" lambda=0.11 dorm=0; + +"TDA" or "cpuDA" "memDA"; +"memDA" csp "memDA1" "memDA2"; +"cpuDA" lambda=0.11 dorm=0; +"memDA1" lambda=0.11 dorm=0; +"memDA2" lambda=0.11 dorm=0; + +"TDB" or "cpuDB" "memDB"; +"memDB" csp "memDB1" "memDB2"; +"cpuDB" lambda=0.11 dorm=0; +"memDB1" lambda=0.11 dorm=0; +"memDB2" lambda=0.11 dorm=0; + +"TDC" or "cpuDC" "memDC"; +"memDC" csp "memDC1" "memDC2"; +"cpuDC" lambda=0.11 dorm=0; +"memDC1" lambda=0.11 dorm=0; +"memDC2" lambda=0.11 dorm=0; + +"TDS" or "cpuDS" "memDS"; +"memDS" csp "memDS1" "memDS2"; +"cpuDS" lambda=0.11 dorm=0; +"memDS1" lambda=0.11 dorm=0; +"memDS2" lambda=0.11 dorm=0; diff --git a/examples/dft/ftpp_large.dft b/examples/dft/ftpp_large.dft new file mode 100644 index 000000000..cdc8032e7 --- /dev/null +++ b/examples/dft/ftpp_large.dft @@ -0,0 +1,63 @@ +toplevel "System"; +"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD" "fE"; + +"triadA" 3of4 "aA" "bA" "cA" "dA"; +"aA" csp "TAA" "TAS"; +"bA" csp "TAB" "TAS"; +"cA" csp "TAC" "TAS"; +"dA" csp "TAD" "TAS"; + +"triadB" 3of4 "aB" "bB" "cB" "dB"; +"aB" csp "TBA" "TBS"; +"bB" csp "TBB" "TBS"; +"cB" csp "TBC" "TBS"; +"dB" csp "TBD" "TBS"; + +"triadC" 3of4 "aC" "bC" "cC" "dC"; +"aC" csp "TCA" "TCS"; +"bC" csp "TCB" "TCS"; +"cC" csp "TCC" "TCS"; +"dC" csp "TCD" "TCS"; + +"triadD" 3of4 "aD" "bD" "cD" "dD"; +"aD" csp "TDA" "TDS"; +"bD" csp "TDB" "TDS"; +"cD" csp "TDC" "TDS"; +"dD" csp "TDD" "TDS"; + +"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; +"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; +"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; +"fD" fdep "NED" "TAD" "TBD" "TCD" "TDD"; +"fE" fdep "NEE" "TAS" "TBS" "TCS" "TDS"; + + +"NEA" lambda=0.017 dorm=1; +"NEB" lambda=0.017 dorm=1; +"NEC" lambda=0.017 dorm=1; +"NED" lambda=0.017 dorm=1; +"NEE" lambda=0.017 dorm=1; + +"TAA" lambda=0.11 dorm=0; +"TAB" lambda=0.11 dorm=0; +"TAC" lambda=0.11 dorm=0; +"TAD" lambda=0.11 dorm=0; +"TAS" lambda=0.11 dorm=0; + +"TBA" lambda=0.11 dorm=0; +"TBB" lambda=0.11 dorm=0; +"TBC" lambda=0.11 dorm=0; +"TBD" lambda=0.11 dorm=0; +"TBS" lambda=0.11 dorm=0; + +"TCA" lambda=0.11 dorm=0; +"TCB" lambda=0.11 dorm=0; +"TCC" lambda=0.11 dorm=0; +"TCD" lambda=0.11 dorm=0; +"TCS" lambda=0.11 dorm=0; + +"TDA" lambda=0.11 dorm=0; +"TDB" lambda=0.11 dorm=0; +"TDC" lambda=0.11 dorm=0; +"TDD" lambda=0.11 dorm=0; +"TDS" lambda=0.11 dorm=0; diff --git a/examples/dft/ftpp_standard.dft b/examples/dft/ftpp_standard.dft new file mode 100644 index 000000000..9eaa7720e --- /dev/null +++ b/examples/dft/ftpp_standard.dft @@ -0,0 +1,53 @@ +toplevel "System"; +"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; + +"triadA" 2of3 "aA" "bA" "cA"; +"aA" csp "TAA" "TAS"; +"bA" csp "TAB" "TAS"; +"cA" csp "TAC" "TAS"; + +"triadB" 2of3 "aB" "bB" "cB"; +"aB" csp "TBA" "TBS"; +"bB" csp "TBB" "TBS"; +"cB" csp "TBC" "TBS"; + +"triadC" 2of3 "aC" "bC" "cC"; +"aC" csp "TCA" "TCS"; +"bC" csp "TCB" "TCS"; +"cC" csp "TCC" "TCS"; + +"triadD" 2of3 "aD" "bD" "cD"; +"aD" csp "TDA" "TDS"; +"bD" csp "TDB" "TDS"; +"cD" csp "TDC" "TDS"; + +"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; +"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; +"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; +"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; + + +"NEA" lambda=0.017 dorm=1; +"NEB" lambda=0.017 dorm=1; +"NEC" lambda=0.017 dorm=1; +"NED" lambda=0.017 dorm=1; + +"TAA" lambda=0.11 dorm=0; +"TAB" lambda=0.11 dorm=0; +"TAC" lambda=0.11 dorm=0; +"TAS" lambda=0.11 dorm=0; + +"TBA" lambda=0.11 dorm=0; +"TBB" lambda=0.11 dorm=0; +"TBC" lambda=0.11 dorm=0; +"TBS" lambda=0.11 dorm=0; + +"TCA" lambda=0.11 dorm=0; +"TCB" lambda=0.11 dorm=0; +"TCC" lambda=0.11 dorm=0; +"TCS" lambda=0.11 dorm=0; + +"TDA" lambda=0.11 dorm=0; +"TDB" lambda=0.11 dorm=0; +"TDC" lambda=0.11 dorm=0; +"TDS" lambda=0.11 dorm=0; From 4ece7e45a9a02f3f3b1388cd6a3b63662f6a645f Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 8 Feb 2016 17:15:09 +0100 Subject: [PATCH 08/17] Added assertions Former-commit-id: c84ad697299c03af471654a2f71431cf9365d136 --- src/builder/ExplicitDFTModelBuilder.cpp | 4 ++++ src/storage/dft/DFT.cpp | 5 +++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 9332044f2..8fab93b8b 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -1,6 +1,7 @@ #include "src/builder/ExplicitDFTModelBuilder.h" #include #include +#include #include namespace storm { @@ -32,6 +33,7 @@ namespace storm { // Build transition matrix modelComponents.transitionMatrix = transitionMatrixBuilder.build(); STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix); + assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size()); @@ -90,6 +92,8 @@ namespace storm { STORM_LOG_TRACE("Added self loop for " << state->getId()); // No further exploration required continue; + } else { + STORM_LOG_THROW(state->nrFailableBEs() > 0, storm::exceptions::UnexpectedException, "State " << state->getId() << " is no target state but behaves like one"); } // Let BE fail diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index c36f0a9e0..49c92e05a 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -133,10 +133,11 @@ namespace storm { for (auto const& elem : mElements) { stream << state->getElementStateInt(elem->id()); if(elem->isSpareGate()) { + stream << "["; if(state->isActiveSpare(elem->id())) { - stream << " actively"; + stream << "actively "; } - stream << " using " << state->uses(elem->id()); + stream << "using " << state->uses(elem->id()) << "]"; } } return stream.str(); From 8896bc55ddd11bb3b52dd4134e34e75df8257c02 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 8 Feb 2016 17:50:59 +0100 Subject: [PATCH 09/17] Added probabilities for FDeps Former-commit-id: c679ebb321d742dea13ceb88cea687e46e48fc75 --- src/parser/DFTGalileoParser.cpp | 2 +- src/storage/dft/DFTBuilder.h | 12 ++++++++++-- src/storage/dft/DFTElements.h | 12 ++++++++++-- 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index d623821e6..d56899d20 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -107,7 +107,7 @@ namespace storm { } else if (tokens[1] == "wsp" || tokens[1] == "csp") { success = builder.addSpareElement(name, childNames); } else if (boost::starts_with(tokens[1], "fdep")) { - success = builder.addFDepElement(name, childNames); + success = builder.addFDepElement(name, childNames, storm::utility::one()); } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 9dfb80ac2..8fc65b0b5 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -53,13 +53,21 @@ namespace storm { return addStandardGate(name, children, DFTElementTypes::SPARE); } - bool addFDepElement(std::string const& name, std::vector const& children) { + bool addFDepElement(std::string const& name, std::vector const& children, ValueType probability) { assert(children.size() > 1); if(mElements.count(name) != 0) { // Element with that name already exists. return false; } std::string trigger = children[0]; + + //TODO Matthias: collect constraints for SMT solving + //0 <= probability <= 1 + if (!storm::utility::isOne(probability) && children.size() > 2) { + //TODO Matthias: introduce additional element for probability and then add fdeps with probability 1 to children + std::cerr << "Probability != 1 currently not supported." << std::endl; + } + for (size_t i = 1; i < children.size(); ++i) { // TODO Matthias: better code std::stringstream stream; @@ -69,7 +77,7 @@ namespace storm { // Element with that name already exists. return false; } - DFTDependencyPointer element = std::make_shared>(mNextId++, s, trigger, children[i]); + DFTDependencyPointer element = std::make_shared>(mNextId++, s, trigger, children[i], storm::utility::one()); mElements[element->name()] = element; mDependencies.push_back(element); } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index d8f9e19b1..063a8a414 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -371,12 +371,13 @@ namespace storm { protected: std::string mNameTrigger; std::string mNameDependent; + ValueType mProbability; DFTGatePointer mTriggerEvent; DFTBEPointer mDependentEvent; public: - DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent) : - DFTElement(id, name), mNameTrigger(trigger), mNameDependent(dependent) + DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) : + DFTElement(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability) { } @@ -397,6 +398,10 @@ namespace storm { return mNameDependent; } + ValueType probability() { + return mProbability; + } + DFTGatePointer const& triggerEvent() const { assert(mTriggerEvent); return mTriggerEvent; @@ -427,6 +432,9 @@ namespace storm { virtual std::string toString() const override { std::stringstream stream; stream << "{" << this->name() << "} FDEP(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")"; + if (!storm::utility::isOne(mProbability)) { + stream << " with probability " << mProbability; + } return stream.str(); } From d507eab7f38003d652c17e18ec5eccd86a87645a Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 09:42:57 +0100 Subject: [PATCH 10/17] Build Markov Automaton instead of CTMC Former-commit-id: 26c299ad345d562542841ae288c80cdc693e238c --- src/builder/ExplicitDFTModelBuilder.cpp | 41 +++++++++++++++---------- src/builder/ExplicitDFTModelBuilder.h | 13 +++++--- src/storage/dft/DFTBuilder.h | 9 ++---- src/storm-dyftee.cpp | 18 +++++------ 4 files changed, 45 insertions(+), 36 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 8fab93b8b..d4de53d64 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -1,5 +1,5 @@ #include "src/builder/ExplicitDFTModelBuilder.h" -#include +#include #include #include #include @@ -7,13 +7,13 @@ namespace storm { namespace builder { - template - ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { + template + ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } - template - std::shared_ptr> ExplicitDFTModelBuilder::buildCTMC() { + template + std::shared_ptr> ExplicitDFTModelBuilder::buildMA() { // Initialize DFTStatePointer state = std::make_shared>(mDft, newIndex++); mStates.findOrAdd(state->status(), state); @@ -21,15 +21,17 @@ namespace storm { std::queue stateQueue; stateQueue.push(state); - bool deterministicModel = true; + bool deterministicModel = false; + ModelComponents modelComponents; + std::vector tmpMarkovianStates; storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); // Begin model generation - exploreStates(stateQueue, transitionMatrixBuilder); + exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); STORM_LOG_DEBUG("Generated " << mStates.size() << " states"); - // Build CTMC - ModelComponents modelComponents; + // Build Markov Automaton + modelComponents.markovianStates = storm::storage::BitVector(mStates.size(), tmpMarkovianStates); // Build transition matrix modelComponents.transitionMatrix = transitionMatrixBuilder.build(); STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix); @@ -65,15 +67,17 @@ namespace storm { } } - std::shared_ptr> model; - model = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling))); + std::shared_ptr> model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); model->printModelInformationToStream(std::cout); return model; } - template - void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder) { + template + void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates) { + assert(exitRates.empty()); + assert(markovianStates.empty()); + // TODO Matthias: set Markovian states std::map outgoingTransitions; while (!stateQueue.empty()) { @@ -90,6 +94,8 @@ namespace storm { if (mDft.hasFailed(state) || mDft.isFailsafe(state)) { transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); + exitRates.push_back(storm::utility::one()); + assert(exitRates.size()-1 == state->getId()); // No further exploration required continue; } else { @@ -169,20 +175,23 @@ namespace storm { } // end while failing BE // Add all transitions + ValueType exitRate = storm::utility::zero(); for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) { transitionMatrixBuilder.addNextValue(state->getId(), it->first, it->second); + exitRate += it->second; } + exitRates.push_back(exitRate); + assert(exitRates.size()-1 == state->getId()); } // end while queue } // Explicitly instantiate the class. - template class ExplicitDFTModelBuilder, uint32_t>; + template class ExplicitDFTModelBuilder; #ifdef STORM_HAVE_CARL - template class ExplicitDFTModelBuilder, uint32_t>; - template class ExplicitDFTModelBuilder, uint32_t>; + template class ExplicitDFTModelBuilder; #endif } // namespace builder diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index ed02e60d4..edb2e1a94 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -16,7 +16,7 @@ namespace storm { namespace builder { - template, typename IndexType = uint32_t> + template class ExplicitDFTModelBuilder { using DFTElementPointer = std::shared_ptr>; @@ -33,8 +33,11 @@ namespace storm { // The state labeling. storm::models::sparse::StateLabeling stateLabeling; - // The reward models associated with the model. - std::unordered_map> rewardModels; + // The Markovian states. + storm::storage::BitVector markovianStates; + + // The exit rates. + std::vector exitRates; // A vector that stores a labeling for each choice. boost::optional>> choiceLabeling; @@ -50,10 +53,10 @@ namespace storm { // 2^nrBE is upper bound for state space } - std::shared_ptr> buildCTMC(); + std::shared_ptr> buildMA(); private: - void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder); + void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); }; } diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 8fc65b0b5..9297d90cf 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -69,15 +69,12 @@ namespace storm { } for (size_t i = 1; i < children.size(); ++i) { - // TODO Matthias: better code - std::stringstream stream; - stream << name << "_" << i; - std::string s = stream.str(); - if(mElements.count(s) != 0) { + std::string nameFdep = name + "_" + std::to_string(i); + if(mElements.count(nameFdep) != 0) { // Element with that name already exists. return false; } - DFTDependencyPointer element = std::make_shared>(mNextId++, s, trigger, children[i], storm::utility::one()); + DFTDependencyPointer element = std::make_shared>(mNextId++, nameFdep, trigger, children[i], storm::utility::one()); mElements[element->name()] = element; mDependencies.push_back(element); } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 4986469e7..a86347e3b 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -6,7 +6,7 @@ #include "utility/storm.h" /*! - * Load DFT from filename, build corresponding CTMC and check against given property. + * Load DFT from filename, build corresponding Markov Automaton and check against given property. * * @param filename Path to DFT file in Galileo format. * @param property PCTC formula capturing the property to check. @@ -19,21 +19,21 @@ void analyzeDFT(std::string filename, std::string property) { storm::storage::DFT dft = parser.parseDFT(filename); std::cout << "Built data structure" << std::endl; - // Building CTMC - std::cout << "Building CTMC..." << std::endl; + // Building Markov Automaton + std::cout << "Building Markov Automaton..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); - std::shared_ptr> model = builder.buildCTMC(); - std::cout << "Built CTMC" << std::endl; + std::shared_ptr> model = builder.buildMA(); + std::cout << "Built Markov Automaton" << std::endl; // Model checking std::cout << "Model checking..." << std::endl; std::vector> formulas = storm::parseFormulasForExplicit(property); assert(formulas.size() == 1); - std::unique_ptr resultCtmc(storm::verifySparseModel(model, formulas[0])); - assert(resultCtmc); + std::unique_ptr resultMA(storm::verifySparseModel(model, formulas[0])); + assert(resultMA); std::cout << "Result: "; - resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *resultCtmc << std::endl; + resultMA->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << *resultMA << std::endl; } /*! From 32c52d227141fa5caf37b26ae816730722db5e0a Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 11:12:20 +0100 Subject: [PATCH 11/17] Parse PDEPs Former-commit-id: 623afd494f3b5ba6ce0453416922bf4bd2dc1daa --- examples/dft/pdep.dft | 12 ++++++++++++ src/parser/DFTGalileoParser.cpp | 7 +++++-- src/storage/dft/DFTBuilder.h | 20 ++++++++++++++------ src/storage/dft/DFTElements.h | 5 +++-- 4 files changed, 34 insertions(+), 10 deletions(-) create mode 100644 examples/dft/pdep.dft diff --git a/examples/dft/pdep.dft b/examples/dft/pdep.dft new file mode 100644 index 000000000..f8cb0382b --- /dev/null +++ b/examples/dft/pdep.dft @@ -0,0 +1,12 @@ +// From Junges2015 +// Example 3.19 + +toplevel "SF"; +"SF" or "A" "B" "PDEP"; +"A" pand "S" "MA"; +"B" and "MA" "MB"; +"PDEP" pdep=0.2 "MA" "S"; + +"S" lambda=0.5 dorm=0; +"MA" lambda=0.5 dorm=0; +"MB" lambda=0.5 dorm=0; diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 262098a68..c8639ae30 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -106,8 +106,11 @@ namespace storm { success = builder.addPandElement(name, childNames); } else if (tokens[1] == "wsp" || tokens[1] == "csp") { success = builder.addSpareElement(name, childNames); - } else if (boost::starts_with(tokens[1], "fdep")) { - success = builder.addFDepElement(name, childNames, storm::utility::one()); + } else if (tokens[1] == "fdep") { + success = builder.addDepElement(name, childNames, storm::utility::one()); + } else if (boost::starts_with(tokens[1], "pdep=")) { + ValueType probability = parseRationalExpression(tokens[1].substr(5)); + success = builder.addDepElement(name, childNames, probability); } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 9297d90cf..a2422522c 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -53,28 +53,36 @@ namespace storm { return addStandardGate(name, children, DFTElementTypes::SPARE); } - bool addFDepElement(std::string const& name, std::vector const& children, ValueType probability) { + bool addDepElement(std::string const& name, std::vector const& children, ValueType probability) { assert(children.size() > 1); if(mElements.count(name) != 0) { // Element with that name already exists. return false; } + + if (storm::utility::isZero(probability)) { + // Element is superfluous + return true; + } std::string trigger = children[0]; //TODO Matthias: collect constraints for SMT solving //0 <= probability <= 1 if (!storm::utility::isOne(probability) && children.size() > 2) { - //TODO Matthias: introduce additional element for probability and then add fdeps with probability 1 to children - std::cerr << "Probability != 1 currently not supported." << std::endl; + //TODO Matthias: introduce additional element for probability and then add pdeps with probability 1 to children + std::cerr << "Probability != 1 for more than one child currently not supported." << std::endl; + return false; } for (size_t i = 1; i < children.size(); ++i) { - std::string nameFdep = name + "_" + std::to_string(i); - if(mElements.count(nameFdep) != 0) { + std::string nameDep = name + "_" + std::to_string(i); + if(mElements.count(nameDep) != 0) { // Element with that name already exists. + std::cerr << "Element with name: " << nameDep << " already exists." << std::endl; return false; } - DFTDependencyPointer element = std::make_shared>(mNextId++, nameFdep, trigger, children[i], storm::utility::one()); + assert(storm::utility::isOne(probability) || children.size() == 2); + DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, trigger, children[i], probability); mElements[element->name()] = element; mDependencies.push_back(element); } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 063a8a414..9dcc42b8d 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -431,8 +431,9 @@ namespace storm { virtual std::string toString() const override { std::stringstream stream; - stream << "{" << this->name() << "} FDEP(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")"; - if (!storm::utility::isOne(mProbability)) { + bool fdep = storm::utility::isOne(mProbability); + stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")"; + if (!fdep) { stream << " with probability " << mProbability; } return stream.str(); From 35f5f9de1529b780a2c21b00b695d80f2de0dc72 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 11:42:07 +0100 Subject: [PATCH 12/17] Small refactoring Former-commit-id: 102054c6043d08de0caf3db6db0ee85684aa1c98 --- src/builder/ExplicitDFTModelBuilder.cpp | 3 ++- src/builder/ExplicitDFTModelBuilder.h | 2 +- src/storm-dyftee.cpp | 16 ++++++++-------- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index d4de53d64..1bfc445e7 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -1,5 +1,6 @@ #include "src/builder/ExplicitDFTModelBuilder.h" #include +#include #include #include #include @@ -13,7 +14,7 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilder::buildMA() { + std::shared_ptr> ExplicitDFTModelBuilder::buildModel() { // Initialize DFTStatePointer state = std::make_shared>(mDft, newIndex++); mStates.findOrAdd(state->status(), state); diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index edb2e1a94..b2d27aadd 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -53,7 +53,7 @@ namespace storm { // 2^nrBE is upper bound for state space } - std::shared_ptr> buildMA(); + std::shared_ptr> buildModel(); private: void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index a86347e3b..a8122f2bd 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -6,7 +6,7 @@ #include "utility/storm.h" /*! - * Load DFT from filename, build corresponding Markov Automaton and check against given property. + * Load DFT from filename, build corresponding Model and check against given property. * * @param filename Path to DFT file in Galileo format. * @param property PCTC formula capturing the property to check. @@ -20,20 +20,20 @@ void analyzeDFT(std::string filename, std::string property) { std::cout << "Built data structure" << std::endl; // Building Markov Automaton - std::cout << "Building Markov Automaton..." << std::endl; + std::cout << "Building Model..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); - std::shared_ptr> model = builder.buildMA(); - std::cout << "Built Markov Automaton" << std::endl; + std::shared_ptr> model = builder.buildModel(); + std::cout << "Built Model" << std::endl; // Model checking std::cout << "Model checking..." << std::endl; std::vector> formulas = storm::parseFormulasForExplicit(property); assert(formulas.size() == 1); - std::unique_ptr resultMA(storm::verifySparseModel(model, formulas[0])); - assert(resultMA); + std::unique_ptr result(storm::verifySparseModel(model, formulas[0])); + assert(result); std::cout << "Result: "; - resultMA->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *resultMA << std::endl; + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << *result << std::endl; } /*! From 46642f2bcad04e386e16bc6e5503ec585936ee28 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 13:11:57 +0100 Subject: [PATCH 13/17] CTMCs are working again Former-commit-id: 259bfefa547dec09cf82849b9a1bbc525aff4c4b --- src/builder/ExplicitDFTModelBuilder.cpp | 53 ++++++++++++++++++++----- src/builder/ExplicitDFTModelBuilder.h | 2 +- 2 files changed, 45 insertions(+), 10 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 1bfc445e7..30ed5fcbe 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -28,14 +28,23 @@ namespace storm { storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); // Begin model generation - exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); + bool deterministic = exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); STORM_LOG_DEBUG("Generated " << mStates.size() << " states"); + STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic")); // Build Markov Automaton modelComponents.markovianStates = storm::storage::BitVector(mStates.size(), tmpMarkovianStates); // Build transition matrix modelComponents.transitionMatrix = transitionMatrixBuilder.build(); - STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix); + STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix); + // TODO: easier output for vectors + std::stringstream stream; + for (uint_fast64_t i = 0; i < modelComponents.exitRates.size() - 1; ++i) { + stream << modelComponents.exitRates[i] << ", "; + } + stream << modelComponents.exitRates.back(); + STORM_LOG_DEBUG("Exit rates: " << stream.str()); + STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates); assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); // Build state labeling @@ -68,22 +77,42 @@ namespace storm { } } - std::shared_ptr> model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); + std::shared_ptr> model; + if (deterministic) { + // Turn the probabilities into rates by multiplying each row with the exit rate of the state. + // TODO Matthias: avoid transforming back and forth + storm::storage::SparseMatrix rateMatrix(modelComponents.transitionMatrix); + for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { + for (auto& entry : rateMatrix.getRow(row)) { + entry.setValue(entry.getValue() * modelComponents.exitRates[row]); + } + } + + model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling)); + } else { + model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); + + } model->printModelInformationToStream(std::cout); return model; } template - void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates) { + bool ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates) { assert(exitRates.empty()); assert(markovianStates.empty()); - // TODO Matthias: set Markovian states + // TODO Matthias: set Markovian states directly as bitvector? std::map outgoingTransitions; + size_t rowOffset = 0; // Captures number of non-deterministic choices + ValueType exitRate; + bool deterministic = true; + //TODO Matthias: Handle dependencies! while (!stateQueue.empty()) { // Initialization outgoingTransitions.clear(); + exitRate = storm::utility::zero(); // Consider next state DFTStatePointer state = stateQueue.front(); @@ -93,10 +122,12 @@ namespace storm { // Add self loop for target states if (mDft.hasFailed(state) || mDft.isFailsafe(state)) { - transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one()); + transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); exitRates.push_back(storm::utility::one()); assert(exitRates.size()-1 == state->getId()); + markovianStates.push_back(state->getId()); // No further exploration required continue; } else { @@ -173,19 +204,23 @@ namespace storm { outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate); } + exitRate += rate; + } // end while failing BE // Add all transitions - ValueType exitRate = storm::utility::zero(); + transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) { - transitionMatrixBuilder.addNextValue(state->getId(), it->first, it->second); - exitRate += it->second; + ValueType probability = it->second / exitRate; // Transform rate to probability + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability); } exitRates.push_back(exitRate); assert(exitRates.size()-1 == state->getId()); + markovianStates.push_back(state->getId()); } // end while queue + return deterministic; } // Explicitly instantiate the class. diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index b2d27aadd..6125b6fa1 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -56,7 +56,7 @@ namespace storm { std::shared_ptr> buildModel(); private: - void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); + bool exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); }; } From 24cd1ec597be2d81bd7566cf3c2beeddf9e9234d Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 14:01:04 +0100 Subject: [PATCH 14/17] Vector output without template seems to work Former-commit-id: 3627729e256d2d14ebd20781fa89a86d2b350776 --- src/builder/ExplicitDFTModelBuilder.cpp | 9 ++------- src/utility/vector.cpp | 9 +++++---- src/utility/vector.h | 6 ++++-- 3 files changed, 11 insertions(+), 13 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 30ed5fcbe..0bd92b069 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -2,6 +2,7 @@ #include #include #include +#include #include #include @@ -37,13 +38,7 @@ namespace storm { // Build transition matrix modelComponents.transitionMatrix = transitionMatrixBuilder.build(); STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix); - // TODO: easier output for vectors - std::stringstream stream; - for (uint_fast64_t i = 0; i < modelComponents.exitRates.size() - 1; ++i) { - stream << modelComponents.exitRates[i] << ", "; - } - stream << modelComponents.exitRates.back(); - STORM_LOG_DEBUG("Exit rates: " << stream.str()); + STORM_LOG_DEBUG("Exit rates: " << modelComponents.exitRates); STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates); assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); diff --git a/src/utility/vector.cpp b/src/utility/vector.cpp index e4a1dd05c..20af3c628 100644 --- a/src/utility/vector.cpp +++ b/src/utility/vector.cpp @@ -1,7 +1,8 @@ #include "src/utility/vector.h" -template -std::ostream& operator<<(std::ostream& out, std::vector const& vector) { +//template +//std::ostream& operator<<(std::ostream& out, std::vector const& vector) { +std::ostream& operator<<(std::ostream& out, std::vector const& vector) { out << "vector (" << vector.size() << ") [ "; for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { out << vector[i] << ", "; @@ -12,5 +13,5 @@ std::ostream& operator<<(std::ostream& out, std::vector const& vector } // Explicitly instantiate functions. -template std::ostream& operator<<(std::ostream& out, std::vector const& vector); -template std::ostream& operator<<(std::ostream& out, std::vector const& vector); +//template std::ostream& operator<<(std::ostream& out, std::vector const& vector); +//template std::ostream& operator<<(std::ostream& out, std::vector const& vector); \ No newline at end of file diff --git a/src/utility/vector.h b/src/utility/vector.h index 665569645..6b09f0467 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -15,8 +15,10 @@ #include "src/utility/macros.h" #include "src/solver/OptimizationDirection.h" -template -std::ostream& operator<<(std::ostream& out, std::vector const& vector); +// Template was causing problems as Carl has the same function +//template +//std::ostream& operator<<(std::ostream& out, std::vector const& vector); +std::ostream& operator<<(std::ostream& out, std::vector const& vector); namespace storm { namespace utility { From 87e51e04b5ea492af71df15544f66b2ee398f7af Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 14:01:35 +0100 Subject: [PATCH 15/17] Improved benchmark script Former-commit-id: 78f0d49a03b3f6157e7c56577dfe0bd58d00bb0f --- benchmark_dft.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/benchmark_dft.py b/benchmark_dft.py index 1b8e29972..7fe59a276 100644 --- a/benchmark_dft.py +++ b/benchmark_dft.py @@ -13,10 +13,16 @@ EXAMPLE_DIR= "/Users/mvolk/develop/storm/examples/dft/" benchmarks = [ ("and", False, [3, 1]), ("and_param", True, ["(4*x^2+2*x+1)/((x) * (2*x+1))", "1"]), + ("cardiac", False, [11378, 1]), + ("cas", False, [0.859736, 1]), ("cm2", False, [0.256272, 1]), #("cm4", False, [0, 1]), ("cps", False, ["inf", 0.333333]), - #("fdep", False, [0, 1]), + ("deathegg", False, [46.667, 1]), + ("fdep", False, [0.666667, 1]), + #("ftpp_complex", False, [0, 1]), # Compute + #("ftpp_large", False, [0, 1]), # Compute + #("ftpp_standard", False, [0, 1]), # Compute ("mdcs", False, [2.85414, 1]), ("mdcs2", False, [2.85414, 1]), ("mp", False, [1.66667, 1]), @@ -59,8 +65,7 @@ def run_storm_dft(filename, prop, parametric, quiet): # Get result match = re.search(r'Result: \[(.*)\]', output) if not match: - print("No valid result found in: " + output) - return + return None result = match.group(1) return result @@ -98,6 +103,10 @@ if __name__ == "__main__": if args.debuglevel > 0: print("Running '{}' with property '{}'".format(benchmark, prop)) result = run_storm_dft(benchmark, prop, parametric, args.debuglevel<2) + if result is None: + print("Error occurred on example '{}' with property '{}'".format(benchmark, prop)) + continue + if not parametric: # Float result = float(result) From 64b24043c57c30efccac7892fb53e2f96071adaf Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 18:08:20 +0100 Subject: [PATCH 16/17] Dependencies working Former-commit-id: e262bfc5aa6631ce9c2b4c795b80922977faa90c --- src/builder/ExplicitDFTModelBuilder.cpp | 86 +++++++++++++++---------- src/storage/dft/DFT.cpp | 6 +- src/storage/dft/DFT.h | 5 ++ src/storage/dft/DFTState.cpp | 38 +++++++++-- src/storage/dft/DFTState.h | 44 ++++++++++--- 5 files changed, 126 insertions(+), 53 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 0bd92b069..817295346 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -40,7 +40,7 @@ namespace storm { STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix); STORM_LOG_DEBUG("Exit rates: " << modelComponents.exitRates); STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates); - assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); + assert(!deterministic || modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size()); @@ -100,24 +100,26 @@ namespace storm { // TODO Matthias: set Markovian states directly as bitvector? std::map outgoingTransitions; size_t rowOffset = 0; // Captures number of non-deterministic choices - ValueType exitRate; bool deterministic = true; - //TODO Matthias: Handle dependencies! while (!stateQueue.empty()) { // Initialization outgoingTransitions.clear(); - exitRate = storm::utility::zero(); + ValueType exitRate = storm::utility::zero(); // Consider next state DFTStatePointer state = stateQueue.front(); stateQueue.pop(); + bool hasDependencies = state->nrFailableDependencies() > 0; + deterministic &= !hasDependencies; + size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); size_t smallest = 0; + transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); + // Add self loop for target states if (mDft.hasFailed(state) || mDft.isFailsafe(state)) { - transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); exitRates.push_back(storm::utility::one()); @@ -130,18 +132,21 @@ namespace storm { } // Let BE fail - while (smallest < state->nrFailableBEs()) { + while (smallest < failableCount) { STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state)); // Construct new state as copy from original one DFTStatePointer newState = std::make_shared>(*state); std::pair>, bool> nextBEPair = newState->letNextBEFail(smallest++); std::shared_ptr> nextBE = nextBEPair.first; - if (nextBE == nullptr) { - break; - } + assert(nextBE); + assert(nextBEPair.second == hasDependencies); STORM_LOG_TRACE("with the failure of: " << nextBE->name() << " [" << nextBE->id() << "]"); + // Update failable dependencies + newState->updateFailableDependencies(nextBE->id()); + + // Propagate failures storm::storage::DFTStateSpaceGenerationQueues queues; for (DFTGatePointer parent : nextBE->parents()) { @@ -179,42 +184,53 @@ namespace storm { stateQueue.push(newState); } - // Set failure rate according to usage - bool isUsed = true; - if (mDft.hasRepresentant(nextBE->id())) { - DFTElementPointer representant = mDft.getRepresentant(nextBE->id()); - // Used must be checked for the state we are coming from as this state is responsible for the - // rate and not the new state we are going to - isUsed = state->isUsed(representant->id()); - } - STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); - ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); - auto resultFind = outgoingTransitions.find(newState->getId()); - if (resultFind != outgoingTransitions.end()) { - // Add to existing transition - resultFind->second += rate; - STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second); + // Set transitions + if (hasDependencies) { + // Failure is due to dependency -> add non-deterministic choice + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), storm::utility::one()); } else { - // Insert new transition - outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); - STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate); + // Set failure rate according to usage + bool isUsed = true; + if (mDft.hasRepresentant(nextBE->id())) { + DFTElementPointer representant = mDft.getRepresentant(nextBE->id()); + // Used must be checked for the state we are coming from as this state is responsible for the + // rate and not the new state we are going to + isUsed = state->isUsed(representant->id()); + } + STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); + ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); + auto resultFind = outgoingTransitions.find(newState->getId()); + if (resultFind != outgoingTransitions.end()) { + // Add to existing transition + resultFind->second += rate; + STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second); + } else { + // Insert new transition + outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate); + } + exitRate += rate; } - exitRate += rate; } // end while failing BE - // Add all transitions - transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); - for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) - { - ValueType probability = it->second / exitRate; // Transform rate to probability - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability); + if (hasDependencies) { + rowOffset--; // One increment to many + } else { + // Add all probability transitions + for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) + { + ValueType probability = it->second / exitRate; // Transform rate to probability + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability); + } + + markovianStates.push_back(state->getId()); } exitRates.push_back(exitRate); assert(exitRates.size()-1 == state->getId()); - markovianStates.push_back(state->getId()); } // end while queue + assert(!deterministic || rowOffset == 0); return deterministic; } diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 112a9273b..1329cab38 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -11,13 +11,13 @@ namespace storm { size_t stateIndex = 0; mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; - for(auto& elem : mElements) { + for (auto& elem : mElements) { mIdToFailureIndex.push_back(stateIndex); stateIndex += 2; if(elem->isBasicElement()) { ++mNrOfBEs; } - else if(elem->isSpareGate()) { + else if (elem->isSpareGate()) { ++mNrOfSpares; for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { if(mActivationIndex.count(spareReprs->id()) == 0) { @@ -39,6 +39,8 @@ namespace storm { mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); stateIndex += mUsageInfoBits; + } else if (elem->isDependency()) { + mDependencies.push_back(elem->id()); } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 2cfbf6422..cff6db0cb 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -51,6 +51,7 @@ namespace storm { size_t mStateSize; std::map mActivationIndex; std::map> mSpareModules; + std::vector mDependencies; std::vector mTopModule; std::vector mIdToFailureIndex; std::map mUsageIndex; @@ -120,6 +121,10 @@ namespace storm { } } + std::vector const& getDependencies() const { + return mDependencies; + } + void propagateActivation(DFTState& state, size_t representativeId) const { state.activate(representativeId); for(size_t id : module(representativeId)) { diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index d760129e0..17bb4aee8 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -78,17 +78,41 @@ namespace storm { } } + template + bool DFTState::updateFailableDependencies(size_t id) { + assert(hasFailed(id)); + for (size_t i = 0; i < mDft.getDependencies().size(); ++i) { + std::shared_ptr> dependency = std::static_pointer_cast>(mDft.getElement(mDft.getDependencies()[i])); + if (dependency->triggerEvent()->id() == id) { + if (!hasFailed(dependency->dependentEvent()->id())) { + mFailableDependencies.push_back(dependency->id()); + STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); + } + } + } + return nrFailableDependencies() > 0; + } + template std::pair>, bool> DFTState::letNextBEFail(size_t index) { - assert(index < mIsCurrentlyFailableBE.size()); STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - // TODO set when implementing functional dependencies - bool dueToFdep = false; - std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), dueToFdep); - mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); - setFailed(res.first->id()); - return res; + if (nrFailableDependencies() > 0) { + // Consider failure due to dependency + assert(index < nrFailableDependencies()); + std::shared_ptr> dependency = std::static_pointer_cast>(mDft.getElement(mFailableDependencies[index])); + std::pair>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true); + mFailableDependencies.erase(mFailableDependencies.begin() + index); + setFailed(res.first->id()); + return res; + } else { + // Consider "normal" failure + assert(index < nrFailableBEs()); + std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); + mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); + setFailed(res.first->id()); + return res; + } } template diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index fed33eee3..a1bab2583 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -25,6 +25,7 @@ namespace storm { size_t mId; std::vector mInactiveSpares; std::vector mIsCurrentlyFailableBE; + std::vector mFailableDependencies; std::vector mUsedRepresentants; bool mValid = true; const DFT& mDft; @@ -110,6 +111,17 @@ namespace storm { return mIsCurrentlyFailableBE.size(); } + size_t nrFailableDependencies() const { + return mFailableDependencies.size(); + } + + /** + * Sets all failable BEs due to dependencies from newly failed element + * @param id Id of the newly failed element + * @return true if failable dependent events exist + */ + bool updateFailableDependencies(size_t id); + /** * Sets the next BE as failed * @param smallestIndex Index in currentlyFailableBE of BE to fail @@ -119,17 +131,31 @@ namespace storm { std::string getCurrentlyFailableString() const { std::stringstream stream; - auto it = mIsCurrentlyFailableBE.begin(); - stream << "{"; - if(it != mIsCurrentlyFailableBE.end()) { - stream << *it; - } - ++it; - while(it != mIsCurrentlyFailableBE.end()) { - stream << ", " << *it; + if (nrFailableDependencies() > 0) { + auto it = mFailableDependencies.begin(); + stream << "{Dependencies: "; + if (it != mFailableDependencies.end()) { + stream << *it; + } + ++it; + while(it != mFailableDependencies.end()) { + stream << ", " << *it; + ++it; + } + stream << "} "; + } else { + auto it = mIsCurrentlyFailableBE.begin(); + stream << "{"; + if(it != mIsCurrentlyFailableBE.end()) { + stream << *it; + } ++it; + while(it != mIsCurrentlyFailableBE.end()) { + stream << ", " << *it; + ++it; + } + stream << "}"; } - stream << "}"; return stream.str(); } From 72b09a693c37bf01cefc63af108eaefd5e197b40 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 18:09:06 +0100 Subject: [PATCH 17/17] More examples Former-commit-id: e4ea9cf5dc3bd60844d91fae4c6a8a5d9da71188 --- benchmark_dft.py | 1 + examples/dft/fdep2.dft | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 examples/dft/fdep2.dft diff --git a/benchmark_dft.py b/benchmark_dft.py index 7fe59a276..54dadeacc 100644 --- a/benchmark_dft.py +++ b/benchmark_dft.py @@ -20,6 +20,7 @@ benchmarks = [ ("cps", False, ["inf", 0.333333]), ("deathegg", False, [46.667, 1]), ("fdep", False, [0.666667, 1]), + ("fdep2", False, [2, 1]), #("ftpp_complex", False, [0, 1]), # Compute #("ftpp_large", False, [0, 1]), # Compute #("ftpp_standard", False, [0, 1]), # Compute diff --git a/examples/dft/fdep2.dft b/examples/dft/fdep2.dft new file mode 100644 index 000000000..a444ed4be --- /dev/null +++ b/examples/dft/fdep2.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" and "B" "C"; +"F" fdep "B" "C"; +"B" lambda=0.5 dorm=0; +"C" lambda=0.5 dorm=0;