| 
					
					
						
							
						
					
					
				 | 
				@ -11,18 +11,24 @@ | 
			
		
		
	
		
			
				 | 
				 | 
				#include "atomic_proposition.h" | 
				 | 
				 | 
				#include "atomic_proposition.h" | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#define USE_STD_UNORDERED_MAP | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				/* Map types: By default, the boost hash map is used. | 
				 | 
				 | 
				/* Map types: By default, the boost hash map is used. | 
			
		
		
	
		
			
				 | 
				 | 
				 * When the macro DEFAULT_MAP is defined, the default C++ class (std::map) | 
				 | 
				 | 
				 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				 * If the macro USE_STD_MAP is defined, the default C++ class (std::map) | 
			
		
		
	
		
			
				 | 
				 | 
				 * is used instead. | 
				 | 
				 | 
				 * is used instead. | 
			
		
		
	
		
			
				 | 
				 | 
				 */ | 
				 | 
				 | 
				 */ | 
			
		
		
	
		
			
				 | 
				 | 
				#ifdef DEFAULT_MAP | 
				 | 
				 | 
				 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#ifdef USE_STD_MAP | 
			
		
		
	
		
			
				 | 
				 | 
				#  include <map> | 
				 | 
				 | 
				#  include <map> | 
			
		
		
	
		
			
				 | 
				 | 
				#  define MAP std::map | 
				 | 
				 | 
				#  define MAP std::map | 
			
		
		
	
		
			
				 | 
				 | 
				#else | 
				 | 
				 | 
				#else | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#  ifdef USE_STD_UNORDERED_MAP | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#     include <unordered_map> | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#     define MAP std::unordered_map | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#  else | 
			
		
		
	
		
			
				 | 
				 | 
				#     include "boost/unordered_map.hpp" | 
				 | 
				 | 
				#     include "boost/unordered_map.hpp" | 
			
		
		
	
		
			
				 | 
				 | 
				#     define MAP boost::unordered_map | 
				 | 
				 | 
				#     define MAP boost::unordered_map | 
			
		
		
	
		
			
				 | 
				 | 
				#  endif | 
				 | 
				 | 
				#  endif | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#endif | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				#include <stdexcept> | 
				 | 
				 | 
				#include <stdexcept> | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
	
		
			
				| 
					
					
					
						
							
						
					
				 | 
				@ -33,11 +39,17 @@ namespace mrmc { | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				namespace dtmc { | 
				 | 
				 | 
				namespace dtmc { | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				/*! This class manages the objects of class atomic_proposition. Access is possible with the | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				 * string identifiers which are used in the input. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				 */ | 
			
		
		
	
		
			
				 | 
				 | 
				class labeling { | 
				 | 
				 | 
				class labeling { | 
			
		
		
	
		
			
				 | 
				 | 
				   public: | 
				 | 
				 | 
				   public: | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! Constructor creating an object of class labeling. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param nodeCount The number of nodes; necessary for class AtomicProposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param propositionCount The number of atomic propositions. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      labeling(const uint_fast32_t nodeCount, | 
				 | 
				 | 
				      labeling(const uint_fast32_t nodeCount, | 
			
		
		
	
		
			
				 | 
				 | 
				               const uint_fast32_t propositionCount) { | 
				 | 
				 | 
				               const uint_fast32_t propositionCount) { | 
			
		
		
	
		
			
				 | 
				 | 
				         node_count = nodeCount; | 
				 | 
				 | 
				         node_count = nodeCount; | 
			
		
		
	
	
		
			
				| 
					
					
					
						
							
						
					
				 | 
				@ -60,6 +72,12 @@ class labeling { | 
			
		
		
	
		
			
				 | 
				 | 
				         propositions = NULL; | 
				 | 
				 | 
				         propositions = NULL; | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! Registers the name of a proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * Will throw an error if more propositions are added than were initialized, | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * or if a proposition is registered twice. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param proposition The name of the proposition to add. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @return The index of the new proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      uint_fast32_t addProposition(std::string proposition) { | 
				 | 
				 | 
				      uint_fast32_t addProposition(std::string proposition) { | 
			
		
		
	
		
			
				 | 
				 | 
				         if (proposition_map.count(proposition) != 0) { | 
				 | 
				 | 
				         if (proposition_map.count(proposition) != 0) { | 
			
		
		
	
		
			
				 | 
				 | 
				            throw std::out_of_range("Proposition does already exist."); | 
				 | 
				 | 
				            throw std::out_of_range("Proposition does already exist."); | 
			
		
		
	
	
		
			
				| 
					
					
					
						
							
						
					
				 | 
				@ -74,11 +92,17 @@ class labeling { | 
			
		
		
	
		
			
				 | 
				 | 
				         return returnValue; | 
				 | 
				 | 
				         return returnValue; | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! Checks whether the name of a proposition is already registered with the labeling. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @return True if the proposition was added to the labeling, false otherwise. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      bool containsProposition(std::string proposition) { | 
				 | 
				 | 
				      bool containsProposition(std::string proposition) { | 
			
		
		
	
		
			
				 | 
				 | 
				         return (proposition_map.count(proposition) != 0); | 
				 | 
				 | 
				         return (proposition_map.count(proposition) != 0); | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! Labels a node with an atomic proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param proposition   The name of the proposition | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param node The index of the node to label | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      void addLabelToNode(std::string proposition, const uint_fast32_t node) { | 
				 | 
				 | 
				      void addLabelToNode(std::string proposition, const uint_fast32_t node) { | 
			
		
		
	
		
			
				 | 
				 | 
				         //TODO (Thomas Heinemann): Differentiate exceptions? | 
				 | 
				 | 
				         //TODO (Thomas Heinemann): Differentiate exceptions? | 
			
		
		
	
		
			
				 | 
				 | 
				         if (proposition_map.count(proposition) == 0) { | 
				 | 
				 | 
				         if (proposition_map.count(proposition) == 0) { | 
			
		
		
	
	
		
			
				| 
					
					
					
						
							
						
					
				 | 
				@ -90,14 +114,28 @@ class labeling { | 
			
		
		
	
		
			
				 | 
				 | 
				         propositions[proposition_map[proposition]]->addLabelToNode(node); | 
				 | 
				 | 
				         propositions[proposition_map[proposition]]->addLabelToNode(node); | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! Checks whether a node is labeled with a proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param proposition The name of the proposition | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param node The index of the node | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @return True if the node is labeled with the proposition, false otherwise. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      bool nodeHasProposition(std::string proposition, const uint_fast32_t node) { | 
				 | 
				 | 
				      bool nodeHasProposition(std::string proposition, const uint_fast32_t node) { | 
			
		
		
	
		
			
				 | 
				 | 
				         return propositions[proposition_map[proposition]]->hasNodeLabel(node); | 
				 | 
				 | 
				         return propositions[proposition_map[proposition]]->hasNodeLabel(node); | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! Returns the number of propositions managed by this object (which was set in the initialization) | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @return The number of propositions. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      uint_fast32_t getNumberOfPropositions() { | 
				 | 
				 | 
				      uint_fast32_t getNumberOfPropositions() { | 
			
		
		
	
		
			
				 | 
				 | 
						  return proposition_count; | 
				 | 
				 | 
						  return proposition_count; | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				      /*! This function provides direct access to an atomic_proposition class object | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * by its string identifier. This object manages the nodes that are labeled with the | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * respective atomic proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @param proposition The name of the proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       * @return A pointer to the atomic_proposition object of the proposition. | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				       */ | 
			
		
		
	
		
			
				 | 
				 | 
				      AtomicProposition* getProposition(std::string proposition) { | 
				 | 
				 | 
				      AtomicProposition* getProposition(std::string proposition) { | 
			
		
		
	
		
			
				 | 
				 | 
				         return (propositions[proposition_map[proposition]]); | 
				 | 
				 | 
				         return (propositions[proposition_map[proposition]]); | 
			
		
		
	
		
			
				 | 
				 | 
				      } | 
				 | 
				 | 
				      } | 
			
		
		
	
	
		
			
				| 
					
						
							
						
					
					
					
				 | 
				
  |