@ -13,22 +13,22 @@ 
			
		
	
		
			
				
					# include  <string> 
  
			
		
	
		
			
				
					# include  <sstream> 
  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// Typedefs
  
			
		
	
		
			
				
					using  RationalFunction  =  storm : : RationalFunction ;  
			
		
	
		
			
				
					using  state_type  =  storm : : storage : : sparse : : state_type ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseRewardModel  =  storm : : models : : sparse : : StandardRewardModel < ValueType > ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					using  ModelBase  =  storm : : models : : ModelBase ;  
			
		
	
		
			
				
					using  state_type  =  storm : : storage : : sparse : : state_type ;  
			
		
	
		
			
				
					using  RationalFunction  =  storm : : RationalFunction ;  
			
		
	
		
			
				
					using  RationalFunctionVariable  =  storm : : RationalFunctionVariable ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  Model  =  storm : : models : : sparse : : Model < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  Dtmc  =  storm : : models : : sparse : : Dtmc < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  Mdp  =  storm : : models : : sparse : : Mdp < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  Ctmc  =  storm : : models : : sparse : : Ctmc < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  MarkovAutomaton  =  storm : : models : : sparse : : MarkovAutomaton < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseMatrix  =  storm : : storage : : SparseMatrix < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  RewardModel  =  storm : : models : : sparse : : StandardRewardModel < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseModel  =  storm : : models : : sparse : : Model < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseDtmc  =  storm : : models : : sparse : : Dtmc < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseMdp  =  storm : : models : : sparse : : Mdp < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseCtmc  =  storm : : models : : sparse : : Ctmc < ValueType > ;  
			
		
	
		
			
				
					template < typename  ValueType >  using  SparseMarkovAutomaton  =  storm : : models : : sparse : : MarkovAutomaton < ValueType > ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// Thin wrapper for getting initial states
  
			
		
	
		
			
				
					template < typename  ValueType >  
			
		
	
		
			
				
					std : : vector < state_type >  getInitialStates ( Model < ValueType >  const &  model )  {  
			
		
	
		
			
				
					std : : vector < state_type >  getInitialStates ( SparseModel < ValueType >  const &  model )  {  
			
		
	
		
			
				
					    std : : vector < state_type >  initialStates ;  
			
		
	
		
			
				
					    for  ( auto  entry  :  model . getInitialStates ( ) )  {  
			
		
	
		
			
				
					        initialStates . push_back ( entry ) ;  
			
		
	
	
		
			
				
					
						
						
						
							
								 
						
					 
				
				@ -38,28 +38,28 @@ std::vector<state_type> getInitialStates(Model<ValueType> const& model) { 
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// Thin wrapper for getting transition matrix
  
			
		
	
		
			
				
					template < typename  ValueType >  
			
		
	
		
			
				
					SparseMatrix < ValueType > &  getTransitionMatrix ( Model < ValueType > &  model )  {  
			
		
	
		
			
				
					storm : : storage : : SparseMatrix < ValueType > &  getTransitionMatrix ( Sparse Model< ValueType > &  model )  {  
			
		
	
		
			
				
					    return  model . getTransitionMatrix ( ) ;  
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					template < typename  ValueType >  
			
		
	
		
			
				
					storm : : storage : : SparseMatrix < ValueType >  getBackwardTransitionMatrix ( storm : : models : : sparse : : Model < ValueType > &  model )  {  
			
		
	
		
			
				
					    return  model . getBackwardTransitions ( ) ;  
			
		
	
		
			
				
					storm : : storage : : SparseMatrix < ValueType >  getBackwardTransitionMatrix ( SparseModel < ValueType >  const &  model )  {  
			
		
	
		
			
				
					    return  std : : move ( model . getBackwardTransitions ( ) ) ;  
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// requires pycarl.Variable
  
			
		
	
		
			
				
					std : : set < RationalFunctionVariable >  probabilityVariables ( Model < RationalFunction >  const &  model )  {  
			
		
	
		
			
				
					std : : set < storm : : RationalFunctionVariable >  probabilityVariables ( Sparse Model< RationalFunction >  const &  model )  {  
			
		
	
		
			
				
					    return  storm : : models : : sparse : : getProbabilityParameters ( model ) ;  
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					std : : set < RationalFunctionVariable >  rewardVariables ( Model < RationalFunction >  const &  model )  {  
			
		
	
		
			
				
					std : : set < storm : : RationalFunctionVariable >  rewardVariables ( Sparse Model< RationalFunction >  const &  model )  {  
			
		
	
		
			
				
					    return  storm : : models : : sparse : : getRewardParameters ( model ) ;  
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					template < typename  ValueType >  
			
		
	
		
			
				
					std : : function < std : : string  ( Model < ValueType >  const & ) >  getModelInfoPrinter ( std : : string  name  =  " Model " )  {  
			
		
	
		
			
				
					std : : function < std : : string  ( storm : : models : : Model < ValueType >  const & ) >  getModelInfoPrinter ( std : : string  name  =  " Model " )  {  
			
		
	
		
			
				
					    // look, C++ has lambdas and stuff!
  
			
		
	
		
			
				
					    return  [ name ] ( Model < ValueType >  const &  model )  {  
			
		
	
		
			
				
					    return  [ name ] ( storm : : models : : Model < ValueType >  const &  model )  {  
			
		
	
		
			
				
					        std : : stringstream  ss ;  
			
		
	
		
			
				
					        model . printModelInformationToStream ( ss ) ;  
			
		
	
		
			
				
					
 
			
		
	
	
		
			
				
					
						
						
						
							
								 
						
					 
				
				@ -75,11 +75,12 @@ std::function<std::string (Model<ValueType> const&)> getModelInfoPrinter(std::st 
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					template < typename  ValueType >  
			
		
	
		
			
				
					storm : : models : : sparse : : StateLabeling &  getLabeling ( storm : : models : : sparse : : Model < ValueType > &  model )  {  
			
		
	
		
			
				
					storm : : models : : sparse : : StateLabeling &  getLabeling ( Sparse Model< ValueType > &  model )  {  
			
		
	
		
			
				
					    return  model . getStateLabeling ( ) ;  
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// Define python bindings
  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// Bindings for general models
  
			
		
	
		
			
				
					void  define_model ( py : : module &  m )  {  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    // ModelType
  
			
		
	
	
		
			
				
					
						
						
						
							
								 
						
					 
				
				@ -98,116 +99,121 @@ void define_model(py::module& m) { 
			
		
	
		
			
				
					        . def_property_readonly ( " supports_parameters " ,  & ModelBase : : supportsParameters ,  " Flag whether model supports parameters " )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_parameters " ,  & ModelBase : : hasParameters ,  " Flag whether model has parameters " )  
			
		
	
		
			
				
					        . def_property_readonly ( " is_exact " ,  & ModelBase : : isExact ,  " Flag whether model is exact " )  
			
		
	
		
			
				
					        . def ( " _as_dtmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < Dtmc < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as DTMC " )  
			
		
	
		
			
				
					        . def ( " _as_pdtmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < Dtmc < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as pDTMC " )  
			
		
	
		
			
				
					        . def ( " _as_mdp " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < Mdp < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as MDP " )  
			
		
	
		
			
				
					        . def ( " _as_pmdp " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < Mdp < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as pMDP " )  
			
		
	
		
			
				
					        . def ( " _as_ctmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < Ctmc < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as CTMC " )  
			
		
	
		
			
				
					        . def ( " _as_pctmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < Ctmc < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as pCTMC " )  
			
		
	
		
			
				
					        . def ( " _as_ma " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < MarkovAutomaton < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as MA " )  
			
		
	
		
			
				
					        . def ( " _as_pma " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < MarkovAutomaton < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as pMA " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_dtmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseDtmc < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse DTMC " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_pdtmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseDtmc < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse pDTMC " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_mdp " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseMdp < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse MDP " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_pmdp " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseMdp < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse pMDP " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_ctmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseCtmc < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse CTMC " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_pctmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseCtmc < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse pCTMC " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_ma " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseMarkovAutomaton < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse MA " )  
			
		
	
		
			
				
					        . def ( " _as_sparse_pma " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SparseMarkovAutomaton < RationalFunction > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as sparse pMA " )  
			
		
	
		
			
				
					         . def ( " _as_symbolic_dtmc " ,  [ ] ( ModelBase  & modelbase )  {  
			
		
	
		
			
				
					                return  modelbase . as < SymbolicDtmc < double > > ( ) ;  
			
		
	
		
			
				
					            } ,  " Get model as symbolic DTMC " )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					}  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					// Bindings for sparse models
  
			
		
	
		
			
				
					void  define_sparse_model ( py : : module &  m )  {  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    // Models
  
			
		
	
		
			
				
					    py : : class_ < Model < double > ,  std : : shared_ptr < Model < double > > >  model ( m ,  " _SparseModel " ,  " A probabilistic model where transitions are represented by doubles and saved in a sparse matrix " ,  modelBase ) ;  
			
		
	
		
			
				
					    py : : class_ < Sparse Model< double > ,  std : : shared_ptr < Sparse Model< double > > ,  ModelBase >  model ( m ,  " _SparseModel " ,  " A probabilistic model where transitions are represented by doubles and saved in a sparse matrix " ) ;  
			
		
	
		
			
				
					    model . def_property_readonly ( " labeling " ,  & getLabeling < double > ,  " Labels " )  
			
		
	
		
			
				
					        . def ( " labels_state " ,  & Model < double > : : getLabelsOfState ,  py : : arg ( " state " ) ,  " Get labels of state " )  
			
		
	
		
			
				
					        . def ( " labels_state " ,  & Sparse Model< double > : : getLabelsOfState ,  py : : arg ( " state " ) ,  " Get labels of state " )  
			
		
	
		
			
				
					        . def_property_readonly ( " initial_states " ,  & getInitialStates < double > ,  " Initial states " )  
			
		
	
		
			
				
					        . def_property_readonly ( " states " ,  [ ] ( Model < double > &  model )  {  
			
		
	
		
			
				
					        . def_property_readonly ( " states " ,  [ ] ( Sparse Model< double > &  model )  {  
			
		
	
		
			
				
					                return  SparseModelStates < double > ( model ) ;  
			
		
	
		
			
				
					            } ,  " Get states " )  
			
		
	
		
			
				
					        . def_property_readonly ( " reward_models " ,  [ ] ( Model < double > &  model )  { return  model . getRewardModels ( ) ;  } ,  " Reward models " )  
			
		
	
		
			
				
					        . def_property_readonly ( " reward_models " ,  [ ] ( Sparse Model< double > &  model )  { return  model . getRewardModels ( ) ;  } ,  " Reward models " )  
			
		
	
		
			
				
					        . def_property_readonly ( " transition_matrix " ,  & getTransitionMatrix < double > ,  py : : return_value_policy : : reference ,  py : : keep_alive < 1 ,  0 > ( ) ,  " Transition matrix " )  
			
		
	
		
			
				
					        . def_property_readonly ( " backward_transition_matrix " ,  & getBackwardTransitionMatrix < double > ,  py : : return_value_policy : : reference ,  py : : keep_alive < 1 ,  0 > ( ) ,  " Backward transition matrix " )  
			
		
	
		
			
				
					        . def ( " reduce_to_state_based_rewards " ,  & Model < double > : : reduceToStateBasedRewards )  
			
		
	
		
			
				
					        . def ( " reduce_to_state_based_rewards " ,  & Sparse Model< double > : : reduceToStateBasedRewards )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < double > ( ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					    py : : class_ < Dtmc < double > ,  std : : shared_ptr < Dtmc < double > > > ( m ,  " SparseDtmc " ,  " DTMC in sparse representation " ,  model )  
			
		
	
		
			
				
					    py : : class_ < Sparse Dtmc< double > ,  std : : shared_ptr < Sparse Dtmc< double > > > ( m ,  " SparseDtmc " ,  " DTMC in sparse representation " ,  model )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < double > ( " DTMC " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					    py : : class_ < Mdp < double > ,  std : : shared_ptr < Mdp < double > > > ( m ,  " SparseMdp " ,  " MDP in sparse representation " ,  model )  
			
		
	
		
			
				
					    py : : class_ < Sparse Mdp< double > ,  std : : shared_ptr < Sparse Mdp< double > > > ( m ,  " SparseMdp " ,  " MDP in sparse representation " ,  model )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < double > ( " MDP " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					    py : : class_ < storm : : models : : sparse : : Ctmc < double > ,  std : : shared_ptr < storm : : models : : sparse : : Ctmc < double > > > ( m ,  " SparseCtmc " ,  " CTMC in sparse representation " ,  model )  
			
		
	
		
			
				
					    py : : class_ < Sparse Ctmc< double > ,  std : : shared_ptr < Sparse Ctmc< double > > > ( m ,  " SparseCtmc " ,  " CTMC in sparse representation " ,  model )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < double > ( " CTMC " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					    py : : class_ < storm : : models : : sparse : : MarkovAutomaton < double > ,  std : : shared_ptr < storm : : models : : sparse : : MarkovAutomaton < double > > > ( m ,  " SparseMA " ,  " MA in sparse representation " ,  model )  
			
		
	
		
			
				
					    py : : class_ < Sparse MarkovAutomaton< double > ,  std : : shared_ptr < Sparse MarkovAutomaton< double > > > ( m ,  " SparseMA " ,  " MA in sparse representation " ,  model )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < double > ( " MA " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					    py : : class_ < storm : : models : : sparse : : StandardRewardModel < double > > ( m ,  " SparseRewardModel " ,  " Reward structure for sparse models " )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_state_rewards " ,  & RewardModel < double > : : hasStateRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_state_action_rewards " ,  & RewardModel < double > : : hasStateActionRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_transition_rewards " ,  & RewardModel < double > : : hasTransitionRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " transition_rewards " ,  [ ] ( RewardModel < double > &  rewardModel )  { return  rewardModel . getTransitionRewardMatrix ( ) ; } )  
			
		
	
		
			
				
					        . def_property_readonly ( " state_rewards " ,  [ ] ( RewardModel < double > &  rewardModel )  { return  rewardModel . getStateRewardVector ( ) ; } )  
			
		
	
		
			
				
					        . def ( " get_state_reward " ,  [ ] ( RewardModel < double > &  rewardModel ,  uint64_t  state )  { return  rewardModel . getStateReward ( state ) ; } )  
			
		
	
		
			
				
					        . def ( " get_state_action_reward " ,  [ ] ( RewardModel < double > &  rewardModel ,  uint64_t  action_index )  { return  rewardModel . getStateActionReward ( action_index ) ; } )  
			
		
	
		
			
				
					            . def_property_readonly ( " state_action_rewards " ,  [ ] ( RewardModel < double > &  rewardModel )  { return  rewardModel . getStateActionRewardVector ( ) ; } )  
			
		
	
		
			
				
					        . def ( " reduce_to_state_based_rewards " ,  [ ] ( RewardModel < double > &  rewardModel ,  SparseMatrix < double >  const &  transitions ,  bool  onlyStateRewards ) { return  rewardModel . reduceToStateBasedRewards ( transitions ,  onlyStateRewards ) ; } ,   py : : arg ( " transition_matrix " ) ,  py : : arg ( " only_state_rewards " ) ,  " Reduce to state-based rewards " )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < SparseRewardModel < double > > ( m ,  " SparseRewardModel " ,  " Reward structure for sparse models " )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_state_rewards " ,  & SparseRewardModel < double > : : hasStateRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_state_action_rewards " ,  & SparseRewardModel < double > : : hasStateActionRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " has_transition_rewards " ,  & SparseRewardModel < double > : : hasTransitionRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " transition_rewards " ,  [ ] ( SparseRewardModel < double > &  rewardModel )  { return  rewardModel . getTransitionRewardMatrix ( ) ; } )  
			
		
	
		
			
				
					        . def_property_readonly ( " state_rewards " ,  [ ] ( SparseRewardModel < double > &  rewardModel )  { return  rewardModel . getStateRewardVector ( ) ; } )  
			
		
	
		
			
				
					        . def ( " get_state_reward " ,  [ ] ( SparseRewardModel < double > &  rewardModel ,  uint64_t  state )  { return  rewardModel . getStateReward ( state ) ; } )  
			
		
	
		
			
				
					        . def ( " get_state_action_reward " ,  [ ] ( SparseRewardModel < double > &  rewardModel ,  uint64_t  action_index )  { return  rewardModel . getStateActionReward ( action_index ) ; } )  
			
		
	
		
			
				
					            . def_property_readonly ( " state_action_rewards " ,  [ ] ( SparseRewardModel < double > &  rewardModel )  { return  rewardModel . getStateActionRewardVector ( ) ; } )  
			
		
	
		
			
				
					        . def ( " reduce_to_state_based_rewards " ,  [ ] ( SparseRewardModel < double > &  rewardModel ,  storm : : storage : : SparseMatrix < double >  const &  transitions ,  bool  onlyStateRewards ) { return  rewardModel . reduceToStateBasedRewards ( transitions ,  onlyStateRewards ) ; } ,   py : : arg ( " transition_matrix " ) ,  py : : arg ( " only_state_rewards " ) ,  " Reduce to state-based rewards " )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < Model < RationalFunction > ,  std : : shared_ptr < Model < RationalFunction > > >  modelRatFunc ( m ,  " _SparseParametricModel " ,  " A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix " ,  modelBase ) ;  
			
		
	
		
			
				
					    py : : class_ < Sparse Model< RationalFunction > ,  std : : shared_ptr < Sparse Model< RationalFunction > > ,  ModelBase >  modelRatFunc ( m ,  " _SparseParametricModel " ,  " A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix " ) ;  
			
		
	
		
			
				
					    modelRatFunc . def ( " collect_probability_parameters " ,  & probabilityVariables ,  " Collect parameters " )  
			
		
	
		
			
				
					        . def ( " collect_reward_parameters " ,  & rewardVariables ,  " Collect reward parameters " )  
			
		
	
		
			
				
					        . def_property_readonly ( " labeling " ,  & getLabeling < storm : : RationalFunction > ,  " Labels " )  
			
		
	
		
			
				
					        . def ( " labels_state " ,  & Model < RationalFunction > : : getLabelsOfState ,  py : : arg ( " state " ) ,  " Get labels of state " )  
			
		
	
		
			
				
					        . def_property_readonly ( " labeling " ,  & getLabeling < RationalFunction > ,  " Labels " )  
			
		
	
		
			
				
					        . def ( " labels_state " ,  & Sparse Model< RationalFunction > : : getLabelsOfState ,  py : : arg ( " state " ) ,  " Get labels of state " )  
			
		
	
		
			
				
					        . def_property_readonly ( " initial_states " ,  & getInitialStates < RationalFunction > ,  " Initial states " )  
			
		
	
		
			
				
					        . def_property_readonly ( " states " ,  [ ] ( Model < storm : : RationalFunction > &  model )  {  
			
		
	
		
			
				
					                return  SparseModelStates < storm : : RationalFunction > ( model ) ;  
			
		
	
		
			
				
					        . def_property_readonly ( " states " ,  [ ] ( Sparse Model< RationalFunction > &  model )  {  
			
		
	
		
			
				
					                return  SparseModelStates < RationalFunction > ( model ) ;  
			
		
	
		
			
				
					            } ,  " Get states " )  
			
		
	
		
			
				
					        . def_property_readonly ( " reward_models " ,  [ ] ( Model < storm : : RationalFunction >  const &  model )  { return  model . getRewardModels ( ) ;  } ,  " Reward models " )  
			
		
	
		
			
				
					        . def_property_readonly ( " reward_models " ,  [ ] ( Sparse Model< RationalFunction >  const &  model )  { return  model . getRewardModels ( ) ;  } ,  " Reward models " )  
			
		
	
		
			
				
					        . def_property_readonly ( " transition_matrix " ,  & getTransitionMatrix < RationalFunction > ,  py : : return_value_policy : : reference ,  py : : keep_alive < 1 ,  0 > ( ) ,  " Transition matrix " )  
			
		
	
		
			
				
					        . def_property_readonly ( " backward_transition_matrix " ,  & getBackwardTransitionMatrix < storm : : RationalFunction > ,  py : : return_value_policy : : reference ,  py : : keep_alive < 1 ,  0 > ( ) ,  " Backward transition matrix " )  
			
		
	
		
			
				
					        . def ( " reduce_to_state_based_rewards " ,  & Model < RationalFunction > : : reduceToStateBasedRewards )  
			
		
	
		
			
				
					        . def_property_readonly ( " backward_transition_matrix " ,  & getBackwardTransitionMatrix < RationalFunction > ,  py : : return_value_policy : : reference ,  py : : keep_alive < 1 ,  0 > ( ) ,  " Backward transition matrix " )  
			
		
	
		
			
				
					        . def ( " reduce_to_state_based_rewards " ,  & Sparse Model< RationalFunction > : : reduceToStateBasedRewards )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < RationalFunction > ( " ParametricModel " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < Dtmc < RationalFunction > ,  std : : shared_ptr < Dtmc < RationalFunction > > > ( m ,  " SparseParametricDtmc " ,  " pDTMC in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					    py : : class_ < Sparse Dtmc< RationalFunction > ,  std : : shared_ptr < Sparse Dtmc< RationalFunction > > > ( m ,  " SparseParametricDtmc " ,  " pDTMC in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < RationalFunction > ( " ParametricDTMC " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < Mdp < RationalFunction > ,  std : : shared_ptr < Mdp < RationalFunction > > > ( m ,  " SparseParametricMdp " ,  " pMDP in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					    py : : class_ < SparseMdp < RationalFunction > ,  std : : shared_ptr < SparseMdp < RationalFunction > > > ( m ,  " SparseParametricMdp " ,  " pMDP in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < RationalFunction > ( " ParametricMDP " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < storm : : models : : sparse : : Ctmc < storm : : RationalFunction > ,  std : : shared_ptr < storm : : models : : sparse : : Ctmc < storm : : RationalFunction > > > ( m ,  " SparseParametricCtmc " ,  " pCTMC in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					    py : : class_ < SparseCtmc < RationalFunction > ,  std : : shared_ptr < SparseCtmc < RationalFunction > > > ( m ,  " SparseParametricCtmc " ,  " pCTMC in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < RationalFunction > ( " ParametricCTMC " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < storm : : models : : sparse : : MarkovAutomaton < storm : : RationalFunction > ,  std : : shared_ptr < storm : : models : : sparse : : MarkovAutomaton < storm : : RationalFunction > > > ( m ,  " SparseParametricMA " ,  " pMA in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					    py : : class_ < SparseMarkovAutomaton < RationalFunction > ,  std : : shared_ptr < SparseMarkovAutomaton < RationalFunction > > > ( m ,  " SparseParametricMA " ,  " pMA in sparse representation " ,  modelRatFunc )  
			
		
	
		
			
				
					        . def ( " __str__ " ,  getModelInfoPrinter < RationalFunction > ( " ParametricMA " ) )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					    py : : class_ < storm : : models : : sparse : : StandardRewardModel < storm : : RationalFunction > > ( m ,  " SparseParametricRewardModel " ,  " Reward structure for parametric sparse models " )  
			
		
	
		
			
				
					            . def_property_readonly ( " has_state_rewards " ,  & RewardModel < storm : : RationalFunction > : : hasStateRewards )  
			
		
	
		
			
				
					            . def_property_readonly ( " has_state_action_rewards " ,  & RewardModel < storm : : RationalFunction > : : hasStateActionRewards )  
			
		
	
		
			
				
					            . def_property_readonly ( " has_transition_rewards " ,  & RewardModel < storm : : RationalFunction > : : hasTransitionRewards )  
			
		
	
		
			
				
					            . def_property_readonly ( " transition_rewards " ,  [ ] ( RewardModel < storm : : RationalFunction > &  rewardModel )  { return  rewardModel . getTransitionRewardMatrix ( ) ; } )  
			
		
	
		
			
				
					            . def_property_readonly ( " state_rewards " ,  [ ] ( RewardModel < storm : : RationalFunction > &  rewardModel )  { return  rewardModel . getStateRewardVector ( ) ; } )  
			
		
	
		
			
				
					            . def ( " get_state_reward " ,  [ ] ( RewardModel < storm : : RationalFunction > &  rewardModel ,  uint64_t  state )  { return  rewardModel . getStateReward ( state ) ; } )  
			
		
	
		
			
				
					            . def ( " get_state_action_reward " ,  [ ] ( RewardModel < storm : : RationalFunction > &  rewardModel ,  uint64_t  action_index )  { return  rewardModel . getStateActionReward ( action_index ) ; } )  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					            . def_property_readonly ( " state_action_rewards " ,  [ ] ( RewardModel < storm : : RationalFunction > &  rewardModel )  { return  rewardModel . getStateActionRewardVector ( ) ; } )  
			
		
	
		
			
				
					            . def ( " reduce_to_state_based_rewards " ,  [ ] ( RewardModel < storm : : RationalFunction > &  rewardModel ,  SparseMatrix < storm : : RationalFunction >  const &  transitions ,  bool  onlyStateRewards ) { return  rewardModel . reduceToStateBasedRewards ( transitions ,  onlyStateRewards ) ; } ,   py : : arg ( " transition_matrix " ) ,  py : : arg ( " only_state_rewards " ) ,  " Reduce to state-based rewards " )  
			
		
	
		
			
				
					    py : : class_ < SparseRewardModel < RationalFunction > > ( m ,  " SparseParametricRewardModel " ,  " Reward structure for parametric sparse models " )  
			
		
	
		
			
				
					            . def_property_readonly ( " has_state_rewards " ,  & Sparse RewardModel< RationalFunction > : : hasStateRewards )  
			
		
	
		
			
				
					            . def_property_readonly ( " has_state_action_rewards " ,  & Sparse RewardModel< RationalFunction > : : hasStateActionRewards )  
			
		
	
		
			
				
					            . def_property_readonly ( " has_transition_rewards " ,  & Sparse RewardModel< RationalFunction > : : hasTransitionRewards )  
			
		
	
		
			
				
					            . def_property_readonly ( " transition_rewards " ,  [ ] ( Sparse RewardModel< RationalFunction > &  rewardModel )  { return  rewardModel . getTransitionRewardMatrix ( ) ; } )  
			
		
	
		
			
				
					            . def_property_readonly ( " state_rewards " ,  [ ] ( Sparse RewardModel< RationalFunction > &  rewardModel )  { return  rewardModel . getStateRewardVector ( ) ; } )  
			
		
	
		
			
				
					            . def ( " get_state_reward " ,  [ ] ( Sparse RewardModel< RationalFunction > &  rewardModel ,  uint64_t  state )  { return  rewardModel . getStateReward ( state ) ; } )  
			
		
	
		
			
				
					            . def ( " get_state_action_reward " ,  [ ] ( Sparse RewardModel< RationalFunction > &  rewardModel ,  uint64_t  action_index )  { return  rewardModel . getStateActionReward ( action_index ) ; } )  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					            . def_property_readonly ( " state_action_rewards " ,  [ ] ( Sparse RewardModel< RationalFunction > &  rewardModel )  { return  rewardModel . getStateActionRewardVector ( ) ; } )  
			
		
	
		
			
				
					            . def ( " reduce_to_state_based_rewards " ,  [ ] ( Sparse RewardModel< RationalFunction > &  rewardModel ,  storm : : storage : : SparseMatrix < RationalFunction >  const &  transitions ,  bool  onlyStateRewards ) { return  rewardModel . reduceToStateBasedRewards ( transitions ,  onlyStateRewards ) ; } ,   py : : arg ( " transition_matrix " ) ,  py : : arg ( " only_state_rewards " ) ,  " Reduce to state-based rewards " )  
			
		
	
		
			
				
					    ;  
			
		
	
		
			
				
					
 
			
		
	
		
			
				
					}