src/smp/components/model_checkers/reachability.h

Go to the documentation of this file.

#ifndef _SMP_MODEL_CHECKER_REACHABILITY_H_
#define _SMP_MODEL_CHECKER_REACHABILITY_H_

#include <smp/components/model_checkers/base.h>
#include <smp/common/region.h>


namespace smp {


    class model_checker_reachability_vertex_data {

    public:    
    

        bool reaches_goal;
    };




    class model_checker_reachability_edge_data {
    
    };




    template < class typeparams, int NUM_DIMENSIONS >
    class model_checker_reachability : public model_checker_base<typeparams> {


        typedef typename typeparams::state state_t;
        typedef typename typeparams::input input_t;
        typedef typename typeparams::vertex_data vertex_data_t;
        typedef typename typeparams::edge_data edge_data_t;
    
        typedef vertex<typeparams> vertex_t;
        typedef edge<typeparams> edge_t;
        typedef trajectory<typeparams> trajectory_t;

        typedef region<NUM_DIMENSIONS> region_t;

        region_t region_goal;
    
    public:

        model_checker_reachability ();    
        ~model_checker_reachability ();

    
        model_checker_reachability (const region_t &region_goal);


        int set_goal_region (const region_t &region_goal);


        int mc_update_insert_vertex (vertex_t *vertex_in);
    

        int mc_update_insert_edge (edge_t *edge_in);  


        int mc_update_delete_vertex (vertex_t *vertex_in);
    
    
        int mc_update_delete_edge (edge_t *edge_in);


        int get_solution (trajectory_t &trajectory_out);
        
    };


}

#endif