diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy index 4d356964c..ad599d310 100644 --- a/src/dstarparse/dstarparse.yy +++ b/src/dstarparse/dstarparse.yy @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -** de l'Epita (LRDE). +** Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. ** @@ -34,34 +34,37 @@ #include "ltlast/constant.hh" #include "public.hh" - typedef std::map map_t; - - struct result_ + inline namespace dstaryy { - spot::dstar_aut_ptr d; - spot::ltl::environment* env; - std::vector guards; - std::vector::const_iterator cur_guard; - map_t dest_map; - int cur_state; + typedef std::map map_t; - unsigned state_count = 0; - unsigned start_state = 0; - std::vector aps; - - bool state_count_seen:1; - bool accpair_count_seen:1; - bool start_state_seen:1; - bool aps_seen:1; - - result_(): - state_count_seen(false), - accpair_count_seen(false), - start_state_seen(false), - aps_seen(false) + struct result_ { - } - }; + spot::dstar_aut_ptr d; + spot::ltl::environment* env; + std::vector guards; + std::vector::const_iterator cur_guard; + map_t dest_map; + int cur_state; + + unsigned state_count = 0; + unsigned start_state = 0; + std::vector aps; + + bool state_count_seen:1; + bool accpair_count_seen:1; + bool start_state_seen:1; + bool aps_seen:1; + + result_(): + state_count_seen(false), + accpair_count_seen(false), + start_state_seen(false), + aps_seen(false) + { + } + }; + } } %parse-param {spot::dstar_parse_error_list& error_list} diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index b4a58a466..dabe20e36 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -40,76 +40,79 @@ #include "priv/accmap.hh" #include "ltlparse/public.hh" - /* Cache parsed formulae. Labels on arcs are frequently identical - and it would be a waste of time to parse them to formula* over and - over, and to register all their atomic_propositions in the - bdd_dict. Keep the bdd result around so we can reuse it. */ - typedef std::map formula_cache; - - typedef std::pair pair; - typedef typename spot::tgba_digraph::namer::type named_tgba_t; - - // Note: because this parser is meant to be used on a stream of - // automata, it tries hard to recover from errors, so that we get a - // chance to reach the end of the current automaton in order to - // process the next one. Several variables below are used to keep - // track of various error conditions. - enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels, - Implicit_Labels }; - - struct result_ + inline namespace hoayy { - spot::hoa_aut_ptr h; - spot::ltl::environment* env; - formula_cache fcache; - named_tgba_t* namer = nullptr; - spot::acc_mapper_int* acc_mapper = nullptr; - std::vector ap; - std::vector guards; - std::vector::const_iterator cur_guard; - std::vector declared_states; // States that have been declared. - std::vector> start; // Initial states; - std::unordered_map alias; - std::unordered_map props; - spot::location states_loc; - spot::location ap_loc; - spot::location state_label_loc; - spot::location accset_loc; - spot::acc_cond::mark_t acc_state; - spot::acc_cond::mark_t neg_acc_sets = 0U; - spot::acc_cond::mark_t pos_acc_sets = 0U; - unsigned cur_state; - int states = -1; - int ap_count = -1; - int accset = -1; - bdd state_label; - bdd cur_label; - bool has_state_label = false; - bool ignore_more_ap = false; // Set to true after the first "AP:" - // line has been read. - bool ignore_acc = false; // Set to true in case of missing - // Acceptance: lines. - bool ignore_acc_silent = false; - bool ignore_more_acc = false; // Set to true after the first - // "Acceptance:" line has been read. + /* Cache parsed formulae. Labels on arcs are frequently identical + and it would be a waste of time to parse them to formula* over and + over, and to register all their atomic_propositions in the + bdd_dict. Keep the bdd result around so we can reuse it. */ + typedef std::map formula_cache; - label_style_t label_style = Mixed_Labels; + typedef std::pair pair; + typedef typename spot::tgba_digraph::namer::type named_tgba_t; - bool accept_all_needed = false; - bool accept_all_seen = false; - bool aliased_states = false; + // Note: because this parser is meant to be used on a stream of + // automata, it tries hard to recover from errors, so that we get a + // chance to reach the end of the current automaton in order to + // process the next one. Several variables below are used to keep + // track of various error conditions. + enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels, + Implicit_Labels }; - bool deterministic = false; - bool complete = false; - - std::map labels; - - ~result_() + struct result_ { - delete namer; - delete acc_mapper; - } - }; + spot::hoa_aut_ptr h; + spot::ltl::environment* env; + formula_cache fcache; + named_tgba_t* namer = nullptr; + spot::acc_mapper_int* acc_mapper = nullptr; + std::vector ap; + std::vector guards; + std::vector::const_iterator cur_guard; + std::vector declared_states; // States that have been declared. + std::vector> start; // Initial states; + std::unordered_map alias; + std::unordered_map props; + spot::location states_loc; + spot::location ap_loc; + spot::location state_label_loc; + spot::location accset_loc; + spot::acc_cond::mark_t acc_state; + spot::acc_cond::mark_t neg_acc_sets = 0U; + spot::acc_cond::mark_t pos_acc_sets = 0U; + unsigned cur_state; + int states = -1; + int ap_count = -1; + int accset = -1; + bdd state_label; + bdd cur_label; + bool has_state_label = false; + bool ignore_more_ap = false; // Set to true after the first "AP:" + // line has been read. + bool ignore_acc = false; // Set to true in case of missing + // Acceptance: lines. + bool ignore_acc_silent = false; + bool ignore_more_acc = false; // Set to true after the first + // "Acceptance:" line has been read. + + label_style_t label_style = Mixed_Labels; + + bool accept_all_needed = false; + bool accept_all_seen = false; + bool aliased_states = false; + + bool deterministic = false; + bool complete = false; + + std::map labels; + + ~result_() + { + delete namer; + delete acc_mapper; + } + }; + } } %parse-param {spot::hoa_parse_error_list& error_list}