diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index f1e8f185f..86ea5f511 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -1415,8 +1415,17 @@ lbtt-guard: STRING } else { - res.cur_label = - formula_to_bdd(f, res.h->aut->get_dict(), res.h->aut); + if (!f->is_boolean()) + { + error(@$, + "non-Boolean transition label (replaced by true)"); + res.cur_label = bddtrue; + } + else + { + res.cur_label = + formula_to_bdd(f, res.h->aut->get_dict(), res.h->aut); + } f->destroy(); } delete $1; diff --git a/src/tests/hoaparse.test b/src/tests/hoaparse.test index f1a010e32..f9d39d818 100755 --- a/src/tests/hoaparse.test +++ b/src/tests/hoaparse.test @@ -86,6 +86,17 @@ State: 1 {0} 1 0 2 0 -1 t -1 +/* Another automaton. Here we make sure that guard must + be Boolean, even though we the LBT parser we use + would accept LTL. */ +2 1t +0 1 +1 -1 G "b" +0 -1 & "a" ! "b" +-1 +1 0 +0 0 -1 t +-1 EOF diff='different state numbers have been used' @@ -97,6 +108,7 @@ input:2.1-9: ... declared here. input:10.5: state number is larger than state count... input:2.1-9: ... declared here. input:12.1-19.2: 2 states have been declared, but 3 $diff +input:25.5-10: non-Boolean transition label (replaced by true) EOF cat >input <