alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

product: add a product_or variant

Browse source 
* src/twaalgos/product.cc, src/twaalgos/product.hh: Implement
the variance.
* src/bin/autfilt.cc: Expose it.
* src/tests/prodor.test: New file.
* src/tests/Makefile.am: Add it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2015-09-26 19:14:08 +02:00
parent b77f7e24c3
commit 51a3cfcede
6 changed files with 331 additions and 84 deletions
Download patch file Download diff file Expand all files Collapse all files

36
NEWS
View file

@ -5,6 +5,16 @@ New in spot 1.99.3a (not yet released)
exactly one acceptance sets. This is useful when targeting parity
acceptance.
* autfilt has a new --product-or option. This builds a synchronized
product of two (completed of needed) automata in order to
recognize the *sum* of their languages. This works by just using
the disjunction of their acceptance conditions (with appropriate
renumbering of the acceptance sets).
For consistency, the --product option (that builds a synchronized
product that recognizes the *intersection* of the languages) now
also has a --product-and alias.
* the parser for ltl2dstar's format has been merged with the parser
for the other automata formats. This implies two things:
- autfilt and dstar2tgba (despite its name) can now both read
@ -18,20 +28,18 @@ New in spot 1.99.3a (not yet released)
* The class hierarchy for temporal formulas has been entirely
rewritten. This change is actually quite massive (~13200 lines
removed, ~8200 lines added), and brings some nice benefits:
- LTL/PSL formulas are now represented by lightweight
ltl::formula objects (instead of ltl::formula* pointers)
that perform reference counting automatically.
- There is no hierachy anymore: all operators are represented
by a single type of node in the syntax tree, and an
enumerator is used to distinguish between operators.
- Visitors have been replaced by member functions such
as map() or traverse(), that take a function (usually
written as a lambda function) and apply it to the
nodes of the tree.
- As a consequence, writing algorithms that manipulate
formula is more friendly, and several functions
algorithms that spanned a few pages have been
reduced to a few lines.
- LTL/PSL formulas are now represented by lightweight ltl::formula
objects (instead of ltl::formula* pointers) that perform
reference counting automatically.
- There is no hierachy anymore: all operators are represented by a
single type of node in the syntax tree, and an enumerator is
used to distinguish between operators.
- Visitors have been replaced by member functions such as map() or
traverse(), that take a function (usually written as a lambda
function) and apply it to the nodes of the tree.
- As a consequence, writing algorithms that manipulate formula is
more friendly, and several algorithms that spanned a few pages
have been reduced to a few lines.
New in spot 1.99.3 (2015-08-26)

41
src/bin/autfilt.cc
View file

@ -85,7 +85,8 @@ enum {
OPT_KEEP_STATES,
OPT_MASK_ACC,
OPT_MERGE,
OPT_PRODUCT,
OPT_PRODUCT_AND,
OPT_PRODUCT_OR,
OPT_RANDOMIZE,
OPT_REM_AP,
OPT_REM_DEAD,
@ -122,8 +123,13 @@ static const argp_option options[] =
{ 0, 0, 0, 0, "Transformations:", 5 },
{ "merge-transitions", OPT_MERGE, 0, 0,
"merge transitions with same destination and acceptance", 0 },
{ "product", OPT_PRODUCT, "FILENAME", 0,
"build the product with the automaton in FILENAME", 0 },
{ "product", OPT_PRODUCT_AND, "FILENAME", 0,
"build the product with the automaton in FILENAME "
"to intersect languages", 0 },
{ "product-and", 0, 0, OPTION_ALIAS, 0, 0 },
{ "product-or", OPT_PRODUCT_OR, "FILENAME", 0,
"build the product with the automaton in FILENAME "
"to sum languages", 0 },
{ "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
"randomize states and transitions (specify 's' or 't' to "
"randomize only states or transitions)", 0 },
@ -231,7 +237,8 @@ static int opt_seed = 0;
static struct opt_t
{
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
spot::twa_graph_ptr product = nullptr;
spot::twa_graph_ptr product_and = nullptr;
spot::twa_graph_ptr product_or = nullptr;
spot::twa_graph_ptr intersect = nullptr;
spot::twa_graph_ptr are_isomorphic = nullptr;
std::unique_ptr<spot::isomorphism_checker>
@ -393,14 +400,24 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_rem_unreach = true;
break;
}
case OPT_PRODUCT:
case OPT_PRODUCT_AND:
{
auto a = read_automaton(arg, opt->dict);
if (!opt->product)
opt->product = std::move(a);
if (!opt->product_and)
opt->product_and = std::move(a);
else
opt->product = spot::product(std::move(opt->product),
std::move(a));
opt->product_and = spot::product(std::move(opt->product_and),
std::move(a));
}
break;
case OPT_PRODUCT_OR:
{
auto a = read_automaton(arg, opt->dict);
if (!opt->product_or)
opt->product_or = std::move(a);
else
opt->product_or = spot::product_or(std::move(opt->product_or),
std::move(a));
}
break;
case OPT_RANDOMIZE:
@ -579,8 +596,10 @@ namespace
else if (opt_rem_unreach)
aut->purge_unreachable_states();
if (opt->product)
aut = spot::product(std::move(aut), opt->product);
if (opt->product_and)
aut = spot::product(std::move(aut), opt->product_and);
if (opt->product_or)
aut = spot::product_or(std::move(aut), opt->product_or);
if (opt_sat_minimize)
{

1
src/tests/Makefile.am
View file

@ -181,6 +181,7 @@ TESTS_twa = \
ltldo2.test \
maskacc.test \
maskkeep.test \
prodor.test \
simdet.test \
sim2.test \
sim3.test \

169
src/tests/prodor.test Executable file
View file

@ -0,0 +1,169 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
ltl2tgba=../../bin/ltl2tgba
autfilt=../../bin/autfilt
$ltl2tgba -DH 'GFa' > gfa.hoa
$ltl2tgba -DH 'FGb' > fgb.hoa
$autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa
cat por.hoa
cat >exp <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[0&1] 1 {1}
[!0&1] 1
[0] 0 {1}
[!0] 0
State: 1
[0&1] 1 {0 1}
[!0&1] 1 {0}
[0&!1] 2 {0 1}
[!0&!1] 2 {0}
State: 2
[0] 2 {1}
[!0] 2
--END--
EOF
diff por.hoa exp
test 2 = `$autfilt -c --intersect por.hoa gfa.hoa fgb.hoa`
$autfilt --product-and gfa.hoa fgb.hoa -H > pand.hoa
cat pand.hoa
cat >exp <<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1] 1 {1}
[!0&1] 1
[0] 0 {1}
[!0] 0
State: 1
[0&1] 1 {0 1}
[!0&1] 1 {0}
--END--
EOF
diff pand.hoa exp
test 2 = `$autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa`
$ltl2tgba -BDH 'GFa' > gfa.hoa
$ltl2tgba -BDH 'Xb' > xb.hoa
$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
cat por.hoa
cat >exp <<EOF
HOA: v1
States: 7
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {0 1}
[0] 1
[!0] 2
State: 1 {0 1}
[0&1] 3
[!0&1] 4
[0&!1] 5
[!0&!1] 6
State: 2 {0}
[0&1] 3
[!0&1] 4
[0&!1] 5
[!0&!1] 6
State: 3 {0 1}
[0] 3
[!0] 4
State: 4 {0}
[0] 3
[!0] 4
State: 5 {1}
[0] 5
[!0] 6
State: 6
[0] 5
[!0] 6
--END--
EOF
diff por.hoa exp
$ltl2tgba -BDH 'GFa' > gfa.hoa
$ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa
$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
cat por.hoa
cat >exp <<EOF
HOA: v1
States: 7
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {0 1}
[0] 1
[!0] 2
State: 1 {0 1}
[0&1] 3
[!0&1] 4
[0&!1] 5
[!0&!1] 6
State: 2 {0}
[0&1] 3
[!0&1] 4
[0&!1] 5
[!0&!1] 6
State: 3 {0 1}
[0] 3
[!0] 4
State: 4 {0}
[0] 3
[!0] 4
State: 5 {1}
[0] 5
[!0] 6
State: 6
[0] 5
[!0] 6
--END--
EOF
diff por.hoa exp

153
src/twaalgos/product.cc
View file

@ -19,6 +19,7 @@
#include "product.hh"
#include "twa/twagraph.hh"
#include "twaalgos/complete.hh"
#include <deque>
#include <unordered_map>
#include "misc/hash.hh"
@ -37,77 +38,115 @@ namespace spot
return wang32_hash(s.first ^ wang32_hash(s.second));
}
};
}
static
twa_graph_ptr product_aux(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state,
bool and_acc)
{
std::unordered_map<product_state, unsigned, product_state_hash> s2n;
std::deque<std::pair<product_state, unsigned>> todo;
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state)
{
std::unordered_map<product_state, unsigned, product_state_hash> s2n;
std::deque<std::pair<product_state, unsigned>> todo;
assert(left->get_dict() == right->get_dict());
auto res = make_twa_graph(left->get_dict());
res->copy_ap_of(left);
res->copy_ap_of(right);
auto left_num = left->num_sets();
auto right_acc = right->get_acceptance();
right_acc.shift_left(left_num);
if (and_acc)
right_acc.append_and(left->get_acceptance());
else
right_acc.append_or(acc_cond::acc_code(left->get_acceptance()));
res->set_acceptance(left_num + right->num_sets(), right_acc);
assert(left->get_dict() == right->get_dict());
auto res = make_twa_graph(left->get_dict());
res->copy_ap_of(left);
res->copy_ap_of(right);
auto left_num = left->num_sets();
auto right_acc = right->get_acceptance();
right_acc.shift_left(left_num);
right_acc.append_and(left->get_acceptance());
res->set_acceptance(left_num + right->num_sets(), right_acc);
auto v = new product_states;
res->set_named_prop("product-states", v);
auto v = new product_states;
res->set_named_prop("product-states", v);
auto new_state =
[&](unsigned left_state, unsigned right_state) -> unsigned
{
product_state x(left_state, right_state);
auto p = s2n.emplace(x, 0);
if (p.second) // This is a new state
{
p.first->second = res->new_state();
todo.emplace_back(x, p.first->second);
assert(p.first->second == v->size());
v->push_back(x);
}
return p.first->second;
};
res->set_init_state(new_state(left_state, right_state));
if (right_acc.is_false())
// Do not bother doing any work if the resulting acceptance is
// false.
return res;
while (!todo.empty())
{
auto top = todo.front();
todo.pop_front();
for (auto& l: left->out(top.first.first))
for (auto& r: right->out(top.first.second))
auto new_state =
[&](unsigned left_state, unsigned right_state) -> unsigned
{
product_state x(left_state, right_state);
auto p = s2n.emplace(x, 0);
if (p.second) // This is a new state
{
auto cond = l.cond & r.cond;
if (cond == bddfalse)
continue;
auto dst = new_state(l.dst, r.dst);
res->new_edge(top.second, dst, cond,
res->acc().join(left->acc(), l.acc,
right->acc(), r.acc));
// If right is deterministic, we can abort immediately!
p.first->second = res->new_state();
todo.emplace_back(x, p.first->second);
assert(p.first->second == v->size());
v->push_back(x);
}
}
return p.first->second;
};
return res;
res->set_init_state(new_state(left_state, right_state));
if (right_acc.is_false())
// Do not bother doing any work if the resulting acceptance is
// false.
return res;
while (!todo.empty())
{
auto top = todo.front();
todo.pop_front();
for (auto& l: left->out(top.first.first))
for (auto& r: right->out(top.first.second))
{
auto cond = l.cond & r.cond;
if (cond == bddfalse)
continue;
auto dst = new_state(l.dst, r.dst);
res->new_edge(top.second, dst, cond,
res->acc().join(left->acc(), l.acc,
right->acc(), r.acc));
// If right is deterministic, we can abort immediately!
}
}
res->prop_deterministic(left->is_deterministic()
&& right->is_deterministic());
res->prop_stutter_invariant(left->is_stutter_invariant()
&& right->is_stutter_invariant());
res->prop_stutter_sensitive(left->is_stutter_sensitive()
&& right->is_stutter_sensitive());
res->prop_state_based_acc(left->has_state_based_acc()
&& right->has_state_based_acc());
return res;
}
}
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state)
{
return product_aux(left, right, left_state, right_state, true);
}
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
return product(left, right,
left->get_init_state_number(),
right->get_init_state_number());
}
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state)
{
return product_aux(tgba_complete(left),
tgba_complete(right),
left_state, right_state, false);
}
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
return product_or(left, right,
left->get_init_state_number(),
right->get_init_state_number());
}
}

15
src/twaalgos/product.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -32,11 +32,22 @@ namespace spot
SPOT_API
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
const const_twa_graph_ptr& right);
SPOT_API
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state);
SPOT_API
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
SPOT_API
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state);
}