From da74b4f1800e41af2bc62285439c6d33bc37d54e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 15 Oct 2010 11:41:18 +0200 Subject: [PATCH] Introduce [->min..max] operator. * src/ltlast/bunop.hh: Declare bunop::Goto * src/ltlast/bunop.cc: Handle it. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Add rules for [->min..max]. * src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Goto in the translation. * src/ltltest/equals.test: Test trivial identities. * src/tgbatest/ltl2tgba.test: Test two more formulae using [->]. --- src/ltlast/bunop.cc | 65 +++++++++++++++++++++++++++++++++++- src/ltlast/bunop.hh | 7 +++- src/ltlparse/ltlparse.yy | 50 ++++++++++++++++++++++++--- src/ltlparse/ltlscan.ll | 1 + src/ltltest/equals.test | 9 +++++ src/tgbaalgos/ltl2tgba_fm.cc | 14 +++++--- src/tgbatest/ltl2tgba.test | 3 ++ 7 files changed, 138 insertions(+), 11 deletions(-) diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 02a49c9bc..19539c97f 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -113,6 +113,8 @@ namespace spot return "Equal"; case Star: return "Star"; + case Goto: + return "Goto"; } // Unreachable code. assert(0); @@ -124,6 +126,9 @@ namespace spot { std::ostringstream out; + unsigned default_min = 0; + unsigned default_max = unbounded; + switch (op_) { case Star: @@ -138,10 +143,36 @@ namespace spot case Equal: out << "[="; break; + case Goto: + out << "[->"; + default_min = 1; + default_max = 1; + break; } - if (min_ != 0 || max_ != unbounded) + // Beware that the default parameters of the Goto operator are + // not the same as Star or Equal: + // + // [->] = [->1..1] + // [->..] = [->1..unbounded] + // [*] = [*0..unbounded] + // [*..] = [*0..unbounded] + // [=] = [=0..unbounded] + // [=..] = [=0..unbounded] + // + // Strictly speaking [=] is not specified by PSL, and anyway we + // automatically rewrite Exp[=0..unbounded] as + // Exp[*0..unbounded], so we should never have to print [=] + // here. + // + // Also + // [*..] = [*0..unbounded] + + if (min_ != default_min || max_ != default_max) { + // Always print the min_, even when it is equal to + // default_min, this way we avoid ambiguities (like + // when reading [*..3] near [*->..2]) out << min_; if (min_ != max_) { @@ -208,6 +239,38 @@ namespace spot unop::instance(unop::Not, child)); break; } + case Goto: + { + // - 0[->min..max] = 0 if min>0 + // - 0[->0..max] = [*0] + if (child == constant::false_instance()) + { + if (min == 0) + return constant::empty_word_instance(); + 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] = [*0] + if (max == 0) + { + child->destroy(); + return constant::empty_word_instance(); + } + break; + } case Star: { // - [*0][*min..max] = [*0] diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 84038bff9..d3f1a74e6 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, Equal }; + enum type { Star, Equal, Goto }; static const unsigned unbounded = -1U; @@ -57,6 +57,11 @@ namespace spot /// - 1[=min..max] = 1[*min..max] if max > 0 /// - Exp[=0..] = [*] /// - Exp[=0] = (!Exp)[*] + /// - 0[->min..max] = 0 if min>0 + /// - 0[->0..max] = [*0] + /// - 1[->0] = [*0] + /// - 1[->min..max] = 1[*min..max] + /// - Exp[->0] = [*0] /// /// 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 7a0a95b67..a1bd5e6de 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -94,6 +94,7 @@ using namespace spot::ltl; %token OP_PLUS "plus operator" %token OP_STAR_OPEN "opening bracket for star operator" %token OP_EQUAL_OPEN "opening bracket for equal operator" +%token OP_GOTO_OPEN "opening bracket for goto 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" @@ -126,7 +127,7 @@ using namespace spot::ltl; %nonassoc OP_X /* High priority regex operator. */ -%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN +%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN OP_GOTO_OPEN /* Not has the most important priority after Wring's `=0' and `=1'. */ %nonassoc OP_NOT @@ -135,7 +136,7 @@ using namespace spot::ltl; %type subformula booleanatom rationalexp %type bracedrationalexp parenthesedsubformula -%type starargs equalargs sqbracketargs +%type starargs equalargs sqbracketargs gotoargs %destructor { delete $$; } %destructor { $$->destroy(); } @@ -192,6 +193,7 @@ enderror: error END_OF_INPUT OP_SQBKT_SEP_opt: | OP_SQBKT_SEP error_opt: | error +/* for [*i..j] and [=i..j] */ 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 @@ -203,6 +205,28 @@ sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_SQBKT_NUM OP_SQBKT_CLOSE { $$.min = $$.max = $1; } +/* [->i..j] has default values that are different than [*] and [=]. */ +gotoargs: OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE + { $$.min = $2; $$.max = $4; } + | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_CLOSE + { $$.min = $2; $$.max = bunop::unbounded; } + | OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE + { $$.min = 1U; $$.max = $3; } + | OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_CLOSE + { $$.min = 1U; $$.max = bunop::unbounded; } + | OP_GOTO_OPEN OP_SQBKT_CLOSE + { $$.min = $$.max = 1U; } + | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_CLOSE + { $$.min = $$.max = $2; } + | OP_GOTO_OPEN error OP_SQBKT_CLOSE + { error_list.push_back(parse_error(@$, + "treating this goto block as [->]")); + $$.min = $$.max = 1U; } + | OP_GOTO_OPEN error_opt END_OF_INPUT + { error_list.push_back(parse_error(@$, + "missing closing bracket for goto operator")); + $$.min = $$.max = 0U; } + starargs: OP_STAR { $$.min = 0U; $$.max = bunop::unbounded; } | OP_PLUS @@ -222,11 +246,11 @@ equalargs: OP_EQUAL_OPEN sqbracketargs { $$ = $2; } | OP_EQUAL_OPEN error OP_SQBKT_CLOSE { error_list.push_back(parse_error(@$, - "treating this star block as [*]")); + "treating this equal 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")); + "missing closing bracket for equal operator")); $$.min = $$.max = 0U; } @@ -352,6 +376,24 @@ rationalexp: booleanatom "be applied to a boolean expression")); error_list.push_back(parse_error(@$, "treating this block as false")); + $1->destroy(); + $$ = constant::false_instance(); + } + } + | rationalexp gotoargs + { + if ((kind_of($1) & Boolean_Kind) == Boolean_Kind) + { + $$ = bunop::instance(bunop::Goto, $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")); + $1->destroy(); $$ = constant::false_instance(); } } diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 4aa269089..4fde032b7 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -98,6 +98,7 @@ flex_set_buffer(const char* buf, int start_tok) "[+]" BEGIN(0); return token::OP_PLUS; "[*" BEGIN(sqbracket); return token::OP_STAR_OPEN; "[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN; +"[->" BEGIN(sqbracket); return token::OP_GOTO_OPEN; "]" BEGIN(0); return token::OP_SQBKT_CLOSE; [0-9]+ { unsigned num = 0; diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index 883d832fc..1e0c4055e 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -151,3 +151,12 @@ run 0 ../equals '{1[=1..2]}' '{[*1..2]}' run 0 ../equals '{1[=..4]}' '{1[*..4]}' run 0 ../equals '{b[=0]}' '{(!b)[*]}' run 0 ../equals '{b[=0..]}' '{*}' + +run 0 ../equals '{0[->10..100];b}' '0' +run 0 ../equals '{0[->1..];b}' '0' +run 0 ../equals '{0[->0..100];b}' '{b}' +run 0 ../equals '{0[->0..];b}' '{b}' +run 0 ../equals '{1[->0];b}' '{b}' +run 0 ../equals '{1[->10,20];b}' '{[*10..20];b}' +run 0 ../equals '{1[->..];b}' '{[*1..];b}' +run 0 ../equals '{{a&!c}[->0];b}' '{b}' diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 384b8a40d..5cee57662 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -416,28 +416,32 @@ namespace spot return; case bunop::Equal: + case bunop::Goto: { // 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] + // 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] == [*0] is a trivial identity, so it will + // never occur here. + + formula* f1 = // !b;b[=min..max] or !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] + formula* f2 = // b;b[=min-1..max-1] or b;b[->min-1..max-1] multop::instance(multop::Concat, bo->child()->clone(), - bunop::instance(bunop::Equal, + bunop::instance(op, 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(); diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 5e3d0fe2b..d8486213a 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -84,6 +84,7 @@ check_psl '{(a* & (c;b*) & d);e}' check_psl '{[*2];a[*2..4]}|->b' check_psl '{a[*2..5] && b[*..3]}|->c' check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c' +check_psl '{(a[->3]) & {[+];b}}<>->c' # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). check_psl '{[*];req;ack}|=>{start;busy[*];done}' @@ -92,6 +93,8 @@ check_psl '{[*];req;ack}|=>{start;busy[*];done}' check_psl '{end[=3]}(false)' # 2.27.A check_psl '{[*]; {read[=3]} && {write[=2]}} |=> {(!read && !write)[*]; ready}' # 3.5.A +check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp; + {status_valid[->]} && {stop[=0]; true}} |-> {!data_out}' # 2.33 # Make sure 'a U (b U c)' has 3 states and 6 transitions,