diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index bf23c5d4f..6e938f289 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -1,10 +1,16 @@ #include "src/builder/ExplicitDFTModelBuilder.h" +#include <src/models/sparse/Ctmc.h> namespace storm { namespace builder { + template <typename ValueType, typename RewardModelType, typename IndexType> + ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { + // Intentionally left empty. + } + template<typename ValueType, typename RewardModelType, typename IndexType> - void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() { + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() { // Initialize storm::storage::DFTState state(mDft, newIndex++); mStates.insert(state); @@ -20,9 +26,29 @@ namespace storm { STORM_LOG_DEBUG("Generated " << mStates.size() << " states"); // Build CTMC - transitionMatrix = transitionMatrixBuilder.build(); - STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << transitionMatrix); - // TODO Matthias: build CTMC + ModelComponents modelComponents; + // Build transition matrix + modelComponents.transitionMatrix = transitionMatrixBuilder.build(); + STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix); + + // Build state labeling + modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size()); + // Also label the initial state with the special label "init". + modelComponents.stateLabeling.addLabel("init"); + modelComponents.stateLabeling.addLabelToState("init", 0); + // TODO Matthias: not fixed + modelComponents.stateLabeling.addLabel("failed"); + modelComponents.stateLabeling.addLabelToState("failed", 7); + + // TODO Matthias: initialize + modelComponents.rewardModels; + modelComponents.choiceLabeling; + + + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model; + model = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); + model->printModelInformationToStream(std::cout); + return model; } template<typename ValueType, typename RewardModelType, typename IndexType> diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 8938e690f..f5920bb52 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -5,6 +5,7 @@ #include <src/models/sparse/StateLabeling.h> #include <src/models/sparse/StandardRewardModel.h> +#include <src/models/sparse/Model.h> #include <src/storage/SparseMatrix.h> #include <boost/container/flat_set.hpp> #include <boost/optional/optional.hpp> @@ -16,25 +17,34 @@ namespace storm { template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t> class ExplicitDFTModelBuilder { - storm::storage::DFT const &mDft; - std::unordered_set<storm::storage::DFTState> mStates; - size_t newIndex = 0; - // The transition matrix. - storm::storage::SparseMatrix<ValueType> transitionMatrix; + // A structure holding the individual components of a model. + struct ModelComponents { + ModelComponents(); + + // The transition matrix. + storm::storage::SparseMatrix<ValueType> transitionMatrix; + + // The state labeling. + storm::models::sparse::StateLabeling stateLabeling; - // The state labeling. - storm::models::sparse::StateLabeling stateLabeling; + // The reward models associated with the model. + std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels; - // A vector that stores a labeling for each choice. - boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling; + // A vector that stores a labeling for each choice. + boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling; + }; + + storm::storage::DFT const &mDft; + std::unordered_set<storm::storage::DFTState> mStates; + size_t newIndex = 0; public: ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) { } - void buildCTMC(); + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC(); private: void exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index bd34cdeea..a5a4feb98 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -1,7 +1,9 @@ +#include "logic/Formula.h" #include "parser/DFTGalileoParser.h" #include "utility/initialize.h" #include "builder/ExplicitDFTModelBuilder.h" - +#include "modelchecker/results/CheckResult.h" +#include "utility/storm.h" /* * Entry point for the DyFTeE backend. @@ -24,10 +26,19 @@ int main(int argc, char** argv) { std::cout << "Building CTMC..." << std::endl; storm::builder::ExplicitDFTModelBuilder<double> builder(dft); - builder.buildCTMC(); + std::shared_ptr<storm::models::sparse::Model<double>> model = builder.buildCTMC(); std::cout << "Built CTMC" << std::endl; std::cout << "Model checking..." << std::endl; - //TODO Matthias: check CTMC + //TODO Matthias: Construct formula, do not fix + std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit("Pmax=?[true U \"failed\"]"); + assert(formulas.size() == 1); + // Verify the model, if a formula was given. + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formulas[0])); + assert(result); + std::cout << "Result (initial states): "; + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << *result << std::endl; + std::cout << "Checked model" << std::endl; }