Browse Source

some refactoring in an attempt to make the state-elimination procedure flexible and readable at the same time

Former-commit-id: 9cbdd21672
tempestpy_adaptions
dehnert 9 years ago
parent
commit
cd8fd76520
  1. 282
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 26
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

282
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

HTTP/1.1 200 OK Content-Type: text/html; charset=UTF-8 Set-Cookie: macaron_flash=; Path=/; Max-Age=0; HttpOnly; SameSite=Lax X-Frame-Options: SAMEORIGIN Date: Sat, 23 Nov 2024 20:29:33 GMT Transfer-Encoding: chunked 3aa72 sp/tempest - resources/3rdparty/stlsoft-1.9.116/include/winstl/time/format_functions.hpp at 6f970f27fe7215529df4cfae69c3da74a3b42a6d - tempest - Gitea: Git with a cup of tea
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 

521 lines
18 KiB

@ -120,6 +120,169 @@ namespace storm {
return false;
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
uint_fast64_t numberOfStates = transitionMatrix.getRowCount();
if (psiStates.empty()) {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>())));
}
if (psiStates.full()) {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::vector<ValueType>(numberOfStates, storm::utility::one<ValueType>())));
}
storm::storage::BitVector const& initialStates = this->getModel().getInitialStates();
STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = this->getModel().getBackwardTransitions();
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), psiStates);
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
// Determine whether we need to perform some further computation.
bool furtherComputationNeeded = true;
if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) {
STORM_LOG_DEBUG("The long-run probability for all initial states was found in a preprocessing step.");
furtherComputationNeeded = false;
}
if (maybeStates.empty()) {
STORM_LOG_DEBUG("The long-run probability for all states was found in a preprocessing step.");
furtherComputationNeeded = false;
}
if (furtherComputationNeeded) {
// Start by decomposing the DTMC into its BSCCs.
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true);
storm::storage::BitVector statesInRelevantBsccs(maybeStates.size());
for (auto const& scc : bsccDecomposition) {
// Since all states in an SCC can reach all other states, we only need to check whether an arbitrary
// state is a maybe state.
if (maybeStates.get(*scc.begin())) {
for (auto const& state : scc) {
statesInRelevantBsccs.set(state, true);
}
}
}
// Determine the set of initial states of the sub-model.
storm::storage::BitVector newInitialStates = initialStates % maybeStates;
storm::storage::BitVector newPsiStates = psiStates % maybeStates;
storm::storage::BitVector newStatesInRelevantBsccs = statesInRelevantBsccs % maybeStates;
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates);
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
std::vector<ValueType> stateValues(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(stateValues, newPsiStates, storm::utility::one<ValueType>());
std::vector<ValueType> subresult = computeLongRunValues(submatrix, submatrixTransposed, newInitialStates, newStatesInRelevantBsccs, computeResultsForInitialStatesOnly, stateValues);
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, subresult);
}
// Construct check result based on whether we have computed values for all states or just the initial states.
std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
if (computeResultsForInitialStatesOnly) {
// If we computed the results for the initial states only, we need to filter the result to only
// communicate these results.
checkResult->filter(ExplicitQualitativeCheckResult(initialStates));
}
return checkResult;
}
template<typename SparseDtmcModelType>
std::vector<typename SparseDtmcEliminationModelChecker<SparseDtmcModelType>::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& statesInBsccs, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& stateValues) {
// std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
//
// std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
// // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
// FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix);
// FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions);
// auto conversionEnd = std::chrono::high_resolution_clock::now();
//
// std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
//
// storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder();
// boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
// if (eliminationOrderNeedsDistances(order)) {
// distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, stateValues,
// eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order));
// }
//
// // Compute the average time to stay in each state for all states in BSCCs.
// boost::optional<std::vector<ValueType>> averageTimeInStates = std::vector<ValueType>(stateValues.size(), storm::utility::zero<ValueType>());
// for (auto state : statesInBsccs) {
// for (auto const& entry : transitionMatrix.getRow(state)) {
// bool hasSelfLoop = false;
// if (entry.getColumn() == state) {
// hasSelfLoop = true;
// averageTimeInStates.get()[state] = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - entry.getValue());
// }
// if (!hasSelfLoop) {
// averageTimeInStates.get()[state] = storm::utility::one<ValueType>();
// }
// }
// }
//
// performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, statesInBsccs, initialStates, computeResultsForInitialStatesOnly, stateValues, averageTimeInStates, distanceBasedPriorities);
//
//
//
//
//
//
// // Create a bit vector that represents the subsystem of states we still have to eliminate.
// storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
//
// uint_fast64_t maximalDepth = 0;
// if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) {
// performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities);
// } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
// maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities);
// }
//
// STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated.");
// STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated.");
//
// std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now();
// std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
//
// if (storm::settings::generalSettings().isShowStatisticsSet()) {
// std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart;
// std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(conversionTime);
// std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart;
// std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(modelCheckingTime);
// std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart;
// std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
//
// STORM_PRINT_AND_LOG(std::endl);
// STORM_PRINT_AND_LOG("Time breakdown:" << std::endl);
// STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl);
// STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl);
// STORM_PRINT_AND_LOG("------------------------------------------" << std::endl);
// STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl);
// STORM_PRINT_AND_LOG(std::endl);
// STORM_PRINT_AND_LOG("Other:" << std::endl);
// STORM_PRINT_AND_LOG(" * number of states eliminated: " << transitionMatrix.getRowCount() << std::endl);
// if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
// STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl);
// }
// }
//
// // Now, we return the value for the only initial state.
// STORM_LOG_DEBUG("Simplifying and returning result.");
// for (auto& value : values) {
// value = storm::utility::simplify(value);
// }
/* /////////////////////////////////////////////////////////////////////////
* File: winstl/time/format_functions.hpp
*
* Purpose: Comparison functions for Windows time structures.
*
* Created: 21st November 2003
* Updated: 7th August 2012
*
* Thanks to: Mikael Pahmp, for spotting the failure to handle 24-hour
* time pictures.
*
* Home: http://stlsoft.org/
*
* Copyright (c) 2003-2012, Matthew Wilson and Synesis Software
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* - Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
* - Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
* - Neither the name(s) of Matthew Wilson and Synesis Software nor the names of
* any contributors may be used to endorse or promote products derived from
* this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
* ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
* LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
* CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
* ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
* POSSIBILITY OF SUCH DAMAGE.
*
* ////////////////////////////////////////////////////////////////////// */
/** \file winstl/time/format_functions.hpp
*
* \brief [C, C++] Formatting functions for Windows time types
* (\ref group__library__time "Time" Library).
*/
#ifndef WINSTL_INCL_WINSTL_TIME_HPP_FORMAT_FUNCTIONS
#define WINSTL_INCL_WINSTL_TIME_HPP_FORMAT_FUNCTIONS
#ifndef STLSOFT_DOCUMENTATION_SKIP_SECTION
# define WINSTL_VER_WINSTL_TIME_HPP_FORMAT_FUNCTIONS_MAJOR 5
# define WINSTL_VER_WINSTL_TIME_HPP_FORMAT_FUNCTIONS_MINOR 1
# define WINSTL_VER_WINSTL_TIME_HPP_FORMAT_FUNCTIONS_REVISION 2
# define WINSTL_VER_WINSTL_TIME_HPP_FORMAT_FUNCTIONS_EDIT 62
#endif /* !STLSOFT_DOCUMENTATION_SKIP_SECTION */
/* /////////////////////////////////////////////////////////////////////////
* Includes
*/
#ifndef WINSTL_INCL_WINSTL_H_WINSTL
# include <winstl/winstl.h>
#endif /* !WINSTL_INCL_WINSTL_H_WINSTL */
#ifndef STLSOFT_INCL_STLSOFT_HPP_MEMORY_AUTO_BUFFER
# include <stlsoft/memory/auto_buffer.hpp>
#endif /* !STLSOFT_INCL_STLSOFT_HPP_MEMORY_AUTO_BUFFER */
#ifndef STLSOFT_INCL_STLSOFT_CONVERSION_HPP_INTEGER_TO_STRING
# include <stlsoft/conversion/integer_to_string.hpp>
#endif /* !STLSOFT_INCL_STLSOFT_CONVERSION_HPP_INTEGER_TO_STRING */
#ifndef WINSTL_INCL_WINSTL_MEMORY_HPP_PROCESSHEAP_ALLOCATOR
# include <winstl/memory/processheap_allocator.hpp>
#endif /* !WINSTL_INCL_WINSTL_MEMORY_HPP_PROCESSHEAP_ALLOCATOR */
#ifndef WINSTL_INCL_WINSTL_REGISTRY_HPP_FUNCTIONS
# include <winstl/registry/functions.hpp> // for reg_get_string_value()
#endif /* !WINSTL_INCL_WINSTL_REGISTRY_HPP_FUNCTIONS */
/* /////////////////////////////////////////////////////////////////////////
* Namespace
*/
#ifndef _WINSTL_NO_NAMESPACE
# if defined(_STLSOFT_NO_NAMESPACE) || \
defined(STLSOFT_DOCUMENTATION_SKIP_SECTION)
/* There is no stlsoft namespace, so must define ::winstl */
namespace winstl
{
# else
/* Define stlsoft::winstl_project */
namespace stlsoft
{
namespace winstl_project
{
# endif /* _STLSOFT_NO_NAMESPACE */
#endif /* !_WINSTL_NO_NAMESPACE */
/* /////////////////////////////////////////////////////////////////////////
* Helper classes
*/
#ifndef STLSOFT_DOCUMENTATION_SKIP_SECTION
template <ss_typename_param_k C>
struct time_format_functions_traits;
STLSOFT_TEMPLATE_SPECIALISATION
struct time_format_functions_traits<ws_char_a_t>
{
typedef ws_char_a_t char_type;
static int GetTimeFormat(LCID Locale, DWORD dwFlags, SYSTEMTIME const* lpTime, char_type const* lpFormat, char_type* lpTimeStr, int cchTime)
{
return ::GetTimeFormatA(Locale, dwFlags, lpTime, lpFormat, lpTimeStr, cchTime);
}
static int GetLocaleInfo(LCID Locale, LCTYPE LCType, char_type* lpLCData, int cchData)
{
return ::GetLocaleInfoA(Locale, LCType, lpLCData, cchData);
}
static ss_size_t lstrlen(char_type const* s)
{
return static_cast<ss_size_t>(::lstrlenA(s));
}
static char_type* lstrcpy(char_type* dest, char_type const* src)
{
return ::lstrcpyA(dest, src);
}
};
STLSOFT_TEMPLATE_SPECIALISATION
struct time_format_functions_traits<ws_char_w_t>
{
typedef ws_char_w_t char_type;
static int GetTimeFormat(LCID Locale, DWORD dwFlags, SYSTEMTIME const* lpTime, char_type const* lpFormat, char_type* lpTimeStr, int cchTime)
{
return ::GetTimeFormatW(Locale, dwFlags, lpTime, lpFormat, lpTimeStr, cchTime);
}
static int GetLocaleInfo(LCID Locale, LCTYPE LCType, char_type* lpLCData, int cchData)
{
return ::GetLocaleInfoW(Locale, LCType, lpLCData, cchData);
}
static ss_size_t lstrlen(char_type const* s)
{
return static_cast<ss_size_t>(::lstrlenW(s));
}
static char_type* lstrcpy(char_type* dest, char_type const* src)
{
return ::lstrcpyW(dest, src);
}
};
#endif /* !STLSOFT_DOCUMENTATION_SKIP_SECTION */
/* /////////////////////////////////////////////////////////////////////////
* Functions
*/
template <ss_typename_param_k C>
inline
int
STLSOFT_STDCALL GetTimeFormat_ms_(
LCID locale // locale
, DWORD dwFlags // options
, CONST SYSTEMTIME* lpTime // time
, C const* lpFormat // time format string
, C const* const* timeMarkers // pointer to array of two pointers to time markers
, C* lpTimeStr // formatted string buffer
, int const cchTime // size of string buffer
)
{
typedef C char_t;
typedef time_format_functions_traits<char_t> traits_t;
typedef stlsoft_ns_qual(auto_buffer_old)<
char_t
, processheap_allocator<char_t>
> buffer_t;
if(dwFlags & (TIME_NOMINUTESORSECONDS | TIME_NOSECONDS))
{
return traits_t::GetTimeFormat(locale, dwFlags, lpTime, lpFormat, lpTimeStr, cchTime);
}
if(dwFlags & LOCALE_NOUSEROVERRIDE)
{
locale = LOCALE_SYSTEM_DEFAULT;
}
buffer_t timePicture(1 + ((NULL == lpFormat) ? static_cast<ss_size_t>(::GetLocaleInfoA(locale, LOCALE_STIMEFORMAT, NULL, 0)) : 0));
if(NULL == lpFormat)
{
ss_size_t n = static_cast<ss_size_t>(traits_t::GetLocaleInfo(LOCALE_USER_DEFAULT, LOCALE_STIMEFORMAT, &timePicture[0], static_cast<int>(timePicture.size())));
lpFormat = &timePicture[0];
if(n < timePicture.size())
{
timePicture[n] = static_cast<C>('\0');
}
}
ss_size_t const cchPicture = 1 + traits_t::lstrlen(lpFormat);
// Following need to be front-padded to be forward compatible with STLSoft 1.10 (which uses
// 'safer' i2s functions
char_t hours12_[] = { '\0', '\0', '\0', '0', '0', '\0' }; // "...00"
char_t hours24_[] = { '\0', '\0', '\0', '0', '0', '\0' }; // "...00"
char_t minutes_[] = { '\0', '\0', '\0', '0', '0', '\0' }; // "...00"
char_t seconds_[] = { '\0', '\0', '\0', '0', '0', '.', '0', '0', '0', '\0' }; // "...00.000"
uint16_t const hour12 = (lpTime->wHour > 12) ? uint16_t(lpTime->wHour - 12) : lpTime->wHour;
#if defined(STLSOFT_CF_STATIC_ARRAY_SIZE_DETERMINATION_SUPPORT)
char_t const* hours12 = stlsoft_ns_qual(integer_to_string)(hours12_, hour12);
char_t const* hours24 = stlsoft_ns_qual(integer_to_string)(hours24_, lpTime->wHour);
char_t const* minutes = stlsoft_ns_qual(integer_to_string)(minutes_, lpTime->wMinute);
#else /* ? STLSOFT_CF_STATIC_ARRAY_SIZE_DETERMINATION_SUPPORT */
char_t const* hours12 = stlsoft_ns_qual(integer_to_string)(&hours12_[0], STLSOFT_NUM_ELEMENTS(hours12_), hour12);
char_t const* hours24 = stlsoft_ns_qual(integer_to_string)(&hours24_[0], STLSOFT_NUM_ELEMENTS(hours24_), lpTime->wHour);
char_t const* minutes = stlsoft_ns_qual(integer_to_string)(&minutes_[0], STLSOFT_NUM_ELEMENTS(minutes_), lpTime->wMinute);
#endif /* STLSOFT_CF_STATIC_ARRAY_SIZE_DETERMINATION_SUPPORT */
stlsoft_ns_qual(integer_to_string)(&seconds_[3], STLSOFT_NUM_ELEMENTS(seconds_) - 3, lpTime->wMilliseconds);
char_t const* seconds = stlsoft_ns_qual(integer_to_string)(&seconds_[0], 6, lpTime->wSecond);
seconds_[5] = '.';
// Get the time markers
char_t const* amMarker = (NULL != timeMarkers && NULL != timeMarkers[0])