00001 00008 #ifndef _SMP_MODEL_CHECKER_MU_CALCULUS_H_ 00009 #define _SMP_MODEL_CHECKER_MU_CALCULUS_H_ 00010 00011 #include <smp/components/model_checkers/base.h> 00012 00013 #include <smp/external_libraries/inc_mu_mc/ms.h> 00014 #include <smp/external_libraries/inc_mu_mc/pt.h> 00015 00016 00017 00018 00019 namespace smp { 00020 00022 00026 class model_checker_mu_calculus_vertex_data { 00027 00028 public: 00029 00031 00037 MS_state *state; 00038 }; 00039 00040 00042 00045 class model_checker_mu_calculus_edge_data { 00046 00047 }; 00048 00049 00051 00058 template< class typeparams > 00059 class model_checker_mu_calculus : public model_checker_base<typeparams>{ 00060 00061 typedef typename typeparams::state state_t; 00062 typedef typename typeparams::input input_t; 00063 00064 typedef vertex<typeparams> vertex_t; 00065 typedef edge<typeparams> edge_t; 00066 00067 typedef trajectory<typeparams> trajectory_t; 00068 00069 int uid_counter; 00070 00071 bool found_solution; 00072 00073 public: 00074 00076 00080 rModelChecker ms; 00081 00082 00083 model_checker_mu_calculus (); 00084 00085 ~model_checker_mu_calculus (); 00086 00087 00088 int mc_update_insert_vertex (vertex_t *vertex_new); 00089 00090 int mc_update_insert_edge (edge_t *edge_new); 00091 00092 int mc_update_delete_vertex (vertex_t *vertex_new); 00093 00094 int mc_update_delete_edge (edge_t *edge_new); 00095 00096 int get_solution (trajectory_t &trajectory_out); 00097 00098 }; 00099 00100 00101 } 00102 00103 #endif
