From e51c3b9f44a902dcb22be2bd56c5c5b5a3f94eab Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Jan 2015 14:28:48 +0100 Subject: [PATCH] Conditional probabilities work for brp model from the paper by Baier et al. Former-commit-id: 02858bf34de64924262ea4ba14281f14cbe741b3 --- examples/pdtmc/brp/brp_128-2.pm | 4 +- examples/pdtmc/brp/brp_128-3.pm | 4 +- examples/pdtmc/brp/brp_128-4.pm | 4 +- examples/pdtmc/brp/brp_128-5.pm | 4 +- examples/pdtmc/brp/brp_16_2.pm | 4 +- examples/pdtmc/brp/brp_256-2.pm | 4 +- examples/pdtmc/brp/brp_256-3.pm | 4 +- examples/pdtmc/brp/brp_256-4.pm | 4 +- examples/pdtmc/brp/brp_256-5.pm | 4 +- examples/pdtmc/brp/brp_32-4.pm | 4 +- examples/pdtmc/brp/brp_64-4.pm | 4 +- examples/pdtmc/brp/brp_64-5.pm | 4 +- .../reachability/SparseSccModelChecker.cpp | 125 +++++------ .../reachability/SparseSccModelChecker.h | 2 +- src/stormParametric.cpp | 199 ++++++++++-------- 15 files changed, 209 insertions(+), 165 deletions(-) diff --git a/examples/pdtmc/brp/brp_128-2.pm b/examples/pdtmc/brp/brp_128-2.pm index 0a408fd03..94f893676 100644 --- a/examples/pdtmc/brp/brp_128-2.pm +++ b/examples/pdtmc/brp/brp_128-2.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-3.pm b/examples/pdtmc/brp/brp_128-3.pm index 9c42792b9..dda40ac75 100644 --- a/examples/pdtmc/brp/brp_128-3.pm +++ b/examples/pdtmc/brp/brp_128-3.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-4.pm b/examples/pdtmc/brp/brp_128-4.pm index c71199649..001df7ce4 100644 --- a/examples/pdtmc/brp/brp_128-4.pm +++ b/examples/pdtmc/brp/brp_128-4.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-5.pm b/examples/pdtmc/brp/brp_128-5.pm index 962953a09..373ec6d71 100644 --- a/examples/pdtmc/brp/brp_128-5.pm +++ b/examples/pdtmc/brp/brp_128-5.pm @@ -135,4 +135,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_16_2.pm b/examples/pdtmc/brp/brp_16_2.pm index 7be6c8130..3b478303d 100644 --- a/examples/pdtmc/brp/brp_16_2.pm +++ b/examples/pdtmc/brp/brp_16_2.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s=5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-2.pm b/examples/pdtmc/brp/brp_256-2.pm index 2e0780909..3eeb36040 100644 --- a/examples/pdtmc/brp/brp_256-2.pm +++ b/examples/pdtmc/brp/brp_256-2.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-3.pm b/examples/pdtmc/brp/brp_256-3.pm index 5b62bc35e..4b4a2dd9d 100644 --- a/examples/pdtmc/brp/brp_256-3.pm +++ b/examples/pdtmc/brp/brp_256-3.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-4.pm b/examples/pdtmc/brp/brp_256-4.pm index d0300b04e..6c7dd7553 100644 --- a/examples/pdtmc/brp/brp_256-4.pm +++ b/examples/pdtmc/brp/brp_256-4.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-5.pm b/examples/pdtmc/brp/brp_256-5.pm index 456d710a0..cbcb4a6e1 100644 --- a/examples/pdtmc/brp/brp_256-5.pm +++ b/examples/pdtmc/brp/brp_256-5.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s = 5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_32-4.pm b/examples/pdtmc/brp/brp_32-4.pm index c12c5f783..0bba62c8a 100644 --- a/examples/pdtmc/brp/brp_32-4.pm +++ b/examples/pdtmc/brp/brp_32-4.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s=5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_64-4.pm b/examples/pdtmc/brp/brp_64-4.pm index 230c5754b..df8641eb3 100644 --- a/examples/pdtmc/brp/brp_64-4.pm +++ b/examples/pdtmc/brp/brp_64-4.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s=5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_64-5.pm b/examples/pdtmc/brp/brp_64-5.pm index 564794574..c500d05a8 100644 --- a/examples/pdtmc/brp/brp_64-5.pm +++ b/examples/pdtmc/brp/brp_64-5.pm @@ -134,4 +134,6 @@ module channelL endmodule -label "target" = s=5; \ No newline at end of file +label "target" = s=5; +label "finished_with_success" = srep=3&rrep=3; +label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index c8c3ce538..e6c88c9e8 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -265,8 +265,8 @@ namespace storm { // Determine the set of initial states of the sub-DTMC. storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates; - // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + // Create a dummy vector for the one-step probabilities. + std::vector oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero()); // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); @@ -303,70 +303,59 @@ namespace storm { } STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); - flexibleMatrix.print(); - - // FIXME: Eliminate backward transitions to initial state. - - // At this point, the initial state has one of the following three scenarios: - // (a) only phi successors - // (b) only psi successors - // (c) phi and psi successors - // - // Case (a): ??? - // Case (b): then we can add the probability of all transitions emanating from the initial state (=: p) - // and then use the regular scheme to compute the probability to reach a phi state (=: q) and then - // compute the result to be q/p. - // Case (c): - - - // Find first occurring representatives. - bool foundPhiRepresentative = false; - storm::storage::sparse::state_type phiRepresentative; - bool foundPsiRepresentative = false; - storm::storage::sparse::state_type psiRepresentative; - for (auto initialState : newInitialStates) { - for (auto const& trans : flexibleMatrix.getRow(initialState)) { - if (!foundPhiRepresentative && phiStates.get(trans.getColumn())) { - foundPhiRepresentative = true; - phiRepresentative = trans.getColumn(); - STORM_LOG_DEBUG("Found phi representative " << phiRepresentative); - } else if (!foundPsiRepresentative && psiStates.get(trans.getColumn())) { - foundPsiRepresentative = true; - psiRepresentative = trans.getColumn(); - STORM_LOG_DEBUG("Found psi representative " << phiRepresentative); + eliminateState(flexibleMatrix, oneStepProbabilities, *newInitialStates.begin(), flexibleBackwardTransitions, missingStateRewards, false); + + // Now eliminate all chains of phi or psi states. + for (auto phiState : phiStates) { + // Only eliminate the state if it has a successor that is not itself. + auto const& currentRow = flexibleMatrix.getRow(phiState); + if (currentRow.size() == 1) { + auto const& firstEntry = currentRow.front(); + if (firstEntry.getColumn() == phiState) { + break; } - if (foundPhiRepresentative && foundPsiRepresentative) { + } + eliminateState(flexibleMatrix, oneStepProbabilities, phiState, flexibleBackwardTransitions, missingStateRewards, false, true, phiStates); + } + for (auto psiState : psiStates) { + // Only eliminate the state if it has a successor that is not itself. + auto const& currentRow = flexibleMatrix.getRow(psiState); + if (currentRow.size() == 1) { + auto const& firstEntry = currentRow.front(); + if (firstEntry.getColumn() == psiState) { break; } } + eliminateState(flexibleMatrix, oneStepProbabilities, psiState, flexibleBackwardTransitions, missingStateRewards, false, true, psiStates); } - STORM_LOG_THROW(foundPhiRepresentative, storm::exceptions::InvalidStateException, "Found no phi representative."); - STORM_LOG_THROW(foundPsiRepresentative, storm::exceptions::InvalidStateException, "Found no psi representative."); - - // Redirect all transitions to the phi states to their representative and do the same for the psi states. - for (auto state : maybeStates) { - std::map newSuccessors; - for (auto const& trans : submatrix.getRow(state)) { - if (phiStates.get(trans.getColumn())) { - newSuccessors[phiRepresentative] += trans.getValue(); - } else if (psiStates.get(trans.getColumn())) { - newSuccessors[psiRepresentative] += trans.getValue(); - } else { - newSuccessors[trans.getColumn()] += trans.getValue(); + ValueType numerator = storm::utility::zero(); + ValueType denominator = storm::utility::zero(); + + for (auto const& trans1 : flexibleMatrix.getRow(*newInitialStates.begin())) { + auto initialStateSuccessor = trans1.getColumn(); + if (phiStates.get(initialStateSuccessor)) { + ValueType additiveTerm = storm::utility::zero(); + for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) { + STORM_LOG_ASSERT(psiStates.get(trans2.getColumn()), "Expected psi state."); + additiveTerm += trans2.getValue(); } + additiveTerm *= trans1.getValue(); + numerator += additiveTerm; + denominator += additiveTerm; + } else { + STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state."); + denominator += trans1.getValue(); + ValueType additiveTerm = storm::utility::zero(); + for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) { + STORM_LOG_ASSERT(phiStates.get(trans2.getColumn()), "Expected phi state."); + additiveTerm += trans2.getValue(); + } + numerator += trans1.getValue() * additiveTerm; } - - std::vector> newTransitions; - for (auto const& stateValuePair : newSuccessors) { - newTransitions.emplace_back(stateValuePair); - } - flexibleMatrix.getRow(state) = newTransitions; } - flexibleMatrix.print(); - - return storm::utility::zero(); + return numerator / denominator; } template @@ -533,7 +522,7 @@ namespace storm { } template - void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards) { + void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { auto eliminationStart = std::chrono::high_resolution_clock::now(); ++counter; @@ -591,6 +580,11 @@ namespace storm { continue; } + // Skip the state if the elimination is constrained, but the predecessor is not in the constraint. + if (constrained && !predecessorConstraint.get(predecessor)) { + continue; + } + // First, find the probability with which the predecessor can move to the current state, because // the other probabilities need to be scaled with this factor. typename FlexibleSparseMatrix::row_type& predecessorForwardTransitions = matrix.getRow(predecessor); @@ -713,11 +707,18 @@ namespace storm { } STORM_LOG_DEBUG("Fixed predecessor lists of successor states."); - // Clear the eliminated row to reduce memory consumption. - currentStateSuccessors.clear(); - currentStateSuccessors.shrink_to_fit(); - currentStatePredecessors.clear(); - currentStatePredecessors.shrink_to_fit(); + if (removeForwardTransitions) { + // Clear the eliminated row to reduce memory consumption. + currentStateSuccessors.clear(); + currentStateSuccessors.shrink_to_fit(); + } + if (!constrained) { + // FIXME: is this safe? If the elimination is constrained, we might have to repair the predecessor + // relation. + currentStatePredecessors.clear(); + currentStatePredecessors.shrink_to_fit(); + } + auto eliminationEnd = std::chrono::high_resolution_clock::now(); auto eliminationTime = eliminationEnd - eliminationStart; diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index fbb0dd99c..ce6ef18a8 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -49,7 +49,7 @@ namespace storm { static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); - static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards); + static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector()); static std::vector getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities); }; diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 0f8bbaa21..a3940e8c5 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -123,6 +123,100 @@ // return std::make_tuple(modelchecker.computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances),submatrix, oneStepProbabilities, newInitialStates, threshold, strict); //} +template +void printApproximateResult(ValueType const& value) { + // Intentionally left empty. +} + +template<> +void printApproximateResult(storm::RationalFunction const& value) { + if (value.isConstant()) { + STORM_PRINT_AND_LOG(" (approximately " << std::setprecision(30) << carl::toDouble(value.constantPart()) << ")" << std::endl); + } +} + +template +void check() { + // From this point on we are ready to carry out the actual computations. + // Program Translation Time Measurement, Start + std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now(); + + // First, we build the model using the given symbolic model description and constant definitions. + std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename(); + std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); + storm::prism::Program program = storm::parser::PrismParser::parse(programFile); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, true, false, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? storm::settings::generalSettings().getSymbolicRewardModelName() : "", constants); + + model->printModelInformationToStream(std::cout); + + // Program Translation Time Measurement, End + std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Parsing and translating the model took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; + + std::shared_ptr> dtmc = model->template as>(); + + STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); + std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); + std::cout << "Checking formula " << *filterFormula << std::endl; + + bool checkRewards = false; + std::shared_ptr> phiStateFormulaApFormula = nullptr; + std::shared_ptr> psiStateFormulaApFormula = nullptr; + + // The first thing we need to do is to make sure the formula is of the correct form. + std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); + std::shared_ptr> phiStateFormula; + std::shared_ptr> psiStateFormula; + if (untilFormula) { + phiStateFormula = untilFormula->getLeft(); + psiStateFormula = untilFormula->getRight(); + } else { + std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); + if (eventuallyFormula) { + + phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); + psiStateFormula = eventuallyFormula->getChild(); + } else { + std::shared_ptr> reachabilityRewardFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); + + STORM_LOG_THROW(reachabilityRewardFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties (probabilities/rewards) are admitted."); + phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); + psiStateFormula = reachabilityRewardFormula->getChild(); + checkRewards = true; + } + } + + // Now we need to make sure the formulas defining the phi and psi states are just labels. + phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); + psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); + STORM_LOG_THROW(phiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); + STORM_LOG_THROW(psiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); + + // Perform bisimulation minimization if requested. + if (storm::settings::generalSettings().isBisimulationSet()) { + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); + dtmc = bisimulationDecomposition.getQuotient()->template as>(); + + dtmc->printModelInformationToStream(std::cout); + } + + assert(dtmc); + +// storm::modelchecker::reachability::CollectConstraints constraintCollector; +// constraintCollector(*dtmc); + + storm::modelchecker::reachability::SparseSccModelChecker modelchecker; + + ValueType valueFunction = modelchecker.computeConditionalProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); + + // storm::RationalFunction valueFunction = checkRewards ? modelchecker.computeReachabilityReward(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula) : modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); + + STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl); + if (std::is_same::value) { + printApproximateResult(valueFunction); + } +} + /*! * Main entry point of the executable storm. */ @@ -135,84 +229,8 @@ int main(const int argc, const char** argv) { return -1; } - // From this point on we are ready to carry out the actual computations. - // Program Translation Time Measurement, Start - std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now(); - - // First, we build the model using the given symbolic model description and constant definitions. - std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename(); - std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); - storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, true, false, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? storm::settings::generalSettings().getSymbolicRewardModelName() : "", constants); - - model->printModelInformationToStream(std::cout); - - // Program Translation Time Measurement, End - std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); - std::cout << "Parsing and translating the model took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; - - std::shared_ptr> dtmc = model->as>(); - - STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); - std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); - std::cout << "Checking formula " << *filterFormula << std::endl; - - bool checkRewards = false; - std::shared_ptr> phiStateFormulaApFormula = nullptr; - std::shared_ptr> psiStateFormulaApFormula = nullptr; - - // The first thing we need to do is to make sure the formula is of the correct form. - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - std::shared_ptr> phiStateFormula; - std::shared_ptr> psiStateFormula; - if (untilFormula) { - phiStateFormula = untilFormula->getLeft(); - psiStateFormula = untilFormula->getRight(); - } else { - std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - if (eventuallyFormula) { - - phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); - psiStateFormula = eventuallyFormula->getChild(); - } else { - std::shared_ptr> reachabilityRewardFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - - STORM_LOG_THROW(reachabilityRewardFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties (probabilities/rewards) are admitted."); - phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); - psiStateFormula = reachabilityRewardFormula->getChild(); - checkRewards = true; - } - } - - // Now we need to make sure the formulas defining the phi and psi states are just labels. - phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); - psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); - STORM_LOG_THROW(phiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - STORM_LOG_THROW(psiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - - // Perform bisimulation minimization if requested. - if (storm::settings::generalSettings().isBisimulationSet()) { - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); - dtmc = bisimulationDecomposition.getQuotient()->as>(); - - dtmc->printModelInformationToStream(std::cout); - } - - assert(dtmc); - storm::modelchecker::reachability::CollectConstraints constraintCollector; - constraintCollector(*dtmc); - - storm::modelchecker::reachability::SparseSccModelChecker modelchecker; + check(); - storm::RationalFunction valueFunction = modelchecker.computeConditionalProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); - -// storm::RationalFunction valueFunction = checkRewards ? modelchecker.computeReachabilityReward(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula) : modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); - - -// STORM_PRINT_AND_LOG(std::endl << "Result: (" << carl::computePolynomial(valueFunction.nominator()) << ") / (" << carl::computePolynomial(valueFunction.denominator()) << ")" << std::endl); -// STORM_PRINT_AND_LOG(std::endl << "Result: (" << valueFunction.nominator() << ") / (" << valueFunction.denominator() << ")" << std::endl); - STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl); - // // Perform bisimulation minimization if requested. // if (storm::settings::generalSettings().isBisimulationSet()) { // storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); @@ -228,22 +246,23 @@ int main(const int argc, const char** argv) { // STORM_PRINT_AND_LOG(std::endl << "difference: " << diff << std::endl); // Get variables from parameter definitions in prism program. - std::set parameters; - for(auto constant : program.getConstants()) - { - if(!constant.isDefined()) - { - carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); - assert(p != storm::Variable::NO_VARIABLE); - parameters.insert(p); - } - } +// std::set parameters; +// for(auto constant : program.getConstants()) +// { +// if(!constant.isDefined()) +// { +// std::cout << "got undef constant " << constant.getName() << std::endl; +// carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); +// assert(p != storm::Variable::NO_VARIABLE); +// parameters.insert(p); +// } +// } // STORM_LOG_ASSERT(parameters == valueFunction.gatherVariables(), "Parameters in result and program definition do not coincide."); - if(storm::settings::parametricSettings().exportResultToFile()) { - storm::utility::exportParametricMcResult(valueFunction, constraintCollector); - } +// if(storm::settings::parametricSettings().exportResultToFile()) { +// storm::utility::exportParametricMcResult(valueFunction, constraintCollector); +// } // if (storm::settings::parametricSettings().exportToSmt2File() && std::get<1>(result) && std::get<2>(result) && std::get<3>(result) && std::get<4>(result) && std::get<5>(result)) { // storm::modelchecker::reachability::DirectEncoding dec;