From 0fc0ea3166c4a0bb01f0912b5e3d2426f00f1920 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Apr 2010 10:44:07 +0200 Subject: [PATCH] Add support for W (weak until) and M (strong release) operators. * src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for these new operators. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them. * src/ltltest/reduccmp.test: Add new tests for W and M. * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc, src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add support for W and M. * src/tgbatest/ltl2neverclaim.test: Test never claim output using LBTT, this is more thorough. Also we cannot use -N any more in the spotlbtt.test. * src/tgbatests/ltl2tgba.cc: Define M and W for ELTL. * src/tgbatest/ltl2neverclaim.test: Test W and M, and use -DS instead of -N, because lbtt-translate does not want to translate these operators for tools that masquerade as Spin. --- ChangeLog | 25 +++++++ src/ltlast/binop.cc | 12 +++- src/ltlast/binop.hh | 11 ++- src/ltlparse/ltlparse.yy | 11 ++- src/ltlparse/ltlscan.ll | 2 + src/ltltest/reduccmp.test | 16 ++++- src/ltlvisit/basicreduce.cc | 29 ++++++-- src/ltlvisit/contain.cc | 52 ++++++++++++++- src/ltlvisit/lunabbrev.cc | 11 ++- src/ltlvisit/nenoform.cc | 12 +++- src/ltlvisit/randomltl.cc | 10 +-- src/ltlvisit/randomltl.hh | 4 ++ src/ltlvisit/reduce.cc | 111 +++++++++++++++++++++++++++---- src/ltlvisit/simpfg.cc | 23 ++++++- src/ltlvisit/simpfg.hh | 18 +++++ src/ltlvisit/syntimpl.cc | 67 ++++++++++++++++++- src/ltlvisit/tostring.cc | 19 +++++- src/tgba/formula2bdd.cc | 4 +- src/tgbaalgos/eltl2tgba_lacim.cc | 6 +- src/tgbaalgos/ltl2taa.cc | 88 ++++++++++++++---------- src/tgbaalgos/ltl2tgba_fm.cc | 21 +++++- src/tgbaalgos/ltl2tgba_lacim.cc | 47 +++++++------ src/tgbatest/ltl2neverclaim.test | 94 +++++++++++++++++++++----- src/tgbatest/ltl2tgba.cc | 4 +- src/tgbatest/spotlbtt.test | 10 ++- 25 files changed, 584 insertions(+), 123 deletions(-) diff --git a/ChangeLog b/ChangeLog index 5a08cafd9..e951609bf 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,28 @@ +2010-04-07 Alexandre Duret-Lutz + + Add support for W (weak until) and M (strong release) operators. + + * src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for + these new operators. + * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them. + * src/ltltest/reduccmp.test: Add new tests for W and M. + * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc, + src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc, + src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh, + src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc, + src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc, + src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, + src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, + src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: + Add support for W and M. + * src/tgbatest/ltl2neverclaim.test: Test never claim output + using LBTT, this is more thorough. Also we cannot use -N + any more in the spotlbtt.test. + * src/tgbatests/ltl2tgba.cc: Define M and W for ELTL. + * src/tgbatest/ltl2neverclaim.test: Test W and M, and use + -DS instead of -N, because lbtt-translate does not want + to translate these operators for tools that masquerade as Spin. + 2010-04-12 Alexandre Duret-Lutz Adjust ltl2tgba.py to call scc_filter() with the "full" option as diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 5d1c703df..91edc7a5f 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -115,6 +115,10 @@ namespace spot return "U"; case R: return "R"; + case W: + return "W"; + case M: + return "M"; } // Unreachable code. assert(0); @@ -126,7 +130,7 @@ namespace spot binop* binop::instance(type op, formula* first, formula* second) { - // Sort the operands of associative operators, so that for + // Sort the operands of commutative operators, so that for // example the formula instance for 'a xor b' is the same as // that for 'b xor a'. switch (op) @@ -139,7 +143,9 @@ namespace spot case Implies: case U: case R: - // Non associative operators. + case W: + case M: + // Non commutative operators. break; } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 364e1eca8..9650fed08 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -47,7 +47,14 @@ namespace spot /// /// And and Or are not here. Because they /// are often nested we represent them as multops. - enum type { Xor, Implies, Equiv, U, R }; + enum type { Xor, + Implies, + Equiv, + U, //< until + R, //< release (dual of until) + W, //< weak until + M //< strong release (dual of weak until) + }; /// Build an unary operator with operation \a op and /// children \a first and \a second. diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 71ec3819d..820d55dd0 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -79,6 +79,7 @@ using namespace spot::ltl; %token OP_OR "or operator" OP_XOR "xor operator" OP_AND "and operator" %token OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator" %token OP_U "until operator" OP_R "release operator" +%token OP_W "weak until operator" OP_M "strong release operator" %token OP_F "sometimes operator" OP_G "always operator" %token OP_X "next operator" OP_NOT "not operator" %token ATOMIC_PROP "atomic proposition" @@ -95,7 +96,7 @@ using namespace spot::ltl; %left OP_AND /* LTL operators. */ -%left OP_U OP_R +%left OP_U OP_R OP_M OP_W %nonassoc OP_F OP_G %nonassoc OP_X @@ -239,6 +240,14 @@ subformula: ATOMIC_PROP { $$ = binop::instance(binop::R, $1, $3); } | subformula OP_R error { missing_right_binop($$, $1, @2, "release operator"); } + | subformula OP_W subformula + { $$ = binop::instance(binop::W, $1, $3); } + | subformula OP_W error + { missing_right_binop($$, $1, @2, "weak until operator"); } + | subformula OP_M subformula + { $$ = binop::instance(binop::M, $1, $3); } + | subformula OP_M error + { missing_right_binop($$, $1, @2, "strong release operator"); } | OP_F subformula { $$ = unop::instance(unop::F, $2); } | OP_F error diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index faef3ae76..3f6efc5b7 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -90,6 +90,8 @@ flex_set_buffer(const char* buf) "U" BEGIN(0); return token::OP_U; "R"|"V" BEGIN(0); return token::OP_R; "X"|"()" BEGIN(0); return token::OP_X; +"W" BEGIN(0); return token::OP_W; +"M" BEGIN(0); return token::OP_M; "=0" return token::OP_POST_NEG; "=1" return token::OP_POST_POS; diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index d45202c5a..ddc7c4f14 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -40,16 +40,26 @@ for x in ../reduccmp ../reductaustr; do # Syntactic reduction run 0 $x 'a & (!b R !a)' 'false' run 0 $x '(!b R !a) & a' 'false' - run 0 $x 'a & (!b R !a) & c' 'false' run 0 $x 'c & (!b R !a) & a' 'false' + run 0 $x 'a & (!b M !a)' 'false' + run 0 $x '(!b M !a) & a' 'false' + run 0 $x 'a & (!b M !a) & c' 'false' + run 0 $x 'c & (!b M !a) & a' 'false' + run 0 $x 'a & (b U a)' 'a' run 0 $x '(b U a) & a' 'a' run 0 $x 'a | (b U a)' '(b U a)' run 0 $x '(b U a) | a' '(b U a)' run 0 $x 'a U (b U a)' '(b U a)' + run 0 $x 'a & (b W a)' 'a' + run 0 $x '(b W a) & a' 'a' + run 0 $x 'a | (b W a)' '(b W a)' + run 0 $x '(b W a) | a' '(b W a)' + run 0 $x 'a W (b W a)' '(b W a)' + run 0 $x 'a & (b U a) & a' 'a' run 0 $x 'a & (b U a) & a' 'a' run 0 $x 'a | (b U a) | a' '(b U a)' @@ -101,6 +111,9 @@ for x in ../reduccmp ../reductaustr; do # reason as above. run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)' run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb' + + run 0 $x 'Gb W a' 'Gb|a' + run 0 $x 'Fb M Fa' 'Fa & Fb' ;; esac @@ -113,5 +126,4 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'GFGa' 'FGa' run 0 $x 'b R Ga' 'Ga' run 0 $x 'b R FGa' 'FGa' - done diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 54d4b73c6..f95b798c3 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -253,7 +253,8 @@ namespace spot formula* f2 = bo->second(); unop* fu1; unop* fu2; - switch (bo->op()) + binop::type op = bo->op(); + switch (op) { case binop::Xor: case binop::Equiv: @@ -262,31 +263,49 @@ namespace spot basic_reduce(f1), basic_reduce(f2)); return; + case binop::W: + case binop::M: case binop::U: case binop::R: + f1 = basic_reduce(f1); f2 = basic_reduce(f2); + // a W false = Ga + if (op == binop::W && f2 == constant::false_instance()) + { + result_ = unop::instance(unop::G, f1); + return; + } + // a M true = Fa + if (op == binop::M && f2 == constant::true_instance()) + { + result_ = unop::instance(unop::F, f1); + return; + } // a U false = false // a U true = true // a R false = false // a R true = true + // a W true = true + // a M false = false if (dynamic_cast(f2)) { result_ = f2; + f1->destroy(); return; } - f1 = basic_reduce(f1); - // X(a) U X(b) = X(a U b) // X(a) R X(b) = X(a R b) + // X(a) W X(b) = X(a W b) + // X(a) M X(b) = X(a M b) fu1 = dynamic_cast(f1); fu2 = dynamic_cast(f2); if (fu1 && fu2 && fu1->op() == unop::X && fu2->op() == unop::X) { - formula* ftmp = binop::instance(bo->op(), + formula* ftmp = binop::instance(op, basic_reduce(fu1->child()), basic_reduce(fu2->child())); result_ = unop::instance(unop::X, basic_reduce(ftmp)); @@ -296,7 +315,7 @@ namespace spot return; } - result_ = binop::instance(bo->op(), f1, f2); + result_ = binop::instance(op, f1, f2); return; } /* Unreachable code. */ diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 2387f0f93..6a11b3bc1 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -202,6 +202,31 @@ namespace spot result_ = binop::instance(binop::U, a, b); } break; + case binop::W: + // if (a W b) => b, then keep b ! + if (stronger && lcc->contained(bo, b)) + { + a->destroy(); + result_ = b; + } + // if a => b, then a W b = b. + else if ((!stronger) && lcc->contained(a, b)) + { + a->destroy(); + result_ = b; + } + // if !a => b, then a W b = 1 + else if (lcc->neg_contained(a, b)) + { + a->destroy(); + b->destroy(); + result_ = constant::true_instance(); + } + else + { + result_ = binop::instance(binop::W, a, b); + } + break; case binop::R: // if (a R b) => b, then keep b ! if (stronger && lcc->contained(b, bo)) @@ -226,6 +251,31 @@ namespace spot result_ = binop::instance(binop::R, a, b); } break; + case binop::M: + // if (a M b) => b, then keep b ! + if (stronger && lcc->contained(b, bo)) + { + a->destroy(); + result_ = b; + } + // if b => a, then a M b = b. + else if ((!stronger) && lcc->contained(b, a)) + { + a->destroy(); + result_ = b; + } + // if a => !b, then a M b = 0 + else if (lcc->contained_neg(a, b)) + { + a->destroy(); + b->destroy(); + result_ = constant::false_instance(); + } + else + { + result_ = binop::instance(binop::M, a, b); + } + break; default: result_ = binop::instance(bo->op(), a, b); } diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index b091e0904..f40262971 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -44,7 +44,8 @@ namespace spot formula* f1 = recurse(bo->first()); formula* f2 = recurse(bo->second()); - switch (bo->op()) + binop::type op = bo->op(); + switch (op) { /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: @@ -74,9 +75,13 @@ namespace spot return; /* f1 U f2 == f1 U f2 */ /* f1 R f2 == f1 R f2 */ + /* f1 W f2 == f1 W f2 */ + /* f1 M f2 == f1 M f2 */ case binop::U: case binop::R: - result_ = binop::instance(bo->op(), f1, f2); + case binop::W: + case binop::M: + result_ = binop::instance(op, f1, f2); return; } /* Unreachable code. */ diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 3d20c8698..286d8d011 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -154,6 +154,16 @@ namespace spot result_ = binop::instance(negated_ ? binop::U : binop::R, recurse(f1), recurse(f2)); return; + case binop::W: + /* !(a W b) == !a M !b */ + result_ = binop::instance(negated_ ? binop::M : binop::W, + recurse(f1), recurse(f2)); + return; + case binop::M: + /* !(a M b) == !a W !b */ + result_ = binop::instance(negated_ ? binop::W : binop::M, + recurse(f1), recurse(f2)); + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 6ef516a46..970a2e119 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -102,7 +102,7 @@ namespace spot namespace { - const int proba_size = 14; + const int proba_size = 16; } random_ltl::random_ltl(const atomic_prop_set* ap) @@ -122,8 +122,10 @@ namespace spot proba_[9].setup("xor", 3, binop_builder); proba_[10].setup("R", 3, binop_builder); proba_[11].setup("U", 3, binop_builder); - proba_[12].setup("and", 3, multop_builder); - proba_[13].setup("or", 3, multop_builder); + proba_[12].setup("W", 3, binop_builder); + proba_[13].setup("M", 3, binop_builder); + proba_[14].setup("and", 3, multop_builder); + proba_[15].setup("or", 3, multop_builder); proba_[0].proba = ap_->size(); diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh index 7ac6db5db..8bee73c50 100644 --- a/src/ltlvisit/randomltl.hh +++ b/src/ltlvisit/randomltl.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -82,6 +84,8 @@ namespace spot /// xor 1 /// R 1 /// U 1 + /// W 1 + /// M 1 /// and 1 /// or 1 /// \endverbatim diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 6f2f8e73e..12bb69afa 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -110,23 +110,46 @@ namespace spot void visit(binop* bo) { + binop::type op = bo->op(); + formula* f2 = recurse(bo->second()); + bool f2_eventual = false; - /* If b is a pure eventuality formula then a U b = b. - If b is a pure universality formula a R b = b. */ - if ((opt_ & Reduce_Eventuality_And_Universality) - && ((is_eventual(f2) && ((bo->op()) == binop::U)) - || (is_universal(f2) && ((bo->op()) == binop::R)))) + if (opt_ & Reduce_Eventuality_And_Universality) { - result_ = f2; - return; + f2_eventual = is_eventual(f2); + /* If b is a pure eventuality formula then a U b = b. + If b is a pure universality formula a R b = b. */ + if ((f2_eventual && (op == binop::U)) + || (is_universal(f2) && (op == binop::R))) + { + result_ = f2; + return; + } } - /* case of implies */ - formula* f1 = recurse(bo->first()); + formula* f1 = recurse(bo->first()); + if (opt_ & Reduce_Eventuality_And_Universality) + { + /* If a&b is a pure eventuality formula then a M b = a & b. + If a is a pure universality formula a W b = a|b. */ + if (is_eventual(f1) && f2_eventual && (op == binop::M)) + { + result_ = multop::instance(multop::And, f1, f2); + return; + } + if (is_universal(f1) && (op == binop::W)) + { + result_ = multop::instance(multop::Or, f1, f2); + return; + } + } + + + /* case of implies */ if (opt_ & Reduce_Syntactic_Implications) { - switch (bo->op()) + switch (op) { case binop::Xor: case binop::Equiv: @@ -149,9 +172,10 @@ namespace spot return; } /* a < b => a U (b U c) = (b U c) */ + /* a < b => a U (b W c) = (b W c) */ { binop* bo = dynamic_cast(f2); - if (bo && bo->op() == binop::U + if (bo && (bo->op() == binop::U || bo->op() == binop::W) && syntactic_implication(f1, bo->first())) { result_ = f2; @@ -188,9 +212,68 @@ namespace spot } } break; + + case binop::W: + /* a < b => a W b = b */ + if (syntactic_implication(f1, f2)) + { + result_ = f2; + f1->destroy(); + return; + } + /* !b < a => a W b = 1 */ + if (syntactic_implication_neg(f2, f1, false)) + { + result_ = constant::true_instance(); + f1->destroy(); + f2->destroy(); + return; + } + /* a < b => a W (b U c) = (b U c) */ + /* a < b => a W (b W c) = (b W c) */ + { + binop* bo = dynamic_cast(f2); + if (bo && (bo->op() == binop::U || bo->op() == binop::W) + && syntactic_implication(f1, bo->first())) + { + result_ = f2; + f1->destroy(); + return; + } + } + break; + + case binop::M: + /* b < a => a M b = b */ + if (syntactic_implication(f2, f1)) + { + result_ = f2; + f1->destroy(); + return; + } + /* b < !a => a M b = 0 */ + if (syntactic_implication_neg(f2, f1, true)) + { + result_ = constant::false_instance(); + f1->destroy(); + f2->destroy(); + return; + } + /* b < a => a R (b R c) = b R c */ + { + binop* bo = dynamic_cast(f2); + if (bo && bo->op() == binop::R + && syntactic_implication(bo->first(), f1)) + { + result_ = f2; + f1->destroy(); + return; + } + } + break; } } - result_ = binop::instance(bo->op(), f1, f2); + result_ = binop::instance(op, f1, f2); } void diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index fa143cfd9..f91d58c6c 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -1,3 +1,7 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -42,13 +46,14 @@ namespace spot { formula* f1 = recurse(bo->first()); formula* f2 = recurse(bo->second()); + binop::type op = bo->op(); - switch (bo->op()) + switch (op) { case binop::Xor: case binop::Implies: case binop::Equiv: - result_ = binop::instance(bo->op(), f1, f2); + result_ = binop::instance(op, f1, f2); return; /* true U f2 == F(f2) */ case binop::U: @@ -64,6 +69,20 @@ namespace spot else result_ = binop::instance(binop::R, f1, f2); return; + /* f1 W false == G(f1) */ + case binop::W: + if (f2 == constant::false_instance()) + result_ = unop::instance(unop::G, f1); + else + result_ = binop::instance(binop::W, f1, f2); + return; + /* f1 M true == F(f1) */ + case binop::M: + if (f1 == constant::true_instance()) + result_ = unop::instance(unop::F, f2); + else + result_ = binop::instance(binop::M, f1, f2); + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/simpfg.hh b/src/ltlvisit/simpfg.hh index 2cd7eadec..02ce24e10 100644 --- a/src/ltlvisit/simpfg.hh +++ b/src/ltlvisit/simpfg.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -30,6 +32,14 @@ namespace spot { /// \brief Replace true U f and false R g by /// F f and G g. + /// + /// Perform the following rewriting (from left to right): + /// + /// - true U a = F a + /// - a M true = F a + /// - false R a = G a + /// - a W false = G a + /// /// \ingroup ltl_visitor class simplify_f_g_visitor : public clone_visitor { @@ -46,6 +56,14 @@ namespace spot /// \brief Replace true U f and false R g by /// F f and G g. + /// + /// Perform the following rewriting (from left to right): + /// + /// - true U a = F a + /// - a M true = F a + /// - false R a = G a + /// - a W false = G a + /// /// \ingroup ltl_rewriting formula* simplify_f_g(const formula* f); } diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index c4e722a01..576c92642 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -108,7 +108,13 @@ namespace spot // Both operand must be purely eventual, unlike in // the proceedings of Concur'00. (The revision of // the paper available at - // http://www1.bell-labs.com/project/TMP/ is fixed.) + // http://www.bell-labs.com/project/TMP/ is fixed.) + || (recurse_ev(f1) && recurse_ev(f2))) + eventual = true; + return; + case binop::W: + universal = recurse_un(f1) && recurse_un(f2); + if ((f2 == constant::true_instance()) || (recurse_ev(f1) && recurse_ev(f2))) eventual = true; return; @@ -118,6 +124,12 @@ namespace spot || (recurse_un(f1) && recurse_un(f2))) universal = true; return; + case binop::M: + eventual = recurse_ev(f1) && recurse_ev(f2); + if ((f2 == constant::false_instance()) + || (recurse_un(f1) && recurse_un(f2))) + universal = true; + return; } /* Unreachable code. */ assert(0); @@ -263,6 +275,7 @@ namespace spot case binop::Implies: return; case binop::U: + case binop::W: if (syntactic_implication(f, f2)) result_ = true; return; @@ -285,6 +298,25 @@ namespace spot && syntactic_implication(f, f2)) result_ = true; return; + case binop::M: + if (fb && fb->op() == binop::M) + if (syntactic_implication(fb->first(), f1) && + syntactic_implication(fb->second(), f2)) + { + result_ = true; + return; + } + if (fu && fu->op() == unop::F) + if (f2 == constant::true_instance() && + syntactic_implication(fu->child(), f1)) + { + result_ = true; + return; + } + if (syntactic_implication(f, f1) + && syntactic_implication(f, f2)) + result_ = true; + return; } /* Unreachable code. */ assert(0); @@ -480,6 +512,26 @@ namespace spot && syntactic_implication(f2, f)) result_ = true; return; + case binop::W: + /* (a < c) && (c < d) => a W b < c W d */ + if (fb && fb->op() == binop::W) + if (syntactic_implication(f1, fb->first()) && + syntactic_implication(f2, fb->second())) + { + result_ = true; + return; + } + if (fu && fu->op() == unop::G) + if (f2 == constant::false_instance() && + syntactic_implication(f1, fu->child())) + { + result_ = true; + return; + } + if (syntactic_implication(f1, f) + && syntactic_implication(f2, f)) + result_ = true; + return; case binop::R: if (fu && fu->op() == unop::G) if (f1 == constant::false_instance() && @@ -491,6 +543,17 @@ namespace spot if (syntactic_implication(f2, f)) result_ = true; return; + case binop::M: + if (fu && fu->op() == unop::F) + if (f2 == constant::true_instance() && + syntactic_implication(f1, fu->child())) + { + result_ = true; + return; + } + if (syntactic_implication(f2, f)) + result_ = true; + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 47eacb0d6..b0ba0de08 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -118,6 +118,12 @@ namespace spot case binop::R: os_ << " R "; break; + case binop::W: + os_ << " W "; + break; + case binop::M: + os_ << " M "; + break; } bo->second()->accept(*this); @@ -276,6 +282,17 @@ namespace spot os_ << " V "; bo->second()->accept(*this); break; + /* W and M are not supported by Spin */ + case binop::W: + bo->first()->accept(*this); + os_ << " W "; + bo->second()->accept(*this); + break; + case binop::M: + bo->first()->accept(*this); + os_ << " M "; + bo->second()->accept(*this); + break; } if (!top_level) diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 50c1fcdaf..6dfc7467d 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -107,6 +107,8 @@ namespace spot return; case binop::U: case binop::R: + case binop::W: + case binop::M: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index c34ffa40c..429be6b4b 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -124,6 +124,8 @@ namespace spot return; case binop::U: case binop::R: + case binop::W: + case binop::M: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index a2e472690..89767cd95 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -155,12 +155,17 @@ namespace spot std::vector::iterator i2; taa_tgba::transition* t = 0; bool contained = false; + bool strong = false; + switch (node->op()) { - case binop::U: // Strong - if (refined_) - contained = lcc_->contained(node->second(), node->first()); - for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) + case binop::U: + strong = true; + // fall thru + case binop::W: + if (refined_) + contained = lcc_->contained(node->second(), node->first()); + for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) { // Refined rule if (refined_ && contained) @@ -168,60 +173,75 @@ namespace spot (remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end()); i1->Q.push_back(init_); // Add the initial state - i1->acc.push_back(node->second()); + if (strong) + i1->acc.push_back(node->second()); t = res_->create_transition(init_, i1->Q); res_->add_condition(t, i1->condition->clone()); - res_->add_acceptance_condition(t, node->second()->clone()); + if (strong) + res_->add_acceptance_condition(t, node->second()->clone()); + else + for (unsigned i = 0; i < i1->acc.size(); ++i) + res_->add_acceptance_condition(t, i1->acc[i]->clone()); succ_.push_back(*i1); } - for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) + for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) { t = res_->create_transition(init_, i2->Q); res_->add_condition(t, i2->condition->clone()); succ_.push_back(*i2); } - return; - case binop::R: // Weak - if (refined_) - contained = lcc_->contained(node->first(), node->second()); - for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) + return; + case binop::M: // Strong Release + strong = true; + case binop::R: // Weak Release + if (refined_) + contained = lcc_->contained(node->first(), node->second()); + + for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) { for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) - { - std::vector u; // Union - std::vector a; // Acceptance conditions - std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end())); - formula* f = i1->condition->clone(); // Refined rule - if (!refined_ || !contained) { - std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end())); - f = multop::instance(multop::And, f, i2->condition->clone()); + std::vector u; // Union + std::vector a; // Acceptance conditions + std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end())); + formula* f = i1->condition->clone(); // Refined rule + if (!refined_ || !contained) + { + std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end())); + f = multop::instance(multop::And, f, + i2->condition->clone()); + } + to_free_.push_back(f); + t = res_->create_transition(init_, u); + res_->add_condition(t, f->clone()); + succ_state ss = { u, f, a }; + succ_.push_back(ss); } - to_free_.push_back(f); - - t = res_->create_transition(init_, u); - res_->add_condition(t, f->clone()); - succ_state ss = { u, f, a }; - succ_.push_back(ss); - } if (refined_) // Refined rule i2->Q.erase (remove(i2->Q.begin(), i2->Q.end(), v2.init_), i2->Q.end()); + i2->Q.push_back(init_); // Add the initial state t = res_->create_transition(init_, i2->Q); res_->add_condition(t, i2->condition->clone()); - if (refined_) + + if (strong) + { + i2->acc.push_back(node->first()); + res_->add_acceptance_condition(t, node->first()->clone()); + } + else if (refined_) for (unsigned i = 0; i < i2->acc.size(); ++i) res_->add_acceptance_condition(t, i2->acc[i]->clone()); succ_.push_back(*i2); } - return; - case binop::Xor: - case binop::Implies: - case binop::Equiv: - assert(0); // TBD + return; + case binop::Xor: + case binop::Implies: + case binop::Equiv: + assert(0); // TBD } /* Unreachable code. */ assert(0); diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 91e26b4d0..8ac292405 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -393,6 +393,13 @@ namespace spot res_ = f2 | (bdd_ithvar(a) & f1 & bdd_ithvar(x)); return; } + case binop::W: + { + // r(f1 W f2) = r(f2) + r(f1)r(X(f1 U f2)) + int x = dict_.register_next_variable(node); + res_ = f2 | (f1 & bdd_ithvar(x)); + return; + } case binop::R: { // r(f1 R f2) = r(f1)r(f2) + r(f2)r(X(f1 U f2)) @@ -400,6 +407,14 @@ namespace spot res_ = (f1 & f2) | (f2 & bdd_ithvar(x)); return; } + case binop::M: + { + // r(f1 M f2) = r(f1)r(f2) + a(f1)r(f2)r(X(f1 M f2)) + int a = dict_.register_a_variable(node->first()); + int x = dict_.register_next_variable(node); + res_ = (f1 & f2) | (bdd_ithvar(a) & f2 & bdd_ithvar(x)); + return; + } } /* Unreachable code. */ assert(0); @@ -449,8 +464,8 @@ namespace spot }; - // Check whether a formula has a R or G operator at its top-level - // (preceding logical operators do not count). + // Check whether a formula has a R, W, or G operator at its + // top-level (preceding logical operators do not count). class ltl_possible_fair_loop_visitor: public const_visitor { public: @@ -501,8 +516,10 @@ namespace spot node->second()->accept(*this); return; case binop::U: + case binop::M: return; case binop::R: + case binop::W: res_ = true; return; } diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index e8a20be01..c3bce3782 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -160,7 +160,8 @@ namespace spot bdd f1 = recurse(node->first()); bdd f2 = recurse(node->second()); - switch (node->op()) + binop::type op = node->op(); + switch (op) { case binop::Xor: res_ = bdd_apply(f1, f2, bddop_xor); @@ -172,39 +173,47 @@ namespace spot res_ = bdd_apply(f1, f2, bddop_biimp); return; case binop::U: + case binop::W: { - /* - f1 U f2 <=> f2 | (f1 & X(f1 U f2)) - In other words: - now <=> f2 | (f1 & next) - */ + // f1 U f2 <=> f2 | (f1 & X(f1 U f2)) + // In other words: + // now <=> f2 | (f1 & next) int v = fact_.create_state(node); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), bddop_biimp)); - /* - The rightmost conjunction, f1 & next, doesn't actually - encode the fact that f2 should be fulfilled eventually. - We declare an acceptance condition for this purpose (see - the comment in the unop::F case). - */ - fact_.declare_acceptance_condition(f2 | !now, node->second()); + if (op == binop::U) + { + // The rightmost conjunction, f1 & next, doesn't + // actually encode the fact that f2 should be + // fulfilled eventually. We declare an acceptance + // condition for this purpose (see the comment in + // the unop::F case). + fact_.declare_acceptance_condition(f2 | !now, node->second()); + } res_ = now; return; } case binop::R: + case binop::M: { - /* - f1 R f2 <=> f2 & (f1 | X(f1 R f2)) - In other words: - now <=> f2 & (f1 | next) - */ + // f1 R f2 <=> f2 & (f1 | X(f1 R f2)) + // In other words: + // now <=> f2 & (f1 | next) int v = fact_.create_state(node); bdd now = bdd_ithvar(v); bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), bddop_biimp)); + if (op == binop::M) + { + // f2 & next, doesn't actually encode the fact that + // f1 should be fulfilled eventually. We declare an + // acceptance condition for this purpose (see the + // comment in the unop::F case). + fact_.declare_acceptance_condition(f1 | !now, node->second()); + } res_ = now; return; } diff --git a/src/tgbatest/ltl2neverclaim.test b/src/tgbatest/ltl2neverclaim.test index 4604fc3c3..73d34e1ce 100755 --- a/src/tgbatest/ltl2neverclaim.test +++ b/src/tgbatest/ltl2neverclaim.test @@ -1,9 +1,6 @@ #!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2010 Laboratoire de Recherche et Développement # de l'Epita (LRDE). -# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -22,22 +19,85 @@ # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA # 02111-1307, USA. +# Do some quick translations to make sure the neverclaim produced by +# spot actually look correct! + +# This test is separate from spotlbtt.test, because lbtt-translate +# will refuse to passe M and W to a tool (spot) that masquerades as +# Spin. . ./defs set -e -# We don't check the output, but just running these might be enough to -# trigger assertions. +cat > config <