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

Relax usage of ->, <->, and xor in SERE.

Browse source 
* src/ltlparse/ltlparse.yy (rationalexp): Allow ->, <->, and xor,
in rational expressions as long as they apply only to Boolean
formulae.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Adjust
assert in handling of unop::Not.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-13 22:29:35 +01:00
parent 8cafa200a5
commit eab91aab68
2 changed files with 111 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

118
src/ltlparse/ltlparse.yy
View file

@ -1,4 +1,4 @@
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement /* Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
** de l'Epita (LRDE). ** de l'Epita (LRDE).
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -236,7 +236,7 @@ starargs: OP_STAR
{ $$ = $2; } { $$ = $2; }
| OP_STAR_OPEN error OP_SQBKT_CLOSE | OP_STAR_OPEN error OP_SQBKT_CLOSE
{ error_list.push_back(parse_error(@$, { error_list.push_back(parse_error(@$,
"treating this star block as [*]")); "treating this star block as [*]"));
$$.min = 0U; $$.max = bunop::unbounded; } $$.min = 0U; $$.max = bunop::unbounded; }
| OP_STAR_OPEN error_opt END_OF_INPUT | OP_STAR_OPEN error_opt END_OF_INPUT
{ error_list.push_back(parse_error(@$, { error_list.push_back(parse_error(@$,
@ -247,7 +247,7 @@ equalargs: OP_EQUAL_OPEN sqbracketargs
{ $$ = $2; } { $$ = $2; }
| OP_EQUAL_OPEN error OP_SQBKT_CLOSE | OP_EQUAL_OPEN error OP_SQBKT_CLOSE
{ error_list.push_back(parse_error(@$, { error_list.push_back(parse_error(@$,
"treating this equal block as [*]")); "treating this equal block as [*]"));
$$.min = 0U; $$.max = bunop::unbounded; } $$.min = 0U; $$.max = bunop::unbounded; }
| OP_EQUAL_OPEN error_opt END_OF_INPUT | OP_EQUAL_OPEN error_opt END_OF_INPUT
{ error_list.push_back(parse_error(@$, { error_list.push_back(parse_error(@$,
@ -316,8 +316,23 @@ booleanatom: ATOMIC_PROP
{ $$ = constant::false_instance(); } { $$ = constant::false_instance(); }
rationalexp: booleanatom rationalexp: booleanatom
| OP_NOT booleanatom | OP_NOT rationalexp
{ $$ = unop::instance(unop::Not, $2); } {
if ($2->is_boolean())
{
$$ = unop::instance(unop::Not, $2);
}
else
{
error_list.push_back(parse_error(@2,
"not a boolean expression: inside a SERE `!' can only "
"be applied to a Boolean expression"));
error_list.push_back(parse_error(@$,
"treating this block as false"));
$2->destroy();
$$ = constant::false_instance();
}
}
| bracedrationalexp | bracedrationalexp
| PAR_OPEN rationalexp PAR_CLOSE | PAR_OPEN rationalexp PAR_CLOSE
{ $$ = $2; } { $$ = $2; }
@ -373,10 +388,10 @@ rationalexp: booleanatom
else else
{ {
error_list.push_back(parse_error(@1, error_list.push_back(parse_error(@1,
"not a boolean expression: [=...] can only " "not a boolean expression: [=...] can only "
"be applied to a boolean expression")); "be applied to a Boolean expression"));
error_list.push_back(parse_error(@$, error_list.push_back(parse_error(@$,
"treating this block as false")); "treating this block as false"));
$1->destroy(); $1->destroy();
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
@ -390,14 +405,95 @@ rationalexp: booleanatom
else else
{ {
error_list.push_back(parse_error(@1, error_list.push_back(parse_error(@1,
"not a boolean expression: [->...] can only " "not a boolean expression: [->...] can only "
"be applied to a boolean expression")); "be applied to a Boolean expression"));
error_list.push_back(parse_error(@$, error_list.push_back(parse_error(@$,
"treating this block as false")); "treating this block as false"));
$1->destroy(); $1->destroy();
$$ = constant::false_instance(); $$ = constant::false_instance();
} }
} }
| rationalexp OP_XOR rationalexp
{
if ($1->is_boolean() && $3->is_boolean())
{
$$ = binop::instance(binop::Xor, $1, $3);
}
else
{
if (!$1->is_boolean())
{
error_list.push_back(parse_error(@1,
"not a boolean expression: inside SERE `<->' can only "
"be applied to Boolean expressions"));
}
if (!$3->is_boolean())
{
error_list.push_back(parse_error(@3,
"not a boolean expression: inside SERE `<->' can only "
"be applied to Boolean expressions"));
}
error_list.push_back(parse_error(@$,
"treating this block as false"));
$1->destroy();
$3->destroy();
$$ = constant::false_instance();
}
}
| rationalexp OP_XOR error
{ missing_right_binop($$, $1, @2, "xor operator"); }
| rationalexp OP_IMPLIES rationalexp
{
if ($1->is_boolean())
{
$$ = binop::instance(binop::Implies, $1, $3);
}
else
{
if (!$1->is_boolean())
{
error_list.push_back(parse_error(@1,
"not a boolean expression: inside SERE `->' can only "
"be applied to a Boolean expression"));
}
error_list.push_back(parse_error(@$,
"treating this block as false"));
$1->destroy();
$3->destroy();
$$ = constant::false_instance();
}
}
| rationalexp OP_IMPLIES error
{ missing_right_binop($$, $1, @2, "implication operator"); }
| rationalexp OP_EQUIV rationalexp
{
if ($1->is_boolean() && $3->is_boolean())
{
$$ = binop::instance(binop::Equiv, $1, $3);
}
else
{
if (!$1->is_boolean())
{
error_list.push_back(parse_error(@1,
"not a boolean expression: inside SERE `<->' can only "
"be applied to Boolean expressions"));
}
if (!$3->is_boolean())
{
error_list.push_back(parse_error(@3,
"not a boolean expression: inside SERE `<->' can only "
"be applied to Boolean expressions"));
}
error_list.push_back(parse_error(@$,
"treating this block as false"));
$1->destroy();
$3->destroy();
$$ = constant::false_instance();
}
}
| rationalexp OP_EQUIV error
{ missing_right_binop($$, $1, @2, "equivalent operator"); }
bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE
{ $$ = $2; } { $$ = $2; }

8
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
@ -397,11 +397,11 @@ namespace spot
return; return;
case unop::Not: case unop::Not:
{ {
// Not can only appear in front of constants or atomic // Not can only appear in front of Boolean
// expressions.
// propositions. // propositions.
const formula* f = node->child(); const formula* f = node->child();
assert(dynamic_cast<const atomic_prop*>(f) assert(f->is_boolean());
|| dynamic_cast<const constant*>(f));
res_ = recurse_and_concat(f, true); res_ = recurse_and_concat(f, true);
return; return;
} }