diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 66a3ed592..3f4476ffd 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -24,6 +24,8 @@ #include #include #include "constant.hh" +#include "unop.hh" +#include "ltlvisit/kind.hh" namespace spot { @@ -107,6 +109,8 @@ namespace spot { switch (op_) { + case Equal: + return "Equal"; case Star: return "Star"; } @@ -120,14 +124,22 @@ namespace spot { std::ostringstream out; - // Syntactic sugaring - if (min_ == 1 && max_ == unbounded) + switch (op_) { - out << "[+]"; - return out.str(); + case Star: + // Syntactic sugaring + if (min_ == 1 && max_ == unbounded) + { + out << "[+]"; + return out.str(); + } + out << "[*"; + break; + case Equal: + out << "[="; + break; } - out << "[*"; if (min_ != 0 || max_ != unbounded) { out << min_; @@ -151,73 +163,115 @@ namespace spot // Some trivial simplifications. - // - [*0][*min..max] = [*0] - if (child == constant::empty_word_instance()) - return child; - - // - 0[*0..max] = [*0] - // - 0[*min..max] = 0 if min > 0 - if (child == constant::false_instance()) + switch (op) { - if (min == 0) - return constant::empty_word_instance(); - else - return child; - } + case Equal: + { + // - 0[=0..max] = [*] + // - 0[=min..max] = 0 if min > 0 + if (child == constant::false_instance()) + { + if (min == 0) + { + max = -1U; + op = Star; + child = constant::true_instance(); + break; + } + else + return child; + } + // - 1[=0] = [*0] + // - 1[=min..max] = 1[*min..max] + if (child == constant::true_instance()) + { + if (max == 0) + return constant::empty_word_instance(); + else + { + op = Star; + break; + } + } + // - Exp[=0] = (!Exp)[*] + if (max == 0) + return bunop::instance(bunop::Star, + unop::instance(unop::Not, child)); + break; + } + case Star: + { + // - [*0][*min..max] = [*0] + if (child == constant::empty_word_instance()) + return child; - // - Exp[*0..0] = [*0] - if (max == 0) - { - child->destroy(); - return constant::empty_word_instance(); - } + // - 0[*0..max] = [*0] + // - 0[*min..max] = 0 if min > 0 + if (child == constant::false_instance()) + { + if (min == 0) + return constant::empty_word_instance(); + else + return child; + } - // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] if i*(min+1)<=j(min)+1. - bunop* s = dynamic_cast(child); - if (s) - { - unsigned i = s->min(); - unsigned j = s->max(); + // - Exp[*0] = [*0] + if (max == 0) + { + child->destroy(); + return constant::empty_word_instance(); + } - // Exp has to be true between i*min and j*min - // then between i*(min+1) and j*(min+1) - // ... - // finally between i*max and j*max - // - // We can merge these intervals into [i*min..j*max] iff the - // first are adjacent or overlap, i.e. iff - // i*(min+1) <= j*min+1. - // (Because i<=j, this entails that the other intervals also - // overlap). + // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] + // if i*(min+1)<=j(min)+1. + bunop* s = dynamic_cast(child); + if (s) + { + unsigned i = s->min(); + unsigned j = s->max(); - formula* exp = s->child(); - if (j == unbounded) - { - min *= i; - max = unbounded; + // Exp has to be true between i*min and j*min + // then between i*(min+1) and j*(min+1) + // ... + // finally between i*max and j*max + // + // We can merge these intervals into [i*min..j*max] iff the + // first are adjacent or overlap, i.e. iff + // i*(min+1) <= j*min+1. + // (Because i<=j, this entails that the other intervals also + // overlap). - // Exp[*min..max] - exp->clone(); - child->destroy(); - child = exp; - } - else - { - if (i * (min + 1) <= (j * min) + 1) - { - min *= i; - if (max != unbounded) - { - if (j == unbounded) - max = unbounded; - else - max *= j; - } - exp->clone(); - child->destroy(); - child = exp; - } - } + formula* exp = s->child(); + if (j == unbounded) + { + min *= i; + max = unbounded; + + // Exp[*min..max] + exp->clone(); + child->destroy(); + child = exp; + } + else + { + if (i * (min + 1) <= (j * min) + 1) + { + min *= i; + if (max != unbounded) + { + if (j == unbounded) + max = unbounded; + else + max *= j; + } + exp->clone(); + child->destroy(); + child = exp; + } + } + } + break; + } } pair p(pairo(op, child), pairu(min, max)); diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 5738c57ad..e1bbd6ddc 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -37,7 +37,7 @@ namespace spot class bunop : public ref_formula { public: - enum type { Star }; + enum type { Star, Equal }; static const unsigned unbounded = -1U; @@ -49,7 +49,13 @@ namespace spot /// - 0[*0..max] = [*0] /// - 0[*min..max] = 0 if min > 0 /// - [*0][*min..max] = [*0] + /// - Exp[*0] = [*0] /// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1. + /// - 0[=0..max] = 1[*] + /// - 0[=min..max] = 0 if min > 0 + /// - 1[=0] = [*0] + /// - 1[=min..max] = 1[*min..max] if max > 0 + /// - Exp[=0] = (!Exp)[*] /// /// These rewriting rules imply that it is not possible to build /// an LTL formula object that is SYNTACTICALLY equal to one of diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 556f1e0a7..7a0a95b67 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -35,6 +35,7 @@ #include #include "public.hh" #include "ltlast/allnodes.hh" +#include "ltlvisit/kind.hh" struct minmax_t { unsigned min, max; }; } @@ -92,9 +93,10 @@ using namespace spot::ltl; %token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator" %token OP_PLUS "plus operator" %token OP_STAR_OPEN "opening bracket for star operator" -%token OP_STAR_CLOSE "closing bracket for star operator" -%token OP_STAR_NUM "number for star operator" -%token OP_STAR_SEP "separator for star operator" +%token OP_EQUAL_OPEN "opening bracket for equal operator" +%token OP_SQBKT_CLOSE "closing bracket" +%token OP_SQBKT_NUM "number for square bracket operator" +%token OP_SQBKT_SEP "separator for square bracket operator" %token OP_UCONCAT "universal concat operator" %token OP_ECONCAT "existential concat operator" %token OP_UCONCAT_NONO "universal non-overlapping concat operator" @@ -124,7 +126,7 @@ using namespace spot::ltl; %nonassoc OP_X /* High priority regex operator. */ -%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS +%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN /* Not has the most important priority after Wring's `=0' and `=1'. */ %nonassoc OP_NOT @@ -133,7 +135,7 @@ using namespace spot::ltl; %type subformula booleanatom rationalexp %type bracedrationalexp parenthesedsubformula -%type starargs +%type starargs equalargs sqbracketargs %destructor { delete $$; } %destructor { $$->destroy(); } @@ -187,24 +189,27 @@ enderror: error END_OF_INPUT } -OP_STAR_SEP_opt: | OP_STAR_SEP +OP_SQBKT_SEP_opt: | OP_SQBKT_SEP error_opt: | error +sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE + { $$.min = $1; $$.max = $3; } + | OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_CLOSE + { $$.min = $1; $$.max = bunop::unbounded; } + | OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE + { $$.min = 0U; $$.max = $2; } + | OP_SQBKT_SEP_opt OP_SQBKT_CLOSE + { $$.min = 0U; $$.max = bunop::unbounded; } + | OP_SQBKT_NUM OP_SQBKT_CLOSE + { $$.min = $$.max = $1; } + starargs: OP_STAR { $$.min = 0U; $$.max = bunop::unbounded; } | OP_PLUS { $$.min = 1U; $$.max = bunop::unbounded; } - | OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE - { $$.min = $2; $$.max = $4; } - | OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_CLOSE - { $$.min = $2; $$.max = bunop::unbounded; } - | OP_STAR_OPEN OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE - { $$.min = 0U; $$.max = $3; } - | OP_STAR_OPEN OP_STAR_SEP_opt OP_STAR_CLOSE - { $$.min = 0U; $$.max = bunop::unbounded; } - | OP_STAR_OPEN OP_STAR_NUM OP_STAR_CLOSE - { $$.min = $$.max = $2; } - | OP_STAR_OPEN error OP_STAR_CLOSE + | OP_STAR_OPEN sqbracketargs + { $$ = $2; } + | OP_STAR_OPEN error OP_SQBKT_CLOSE { error_list.push_back(parse_error(@$, "treating this star block as [*]")); $$.min = 0U; $$.max = bunop::unbounded; } @@ -213,6 +218,17 @@ starargs: OP_STAR "missing closing bracket for star")); $$.min = $$.max = 0U; } +equalargs: OP_EQUAL_OPEN sqbracketargs + { $$ = $2; } + | OP_EQUAL_OPEN error OP_SQBKT_CLOSE + { error_list.push_back(parse_error(@$, + "treating this star block as [*]")); + $$.min = 0U; $$.max = bunop::unbounded; } + | OP_EQUAL_OPEN error_opt END_OF_INPUT + { error_list.push_back(parse_error(@$, + "missing closing bracket for star")); + $$.min = $$.max = 0U; } + /* The reason we use `constant::false_instance()' for error recovery is that it isn't reference counted. (Hence it can't leak references.) */ @@ -323,6 +339,22 @@ rationalexp: booleanatom | starargs { $$ = bunop::instance(bunop::Star, constant::true_instance(), $1.min, $1.max); } + | rationalexp equalargs + { + if ((kind_of($1) & Boolean_Kind) == Boolean_Kind) + { + $$ = bunop::instance(bunop::Equal, $1, $2.min, $2.max); + } + else + { + error_list.push_back(parse_error(@1, + "not a boolean expression: [=...] can only " + "be applied to a boolean expression")); + error_list.push_back(parse_error(@$, + "treating this block as false")); + $$ = constant::false_instance(); + } + } bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE { $$ = $2; } diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 9a1a315c9..4aa269089 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -59,7 +59,7 @@ flex_set_buffer(const char* buf, int start_tok) %} %s not_prop -%x star +%x sqbracket %% @@ -96,14 +96,15 @@ flex_set_buffer(const char* buf, int start_tok) ":" BEGIN(0); return token::OP_FUSION; "*"|"[*]" BEGIN(0); return token::OP_STAR; "[+]" BEGIN(0); return token::OP_PLUS; -"[*" BEGIN(star); return token::OP_STAR_OPEN; -"]" BEGIN(0); return token::OP_STAR_CLOSE; -[0-9]+ { +"[*" BEGIN(sqbracket); return token::OP_STAR_OPEN; +"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN; +"]" BEGIN(0); return token::OP_SQBKT_CLOSE; +[0-9]+ { unsigned num = 0; try { num = boost::lexical_cast(yytext); yylval->num = num; - return token::OP_STAR_NUM; + return token::OP_SQBKT_NUM; } catch (boost::bad_lexical_cast &) { @@ -114,7 +115,7 @@ flex_set_buffer(const char* buf, int start_tok) yylloc->step(); } } -","|".." return token::OP_STAR_SEP; +","|".." return token::OP_SQBKT_SEP; /* & and | come from Spin. && and || from LTL2BA. diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index a2cc0f48b..439a27daf 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -139,3 +139,14 @@ run 0 ../equals '{a[+][*1..3]}' '{a[+]}' run 0 ../equals '{a[*1..3][+]}' '{a[+]}' run 0 ../equals '{[*2][+]}' '{[*2][+]}' run 0 ../equals '{[+][*2]}' '{[*2..]}' + +run 0 ../equals '{0[=2]}' '0' +run 0 ../equals '{0[=2..]}' '0' +run 0 ../equals '{0[=1..10]}' '0' +run 0 ../equals '{0[=0]}' '{[*]}' +run 0 ../equals '{0[=0..10]}' '{*}' +run 0 ../equals '{0[=0..]}' '{*}' +run 0 ../equals '{1[=0]}' '{[*0]}' +run 0 ../equals '{1[=1..2]}' '{[*1..2]}' +run 0 ../equals '{1[=..4]}' '{1[*..4]}' +run 0 ../equals '{b[=0]}' '{(!b)[*]}' diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index cdfce762d..384b8a40d 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -233,6 +233,9 @@ namespace spot std::ostream& trace_ltl_bdd(const translate_dict& d, bdd f) { + std::cerr << "Displaying BDD "; + bdd_print_set(std::cerr, d.dict, f) << ":" << std::endl; + minato_isop isop(f); bdd cube; while ((cube = isop.next()) != bddfalse) @@ -318,7 +321,7 @@ namespace spot bdd next_to_concat() { if (!to_concat_) - to_concat_ = constant::empty_word_instance(); + return bddtrue; int x = dict_.register_next_variable(to_concat_); return bdd_ithvar(x); } @@ -391,6 +394,9 @@ namespace spot formula* f; unsigned min = bo->min(); unsigned max = bo->max(); + + assert(max > 0); + unsigned min2 = (min == 0) ? 0 : (min - 1); unsigned max2 = (max == bunop::unbounded) ? bunop::unbounded : (max - 1); @@ -407,7 +413,36 @@ namespace spot res_ = recurse(bo->child(), f); if (min == 0) res_ |= now_to_concat(); + return; + case bunop::Equal: + { + // b[=min..max] == (!b;b[=min..max]) | (b;b[=min-1..max-1]) + // b[=0..max] == [*0] | (!b;b[=0..max]) | (b;b[=0..max-1]) + // Note: b[=0] == (!b)[*] is a trivial identity, so it will + // never occur here. + + formula* f1 = // !b;b[min..max] + multop::instance(multop::Concat, + unop::instance(unop::Not, + bo->child()->clone()), + bo->clone()); + + formula* f2 = // b;b[=min-1..max-1] + multop::instance(multop::Concat, + bo->child()->clone(), + bunop::instance(bunop::Equal, + bo->child()->clone(), + min2, max2)); + f = multop::instance(multop::Or, f1, f2); + + res_ = recurse_and_concat(f); + + f->destroy(); + if (min == 0) + res_ |= now_to_concat(); + return; + } } /* Unreachable code. */ assert(0); diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index e040f9b19..5e3d0fe2b 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -87,6 +87,12 @@ check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c' # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). check_psl '{[*];req;ack}|=>{start;busy[*];done}' +# Examples from "Property-by-Example Guide: a Handbook of PSL Examples" +# by Ben David and Orni (2005)/ +check_psl '{end[=3]}(false)' # 2.27.A +check_psl '{[*]; {read[=3]} && {write[=2]}} |=> + {(!read && !write)[*]; ready}' # 3.5.A + # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization.