formula opt_dest
%type transition src_dest
%type transitions transition_block
%type ident_list
%destructor { delete $$; }
%destructor { $$->first->destroy(); delete $$->second; delete $$; }
%destructor {
for (std::list::iterator i = $$->begin();
i != $$->end(); ++i)
{
i->first->destroy();
delete i->second;
}
delete $$;
}
%printer {
if ($$)
debug_stream() << *$$;
else
debug_stream() << "\"\""; }
%%
neverclaim:
"never" '{' states '}'
states:
/* empty */
| state
| states ';' state
| states ';'
ident_list:
IDENT ':'
{
$$ = $1;
}
| ident_list IDENT ':'
{
result->add_state_alias(*$2, *$1);
// Keep any identifier that starts with accept.
if (strncmp("accept", $1->c_str(), 6))
{
delete $1;
$$ = $2;
}
else
{
delete $2;
$$ = $1;
}
}
transition_block:
"if" transitions "fi"
{
$$ = $2;
}
| "do" transitions "od"
{
$$ = $2;
}
state:
ident_list "skip"
{
if (*$1 == "accept_all")
accept_all_seen = true;
spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1);
bool acc = !strncmp("accept", $1->c_str(), 6);
if (acc)
result->add_acceptance_condition(t,
spot::ltl::constant::true_instance());
delete $1;
}
| ident_list { delete $1; }
| ident_list "false" { delete $1; }
| ident_list transition_block
{
std::list::iterator it;
bool acc = !strncmp("accept", $1->c_str(), 6);
for (it = $2->begin(); it != $2->end(); ++it)
{
spot::state_explicit_string::transition* t =
result->create_transition(*$1, *it->second);
result->add_condition(t, it->first);
if (acc)
result
->add_acceptance_condition(t, spot::ltl::constant::true_instance());
}
// Free the list
delete $1;
for (std::list::iterator it = $2->begin();
it != $2->end(); ++it)
delete it->second;
delete $2;
}
transitions:
/* empty */ { $$ = new std::list; }
| transitions transition
{
if ($2)
{
$1->push_back(*$2);
delete $2;
}
$$ = $1;
}
formula: FORMULA | "false" { $$ = new std::string("0"); }
opt_dest:
/* empty */
{
$$ = 0;
}
| "->" "goto" IDENT
{
$$ = $3;
}
| "->" "assert" FORMULA
{
delete $3;
$$ = new std::string("accept_all");
accept_all_needed = true;
}
src_dest: formula opt_dest
{
// If there is no destination, do ignore the transition.
// This happens for instance with
// if
// :: false
// fi
if (!$2)
{
delete $1;
$$ = 0;
}
else
{
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f =
spot::ltl::parse_boolean(*$1, pel, parse_environment,
debug_level(), true);
delete $1;
for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
i != pel.end(); ++i)
{
// Adjust the diagnostic to the current position.
spot::location here = @1;
here.end.line = here.begin.line + i->first.end.line - 1;
here.end.column = here.begin.column + i->first.end.column -1;
here.begin.line += i->first.begin.line - 1;
here.begin.column += i->first.begin.column - 1;
error(here, i->second);
}
$$ = new pair(f, $2);
}
}
transition:
':' ':' "atomic" '{' src_dest '}'
{
$$ = $5;
}
| ':' ':' src_dest
{
$$ = $3;
}
%%
void
neverclaimyy::parser::error(const location_type& location,
const std::string& message)
{
error_list.emplace_back(location, message);
}
namespace spot
{
tgba_explicit_string*
neverclaim_parse(const std::string& name,
neverclaim_parse_error_list& error_list,
bdd_dict* dict,
environment& env,
bool debug)
{
if (neverclaimyyopen(name))
{
error_list.emplace_back(spot::location(),
std::string("Cannot open file ") + name);
return 0;
}
tgba_explicit_string* result = new tgba_explicit_string(dict);
result->declare_acceptance_condition(spot::ltl::constant::true_instance());
neverclaimyy::parser parser(error_list, env, result);
parser.set_debug_level(debug);
parser.parse();
neverclaimyyclose();
if (accept_all_needed && !accept_all_seen)
{
spot::state_explicit_string::transition* t =
result->create_transition("accept_all", "accept_all");
result->add_acceptance_condition
(t, spot::ltl::constant::true_instance());
}
accept_all_needed = false;
accept_all_seen = false;
return result;
}
}
// Local Variables:
// mode: c++
// End: