alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

parseaut: keep track of the format of each parsed automaton

Browse source 
* src/parseaut/public.hh (parsed_aut): Add a type field.
* src/parseaut/parseaut.yy: Fill it.
* src/dstarparse/dstarparse.yy: Use this field instead of
the private enumeration.
This commit is contained in:
Alexandre Duret-Lutz 2015-09-06 17:07:32 +02:00
parent 6079b1dcdf
commit 14c0577650
3 changed files with 11 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/dstarparse/dstarparse.yy
View file

@ -38,12 +38,9 @@
{ {
typedef std::map<int, bdd> map_t; typedef std::map<int, bdd> map_t;
enum dstar_type { Rabin, Streett };
struct result_ struct result_
{ {
spot::parsed_aut_ptr d; spot::parsed_aut_ptr d;
dstar_type type;
spot::ltl::environment* env; spot::ltl::environment* env;
std::vector<bdd> guards; std::vector<bdd> guards;
std::vector<bdd>::const_iterator cur_guard; std::vector<bdd>::const_iterator cur_guard;
@ -128,13 +125,13 @@ opt_eols: | opt_eols EOL
auttype: DRA auttype: DRA
{ {
result.type = Rabin; result.d->type = spot::parsed_aut_type::DRA;
result.plus = 1; result.plus = 1;
result.minus = 0; result.minus = 0;
} }
| DSA | DSA
{ {
result.type = Streett; result.d->type = spot::parsed_aut_type::DSA;
result.plus = 0; result.plus = 0;
result.minus = 1; result.minus = 1;
} }
@ -189,9 +186,9 @@ sizes:
result.accpair_count = $4; result.accpair_count = $4;
result.accpair_count_seen = true; result.accpair_count_seen = true;
result.d->aut->set_acceptance(2 * $4, result.d->aut->set_acceptance(2 * $4,
result.type == Rabin ? result.d->type == spot::parsed_aut_type::DRA
spot::acc_cond::acc_code::rabin($4) : ? spot::acc_cond::acc_code::rabin($4)
spot::acc_cond::acc_code::streett($4)); : spot::acc_cond::acc_code::streett($4));
} }
| sizes STATES opt_eols NUMBER opt_eols | sizes STATES opt_eols NUMBER opt_eols
{ {

7
src/parseaut/parseaut.yy
View file

@ -246,10 +246,9 @@ aut: aut-1 { res.h->loc = @$; YYACCEPT; }
| ENDOFFILE { YYABORT; } | ENDOFFILE { YYABORT; }
| error ENDOFFILE { YYABORT; } | error ENDOFFILE { YYABORT; }
aut-1: hoa aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; }
| never | never { res.h->type = spot::parsed_aut_type::NeverClaim; }
| lbtt | lbtt { res.h->type = spot::parsed_aut_type::LBTT; }
/**********************************************************************/ /**********************************************************************/
/* Rules for HOA */ /* Rules for HOA */

3
src/parseaut/public.hh
View file

@ -43,6 +43,8 @@ namespace spot
struct parse_aut_error_list {}; struct parse_aut_error_list {};
#endif #endif
enum class parsed_aut_type { HOA, NeverClaim, LBTT, DRA, DSA, Unknown };
/// \brief Temporary encoding of an omega automaton produced by /// \brief Temporary encoding of an omega automaton produced by
/// the parser. /// the parser.
struct SPOT_API parsed_aut struct SPOT_API parsed_aut
@ -52,6 +54,7 @@ namespace spot
twa_graph_ptr aut; twa_graph_ptr aut;
bool aborted = false; bool aborted = false;
spot::location loc; spot::location loc;
parsed_aut_type type = parsed_aut_type::Unknown;
}; };
typedef std::shared_ptr<parsed_aut> parsed_aut_ptr; typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;