@ -1,40 +1,35 @@
# include <queue>
# include "NonMarkovianChainTransformer.h"
# include "storm/logic/Formulas.h"
# include "storm/logic/FragmentSpecification.h"
# include <queue>
# 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 <storm/solver/stateelimination/NondeterministicModelStateEliminator.h>
# 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 < typename ValueType , typename RewardModelType >
std : : shared_ptr < models : : sparse : : Model < ValueType , RewardModelType > >
NonMarkovianChainTransformer < ValueType , RewardModelType > : : eliminateNonmarkovianStates (
std : : shared_ptr < models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > > ma ,
EliminationLabelBehavior labelBehavior ) {
// TODO reward models
NonMarkovianChainTransformer < ValueType , RewardModelType > : : eliminateNonmarkovianStates ( std : : shared_ptr < models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > > 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 < ValueType , RewardModelType > 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 < ValueType , RewardModelType > 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 < storm : : models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > > (
std : : move ( components ) ) ;
return std : : make_shared < storm : : models : : sparse : : Ctmc < ValueType , RewardModelType > > ( std : : move ( components ) ) ;
}
std : : map < uint_fast64_t , uint_fast64_t > eliminationMapping ;
std : : set < uint_fast64_t > statesToKeep ;
std : : queue < uint_fast64_t > changedStates ;
std : : queue < uint_fast64_t > queue ;
storm : : storage : : SparseMatrix < ValueType > backwards = ma - > getBackwardTransitions ( ) ;
// Initialize
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleMatrix ( ma - > getTransitionMatrix ( ) ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > 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 < std : : string , RewardModelType > 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 < ValueType > ( ma - > getTransitionMatrix ( ) . getRowCount ( ) , storm : : utility : : zero < ValueType > ( ) ) ;
storm : : solver : : stateelimination : : NondeterministicModelStateEliminator < ValueType > 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 < ValueType > : : 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 < ValueType > : : 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 < ValueType > : : 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 < ValueType > : : 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 < std : : set < std : : string > > labelMap ( newStateCount , std : : set < std : : string > ( ) ) ;
// Construct a mapping of old state space to new one
std : : vector < uint_fast64_t > 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 < ValueType > newTransitionMatrix ;
storm : : models : : sparse : : StateLabeling newStateLabeling ( newStateCount ) ;
storm : : storage : : BitVector newMarkovianStates ( ma - > getNumberOfStates ( ) - eliminationMapping . size ( ) , false ) ;
std : : vector < ValueType > newExitRates ;
//TODO choice labeling
boost : : optional < storm : : models : : sparse : : ChoiceLabeling > newChoiceLabeling ;
// Create the new matrix
auto keptRows = ma - > getTransitionMatrix ( ) . getRowFilter ( keepStates ) ;
storm : : storage : : SparseMatrix < ValueType > matrix = flexibleMatrix . createSparseMatrix ( keptRows , keepStates ) ;
// Initialize the matrix builder and helper variables
storm : : storage : : SparseMatrixBuilder < ValueType > matrixBuilder = storm : : storage : : SparseMatrixBuilder < ValueType > (
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 < ValueType , RewardModelType > components ( matrix , labeling , ma - > getRewardModels ( ) , false , markovianStates ) ;
std : : vector < ValueType > exitRates ( markovianStates . size ( ) ) ;
storm : : utility : : vector : : selectVectorValues ( exitRates , keepStates , ma - > getExitRates ( ) ) ;
components . exitRates = exitRates ;
std : : set < std : : string > 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 < std : : map < uint_fast64_t , ValueType > > rowSet ;
for ( uint_fast64_t row = 0 ; row < ma - > getTransitionMatrix ( ) . getRowGroupSize ( state ) ; + + row ) {
std : : map < uint_fast64_t , ValueType > transitions ;
for ( typename storm : : storage : : SparseMatrix < ValueType > : : 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 < ValueType > ( ) ;
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 < ValueType , RewardModelType > newComponents = storm : : storage : : sparse : : ModelComponents < ValueType , RewardModelType > (
std : : move ( newTransitionMatrix ) , std : : move ( newStateLabeling ) ) ;
newComponents . rateTransitions = false ;
newComponents . markovianStates = std : : move ( newMarkovianStates ) ;
newComponents . exitRates = std : : move ( newExitRates ) ;
auto model = std : : make_shared < storm : : models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > > (
std : : move ( newComponents ) ) ;
// Build transformed model
auto model = std : : make_shared < storm : : models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > > ( std : : move ( components ) ) ;
if ( model - > isConvertibleToCtmc ( ) ) {
return model - > convertToCtmc ( ) ;
} else {
@ -290,50 +140,49 @@ namespace storm {
}
template < typename ValueType , typename RewardModelType >
bool NonMarkovianChainTransformer < ValueType , RewardModelType > : : preservesFormula (
storm : : logic : : Formula const & formula ) {
bool NonMarkovianChainTransformer < ValueType , RewardModelType > : : 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 < typename ValueType , typename RewardModelType >
std : : vector < std : : shared_ptr < storm : : logic : : Formula const > >
NonMarkovianChainTransformer < ValueType , RewardModelType > : : checkAndTransformFormulas (
std : : vector < std : : shared_ptr < storm : : logic : : Formula const > > const & formulas ) {
NonMarkovianChainTransformer < ValueType , RewardModelType > : : checkAndTransformFormulas ( std : : vector < std : : shared_ptr < storm : : logic : : Formula const > > const & formulas ) {
std : : vector < std : : shared_ptr < storm : : logic : : Formula const > > 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 < double > ;
template class NonMarkovianChainTransformer < double > ;
template
class NonMarkovianChainTransformer < double , storm : : models : : sparse : : StandardRewardModel < storm : : Interval > > ;
# ifdef STORM_HAVE_CARL
template class NonMarkovianChainTransformer < double , storm : : models : : sparse : : StandardRewardModel < storm : : Interval > > ;
template
class NonMarkovianChainTransformer < storm : : RationalFunction > ;
# ifdef STORM_HAVE_CARL
template class NonMarkovianChainTransformer < storm : : RationalFunction > ;
template
class NonMarkovianChainTransformer < storm : : RationalNumber > ;
template class NonMarkovianChainTransformer < storm : : RationalNumber > ;
# endif
}
}
Matthias Volk
5 years ago
xxxxxxxxxx