domain_transition_graph.cpp
Go to the documentation of this file.
00001 #include "domain_transition_graph.h"
00002 #include "domain_transition_graph_symb.h"
00003 #include "domain_transition_graph_func.h"
00004 #include "domain_transition_graph_subterm.h"
00005 #include "operator.h"
00006 #include "axiom.h"
00007 #include "variable.h"
00008 
00009 #include <algorithm>
00010 #include <cassert>
00011 #include <iostream>
00012 using namespace std;
00013 
00014 void build_DTGs(const vector<Variable *> &var_order,
00015         const vector<Operator> &operators,
00016         const vector<Axiom_relational> &axioms_rel,
00017         const vector<Axiom_functional> &axioms_func,
00018         vector<DomainTransitionGraph *> &transition_graphs) {
00019 
00020     for(int i = 0; i < var_order.size(); i++) {
00021         Variable v = *var_order[i];
00022         if(v.is_module()) {
00023             DomainTransitionGraphModule *dtg = new DomainTransitionGraphModule();
00024             transition_graphs.push_back(dtg);
00025         } else if(v.is_subterm() || v.is_comparison()) {
00026             DomainTransitionGraphSubterm *dtg = new DomainTransitionGraphSubterm(v);
00027             transition_graphs.push_back(dtg);
00028         } else if(v.is_functional()) {
00029             DomainTransitionGraphFunc *dtg = new DomainTransitionGraphFunc(v);
00030             transition_graphs.push_back(dtg);
00031         } else {
00032             DomainTransitionGraphSymb *dtg = new DomainTransitionGraphSymb(v);
00033             transition_graphs.push_back(dtg);
00034         }
00035     }
00036 
00037     for(int i = 0; i < operators.size(); i++) {
00038         const Operator &op = operators[i];
00039         const vector<Operator::PrePost> &pre_post_start = op.get_pre_post_start();
00040         const vector<Operator::PrePost> &pre_post_end = op.get_pre_post_end();
00041         vector<std::pair<Operator::PrePost,trans_type> > pre_posts_to_add;
00042         for(int j = 0; j < pre_post_start.size(); ++j) {
00043             pre_posts_to_add.push_back(make_pair(pre_post_start[j],start));
00044             //      pre_posts_to_add.push_back(make_pair(Operator::PrePost(
00045             //                    pre_post_start[j].var, pre_post_start[j].post,
00046             //                    pre_post_start[j].pre), DomainTransitionGraph::ax_rel));
00047         }
00048         //    bool pre_post_overwritten = false;
00049         //    for(int j = 0; j < pre_post_end.size(); ++j) {
00050         //      for(int k = 0; k < pre_posts_to_add.size(); ++k) {
00051         //      if(pre_post_end[j].var == pre_posts_to_add[k].first.var) {
00056         //          // compress original transition!
00057         //        pre_posts_to_add[k].first.post = pre_post_end[j].post;
00058         //        pre_posts_to_add[k].second = end;
00059         //        pre_post_overwritten = true;
00060         //        break;
00061         //      }
00062         //    }
00063         //    if(!pre_post_overwritten) {
00064         //      pre_posts_to_add.push_back(make_pair(pre_post_end[j],end));
00065         //      }
00066         //      pre_post_overwritten = false;
00067         //    }
00068 
00069         bool pre_post_overwritten = false;
00070         for(int j = 0; j < pre_post_end.size(); ++j) {
00071             for(int k = 0; k < pre_posts_to_add.size(); ++k) {
00072                 if(pre_post_end[j].var == pre_posts_to_add[k].first.var) {
00073                     int intermediate_value = pre_posts_to_add[k].first.post;
00074                     // compress original transition!
00075                     pre_posts_to_add[k].first.post = pre_post_end[j].post;
00076                     pre_posts_to_add[k].second = end;
00077                     pre_post_overwritten = true;
00078                     // If the intermediate value is something meaningful (i.e. unequal to
00079                     // <none_of_those>), we add an addtional start transition with the
00080                     // intermediate value as target.
00081                     if(intermediate_value < pre_posts_to_add[k].first.var->get_range() - 1) {
00082                         pre_posts_to_add.push_back(make_pair(Operator::PrePost(
00083                                         pre_posts_to_add[k].first.var,
00084                                         pre_posts_to_add[k].first.pre,
00085                                         intermediate_value), end));
00086                     }
00087                     break;
00088                 }
00089             }
00090             if(!pre_post_overwritten) {
00091                 pre_posts_to_add.push_back(make_pair(pre_post_end[j],end));
00092             }
00093             pre_post_overwritten = false;
00094         }
00095 
00096         for(int j = 0; j < pre_posts_to_add.size(); j++) {
00097             if(pre_posts_to_add[j].first.pre == pre_posts_to_add[j].first.post)
00098                 continue;
00099             const Variable *var = pre_posts_to_add[j].first.var;
00100             assert(var->get_layer() == -1);
00101             int var_level = var->get_level();
00102             if(var_level != -1) {
00103                 int pre = pre_posts_to_add[j].first.pre;
00104                 int post = pre_posts_to_add[j].first.post;
00105                 if(pre != -1) {
00106                     transition_graphs[var_level]->addTransition(pre, post, op, i,
00107                             pre_posts_to_add[j].second, var_order);
00108                 } else {
00109                     for(int pre = 0; pre < var->get_range(); pre++)
00110                         if(pre != post) {
00111                             transition_graphs[var_level]->addTransition(pre, post, op, i,
00112                                     pre_posts_to_add[j].second, var_order);
00113                         }
00114                 }
00115             }
00116         }
00117         const vector<Operator::NumericalEffect> &numerical_effs_start =
00118             op.get_numerical_effs_start();
00119         for(int j = 0; j < numerical_effs_start.size(); j++) {
00120             const Variable *var = numerical_effs_start[j].var;
00121             int var_level = var->get_level();
00122             if(var_level != -1) {
00123                 int foperator = static_cast<int>(numerical_effs_start[j].fop);
00124                 int right_var = numerical_effs_start[j].foperand->get_level();
00125                 transition_graphs[var_level]->addTransition(foperator, right_var, op,
00126                         i, start, var_order);
00127             }
00128         }
00129         const vector<Operator::NumericalEffect> &numerical_effs_end =
00130             op.get_numerical_effs_end();
00131         for(int j = 0; j < numerical_effs_end.size(); j++) {
00132             const Variable *var = numerical_effs_end[j].var;
00133             int var_level = var->get_level();
00134             if(var_level != -1) {
00135                 int foperator = static_cast<int>(numerical_effs_end[j].fop);
00136                 int right_var = numerical_effs_end[j].foperand->get_level();
00137                 transition_graphs[var_level]->addTransition(foperator, right_var, op,
00138                         i, end, var_order);
00139             }
00140         }
00141     }
00142 
00143     for(int i = 0; i < axioms_rel.size(); i++) {
00144         const Axiom_relational &ax = axioms_rel[i];
00145         Variable *var = ax.get_effect_var();
00146         int var_level = var->get_level();
00147         assert(var->get_layer()> -1);
00148         assert(var_level != -1);
00149         int old_val = ax.get_old_val();
00150         int new_val = ax.get_effect_val();
00151         transition_graphs[var_level]->addAxRelTransition(old_val, new_val, ax, i);
00152     }
00153 
00154     for(int i = 0; i < axioms_func.size(); i++) {
00155         const Axiom_functional &ax = axioms_func[i];
00156         Variable *var = ax.get_effect_var();
00157         if(!var->is_necessary()&&!var->is_used_in_duration_condition())
00158             continue;
00159         int var_level = var->get_level();
00160         assert(var->get_layer()> -1);
00161         Variable* left_var = ax.get_left_var();
00162         Variable* right_var = ax.get_right_var();
00163         DomainTransitionGraphSubterm *dtgs = dynamic_cast<DomainTransitionGraphSubterm*>(transition_graphs[var_level]);
00164         assert(dtgs);
00165         if(var->is_comparison()) {
00166             dtgs->setRelation(left_var, ax.cop, right_var);
00167         } else {
00168             dtgs->setRelation(left_var, ax.fop, right_var);
00169         }
00170     }
00171 
00172     for(int i = 0; i < transition_graphs.size(); i++)
00173         transition_graphs[i]->finalize();
00174 }
00175 
00176 bool are_DTGs_strongly_connected(
00177         const vector<DomainTransitionGraph*> &transition_graphs) {
00178     bool connected = true;
00179     // no need to test last variable's dtg (highest level variable)
00180     for(int i = 0; i < transition_graphs.size() - 1; i++)
00181         if(!transition_graphs[i]->is_strongly_connected())
00182             connected = false;
00183     return connected;
00184 }


tfd_modules
Author(s): Maintained by Christian Dornhege (see AUTHORS file).
autogenerated on Mon Oct 6 2014 07:52:06