From c8158018b8796c9c90d1169e0ce8a5db10f62a3d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 31 Jan 2020 16:41:19 +0100 Subject: [PATCH] Use state elimination to eliminate chains of non-Markovian states in MA --- .../testfiles/ma/chain_elimination1.drn | 155 ++++++++ .../testfiles/ma/chain_elimination2.drn | 34 ++ .../NonMarkovianChainTransformer.cpp | 357 +++++------------- .../NonMarkovianChainTransformer.h | 7 +- .../NonMarkovianChainTransformerTest.cpp | 249 ++++++++++++ 5 files changed, 543 insertions(+), 259 deletions(-) create mode 100644 resources/examples/testfiles/ma/chain_elimination1.drn create mode 100644 resources/examples/testfiles/ma/chain_elimination2.drn create mode 100644 src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp diff --git a/resources/examples/testfiles/ma/chain_elimination1.drn b/resources/examples/testfiles/ma/chain_elimination1.drn new file mode 100644 index 000000000..4be37cb3a --- /dev/null +++ b/resources/examples/testfiles/ma/chain_elimination1.drn @@ -0,0 +1,155 @@ +// Exported by storm +// Original model type: Markov Automaton +@type: Markov Automaton +@parameters + +@reward_models + +@nr_states +43 +@model +state 0 !0 init + action 0 + 1 : 1 +state 1 !0.0003 + action 0 + 2 : 0.3333333333 + 3 : 0.3333333333 + 4 : 0.3333333333 +state 2 !0 + action 0 + 5 : 1 +state 3 !0 + action 0 + 6 : 1 +state 4 !0 + action 0 + 7 : 1 +state 5 !0 + action 0 + 8 : 1 +state 6 !0 + action 0 + 9 : 1 +state 7 !0 + action 0 + 10 : 1 +state 8 !0 + action 0 + 12 : 1 +state 9 !0 + action 0 + 14 : 1 +state 10 !0.1002 Fail + action 0 + 11 : 0.000998003992 + 13 : 0.000998003992 + 15 : 0.998003992 +state 11 !0 Fail + action 0 + 18 : 1 +state 12 !0.1002 Fail + action 0 + 16 : 0.000998003992 + 19 : 0.000998003992 + 20 : 0.998003992 +state 13 !0 Fail + action 0 + 21 : 1 +state 14 !0.1002 Fail + action 0 + 17 : 0.000998003992 + 22 : 0.000998003992 + 23 : 0.998003992 +state 15 !0 Fail + action 0 + 24 : 1 +state 16 !0 Fail + action 0 + 25 : 1 +state 17 !0 Fail + action 0 + 25 : 1 +state 18 !0 Fail + action 0 + 26 : 1 +state 19 !0 Fail + action 0 + 26 : 1 +state 20 !0 Fail + action 0 + 27 : 1 +state 21 !0 Fail + action 0 + 28 : 1 +state 22 !0 Fail + action 0 + 28 : 1 +state 23 !0 Fail + action 0 + 27 : 1 +state 24 !0 Fail + action 0 + 1 : 1 +state 25 !0.2001 Fail + action 0 + 31 : 0.0004997501249 + 32 : 0.4997501249 + 33 : 0.4997501249 +state 26 !0.2001 Fail + action 0 + 29 : 0.0004997501249 + 34 : 0.4997501249 + 35 : 0.4997501249 +state 27 !0 Fail + action 0 + 24 : 1 +state 28 !0.2001 Fail + action 0 + 30 : 0.0004997501249 + 36 : 0.4997501249 + 37 : 0.4997501249 +state 29 !0 Fail + action 0 + 38 : 1 +state 30 !0 Fail + action 0 + 38 : 1 +state 31 !0 Fail + action 0 + 38 : 1 +state 32 !0 Fail + action 0 + 14 : 1 +state 33 !0 Fail + action 0 + 12 : 1 +state 34 !0 Fail + action 0 + 12 : 1 +state 35 !0 Fail + action 0 + 39 : 1 +state 36 !0 Fail + action 0 + 14 : 1 +state 37 !0 Fail + action 0 + 39 : 1 +state 38 !0.3 Fail + action 0 + 40 : 0.3333333333 + 41 : 0.3333333333 + 42 : 0.3333333333 +state 39 !0 Fail + action 0 + 10 : 1 +state 40 !0 Fail + action 0 + 25 : 1 +state 41 !0 Fail + action 0 + 28 : 1 +state 42 !0 Fail + action 0 + 26 : 1 diff --git a/resources/examples/testfiles/ma/chain_elimination2.drn b/resources/examples/testfiles/ma/chain_elimination2.drn new file mode 100644 index 000000000..225843eec --- /dev/null +++ b/resources/examples/testfiles/ma/chain_elimination2.drn @@ -0,0 +1,34 @@ +// Exported by storm +// Original model type: Markov Automaton +@type: Markov Automaton +@parameters + +@reward_models + +@nr_states +10 +@model +state 0 !0.1 init + 1 : 1 +state 1 !0 + 2 : 1 +state 2 !0 + 3 : 1 +state 3 !0 + 4 : 0.1 + 5 : 0.9 +state 4 !0.2 Fail + 5 : 0.5 + 6 : 0.5 +state 5 !0.1 + 0 : 1 +state 6 !0.2 + 0 : 0.5 + 7 : 0.5 +state 7 !0.2 Fail + 6 : 0.5 + 8 : 0.5 +state 8 !0 Fail + 9 : 1 +state 9 !0 Fail + 3 : 1 diff --git a/src/storm/transformer/NonMarkovianChainTransformer.cpp b/src/storm/transformer/NonMarkovianChainTransformer.cpp index 7f5bd61c4..b51bcc7a0 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.cpp +++ b/src/storm/transformer/NonMarkovianChainTransformer.cpp @@ -1,40 +1,35 @@ -#include - #include "NonMarkovianChainTransformer.h" -#include "storm/logic/Formulas.h" -#include "storm/logic/FragmentSpecification.h" +#include -#include "storm/storage/sparse/ModelComponents.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/InvalidModelException.h" +#include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" +#include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/StandardRewardModel.h" +#include +#include "storm/storage/FlexibleSparseMatrix.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/utility/constants.h" -#include "storm/utility/ConstantsComparator.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/utility/graph.h" + namespace storm { namespace transformer { template std::shared_ptr> - NonMarkovianChainTransformer::eliminateNonmarkovianStates( - std::shared_ptr> ma, - EliminationLabelBehavior labelBehavior) { - // TODO reward models - + NonMarkovianChainTransformer::eliminateNonmarkovianStates(std::shared_ptr> ma, + EliminationLabelBehavior labelBehavior) { STORM_LOG_WARN_COND(labelBehavior == EliminationLabelBehavior::KeepLabels, "Labels are not preserved! Results may be incorrect. Continue at your own caution."); - if (labelBehavior == EliminationLabelBehavior::DeleteLabels) { - STORM_PRINT("Use Label Deletion" << std::endl) - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - STORM_PRINT("Use Label Merging" << std::endl) - } - STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!"); - if (ma->isClosed() && ma->getMarkovianStates().full()) { - storm::storage::sparse::ModelComponents components( - ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); + STORM_LOG_THROW(ma->isClosed(), storm::exceptions::InvalidModelException, "MA should be closed first."); + + if (ma->getMarkovianStates().full()) { + // Is already a CTMC + storm::storage::sparse::ModelComponents components(ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); components.exitRates = ma->getExitRates(); if (ma->hasChoiceLabeling()) { components.choiceLabeling = ma->getChoiceLabeling(); @@ -45,243 +40,98 @@ namespace storm { if (ma->hasChoiceOrigins()) { components.choiceOrigins = ma->getChoiceOrigins(); } - return std::make_shared>( - std::move(components)); + return std::make_shared>(std::move(components)); } - std::map eliminationMapping; - std::set statesToKeep; - std::queue changedStates; - std::queue queue; - - storm::storage::SparseMatrix backwards = ma->getBackwardTransitions(); + // Initialize + storm::storage::FlexibleSparseMatrix flexibleMatrix(ma->getTransitionMatrix()); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(ma->getTransitionMatrix().transpose(), true); + storm::models::sparse::StateLabeling stateLabeling = ma->getStateLabeling(); + // TODO: update reward models and choice labels according to kept states + STORM_LOG_WARN_COND(ma->getRewardModels().empty(), "Reward models are not preserved in chain elimination."); + std::unordered_map rewardModels; + STORM_LOG_WARN_COND(!ma->hasChoiceLabeling(), "Choice labels are not preserved in chain elimination."); + STORM_LOG_WARN_COND(!ma->hasStateValuations(), "State valuations are not preserved in chain elimination."); + STORM_LOG_WARN_COND(!ma->hasChoiceOrigins(), "Choice origins are not preserved in chain elimination."); + + // Eliminate all probabilistic states by state elimination + auto actionRewards = std::vector(ma->getTransitionMatrix().getRowCount(), storm::utility::zero()); + storm::solver::stateelimination::NondeterministicModelStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards); + storm::storage::BitVector keepStates(ma->getNumberOfStates(), true); - // Determine the state remapping - for (uint_fast64_t base_state = 0; base_state < ma->getNumberOfStates(); ++base_state) { - STORM_LOG_ASSERT(!ma->isHybridState(base_state), "Base state is hybrid."); - if (ma->isMarkovianState(base_state)) { - queue.push(base_state); - - while (!queue.empty()) { - auto currState = queue.front(); - queue.pop(); - - auto currLabels = ma->getLabelsOfState(currState); - - // Get predecessors from matrix - typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow(currState); - for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { - uint_fast64_t predecessor = entryIt->getColumn(); - if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { - if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels || - currLabels == ma->getLabelsOfState(predecessor)) { - // If labels are not to be preserved or states are labeled the same - if (!eliminationMapping.count(predecessor)) { - eliminationMapping[predecessor] = base_state; - queue.push(predecessor); - } else if (eliminationMapping[predecessor] != base_state) { - eliminationMapping.erase(predecessor); - statesToKeep.insert(predecessor); - changedStates.push(predecessor); - } - } else { - // Labels are to be preserved and states have different labels - if (eliminationMapping.count(predecessor)) { - eliminationMapping.erase(predecessor); - } - statesToKeep.insert(predecessor); - changedStates.push(predecessor); + for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { + STORM_LOG_ASSERT(!ma->isHybridState(state), "State is hybrid."); + if (ma->isProbabilisticState(state)) { + // Only eliminate immediate states (and no Markovian states) + if (ma->getNumberOfChoices(state) <= 1) { + // Eliminate only if no non-determinism occurs + STORM_LOG_ASSERT(ma->getNumberOfChoices(state) == 1, "State " << state << " has no choices."); + STORM_LOG_ASSERT(flexibleMatrix.getRowGroupSize(state) == 1, "State " << state << " has too many rows."); + + if (labelBehavior == EliminationLabelBehavior::KeepLabels) { + // Only eliminate if eliminated state and all its successors have the same labels + bool sameLabels = true; + auto currLabels = stateLabeling.getLabelsOfState(state); + typename storm::storage::FlexibleSparseMatrix::row_type entriesInRow = flexibleMatrix.getRow(state, 0); // Row group + for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { + if (currLabels != stateLabeling.getLabelsOfState(entryIt->getColumn())) { + STORM_LOG_TRACE("Do not eliminate state " << state << " because labels of state " << entryIt->getColumn() << " are different."); + sameLabels = false; + break; } } - } - } - } - } - - // Correct the mapping with the states which have to be kept - while (!changedStates.empty()) { - uint_fast64_t base_state = changedStates.front(); - queue.push(base_state); - - while (!queue.empty()) { - auto currState = queue.front(); - queue.pop(); - - auto currLabels = ma->getLabelsOfState(currState); + if (!sameLabels) { + continue; + } + } else { + // As helper for the labeling we create a bitvector representing all successor states + storm::storage::BitVector successors(stateLabeling.getNumberOfItems()); + typename storm::storage::FlexibleSparseMatrix::row_type entriesInRow = flexibleMatrix.getRow(state, 0); // Row group + for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { + successors.set(entryIt->getColumn()); + } - // Get predecessors from matrix - typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow(currState); - for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { - uint_fast64_t predecessor = entryIt->getColumn(); - if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { - if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels || - currLabels == ma->getLabelsOfState(predecessor)) { - // If labels are not to be preserved or states are labeled the same - if (!eliminationMapping.count(predecessor)) { - eliminationMapping[predecessor] = base_state; - queue.push(predecessor); - } else if (eliminationMapping[predecessor] != base_state) { - eliminationMapping.erase(predecessor); - statesToKeep.insert(predecessor); - changedStates.push(predecessor); + if (labelBehavior == EliminationLabelBehavior::MergeLabels) { + // Add labels from eliminated state to successors + for (std::string const& label : stateLabeling.getLabelsOfState(state)) { + storm::storage::BitVector states = stateLabeling.getStates(label); + // Add successor states for this label as well + stateLabeling.setStates(label, states | successors); } } else { - // Labels are to be preserved and states have different labels - if (eliminationMapping.count(predecessor)) { - eliminationMapping.erase(predecessor); + STORM_LOG_ASSERT(labelBehavior == EliminationLabelBehavior::DeleteLabels, "Unknown label behavior."); + if (stateLabeling.getStateHasLabel("init", state)) { + // Add "init" label of eliminated state to successor states + storm::storage::BitVector states = stateLabeling.getStates("init"); + // Add successor states for this label as well + stateLabeling.setStates("init", states | successors); } - statesToKeep.insert(predecessor); - changedStates.push(predecessor); } } - } - } - - changedStates.pop(); - } - - // At this point, we hopefully have a valid mapping which eliminates a lot of states - - STORM_LOG_TRACE("Elimination Mapping:"); - for (auto entry : eliminationMapping) { - STORM_LOG_TRACE(std::to_string(entry.first) << " -> " << std::to_string(entry.second)); - } - STORM_LOG_INFO("Eliminating " << eliminationMapping.size() << " states" << std::endl); - - // TODO explore if one can construct elimination mapping and state remapping in one step - uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size(); - - std::vector> labelMap(newStateCount, std::set()); - - // Construct a mapping of old state space to new one - std::vector stateRemapping(ma->getNumberOfStates(), -1); - uint_fast64_t currentNewState = 0; - for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { - if (eliminationMapping.count(state) > 0) { - if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) { - stateRemapping[eliminationMapping[state]] = currentNewState; - stateRemapping[state] = currentNewState; - ++currentNewState; - queue.push(eliminationMapping[state]); - } else { - stateRemapping[state] = stateRemapping[eliminationMapping[state]]; - } - if (labelBehavior == EliminationLabelBehavior::DeleteLabels && ma->getInitialStates().get(state)) { - // Keep initial label for 'delete' behavior - labelMap[stateRemapping[eliminationMapping[state]]].insert("init"); - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - //add all labels to the label set for the representative - for (auto const &label : ma->getLabelsOfState(state)) { - labelMap[stateRemapping[eliminationMapping[state]]].insert(label); - } - } - } else { - if (stateRemapping[state] == uint_fast64_t(-1)) { - stateRemapping[state] = currentNewState; - queue.push(state); - ++currentNewState; - } - if (labelBehavior == EliminationLabelBehavior::DeleteLabels && ma->getInitialStates().get(state)) { - // Keep initial label for 'delete' behavior - labelMap[stateRemapping[state]].insert("init"); - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - for (auto const &label : ma->getLabelsOfState(state)) { - labelMap[stateRemapping[state]].insert(label); - } + // Eliminate this probabilistic state + stateEliminator.eliminateState(state, true); + keepStates.set(state, false); } } } - // Build the new MA - storm::storage::SparseMatrix newTransitionMatrix; - storm::models::sparse::StateLabeling newStateLabeling(newStateCount); - storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(),false); - std::vector newExitRates; - //TODO choice labeling - boost::optional newChoiceLabeling; + // Create the new matrix + auto keptRows = ma->getTransitionMatrix().getRowFilter(keepStates); + storm::storage::SparseMatrix matrix = flexibleMatrix.createSparseMatrix(keptRows, keepStates); - // Initialize the matrix builder and helper variables - storm::storage::SparseMatrixBuilder matrixBuilder = storm::storage::SparseMatrixBuilder( - 0, 0, 0, false, true, 0); + // TODO: obtain the reward model for the resulting system - for (auto const &label : ma->getStateLabeling().getLabels()) { - if (!newStateLabeling.containsLabel(label)) { - newStateLabeling.addLabel(label); - } - } - uint_fast64_t currentRow = 0; - uint_fast64_t state = 0; - while (!queue.empty()) { - state = queue.front(); - queue.pop(); + // Prepare model components + storm::storage::BitVector markovianStates = ma->getMarkovianStates() % keepStates; + storm::models::sparse::StateLabeling labeling = stateLabeling.getSubLabeling(keepStates); + storm::storage::sparse::ModelComponents components(matrix, labeling, ma->getRewardModels(), false, markovianStates); + std::vector exitRates(markovianStates.size()); + storm::utility::vector::selectVectorValues(exitRates, keepStates, ma->getExitRates()); + components.exitRates = exitRates; - std::set labelSet = ma->getLabelsOfState(state); - if (labelBehavior == EliminationLabelBehavior::DeleteLabels) { - labelSet.insert(labelMap[stateRemapping[state]].begin(), labelMap[stateRemapping[state]].end()); - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - labelSet = labelMap[stateRemapping[state]]; - } - - for (auto const &label : labelSet) { - if (!newStateLabeling.containsLabel(label)) { - newStateLabeling.addLabel(label); - } - - newStateLabeling.addLabelToState(label, stateRemapping[state]); - } - - // Use a set to not include redundant rows - std::set> rowSet; - for (uint_fast64_t row = 0; row < ma->getTransitionMatrix().getRowGroupSize(state); ++row) { - std::map transitions; - for (typename storm::storage::SparseMatrix::const_iterator itEntry = ma->getTransitionMatrix().getRow( - state, row).begin(); - itEntry != ma->getTransitionMatrix().getRow(state, row).end(); ++itEntry) { - uint_fast64_t newId = stateRemapping[itEntry->getColumn()]; - if (transitions.count(newId) == 0) { - transitions[newId] = itEntry->getValue(); - } else { - transitions[newId] += itEntry->getValue(); - } - } - rowSet.insert(transitions); - } - - // correctly set rates - auto rate = storm::utility::zero(); - - if (ma->isMarkovianState(state)) { - newMarkovianStates.set(stateRemapping[state], true); - rate = ma->getExitRates().at(state); - } - - newExitRates.push_back(rate); - // Build matrix - matrixBuilder.newRowGroup(currentRow); - for (auto const &row : rowSet) { - for (auto const &transition : row) { - matrixBuilder.addNextValue(currentRow, transition.first, transition.second); - STORM_LOG_TRACE(stateRemapping[state] << "->" << transition.first << " : " << transition.second - << std::endl); - } - ++currentRow; - } - } - // explicitly force dimensions of the matrix in case a column is missing - newTransitionMatrix = matrixBuilder.build(newStateCount, newStateCount, newStateCount); - - storm::storage::sparse::ModelComponents newComponents = storm::storage::sparse::ModelComponents( - std::move(newTransitionMatrix), std::move(newStateLabeling)); - - newComponents.rateTransitions = false; - newComponents.markovianStates = std::move(newMarkovianStates); - newComponents.exitRates = std::move(newExitRates); - auto model = std::make_shared>( - std::move(newComponents)); + // Build transformed model + auto model = std::make_shared>(std::move(components)); if (model->isConvertibleToCtmc()) { return model->convertToCtmc(); } else { @@ -290,50 +140,49 @@ namespace storm { } template - bool NonMarkovianChainTransformer::preservesFormula( - storm::logic::Formula const &formula) { + bool NonMarkovianChainTransformer::preservesFormula(storm::logic::Formula const& formula) { storm::logic::FragmentSpecification fragment = storm::logic::propositional(); fragment.setProbabilityOperatorsAllowed(true); fragment.setGloballyFormulasAllowed(true); fragment.setReachabilityProbabilityFormulasAllowed(true); fragment.setUntilFormulasAllowed(true); + fragment.setBoundedUntilFormulasAllowed(true); fragment.setTimeBoundedUntilFormulasAllowed(true); + fragment.setNextFormulasAllowed(false); + fragment.setStepBoundedUntilFormulasAllowed(false); + return formula.isInFragment(fragment); } template std::vector> - NonMarkovianChainTransformer::checkAndTransformFormulas( - std::vector> const &formulas) { + NonMarkovianChainTransformer::checkAndTransformFormulas(std::vector> const& formulas) { std::vector> result; - for (auto const &f : formulas) { + for (auto const& f : formulas) { if (preservesFormula(*f)) { result.push_back(f); } else { - STORM_LOG_INFO("Non-Markovian chain elimination does not preserve formula " << *f); + STORM_LOG_WARN("Non-Markovian chain elimination does not preserve formula " << *f); } } return result; } - template - class NonMarkovianChainTransformer; + template class NonMarkovianChainTransformer; - template - class NonMarkovianChainTransformer>; -#ifdef STORM_HAVE_CARL + template class NonMarkovianChainTransformer>; - template - class NonMarkovianChainTransformer; +#ifdef STORM_HAVE_CARL + template class NonMarkovianChainTransformer; - template - class NonMarkovianChainTransformer; + template class NonMarkovianChainTransformer; #endif + } } diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h index 691fcc9ee..64831ca70 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.h +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -21,13 +21,10 @@ namespace storm { * If no non-determinism occurs, a CTMC is generated. * * @param ma The input Markov Automaton. - * @param preserveLabels If set, the procedure considers the labels of non-Markovian states when eliminating states. + * @param labelBehavior How the labels of non-Markovian states should be treated when eliminating states. * @return A reference to the new model after eliminating non-Markovian states. */ - static std::shared_ptr> eliminateNonmarkovianStates( - std::shared_ptr> ma, - EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels - ); + static std::shared_ptr> eliminateNonmarkovianStates(std::shared_ptr> ma, EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels); /** * Check if the property specified by the given formula is preserved by the transformation. diff --git a/src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp b/src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp new file mode 100644 index 000000000..efe5acf5d --- /dev/null +++ b/src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp @@ -0,0 +1,249 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" +#include "storm/api/storm.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/api/storm-parsers.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/jani/Property.h" + + +TEST(NonMarkovianChainTransformerTest, StreamExampleTest) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); + std::string formulasString = "Pmin=? [ F \"done\"];Pmin=? [ F<=1 \"done\"];Tmin=? [ F \"done\" ]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); + auto model = storm::api::buildSparseModel(program, formulas)->template as>(); + + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(14ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + size_t initState = 0; + + auto labeling = model->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 10)); + + auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[2], true)); + EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Keep labels + auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels); + ASSERT_EQ(9ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 8)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Merge labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 7)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Delete labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 7)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + +} + +TEST(NonMarkovianChainTransformerTest, ChainElimination1ExampleTest) { + auto model = storm::parser::DirectEncodingParser::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination1.drn")->template as>(); + std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString)); + + EXPECT_EQ(43ul, model->getNumberOfStates()); + EXPECT_EQ(59ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + size_t initState = 0; + + auto labeling = model->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + for (size_t i = 10; i < 43; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + + auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[2], true)); + EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Keep labels + auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels); + ASSERT_EQ(13ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(29ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + for (size_t i = 5; i < 13; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Merge labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + for (size_t i = 0; i < 8; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Delete labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 0)); + for (size_t i = 1; i < 8; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); +} + +TEST(NonMarkovianChainTransformerTest, ChainElimination2ExampleTest) { + auto model = storm::parser::DirectEncodingParser::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination2.drn")->template as>(); + std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString)); + + EXPECT_EQ(10ul, model->getNumberOfStates()); + EXPECT_EQ(14ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + size_t initState = 0; + + auto labeling = model->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 7)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 8)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 9)); + + auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[2], true)); + EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Keep labels + auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels); + ASSERT_EQ(7ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 5)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 6)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Merge labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels); + ASSERT_EQ(5ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Delete labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels); + ASSERT_EQ(5ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 2)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); +}