@ -15,8 +15,6 @@
# include "src/models/Mdp.h"
# include "src/models/Ctmdp.h"
typedef std : : pair < std : : vector < bool > , std : : vector < int_fast64_t > > StateType ;
# include <sstream>
# include "log4cplus/logger.h"
@ -24,12 +22,11 @@ typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType;
extern log4cplus : : Logger logger ;
namespace storm {
namespace adapters {
namespace adapters {
ExplicitModelAdapter : : ExplicitModelAdapter ( storm : : ir : : Program program ) : program ( program ) ,
booleanVariables ( ) , integerVariables ( ) , booleanVariableToIndexMap ( ) , integerVariableToIndexMap ( ) ,
allStates ( ) , stateToIndexMap ( ) , numberOfTransitions ( 0 ) , numberOfChoices ( 0 ) , transitionMap ( ) {
ExplicitModelAdapter : : ExplicitModelAdapter ( storm : : ir : : Program program ) : program ( program ) , booleanVariables ( ) ,
integerVariables ( ) , booleanVariableToIndexMap ( ) , integerVariableToIndexMap ( ) , allStates ( ) , stateToIndexMap ( ) ,
numberOfTransitions ( 0 ) , numberOfChoices ( 0 ) , choiceLabeling ( ) , transitionMap ( ) {
// Get variables from program.
this - > initializeVariables ( ) ;
storm : : settings : : Settings * s = storm : : settings : : Settings : : getInstance ( ) ;
@ -40,8 +37,8 @@ namespace adapters {
this - > clearInternalState ( ) ;
}
std : : shared_ptr < storm : : models : : AbstractModel < double > > ExplicitModelAdapter : : getModel ( std : : string const & rewardModelName ) {
// Initialize rewardM odel.
std : : shared_ptr < storm : : models : : AbstractModel < double > > ExplicitModelAdapter : : getModel ( std : : string const & rewardModelName ) {
// Initialize reward m odel.
this - > rewardModel = nullptr ;
if ( rewardModelName ! = " " ) {
this - > rewardModel = std : : unique_ptr < storm : : ir : : RewardModel > ( new storm : : ir : : RewardModel ( this - > program . getRewardModel ( rewardModelName ) ) ) ;
@ -65,79 +62,79 @@ namespace adapters {
case storm : : ir : : Program : : DTMC :
{
storm : : storage : : SparseMatrix < double > matrix = this - > buildDeterministicMatrix ( ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Dtmc < double > ( matrix , stateLabeling , stateRewards , this - > transitionRewards ) ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Dtmc < double > ( matrix , stateLabeling , stateRewards , this - > transitionRewards , this - > choiceLabeling ) ) ;
break ;
}
case storm : : ir : : Program : : CTMC :
{
storm : : storage : : SparseMatrix < double > matrix = this - > buildDeterministicMatrix ( ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Ctmc < double > ( matrix , stateLabeling , stateRewards , this - > transitionRewards ) ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Ctmc < double > ( matrix , stateLabeling , stateRewards , this - > transitionRewards , this - > choiceLabeling ) ) ;
break ;
}
case storm : : ir : : Program : : MDP :
{
storm : : storage : : SparseMatrix < double > matrix = this - > buildNondeterministicMatrix ( ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Mdp < double > ( matrix , stateLabeling , this - > choiceIndices , stateRewards , this - > transitionRewards ) ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Mdp < double > ( matrix , stateLabeling , this - > choiceIndices , stateRewards , this - > transitionRewards , this - > choiceLabeling ) ) ;
break ;
}
case storm : : ir : : Program : : CTMDP :
{
storm : : storage : : SparseMatrix < double > matrix = this - > buildNondeterministicMatrix ( ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Ctmdp < double > ( matrix , stateLabeling , this - > choiceIndices , stateRewards , this - > transitionRewards ) ) ;
return std : : shared_ptr < storm : : models : : AbstractModel < double > > ( new storm : : models : : Ctmdp < double > ( matrix , stateLabeling , this - > choiceIndices , stateRewards , this - > transitionRewards , this - > choiceLabeling ) ) ;
break ;
}
default :
LOG4CPLUS_ERROR ( logger , " Error while creating model from probabilistic program: We can' t handle this model type. " ) ;
throw storm : : exceptions : : WrongFormatException ( ) < < " Error while creating model from probabilistic program: We can' t handle this model type. " ;
LOG4CPLUS_ERROR ( logger , " Error while creating model from probabilistic program: canno t handle this model type. " ) ;
throw storm : : exceptions : : WrongFormatException ( ) < < " Error while creating model from probabilistic program: canno t handle this model type. " ;
break ;
}
}
void ExplicitModelAdapter : : setValue ( StateType * const state , uint_fast64_t const index , bool const value ) {
void ExplicitModelAdapter : : setValue ( StateType * state , uint_fast64_t index , bool value ) {
std : : get < 0 > ( * state ) [ index ] = value ;
}
void ExplicitModelAdapter : : setValue ( StateType * const state , uint_fast64_t const index , int_fast64_t cons t value ) {
void ExplicitModelAdapter : : setValue ( StateType * state , uint_fast64_t index , int_fast64_t value ) {
std : : get < 1 > ( * state ) [ index ] = value ;
}
std : : string ExplicitModelAdapter : : toString ( StateType const * const state ) {
std : : string ExplicitModelAdapter : : toString ( StateType const * state ) {
std : : stringstream ss ;
for ( unsigned int i = 0 ; i < state - > first . size ( ) ; i + + ) ss < < state - > first [ i ] < < " \t " ;
for ( unsigned int i = 0 ; i < state - > second . size ( ) ; i + + ) ss < < state - > second [ i ] < < " \t " ;
return ss . str ( ) ;
}
std : : vector < double > ExplicitModelAdapter : : getStateRewards ( std : : vector < storm : : ir : : StateReward > const & rewards ) {
std : : vector < double > results ( this - > allStates . size ( ) ) ;
std : : vector < double > ExplicitModelAdapter : : getStateRewards ( std : : vector < storm : : ir : : StateReward > const & rewards ) {
std : : vector < double > result ( this - > allStates . size ( ) ) ;
for ( uint_fast64_t index = 0 ; index < this - > allStates . size ( ) ; index + + ) {
results [ index ] = 0 ;
for ( auto reward : rewards ) {
result [ index ] = 0 ;
for ( auto const & reward : rewards ) {
// Add this reward to the state if the state is included in the state reward.
if ( reward . getStatePredicate ( ) - > getValueAsBool ( this - > allStates [ index ] ) = = true ) {
results [ index ] + = reward . getRewardValue ( ) - > getValueAsDouble ( this - > allStates [ index ] ) ;
result [ index ] + = reward . getRewardValue ( ) - > getValueAsDouble ( this - > allStates [ index ] ) ;
}
}
}
return results ;
return result ;
}
storm : : models : : AtomicPropositionsLabeling ExplicitModelAdapter : : getStateLabeling ( std : : map < std : : string , std : : shared_ptr < storm : : ir : : expressions : : BaseExpression > > labels ) {
storm : : models : : AtomicPropositionsLabeling results ( this - > allStates . size ( ) , labels . size ( ) + 1 ) ;
// Initialize labeling.
for ( auto it : labels ) {
results . addAtomicProposition ( it . first ) ;
for ( auto const & labelExpressionPair : labels ) {
results . addAtomicProposition ( labelExpressionPair . first ) ;
}
for ( uint_fast64_t index = 0 ; index < this - > allStates . size ( ) ; index + + ) {
for ( auto label : labels ) {
// Add label to state, if guard is true.
if ( label . second - > getValueAsBool ( this - > allStates [ index ] ) ) {
results . addAtomicPropositionToState ( label . first , index ) ;
for ( auto const & labelExpressionPair : labels ) {
// Add label to state, if the corresponding expression is true.
if ( labelExpressionPair . second - > getValueAsBool ( this - > allStates [ index ] ) ) {
results . addAtomicPropositionToState ( labelExpressionPair . first , index ) ;
}
}
}
// Also label the initial state.
// Also label the initial state with the special label "init" .
results . addAtomicProposition ( " init " ) ;
StateType * initialState = this - > getInitialState ( ) ;
uint_fast64_t initialIndex = this - > stateToIndexMap [ initialState ] ;
@ -150,6 +147,7 @@ namespace adapters {
void ExplicitModelAdapter : : initializeVariables ( ) {
uint_fast64_t numberOfIntegerVariables = 0 ;
uint_fast64_t numberOfBooleanVariables = 0 ;
// Count number of variables.
for ( uint_fast64_t i = 0 ; i < program . getNumberOfModules ( ) ; + + i ) {
numberOfIntegerVariables + = program . getModule ( i ) . getNumberOfIntegerVariables ( ) ;
@ -176,59 +174,45 @@ namespace adapters {
}
}
/*!
* Retrieves all active command labeled by some label , ordered by modules .
*
* This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state .
* The result will be a list of lists of commands .
*
* For each module that has appropriately labeled commands , there will be a list .
* If none of these commands is active , this list is empty .
* Note the difference between * no list * and * empty list * : Modules that produce no list are not relevant for this action while an empty list means , that it is not possible to do anything with this label .
* @ param state Current state .
* @ param action Action label .
* @ return Active commands .
*/
std : : unique_ptr < std : : list < std : : list < storm : : ir : : Command > > > ExplicitModelAdapter : : getActiveCommandsByAction ( StateType const * state , std : : string & action ) {
std : : unique_ptr < std : : list < std : : list < storm : : ir : : Command > > > res = std : : unique_ptr < std : : list < std : : list < storm : : ir : : Command > > > ( new std : : list < std : : list < storm : : ir : : Command > > ( ) ) ;
boost : : optional < std : : vector < std : : list < storm : : ir : : Command > > > ExplicitModelAdapter : : getActiveCommandsByAction ( StateType const * state , std : : string const & action ) {
boost : : optional < std : : vector < std : : list < storm : : ir : : Command > > > result ( ( std : : vector < std : : list < storm : : ir : : Command > > ( ) ) ) ;
// Iterate over all modules.
for ( uint_fast64_t i = 0 ; i < this - > program . getNumberOfModules ( ) ; + + i ) {
storm : : ir : : Module const & module = this - > program . getModule ( i ) ;
// If the module has no command labeled with the given action, skip this module.
// If the module has no command labeled with the given action, we can skip this module.
if ( ! module . hasAction ( action ) ) {
continue ;
}
std : : set < uint_fast64_t > const & id s= module . getCommandsByAction ( action ) ;
std : : set < uint_fast64_t > const & commandIndices = module . getCommandsByAction ( action ) ;
std : : list < storm : : ir : : Command > commands ;
// Look up commands by their id. Add, if guard holds.
for ( uint_fast64_t id : ids ) {
storm : : ir : : Command const & cmd = module . getCommand ( id ) ;
if ( cmd . getGuard ( ) - > getValueAsBool ( state ) ) {
commands . push_back ( module . getCommand ( id ) ) ;
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for ( uint_fast64_t commandIndex : commandIndices ) {
storm : : ir : : Command const & command = module . getCommand ( commandIndex ) ;
if ( command . getGuard ( ) - > getValueAsBool ( state ) ) {
commands . push_back ( command ) ;
}
}
// If there was no enabled command although the module has some command with the required action label,
// we must not return anything.
if ( commands . size ( ) = = 0 ) {
return boost : : optional < std : : vector < std : : list < storm : : ir : : Command > > > ( ) ;
}
res - > push_back ( commands ) ;
result . get ( ) . push_back ( std : : move ( commands ) ) ;
}
// Sort the result in the vague hope that having small lists at the beginning will speed up the expanding.
res - > sort ( [ ] ( const std : : list < storm : : ir : : Command > & a , const std : : list < storm : : ir : : Command > & b ) - > bool { return a . size ( ) < b . size ( ) ; } ) ;
return res ;
return result ;
}
/*!
* Apply an update to the given state and return resulting state .
* @ params state Current state .
* @ params update Update to be applied .
* @ return Resulting state .
*/
StateType * ExplicitModelAdapter : : applyUpdate ( StateType const * const state , storm : : ir : : Update const & update ) const {
StateType * ExplicitModelAdapter : : applyUpdate ( StateType const * state , storm : : ir : : Update const & update ) const {
return this - > applyUpdate ( state , state , update ) ;
}
StateType * ExplicitModelAdapter : : applyUpdate ( StateType const * const state , StateType const * const baseState , storm : : ir : : Update const & update ) const {
StateType * ExplicitModelAdapter : : applyUpdate ( StateType const * state , StateType const * baseState , storm : : ir : : Update const & update ) const {
StateType * newState = new StateType ( * state ) ;
for ( auto assignedVariable : update . getBooleanAssignments ( ) ) {
setValue ( newState , this - > booleanVariableToIndexMap . at ( assignedVariable . first ) , assignedVariable . second . getExpression ( ) - > getValueAsBool ( baseState ) ) ;
@ -239,9 +223,6 @@ namespace adapters {
return newState ;
}
/*!
* Generates the initial state .
*/
StateType * ExplicitModelAdapter : : getInitialState ( ) {
StateType * initialState = new StateType ( ) ;
initialState - > first . resize ( this - > booleanVariables . size ( ) ) ;
@ -259,6 +240,7 @@ namespace adapters {
std : : get < 0 > ( * initialState ) [ i ] = initialValue ;
}
}
// Now process integer variables.
for ( uint_fast64_t i = 0 ; i < this - > integerVariables . size ( ) ; + + i ) {
// Check if an initial value was given.
@ -271,74 +253,75 @@ namespace adapters {
std : : get < 1 > ( * initialState ) [ i ] = initialValue ;
}
}
LOG4CPLUS_DEBUG ( logger , " Generated initial state. " ) ;
return initialState ;
}
/*!
* Retrieves the state id of the given state .
* If the state has not been hit yet , it will be added to allStates and given a new id .
* In this case , the pointer must not be deleted , as it is used within allStates .
* If the state is already known , the pointer is deleted and the old state id is returned .
* Hence , the given state pointer should not be used afterwards .
* @ param state Pointer to state , shall not be used afterwards .
* @ returns State id of given state .
*/
uint_fast64_t ExplicitModelAdapter : : getOrAddStateId ( StateType * state ) {
// Check, if we already know this state at all.
uint_fast64_t ExplicitModelAdapter : : getOrAddStateIndex ( StateType * state ) {
// Check, if the state was already registered.
auto indexIt = this - > stateToIndexMap . find ( state ) ;
if ( indexIt = = this - > stateToIndexMap . end ( ) ) {
// No, add to allStates, initialize index .
// The state has not been seen, yet, so add it to the list of all reachable states.
allStates . push_back ( state ) ;
stateToIndexMap [ state ] = allStates . size ( ) - 1 ;
return allStates . size ( ) - 1 ;
stateToIndexMap [ state ] = allStates . size ( ) - 1 ;
return allStates . size ( ) - 1 ;
} else {
// Yes, obtain index and delete state object .
// The state was already encountered. Delete the copy of the old state and return its index.
delete state ;
return indexIt - > second ;
}
}
/*!
* Expands all unlabeled transitions for a given state and adds them to the given list of results .
* @ params state State to be explored .
* @ params res Intermediate transition map .
*/
void ExplicitModelAdapter : : addUnlabeledTransitions ( const uint_fast64_t stateID , std : : list < std : : pair < std : : string , std : : map < uint_fast64_t , double > > > & res ) {
const StateType * state = this - > allStates [ stateID ] ;
void ExplicitModelAdapter : : addUnlabeledTransitions ( uint_fast64_t stateIndex , std : : list < std : : pair < std : : pair < std : : string , std : : list < uint_fast64_t > > , std : : map < uint_fast64_t , double > > > & transitionList ) {
StateType const * state = this - > allStates [ stateIndex ] ;
// Iterate over all modules.
for ( uint_fast64_t i = 0 ; i < program . getNumberOfModules ( ) ; + + i ) {
storm : : ir : : Module const & module = program . getModule ( i ) ;
// Iterate over all commands.
for ( uint_fast64_t j = 0 ; j < module . getNumberOfCommands ( ) ; + + j ) {
storm : : ir : : Command const & command = module . getCommand ( j ) ;
// Only consider unlabeled commands.
if ( command . getActionName ( ) ! = " " ) continue ;
// Omit, if command is not active .
// Skip the command, if it is not enabled .
if ( ! command . getGuard ( ) - > getValueAsBool ( state ) ) continue ;
// Add a new map and get pointer.
res . emplace_back ( ) ;
std : : map < uint_fast64_t , double > * states = & res . back ( ) . second ;
double probSum = 0 ;
// Add a new choice for the state.
transitionList . emplace_back ( ) ;
// Add the index of the current command to the labeling of the choice.
transitionList . back ( ) . first . second . emplace_back ( command . getGlobalIndex ( ) ) ;
// Create an alias for all target states for convenience.
std : : map < uint_fast64_t , double > & targetStates = transitionList . back ( ) . second ;
// Also keep track of the total probability leaving the state.
double probabilitySum = 0 ;
// Iterate over all updates.
// Iterate over all updates of the current command .
for ( uint_fast64_t k = 0 ; k < command . getNumberOfUpdates ( ) ; + + k ) {
// Obtain new state id.
storm : : ir : : Update const & update = command . getUpdate ( k ) ;
uint_fast64_t newStateId = this - > getOrAddStateId ( this - > applyUpdate ( state , update ) ) ;
probSum + = update . getLikelihoodExpression ( ) - > getValueAsDouble ( state ) ;
// Check, if we already know this state, add up probabilities for every state.
auto stateIt = states - > find ( newStateId ) ;
if ( stateIt = = states - > end ( ) ) {
( * states ) [ newStateId ] = update . getLikelihoodExpression ( ) - > getValueAsDouble ( state ) ;
// Obtain target state index.
uint_fast64_t newTargetStateIndex = this - > getOrAddStateIndex ( this - > applyUpdate ( state , update ) ) ;
probabilitySum + = update . getLikelihoodExpression ( ) - > getValueAsDouble ( state ) ;
// Check, if we already saw this state in another update and, if so, add up probabilities.
auto stateIt = targetStates . find ( newTargetStateIndex ) ;
if ( stateIt = = targetStates . end ( ) ) {
targetStates [ newTargetStateIndex ] = update . getLikelihoodExpression ( ) - > getValueAsDouble ( state ) ;
this - > numberOfTransitions + + ;
} else {
( * states ) [ newStateId ] + = update . getLikelihoodExpression ( ) - > getValueAsDouble ( state ) ;
targetStates [ newTargetStateIndex ] + = update . getLikelihoodExpression ( ) - > getValueAsDouble ( state ) ;
}
}
if ( std : : abs ( 1 - probSum ) > this - > precision ) {
if ( std : : abs ( 1 - probabilitySum ) > this - > precision ) {
LOG4CPLUS_ERROR ( logger , " Sum of update probabilities should be one for command: \n \t " < < command . toString ( ) ) ;
throw storm : : exceptions : : WrongFormatException ( ) < < " Sum of update probabilities should be one for command: \n \t " < < command . toString ( ) ;
}
@ -346,144 +329,172 @@ namespace adapters {
}
}
/*!
* Explores reachable state from given state by using labeled transitions .
* Found transitions are stored in given map .
* @ param stateID State to be explored .
* @ param res Intermediate transition map .
*/
void ExplicitModelAdapter : : addLabeledTransitions ( const uint_fast64_t stateID , std : : list < std : : pair < std : : string , std : : map < uint_fast64_t , double > > > & res ) {
// Create a copy of the current state, as we will free intermediate states...
for ( std : : string action : this - > program . getActions ( ) ) {
StateType * state = new StateType ( * this - > allStates [ stateID ] ) ;
std : : unique_ptr < std : : list < std : : list < storm : : ir : : Command > > > cmds = this - > getActiveCommandsByAction ( state , action ) ;
void ExplicitModelAdapter : : addLabeledTransitions ( uint_fast64_t stateIndex , std : : list < std : : pair < std : : pair < std : : string , std : : list < uint_fast64_t > > , std : : map < uint_fast64_t , double > > > & transitionList ) {
for ( std : : string const & action : this - > program . getActions ( ) ) {
StateType * currentState = this - > allStates [ stateIndex ] ;
boost : : optional < std : : vector < std : : list < storm : : ir : : Command > > > optionalActiveCommandLists = this - > getActiveCommandsByAction ( currentState , action ) ;
// Start with current state
std : : unordered_map < StateType * , double , StateHash , StateCompare > resultStates ;
resultStates [ state ] = 1.0 ;
// Only process this action label, if there is at least one feasible solution.
if ( optionalActiveCommandLists ) {
std : : vector < std : : list < storm : : ir : : Command > > const & activeCommandList = optionalActiveCommandLists . get ( ) ;
std : : vector < std : : list < storm : : ir : : Command > : : const_iterator > iteratorList ( activeCommandList . size ( ) ) ;
for ( std : : list < storm : : ir : : Command > module : * cmds ) {
if ( resultStates . size ( ) = = 0 ) break ;
std : : unordered_map < StateType * , double , StateHash , StateCompare > newStates ;
// Initialize the list of iterators.
for ( int i = 0 ; i < activeCommandList . size ( ) ; + + i ) {
iteratorList [ i ] = activeCommandList [ i ] . cbegin ( ) ;
}
// Iterate over all commands within this module.
for ( storm : : ir : : Command command : module ) {
// Iterate over all updates of this command.
double probSum = 0 ;
for ( uint_fast64_t k = 0 ; k < command . getNumberOfUpdates ( ) ; + + k ) {
storm : : ir : : Update const update = command . getUpdate ( k ) ;
// Iterate over all resultStates.
for ( auto it : resultStates ) {
// Apply the new update and get resulting state.
StateType * newState = this - > applyUpdate ( it . first , this - > allStates [ stateID ] , update ) ;
probSum + = it . second * update . getLikelihoodExpression ( ) - > getValueAsDouble ( it . first ) ;
// Insert the new state into newStates array.
// Take care of calculation of likelihood, combine identical states.
auto s = newStates . find ( newState ) ;
if ( s = = newStates . end ( ) ) {
newStates [ newState ] = it . second * update . getLikelihoodExpression ( ) - > getValueAsDouble ( it . first ) ;
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false ;
while ( ! done ) {
std : : unordered_map < StateType * , double , StateHash , StateCompare > * currentTargetStates = new std : : unordered_map < StateType * , double , StateHash , StateCompare > ( ) ;
std : : unordered_map < StateType * , double , StateHash , StateCompare > * newTargetStates = new std : : unordered_map < StateType * , double , StateHash , StateCompare > ( ) ;
( * currentTargetStates ) [ new StateType ( * currentState ) ] = 1.0 ;
double probabilitySum = 0 ;
for ( uint_fast64_t i = 0 ; i < iteratorList . size ( ) ; + + i ) {
storm : : ir : : Command const & command = * iteratorList [ i ] ;
for ( uint_fast64_t j = 0 ; j < command . getNumberOfUpdates ( ) ; + + j ) {
storm : : ir : : Update const & update = command . getUpdate ( j ) ;
for ( auto const & stateProbabilityPair : * currentTargetStates ) {
StateType * newTargetState = this - > applyUpdate ( stateProbabilityPair . first , currentState , update ) ;
probabilitySum + = stateProbabilityPair . second * update . getLikelihoodExpression ( ) - > getValueAsDouble ( currentState ) ;
auto existingStateProbabilityPair = newTargetStates - > find ( newTargetState ) ;
if ( existingStateProbabilityPair = = newTargetStates - > end ( ) ) {
( * newTargetStates ) [ newTargetState ] = stateProbabilityPair . second * update . getLikelihoodExpression ( ) - > getValueAsDouble ( currentState ) ;
} else {
newStates [ newState ] + = it . second * update . getLikelihoodExpression ( ) - > getValueAsDouble ( it . first ) ;
existingStateProbabilityPair - > second + = stateProbabil ityPair . second * update . getLikelihoodExpression ( ) - > getValueAsDouble ( currentState ) ;
}
}
}
if ( std : : abs ( 1 - probSum ) > this - > precision ) {
LOG4CPLUS_ERROR ( logger , " Sum of update probabilities should be one for command: \n \t " < < command . toString ( ) ) ;
throw storm : : exceptions : : WrongFormatException ( ) < < " Sum of update probabilities should be one for command: \n \t " < < command . toString ( ) ;
}
// If there is one more command to come, shift the target states one time step back.
if ( i < iteratorList . size ( ) - 1 ) {
for ( auto const & stateProbabilityPair : * currentTargetStates ) {
delete stateProbabilityPair . first ;
}
for ( auto it : resultStates ) {
delete it . first ;
delete currentTargetStates ;
currentTargetStates = newTargetStates ;
newTargetStates = new std : : unordered_map < StateType * , double , StateHash , StateCompare > ( ) ;
}
// Move new states to resultStates.
resultStates . clear ( ) ;
resultStates . insert ( newStates . begin ( ) , newStates . end ( ) ) ;
}
if ( resultStates . size ( ) > 0 ) {
res . push_back ( std : : make_pair ( action , std : : map < uint_fast64_t , double > ( ) ) ) ;
std : : map < uint_fast64_t , double > * states = & res . back ( ) . second ;
// At this point, we applied all commands of the current command combination and newTargetStates
// contains all target states and their respective probabilities. That means we are now ready to
// add the choice to the list of transitions.
transitionList . emplace_back ( std : : make_pair ( std : : make_pair ( action , std : : list < uint_fast64_t > ( ) ) , std : : map < uint_fast64_t , double > ( ) ) ) ;
// Now add our final result states to our global result.
for ( auto const & it : resultStates ) {
uint_fast64_t newStateID = this - > getOrAddStateId ( it . first ) ;
( * states ) [ newStateID ] = it . second ;
// Add the commands that were involved in creating this distribution to the labeling.
for ( uint_fast64_t i = 0 ; i < iteratorList . size ( ) ; + + i ) {
transitionList . back ( ) . first . second . push_back ( iteratorList [ i ] - > getGlobalIndex ( ) ) ;
}
this - > numberOfTransitions + = states - > size ( ) ;
// Now create the actual distribution.
std : : map < uint_fast64_t , double > & states = transitionList . back ( ) . second ;
for ( auto const & stateProbabilityPair : * newTargetStates ) {
uint_fast64_t newStateIndex = this - > getOrAddStateIndex ( stateProbabilityPair . first ) ;
states [ newStateIndex ] = stateProbabilityPair . second ;
}
this - > numberOfTransitions + = states . size ( ) ;
// Dispose of the temporary maps.
delete currentTargetStates ;
delete newTargetStates ;
// Now, check whether there is one more command combination to consider.
bool movedIterator = false ;
for ( int_fast64_t j = iteratorList . size ( ) - 1 ; j > = 0 ; - - j ) {
+ + iteratorList [ j ] ;
if ( iteratorList [ j ] ! = activeCommandList [ j ] . end ( ) ) {
movedIterator = true ;
} else {
// Reset the iterator to the beginning of the list.
iteratorList [ j ] = activeCommandList [ j ] . begin ( ) ;
}
}
done = ! movedIterator ;
}
}
}
}
/*!
* Create matrix from intermediate mapping , assuming it is a dtmc model .
* @ param intermediate Intermediate representation of transition mapping .
* @ return result matrix .
*/
storm : : storage : : SparseMatrix < double > ExplicitModelAdapter : : buildDeterministicMatrix ( ) {
// ***** ATTENTION *****
// this->numberOfTransitions is meaningless, as we combine all choices into one for each state.
// Hence, we compute the correct number of transitions now.
// Note: this->numberOfTransitions may be meaningless here, as we need to combine all nondeterministic
// choices for all states into one determinstic one, which might reduce the number of transitions.
// Hence, we compute the correct number now.
uint_fast64_t numberOfTransitions = 0 ;
for ( uint_fast64_t state = 0 ; state < this - > allStates . size ( ) ; state + + ) {
// Collect all target nodes in a set to get number of distinct nodes.
for ( uint_fast64_t state = 0 ; state < this - > allStates . size ( ) ; + + state ) {
// Collect all target nodes in a set to get the number of distinct nodes.
std : : set < uint_fast64_t > set ;
for ( auto choice : transitionMap [ state ] ) {
for ( auto elem : choice . second ) {
set . insert ( elem . first ) ;
for ( auto const & choice : transitionMap [ state ] ) {
for ( auto const & targetStates : choice . second ) {
set . insert ( targetStates . first ) ;
}
}
numberOfTransitions + = set . size ( ) ;
}
LOG4CPLUS_INFO ( logger , " Building deterministic transition matrix: " < < allStates . size ( ) < < " x " < < allStates . size ( ) < < " with " < < numberOfTransitions < < " transitions. " ) ;
// Now build matrix.
this - > choiceLabeling . clear ( ) ;
this - > choiceLabeling . reserve ( allStates . size ( ) ) ;
// Now build the actual matrix.
storm : : storage : : SparseMatrix < double > result ( allStates . size ( ) ) ;
result . initialize ( numberOfTransitions ) ;
if ( ( this - > rewardModel ! = nullptr ) & & ( this - > rewardModel - > hasTransitionRewards ( ) ) ) {
this - > transitionRewards . reset ( std : : move ( storm : : storage : : SparseMatrix < double > ( allStates . size ( ) ) ) ) ;
this - > transitionRewards . get ( ) . initialize ( numberOfTransitions ) ;
}
for ( uint_fast64_t state = 0 ; state < this - > allStates . size ( ) ; state + + ) {
if ( transitionMap [ state ] . size ( ) > 1 ) {
LOG4CPLUS_WARN ( logger , " State " < < state < < " has " < < transitionMap [ state ] . size ( ) < < " overlapping guards in deterministic model. " ) ;
}
// Combine choices to one map.
// Combine nondeterministic choices into one by weighting them equally.
std : : map < uint_fast64_t , double > map ;
std : : map < uint_fast64_t , double > rewardMap ;
for ( auto choice : transitionMap [ state ] ) {
for ( auto elem : choice . second ) {
map [ elem . first ] + = elem . second ;
std : : list < uint_fast64_t > commandList ;
for ( auto const & choice : transitionMap [ state ] ) {
commandList . insert ( commandList . end ( ) , choice . first . second . begin ( ) , choice . first . second . end ( ) ) ;
for ( auto const & targetStates : choice . second ) {
map [ targetStates . first ] + = targetStates . second ;
if ( ( this - > rewardModel ! = nullptr ) & & ( this - > rewardModel - > hasTransitionRewards ( ) ) ) {
for ( auto reward : this - > rewardModel - > getTransitionRewards ( ) ) {
for ( auto const & reward : this - > rewardModel - > getTransitionRewards ( ) ) {
if ( reward . getStatePredicate ( ) - > getValueAsBool ( this - > allStates [ state ] ) = = true ) {
rewardMap [ elem . first ] + = reward . getRewardValue ( ) - > getValueAsDouble ( this - > allStates [ state ] ) ;
rewardMap [ targetStates . first ] + = reward . getRewardValue ( ) - > getValueAsDouble ( this - > allStates [ state ] ) ;
}
}
}
}
}
// Make sure that each command is only added once to the label of the transition.
commandList . sort ( ) ;
commandList . unique ( ) ;
// Add the labeling for the behaviour of the current state.
this - > choiceLabeling . emplace_back ( std : : move ( commandList ) ) ;
// Scale probabilities by number of choices.
double factor = 1.0 / transitionMap [ state ] . size ( ) ;
for ( auto it : map ) {
result . addNextValue ( state , it . first , it . second * factor ) ;
for ( auto & targetStates : map ) {
result . addNextValue ( state , targetStates . first , targetStates . second * factor ) ;
if ( ( this - > rewardModel ! = nullptr ) & & ( this - > rewardModel - > hasTransitionRewards ( ) ) ) {
this - > transitionRewards . get ( ) . addNextValue ( state , it . first , rewardMap [ it . first ] * factor ) ;
this - > transitionRewards . get ( ) . addNextValue ( state , targetStates . first , rewardMap [ targetStates . first ] * factor ) ;
}
}
}
result . finalize ( ) ;
return result ;
}
/*!
* Create matrix from intermediate mapping , assuming it is a mdp model .
* @ param intermediate Intermediate representation of transition mapping .
* @ param choices Overall number of choices for all nodes .
* @ return result matrix .
*/
storm : : storage : : SparseMatrix < double > ExplicitModelAdapter : : buildNondeterministicMatrix ( ) {
LOG4CPLUS_INFO ( logger , " Building nondeterministic transition matrix: " < < this - > numberOfChoices < < " x " < < allStates . size ( ) < < " with " < < this - > numberOfTransitions < < " transitions. " ) ;
storm : : storage : : SparseMatrix < double > result ( this - > numberOfChoices , allStates . size ( ) ) ;
@ -493,63 +504,64 @@ namespace adapters {
this - > transitionRewards . get ( ) . initialize ( this - > numberOfTransitions ) ;
}
this - > choiceIndices . clear ( ) ;
this - > choiceIndices . reserve ( allStates . size ( ) ) ;
// Build matrix.
this - > choiceIndices . reserve ( allStates . size ( ) + 1 ) ;
this - > choiceLabeling . clear ( ) ;
this - > choiceLabeling . reserve ( allStates . size ( ) ) ;
// Now build the actual matrix.
uint_fast64_t nextRow = 0 ;
this - > choiceIndices . push_back ( 0 ) ;
for ( uint_fast64_t state = 0 ; state < this - > allStates . size ( ) ; state + + ) {
this - > choiceIndices . push_back ( transitionMap [ state ] . size ( ) ) ;
for ( auto choice : transitionMap [ state ] ) {
for ( auto it : choice . second ) {
result . addNextValue ( nextRow , it . first , it . second ) ;
this - > choiceIndices . push_back ( this - > choiceIndices [ state ] + transitionMap [ state ] . size ( ) ) ;
for ( auto const & choice : transitionMap [ state ] ) {
this - > choiceLabeling . emplace_back ( std : : move ( choice . first . second ) ) ;
for ( auto const & targetStates : choice . second ) {
result . addNextValue ( nextRow , targetStates . first , targetStates . second ) ;
if ( ( this - > rewardModel ! = nullptr ) & & ( this - > rewardModel - > hasTransitionRewards ( ) ) ) {
double rewardValue = 0 ;
for ( auto reward : this - > rewardModel - > getTransitionRewards ( ) ) {
for ( auto const & reward : this - > rewardModel - > getTransitionRewards ( ) ) {
if ( reward . getStatePredicate ( ) - > getValueAsBool ( this - > allStates [ state ] ) = = true ) {
rewardValue = reward . getRewardValue ( ) - > getValueAsDouble ( this - > allStates [ state ] ) ;
}
}
this - > transitionRewards . get ( ) . addNextValue ( nextRow , it . first , rewardValue ) ;
this - > transitionRewards . get ( ) . addNextValue ( nextRow , targetStates . first , rewardValue ) ;
}
}
nextRow + + ;
+ + nextRow ;
}
}
result . finalize ( ) ;
return result ;
}
/*!
* Build matrix from model . Starts with all initial states and explores the reachable state space .
* While exploring , the transitions are stored in a temporary map .
* Afterwards , we transform this map into the actual matrix .
* @ return result matrix .
*/
void ExplicitModelAdapter : : buildTransitionMap ( ) {
LOG4CPLUS_DEBUG ( logger , " Starting to create transition map from program.. ." ) ;
LOG4CPLUS_DEBUG ( logger , " Creating transition map from program. " ) ;
this - > clearInternalState ( ) ;
this - > allStates . clear ( ) ;
this - > allStates . push_back ( this - > getInitialState ( ) ) ;
stateToIndexMap [ this - > allStates [ 0 ] ] = 0 ;
for ( uint_fast64_t curIndex = 0 ; curIndex < this - > allStates . size ( ) ; curIndex + + )
{
this - > addUnlabeledTransitions ( curIndex , this - > transitionMap [ curIndex ] ) ;
this - > addLabeledTransitions ( curIndex , this - > transitionMap [ curIndex ] ) ;
for ( uint_fast64_t state = 0 ; state < this - > allStates . size ( ) ; + + state ) {
this - > addUnlabeledTransitions ( state , this - > transitionMap [ state ] ) ;
this - > addLabeledTransitions ( state , this - > transitionMap [ state ] ) ;
this - > numberOfChoices + = this - > transitionMap [ state ] . size ( ) ;
this - > numberOfChoices + = this - > transitionMap [ curIndex ] . size ( ) ;
if ( this - > transitionMap [ curIndex ] . size ( ) = = 0 ) {
// This is a deadlock state.
// Check whether the current state is a deadlock state and treat it accordingly.
if ( this - > transitionMap [ state ] . size ( ) = = 0 ) {
if ( storm : : settings : : Settings : : getInstance ( ) - > isSet ( " fixDeadlocks " ) ) {
this - > numberOfTransitions + + ;
this - > numberOfChoices + + ;
this - > transitionMap [ curIndex ] . emplace_back ( ) ;
this - > transitionMap [ curIndex ] . back ( ) . second [ curIndex ] = 1 ;
+ + this - > numberOfTransitions ;
+ + this - > numberOfChoices ;
this - > transitionMap [ state ] . emplace_back ( ) ;
this - > transitionMap [ state ] . back ( ) . second [ state ] = 1 ;
} else {
LOG4CPLUS_ERROR ( logger , " Error while creating sparse matrix from probabilistic program: found deadlock state. " ) ;
throw storm : : exceptions : : WrongFormatException ( ) < < " Error while creating sparse matrix from probabilistic program: found deadlock state. " ;
LOG4CPLUS_ERROR ( logger , " Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option . " ) ;
throw storm : : exceptions : : WrongFormatException ( ) < < " Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option . " ;
}
}
}
LOG4CPLUS_DEBUG ( logger , " Finished creating transition map. " ) ;
}
@ -566,6 +578,5 @@ namespace adapters {
this - > transitionMap . clear ( ) ;
}
} // namespace adapters
} // namespace adapters
} // namespace storm
dehnert
11 years ago