diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index cfd20f356..6d55e5111 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -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(); } diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc index 864442c6a..87f5afb7f 100644 --- a/src/ltlvisit/consterm.cc +++ b/src/ltlvisit/consterm.cc @@ -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; } } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 54d8c808c..b4dfec499 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -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(f) + || dynamic_cast(f)); + res_ = !recurse(f) & next_to_concat(); + return; + } case unop::Star: { formula* f; diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index d073675dd..bb77e43af 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -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).