Commit 4aa82ec7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Allow boolean atoms to be negated in rational expressions.

* src/ltlparse/ltlparse.yy (rationalexp): Recognize "OP_NOT
booleanatom".
* src/ltlvisit/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust.
* src/tgbatest/ltl2tgba.test: Add one test.
parent bbb645e1
......@@ -234,6 +234,8 @@ booleanatom: ATOMIC_PROP
{ $$ = constant::false_instance(); }
rationalexp: booleanatom
| OP_NOT booleanatom
{ $$ = unop::instance(unop::Not, $2); }
| bracedrationalexp
| CONST_EMPTYWORD
{ $$ = constant::empty_word_instance(); }
......
......@@ -76,6 +76,11 @@ namespace spot
switch (uo->op())
{
case unop::Not:
result_ = false;
break;
case unop::Star:
result_ = true;
break;
case unop::X:
case unop::F:
case unop::G:
......@@ -84,9 +89,6 @@ namespace spot
case unop::NegClosure:
assert(!"unsupported operator");
break;
case unop::Star:
result_ = true;
break;
}
}
......
......@@ -364,14 +364,22 @@ namespace spot
{
case unop::F:
case unop::G:
case unop::Not:
case unop::X:
case unop::Finish:
case unop::Closure:
case unop::NegClosure:
break;
assert(!"not a rational operator");
return;
case unop::Not:
{
// Not can only appear in front of constants or atomic
// propositions.
const formula* f = node->child();
assert(dynamic_cast<const atomic_prop*>(f)
|| dynamic_cast<const constant*>(f));
res_ = !recurse(f) & next_to_concat();
return;
}
case unop::Star:
{
formula* f;
......
......@@ -78,7 +78,7 @@ check_psl 'G{(a;b)*}'
check_psl '{a*}[]->{b*}'
check_psl '{a*&b}'
check_psl '{a*&b*}'
check_psl '{((c;b*) & d);e}'
check_psl '{((!c;b*) & d);e}'
check_psl '{(a* & (c;b*) & d);e}'
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
# Ruah, Zarpas (2007).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment