Line data    Source code

       1             : /*******************************************************************************
       2             :  *                                                                             *
       3             :  * Cosmos:(C)oncept et (O)utils (S)tatistique pour les (Mo)deles               *
       4             :  * (S)tochastiques                                                             *
       5             :  *                                                                             *
       6             :  * Copyright (C) 2009-2012 LSV & LACL                                          *
       7             :  * Authors: Paolo Ballarini Benoît Barbot & Hilal Djafri                       *
       8             :  * Website: http://www.lsv.ens-cachan.fr/Software/cosmos                       *
       9             :  *                                                                             *
      10             :  * This program is free software; you can redistribute it and/or modify        *
      11             :  * it under the terms of the GNU General Public License as published by        *
      12             :  * the Free Software Foundation; either version 3 of the License, or           *
      13             :  * (at your option) any later version.                                         *
      14             :  *                                                                             *
      15             :  * This program is distributed in the hope that it will be useful,             *
      16             :  * but WITHOUT ANY WARRANTY; without even the implied warranty of              *
      17             :  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the               *
      18             :  * GNU General Public License for more details.                                *
      19             :  *                                                                             *
      20             :  * You should have received a copy of the GNU General Public License along     *
      21             :  * with this program; if not, write to the Free Software Foundation, Inc.,     *
      22             :  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.                 *
      23             :  * file stateSpace.hpp created by Benoit Barbot on 01/12/11.                   *
      24             :  *******************************************************************************
      25             :  */
      26             : 
      27             : /*
      28             :  *      This class is used to compute the state space of the synchronized product
      29             :  * between the SPN and the LHA.
      30             :  *
      31             :  * This class also export and import this state space and the transition matrix
      32             :  *
      33             :  */
      34             : 
      35             : 
      36             : #ifndef _STATESPACE_HPP
      37             : #define _STATESPACE_HPP
      38             : 
      39             : #include <set>
      40             : #include <utility>
      41             : #include <string>
      42             : #include <iostream>
      43             : #include <vector>
      44             : #include <list>
      45             : #include <map>
      46             : #include <stack>
      47             : #include <cstring>
      48             : #include <iostream>
      49             : #include <boost/numeric/ublas/fwd.hpp>
      50             : #include <boost/numeric/ublas/matrix_proxy.hpp>
      51             : #include <boost/numeric/ublas/matrix_sparse.hpp>
      52             : #include <boost/numeric/ublas/io.hpp>
      53             : #include <unordered_map>
      54             : 
      55             : #include "marking.hpp"
      56             : #include "LHA_orig.hpp"
      57             : #include "spn.hpp"
      58             : 
      59             : //using namespace arma;
      60             : using namespace std;
      61             : 
      62           4 : struct eqstate{
      63     4254741 :         bool operator()(const vector<int>* t1,const vector<int>* t2) const {
      64    12769090 :                 for(size_t it=0; it < t1->size() ; it++)
      65     8514376 :                         if((*t1)[it] != (*t2)[it]) return false;
      66     4254714 :                 return true;
      67             :         }
      68             : };
      69             : 
      70           4 : struct hashstate{
      71     4256206 :         int operator()(const vector<int>* t1) const {
      72     4256206 :                 int h = 0;
      73    12775902 :                 for(size_t it=0; it < t1->size() ; it++)
      74     8519696 :                         h = h * 524287 + (*t1)[it];
      75     4256206 :                 return h;
      76             :         }
      77             : };
      78             : 
      79             : /*
      80             :  * The hash_map structure implement a mapping between a state as a vector
      81             :  * of integer and its index.
      82             :  */
      83             : typedef unordered_map<const vector<int>*, int , hashstate , eqstate > hash_state;
      84             : 
      85             : /*
      86             :  * This class manage the state space of the model. The state space is
      87             :  * stored as a mapping between the states and [0..nbState] the number of state.
      88             :  * This class can generate the state space by exploring it.
      89             :  *
      90             :  */
      91           0 : class stateSpace {
      92             : public:
      93             :         stateSpace();
      94             :         hash_state S;
      95             :         int findHash(const vector<int>* vect)const ;
      96             :     virtual double getMu(int)const;
      97             : 
      98             :         size_t nbState;
      99             :         size_t nbTrans;
     100             :         boost::numeric::ublas::compressed_matrix<double>* transitionsMatrix;
     101             :         boost::numeric::ublas::vector<double>* finalVector;
     102             :     vector<double>* muvect;
     103             :     
     104             :         void exploreStateSpace();
     105             :         void buildTransitionMatrix();
     106             :         
     107             :         SPN N; //The object representing the SPN
     108             :         LHA_orig<typename SPN::stateType> A; //The object representing the LHA
     109             :         
     110             :     //double maxRate();
     111             :     double uniformizeMatrix();
     112             :     double maxRate;
     113             :     
     114             :         void printP();
     115             :         
     116             :     void outputMat();
     117             :         void inputMat();
     118             :     
     119             :     void inputVect();
     120             :     void outputVect();
     121             :         void outputTmpLumpingFun();
     122             :     double returnPrismResult();
     123             :     
     124             :     void outputPrism();
     125             :     void launchPrism(string prismPath);
     126             :         void importPrism();
     127             :     
     128             : private:
     129             :     vector<vector<int> > *findstate;
     130             :     void add_state(vector<int> v);
     131             : };
     132             : 
     133             : #endif