#include "coin_common.hh" #include #include using namespace std; #define DEB(x) //std::cerr << x << endl string translist; #define TL(x) (translist += (x)) string renamelist; #define RL(x) (renamelist += (x)) coin_system_t * the_coin_system; void aut_t::add_state(name_t s) { coin_state_t * tmp = new coin_state_t; tmp->name = s; tmp->outtrans.clear(); int result = states.add_new(s, tmp); if (result == -1) { yyerror ("duplicate state name"); exit(1); } } void aut_t::set_init_state(name_t s) { int result = states.find_id(s); if (result == -1) { yyerror("initial state is an udeclared identifier"); exit(1); } init_state = result; } void aut_t::add_trans(name_t f, const label_t & l, name_t t) { int from = states.find_id(f); if (from == -1) { yyerror("transition's 'from' state not declared"); exit(1); } int to = states.find_id(t); if (to == -1) { yyerror("transition's 'to' state not declared"); exit(1); } trans_t * tmp = new trans_t; tmp->label = l; tmp->tostate_id = to; states.get(from)->add_trans(tmp); } bool aut_t::is_Ap_visible_trans(int from_id, int to_id) { coin_state_t * fst = states[from_id]; return (fst->visible_trans_to.find(to_id) != fst->visible_trans_to.end()); } void coin_system_t::automaton_begin(name_t s, bool prim) { aut_t * tmp = new aut_t(s, prim); // std::cerr << "adding " << s << endl; int result = automata.add_new(s, tmp); if (result == -1) { yyerror ("another automaton with this name already declared"); exit(1); } act_aut_id = result; // DEB("automaton_begin: " << s << " (id: " << result << ")"); } void coin_system_t::automaton_end() { // DEB("automaton_end id: " << act_aut_id); act_aut_id = -1; } void coin_system_t::add_state(name_t s) { if (act_aut_id >= 0) (automata.get(act_aut_id))->add_state(s); else if (act_prop) { if (!acc_states) { prop_state * tmp = new prop_state; tmp->name = s; int result = property->prop_states.add_new(s, tmp); if (result == -1) { yyerror ("property: duplicate state name"); exit(1);} } else { int result = property->prop_states.find_id(s); if (result == -1) { yyerror ("property: accepting state undeclared"); exit(1); } property->accepting_states.insert(result); } } } void coin_system_t::set_init_state(name_t s) { if (act_aut_id >= 0) (automata.get(act_aut_id))->set_init_state(s); else if (act_prop) { int result = property->prop_states.find_id(s); if (result == -1) { yyerror("property: initial state undeclared");exit(1);} property->init_state = result; } } void coin_system_t::add_trans(name_t f, const label_t & l, name_t t) { if (act_aut_id >= 0) (automata.get(act_aut_id))->add_trans(f, l, t); last_state = f; } void coin_system_t::add_trans(const label_t & l, name_t s) { if (act_aut_id >= 0) (automata.get(act_aut_id))->add_trans(last_state, l, s); } void coin_system_t::add_comp_name(name_t s) { component_t * tmp = new component_t; tmp->name = s; components.add_new(s, tmp); if (act_aut_id >= 0) (automata.get(act_aut_id))->components.add_new(s, new component_t(*tmp)); } void coin_system_t::set_system(name_t s) { system_aut_id = automata.find_id(s); if (system_aut_id == -1) { yyerror("undeclared automaton proposed as system"); exit(1); } } void coin_system_t::set_restrict(bool r) { if (act_aut_id >= 0) (automata.get(act_aut_id))->is_restrict = r; } void coin_system_t::add_to_complist(name_t s) { int newid = automata.find_id(s); if (newid == -1) { yyerror ("automaton name not declared"); } (automata.get(act_aut_id))->composed_of.push_back(newid); (automata.find(s))->setParent(automata.get(act_aut_id)); } void coin_system_t::add_to_restrict(const label_t & l) { if (act_aut_id >= 0) (automata.get(act_aut_id))->restrictions.insert(l); else if (act_prop) { // insert label into Act' (interesting actions) int_Act.insert(l); // ------ // hack property->act_trans->labels.insert(l); property->act_trans->any_label = false; } } void coin_system_t::any_label() { property->act_trans->any_label = true; } label_t coin_system_t::mklabel_int (name_t from, name_t act, name_t to) { label_t tmp; tmp.fromc_id = components.find_id(from); if (tmp.fromc_id == -1) { yyerror ("unknown component name"); exit(1); } tmp.toc_id = components.find_id(to); if (tmp.toc_id == -1) { yyerror ("unknown component name"); exit(1); } tmp.act_id = actions.find_id(act); if (tmp.act_id == -1) { action_t * newa = new action_t; newa->name = act; tmp.act_id = actions.add_new(act, newa); } return tmp; } label_t coin_system_t::mklabel_out (name_t from, name_t act) { label_t tmp; tmp.fromc_id = components.find_id(from); if (tmp.fromc_id == -1) { yyerror ("unknown component name"); exit(1); } tmp.toc_id = -1; tmp.act_id = actions.find_id(act); if (tmp.act_id == -1) { action_t * newa = new action_t; newa->name = act; tmp.act_id = actions.add_new(act, newa); } return tmp; } label_t coin_system_t::mklabel_in (name_t act, name_t to) { label_t tmp; tmp.fromc_id = -1; tmp.toc_id = components.find_id(to); if (tmp.toc_id == -1) { yyerror ("unknown component name"); exit(1); } tmp.act_id = actions.find_id(act); if (tmp.act_id == -1) { action_t * newa = new action_t; newa->name = act; tmp.act_id = actions.add_new(act, newa); } return tmp; } bool common_elem(const set & a, const set & b) { set::iterator i, j; i = a.begin(); j = b.begin(); while (i != a.end() && j != b.end()) { if (*i == *j) return true; else if (*i < *j) i++; else if (*i > *j) j++; } return false; } bool subset(const set & a, const set & b) { // a \subseteq b set::iterator i, j; i = a.begin(); j = b.begin(); while (i != a.end() && j != b.end()) { if (*i == *j) { i++; j++; } else if (*i < *j) return false; // v a je neco, co neni v b else if (*i > *j) j++; // v b je neco, co neni v a, to je ok } return (i == a.end()); // dosli jsme na konec a, je to ok // jinak je v a neco, co neni v b -> false } string coin_system_t::get_hier(int aid) { aut_t * tmp = automata.get(aid); string s; if (tmp->is_prim()) { s = "("; for (int i = 0; i < tmp->components.size(); i++) { if (i > 0) s += ","; s += tmp->components.get(i)->name; } s += ")"; } else { s = "("; bool first = true; for (vector::iterator i = tmp->composed_of.begin(); i != tmp->composed_of.end(); i++) { if (!first) s += ","; first = false; s += get_hier(*i); } s += ")"; } return s; } void coin_system_t::prop_begin() { act_prop = true; act_aut_id = -1; property = new prop_t; //std::cerr << "PROPERTY IS ON!" << endl; acc_states = false; } void coin_system_t::prop_end() { act_prop = false; } void coin_system_t::precompute() { // we now precompute some por info act_count = actions.size(); // all bitset of actions will be of act_count size // the visibility relation for all transitions of all simple automata for (int i = 0; i < automata.size(); i++) { if (automata[i]->is_primitive) { // first, compute enAp, input_act, output_act for all states // and all_input_act, all_output_act for all automata aut_t * aut = automata[i]; aut->all_input_act = new bit_set_t(act_count); aut->all_output_act = new bit_set_t(act_count); for (int i = 0; i < aut->states.size(); i++) { coin_state_t * cst = aut->states[i]; cst->enAp = new bit_set_t(act_count); cst->input_act = new bit_set_t(act_count); cst->output_act = new bit_set_t(act_count); for (vector::iterator j = cst->outtrans.begin(); j != cst->outtrans.end(); j++) { // this is probably not optimal int act_id = (*j)->label.act_id; if (int_Ap.find(act_id) != int_Ap.end()) { cst->enAp->insert(act_id); } if ((*j)->label.fromc_id == -1) { // input aut->all_input_act->insert((*j)->label.act_id); cst->input_act->insert((*j)->label.act_id); } else if ((*j)->label.toc_id == -1) { // output aut->all_output_act->insert((*j)->label.act_id); cst->output_act->insert((*j)->label.act_id); } } } // second, compare enAp for all transitions' from and to states for (int i = 0; i < aut->states.size(); i++) { coin_state_t * cst = aut->states[i]; for (vector::iterator j = cst->outtrans.begin(); j != cst->outtrans.end(); j++) { coin_state_t * cst2 = aut->states[ (*j)->tostate_id ]; if (*(cst->enAp) != *(cst2->enAp)) { cst->visible_trans_to.insert((*j)->tostate_id); } } } } } } void coin_system_t::accept_start() { acc_states = true; } void coin_system_t::prop_trans_begin(name_t f, name_t t) { int from = property->prop_states.find_id(f); if (from == -1) { yyerror("property: transition's 'from' state not declared"); exit(1); } int to = property->prop_states.find_id(t); if (to == -1) { yyerror("property: transition's 'to' state not declared"); exit(1); } prop_trans_t * tmp = new prop_trans_t; tmp->tostate_id = to; (property->prop_states.get(from))->outtrans.push_back(tmp); property->act_trans = tmp; } void coin_system_t::add_guard(label_t const & l, bool type) { // insert label into Ap' (interesting atomic propositions) int_Ap.insert(l.act_id); // this is overapproximation of c(Ap') // ------ if (act_prop && property->act_trans != NULL) { if (type) { property->act_trans->guard_true.insert(l); } else { property->act_trans->guard_false.insert(l); } } } symtable * coin_system_t::get_automata_list() { return &automata; }