Commit 62fd38e6 authored by Thomas Medioni's avatar Thomas Medioni

Implement sum(..) and sum_and(..).

See #231.

* bin/autfilt.cc: Add --sum, --sum-or and --sum-and options.
* python/spot/impl.i: Add bindings for sum, sum_and.
* spot/twaalgos/Makefile.am: Add sum.cc, sum.hh.
* spot/twaalgos/sum.cc: Implement sum, sum_and.
* spot/twaalgos/sum.hh: Declaration of sum, sum_and.
* tests/Makefile.am: Add sum tests.
* tests/core/.gitignore: Ignore ltlsum binary.
* tests/core/explsu2.test: Test false or false.
* tests/core/explsu3.test: Test whether unsatisfied marks propagate
  onto other automaton sum of the term.
* tests/core/explsu4.test: Test whether universal transitions are
  handled.
* tests/core/explsu5.test: Generate two sets of persistence LTL
  formulas, apply both sum and sum_and on both sets, test equivalence
  of the result with the disjunction resp. conjunction of the formulas.
* tests/core/explsum.test: Test the sum of two automatons
* tests/core/ltlsum.cc: Standalone sum program that takes two formulas
  as input
* tests/core/ltlsum.test: Test some random formulas, in order to
  trigger basic assertions
* tests/python/sumexpt.py: Check that two automatons that does not
  share their bdd dict are not accepted
parent a66e7704
......@@ -41,6 +41,7 @@
#include "common_hoaread.hh"
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/sum.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/isunamb.hh>
......@@ -137,6 +138,8 @@ enum {
OPT_SIMPLIFY_EXCLUSIVE_AP,
OPT_STATES,
OPT_STRIPACC,
OPT_SUM_OR,
OPT_SUM_AND,
OPT_TERMINAL_SCCS,
OPT_TRIV_SCCS,
OPT_USED_AP_N,
......@@ -317,6 +320,13 @@ static const argp_option options[] =
{ "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
"remove states that are unreachable, or that cannot belong to an "
"infinite path", 0 },
{ "sum", OPT_SUM_OR, "FILENAME", 0,
"build the sum with the automaton in FILENAME "
"to sum languages", 0 },
{ "sum-or", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "sum-and", OPT_SUM_AND, "FILENAME", 0,
"build the sum with the automaton in FILENAME "
"to intersect languages", 0 },
{ "separate-sets", OPT_SEP_SETS, nullptr, 0,
"if both Inf(x) and Fin(x) appear in the acceptance condition, replace "
"Fin(x) by a new Fin(y) and adjust the automaton", 0 },
......@@ -412,6 +422,8 @@ static struct opt_t
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
spot::twa_graph_ptr product_and = nullptr;
spot::twa_graph_ptr product_or = nullptr;
spot::twa_graph_ptr sum_and = nullptr;
spot::twa_graph_ptr sum_or = nullptr;
spot::twa_graph_ptr intersect = nullptr;
spot::twa_graph_ptr included_in = nullptr;
spot::twa_graph_ptr equivalent_pos = nullptr;
......@@ -846,6 +858,26 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_STRIPACC:
opt_stripacc = true;
break;
case OPT_SUM_OR:
{
auto a = read_automaton(arg, opt->dict);
if (!opt->sum_or)
opt->sum_or = std::move(a);
else
opt->sum_or = spot::sum(std::move(opt->sum_or),
std::move(a));
}
break;
case OPT_SUM_AND:
{
auto a = read_automaton(arg, opt->dict);
if (!opt->sum_and)
opt->sum_and = std::move(a);
else
opt->sum_and = spot::sum_and(std::move(opt->sum_and),
std::move(a));
}
break;
case OPT_TERMINAL_SCCS:
opt_terminal_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
opt_terminal_sccs_set = true;
......@@ -1188,6 +1220,11 @@ namespace
if (opt->product_or)
aut = spot::product_or(std::move(aut), opt->product_or);
if (opt->sum_or)
aut = spot::sum(std::move(aut), opt->sum_or);
if (opt->sum_and)
aut = spot::sum_and(std::move(aut), opt->sum_and);
if (opt_decompose_strength)
{
aut = decompose_strength(aut, opt_decompose_strength);
......
......@@ -141,6 +141,7 @@
#include <spot/twaalgos/isunamb.hh>
#include <spot/twaalgos/langmap.hh>
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/sum.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/stutter.hh>
......@@ -545,6 +546,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/simulation.hh>
%include <spot/twaalgos/postproc.hh>
%include <spot/twaalgos/product.hh>
%include <spot/twaalgos/sum.hh>
%include <spot/twaalgos/stutter.hh>
%include <spot/twaalgos/translate.hh>
%include <spot/twaalgos/hoa.hh>
......
......@@ -78,6 +78,7 @@ twaalgos_HEADERS = \
stats.hh \
stripacc.hh \
stutter.hh \
sum.hh \
tau03.hh \
tau03opt.hh \
totgba.hh \
......@@ -136,6 +137,7 @@ libtwaalgos_la_SOURCES = \
stats.cc \
stripacc.cc \
stutter.cc \
sum.cc \
tau03.cc \
tau03opt.cc \
totgba.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
Please register or sign in to reply
// 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/>.
#include <spot/twaalgos/sum.hh>
#include <spot/twa/twagraph.hh>
#include <vector>
#include <map>
namespace spot
{
namespace
{
// Helper function that connects a new initial state to the automaton,
// in replacement of graph_init
static inline
Please register or sign in to reply
void connect_init_state(const twa_graph_ptr& res,
const const_twa_graph_ptr& graph,
unsigned init,
unsigned graph_init,
unsigned offset = 0U)
{
std::map<unsigned, bdd> edges;
for (auto& e : graph->out(graph_init))
{
std::vector<unsigned> dst;
for (auto& d : graph->univ_dests(e))
{
dst.push_back(d + offset);
}
if (dst.size() > 1)
{
res->new_univ_edge(init, dst.begin(), dst.end(), e.cond, 0U);
}
else
{
edges[dst[0]] |= e.cond;
}
}
for (auto& p : edges)
{
res->new_edge(init, p.first, p.second);
}
}
// Helper function that copies the states of graph into res, adding
// offset to the state ID, mark to the current mark of the edges,
// and setting the number of states to num_sets
static inline
Please register or sign in to reply
void copy_union(const twa_graph_ptr& res,
const const_twa_graph_ptr& graph,
size_t num_sets,
acc_cond::mark_t mark = 0U,
unsigned offset = 0U)
{
auto state_offset = res->num_states();
  • If someone can think of a way to reliably detect two consecutive empty lines inside a function body, that would be a nice thing to add to style.test.

Please register or sign in to reply
res->new_states(graph->num_states());
for (auto& e : graph->edges())
{
std::vector<unsigned> dst;
  • This is going to be allocated and unallocated for each iteration. It's should be better to create the vector out of the loop, and only clear() it in the loop.

Please register or sign in to reply
for (auto& d : graph->univ_dests(e))
{
dst.push_back(d + state_offset);
}
decltype(mark) mask = (1U << num_sets) - 1;
  • Please reserve decltype for cases where you cannot specify the type yourself, as it is a pain for the (human) reader.

    acc_cond::mark_t mask(1U << sum_sets) - 1) would do the same thing; however the point of mark_t is that you should never work using an unsigned (except 0U), so it would be better to avoid this type of construction.

    You should be able to avoid all this by passing directly mask instead of num_sets to this function. Then the caller would simply specify the mask as left_aut->acc().all_sets().

    But really why do you need a mask at all? (If a mark has sets outside of the declared number of set, that automaton is ill-formed.)

Please register or sign in to reply
auto trimmed = e.acc & mask;
res->new_univ_edge(e.src + state_offset,
dst.begin(), dst.end(),
e.cond,
(trimmed << offset)| mark);
}
}
// Helper function that perform the sum of the automaton in left and the
// automaton in right, using is_sum true for sum_or and is_sum false
// as sum_and
static inline
twa_graph_ptr sum_aux(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state,
bool is_sum)
{
// Only compute the sum of graphs that share the same bdd dictionnary.
Please register or sign in to reply
if (left->get_dict() != right->get_dict())
throw std::runtime_error("sum: left and right automata should "
"share their bdd_dict");
// Create an empty resulting graph that share the same bdd dictionnary as
// input graphs
auto res = make_twa_graph(left->get_dict());
res->copy_ap_of(left);
res->copy_ap_of(right);
auto unsatl = left->acc().unsat_mark();
acc_cond::mark_t markl = 0U;
acc_cond::mark_t markr = 0U;
auto left_acc = left->get_acceptance();
auto left_num_sets = left->num_sets();
if (unsatl.first == false)
  • I tend to prefer x and !x over the lengthy x == true and x == false. (Personal taste: I find both equally readable, but the justification for using x == false should also work for using (x == false) == true.)

Please register or sign in to reply
{
markl |= 1U;
left_num_sets = 1;
left_acc = acc_cond::acc_code::buchi();
}
else
markr |= unsatl.second;
auto unsatr = right->acc().unsat_mark();
auto right_acc = right->get_acceptance();
auto right_num_sets = right->num_sets();
if (unsatr.first == false)
{
markr |= (1U << left_num_sets);
right_num_sets = 1;
right_acc = acc_cond::acc_code::buchi();
}
else
markl |= (unsatr.second << left_num_sets);
const auto res_num_sets = left_num_sets + right_num_sets;
decltype(markl) mask((1U << res_num_sets) - 1);
Please register or sign in to reply
res->set_acceptance(left_num_sets + right_num_sets,
(right_acc << left_num_sets) |= left_acc);
copy_union(res, left, left_num_sets, markl & mask);
copy_union(res, right, right_num_sets, markr & mask, left_num_sets);
if (is_sum)
{
unsigned init = res->new_state();
res->set_init_state(init);
connect_init_state(res, left, init, left_state);
connect_init_state(res, right, init, right_state, left->num_states());
}
else
{
std::array<unsigned, 2> init;
init[0] = left_state;
init[1] = right_state + left->num_states();
res->set_univ_init_state(init.begin(), init.end());
  • res->set_univ_init_state({ left_state, right + left->num_states() }); does not work?

  • Actually, it doesn't, the reason being the function is defined with a template parameter I (used in iterator overload as iterator type), where here we simply need an initializer_list. After a simple check on teamcity, the template version using an initializer_list is never instantiated, but i am not sure whether teamcity is able to detect code coverage on template instantiation.

    Edited by Thomas Medioni
  • Good catch. I'm working on a patch to fix set_univ_init_state({s,t}) on a short test case.

  • set_univ_init_state({s,t}) is fixed by 2c9f201c (on next). The coverage now shows the function has called once; but your patch will increase this.

Please register or sign in to reply
}
return res;
}
}
twa_graph_ptr sum(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state)
{
return sum_aux(left, right, left_state, right_state, true);
}
twa_graph_ptr sum(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
return sum(left, right,
left->get_init_state_number(),
right->get_init_state_number());
}
twa_graph_ptr sum_and(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state)
{
return sum_aux(left, right, left_state, right_state, false);
}
twa_graph_ptr sum_and(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
return sum_and(left,
right,
left->get_init_state_number(),
right->get_init_state_number());
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2017 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/>.
#pragma once
#include <spot/misc/common.hh>
#include <spot/twa/fwd.hh>
#include <vector>
#include <utility>
namespace spot
{
/// \brief Sum two twa into a new twa, performing the union of the two input
/// automatons.
///
/// \param left Left term of the sum.
/// \param right Right term of the sum.
/// \return A spot::twa_graph containing the sum of \a left and \a right
SPOT_API
twa_graph_ptr sum(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \brief Sum two twa into a new twa, performing the union of the two input
/// automatons.
///
/// \param left Left term of the sum.
/// \param right Right term of the sum.
/// \param left_state Initial state of the left term of the sum.
/// \param right_state Initial state of the right term of the sum.
/// \return A spot::twa_graph containing the sum of \a left and \a right
SPOT_API
twa_graph_ptr sum(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state);
/// \brief Sum two twa into a new twa, using an universal initial transition,
/// performing the intersection of the two languages of the input automatons.
///
/// \param left Left term of the sum.
/// \param right Right term of the sum.
/// \return A spot::twa_graph containing the sum of \a left and \a right
SPOT_API
twa_graph_ptr sum_and(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \brief Sum two twa into a new twa, using an universal initial transition,
/// performing the intersection of the two languages of the input automatons.
///
/// \param left Left term of the sum.
/// \param right Right term of the sum.
/// \param left_state Initial state of the left term of the sum.
/// \param right_state Initial state of the right term of the sum.
/// \return A spot::twa_graph containing the sum of \a left and \a right
SPOT_API
twa_graph_ptr sum_and(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state);
}
......@@ -78,6 +78,7 @@ check_PROGRAMS = \
core/ltl2dot \
core/ltl2text \
core/ltlrel \
core/ltlsum \
core/lunabbrev \
core/nequals \
core/nenoform \
......@@ -122,6 +123,7 @@ core_ltl2dot_SOURCES = core/readltl.cc
core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
core_ltl2text_SOURCES = core/readltl.cc
core_ltlrel_SOURCES = core/ltlrel.cc
core_ltlsum_SOURCES = core/ltlsum.cc
core_lunabbrev_SOURCES = core/equalsf.cc
core_lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ie"'
core_nenoform_SOURCES = core/equalsf.cc
......@@ -166,6 +168,7 @@ TESTS_tl = \
core/ltlgrind.test \
core/ltlcrossgrind.test \
core/ltlfilt.test \
core/ltlsum.test \
core/exclusive-ltl.test \
core/latex.test \
core/lbt.test \
......@@ -230,10 +233,16 @@ TESTS_twa = \
core/ltl2neverclaim.test \
core/ltl2neverclaim-lbtt.test \
core/ltlprod.test \
core/ltlsum.test \
core/explprod.test \
core/explpro2.test \
core/explpro3.test \
core/explpro4.test \
core/explsum.test \
core/explsu2.test \
core/explsu3.test \
core/explsu4.test \
core/explsu5.test \
core/tripprod.test \
core/dupexp.test \
core/exclusive-tgba.test \
......@@ -351,6 +360,7 @@ TESTS_python = \
python/setacc.py \
python/sccfilter.py \
python/setxor.py \
python/sumexpt.py \
python/trival.py \
$(TESTS_ipython)
endif
......
......@@ -35,6 +35,7 @@ ltl2text
ltlmagic
ltlprod
ltlrel
ltlsum
lunabbrev
Makefile
Makefile.in
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 Laboratoire
# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
# Coopératifs (SRC), Université Pierre et Marie Curie.
Please register or sign in to reply
#
# 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
cat >false1 <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[t] 0 {0}
--END--
EOF
cat >false2 <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[t] 0
--END--
EOF
cat >expected <<'EOF'
HOA: v1
States: 3
Start: 2
AP: 1 "a"
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {0}
State: 1
[t] 1 {0}
State: 2
[t] 0
[t] 1
--END--
EOF
run 0 autfilt false1 --sum false2 --hoaf=t | tee stdout
run 0 autfilt -F stdout --isomorph expected
rm false1 false2 stdout expected
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 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.
#
# 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
cat >input1 <<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 0 {0}
[1] 1
State: 1
[1] 1
--END--
EOF
cat >input2 <<EOF
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[1] 0 {0}
[0] 0
--END--
EOF
cat >expected <<'EOF'
HOA: v1
States: 4
Start: 3
AP: 2 "a" "b"
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[1] 1
[0] 0 {0}
State: 1
[1] 1
State: 2
[0] 2 {0}
[1] 2 {0 1}
State: 3
[0] 0