Commit fd1f6c4d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Preliminirary support for generic acceptance.

* src/tgba/acc.hh: Add creation and printing of generic acceptance
code.
* src/tgba/acc.cc: New file.
* src/tgba/Makefile.am: Add it.
* src/tgbatest/acc.cc: More tests.
* src/tgbatest/acc.test: Update.
* src/tgba/tgba.hh (set_acceptance, get_acceptance): New methods.
* src/tgba/tgbagraph.hh: Store acceptance code.
* src/hoaparse/hoaparse.yy: Read any acceptance.
* src/dstarparse/nsa2tgba.cc, src/ta/taexplicit.cc,
src/tgba/tgbaproduct.cc, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/degen.cc, src/tgbaalgos/hoa.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/product.cc, src/tgbaalgos/stutter.cc,
src/tgbatest/hoaparse.test: Adjust.
parent c61f053e
......@@ -199,6 +199,7 @@ namespace spot
while (i != bs2num.end())
delete (i++)->first.pend;
res->acc().set_generalized_buchi();
return res;
}
......
......@@ -135,6 +135,7 @@
spot::acc_cond::mark_t mark;
pair* p;
std::list<pair>* list;
spot::acc_cond::acc_code* code;
}
%code
......@@ -201,6 +202,7 @@
%type <p> nc-transition nc-src-dest
%type <list> nc-transitions nc-transition-block
%type <str> nc-one-ident nc-ident-list
%type <code> acceptance-cond
/**** LBTT tokens *****/
// Also using INT, STRING
......@@ -216,6 +218,7 @@
%destructor { delete $$; } <str>
%destructor { bdd_delref($$); } <b>
%destructor { bdd_delref($$->first); delete $$->second; delete $$; } <p>
%destructor { delete $$; } <code>
%destructor {
for (std::list<pair>::iterator i = $$->begin();
i != $$->end(); ++i)
......@@ -484,7 +487,7 @@ header-item: "States:" INT
}
else
{
res.h->aut->set_acceptance_conditions($2);
res.h->aut->acc().add_sets($2);
res.accset = $2;
res.accset_loc = @1 + @2;
}
......@@ -492,6 +495,8 @@ header-item: "States:" INT
acceptance-cond
{
res.ignore_more_acc = true;
res.h->aut->set_acceptance($2, *$4);
delete $4;
}
| "acc-name:" IDENTIFIER acc-spec
{
......@@ -659,36 +664,65 @@ acc-set: INT
acceptance-cond: IDENTIFIER '(' acc-set ')'
{
if (!res.ignore_more_acc && *$1 != "Inf")
error(@1, "this implementation only supports "
"'Inf' acceptance");
if ($3 != -1U)
res.pos_acc_sets |= res.h->aut->acc().mark($3);
{
res.pos_acc_sets |= res.h->aut->acc().mark($3);
if (*$1 == "Inf")
$$ = new spot::acc_cond::acc_code
(res.h->aut->acc().inf({$3}));
else
$$ = new spot::acc_cond::acc_code
(res.h->aut->acc().fin({$3}));
}
else
{
$$ = new spot::acc_cond::acc_code;
}
delete $1;
}
| IDENTIFIER '(' '!' acc-set ')'
{
if (!res.ignore_more_acc && *$1 != "Inf")
error(@1, "this implementation only supports "
"'Inf' acceptance");
if ($4 != -1U)
res.neg_acc_sets |= res.h->aut->acc().mark($4);
{
res.neg_acc_sets |= res.h->aut->acc().mark($4);
if (*$1 == "Inf")
$$ = new spot::acc_cond::acc_code
(res.h->aut->acc().inf_neg({$4}));
else
$$ = new spot::acc_cond::acc_code
(res.h->aut->acc().fin_neg({$4}));
}
else
{
$$ = new spot::acc_cond::acc_code;
}
delete $1;
}
| '(' acceptance-cond ')'
{
$$ = $2;
}
| acceptance-cond '&' acceptance-cond
{
$3->append_and(std::move(*$1));
$$ = $3;
delete $1;
}
| acceptance-cond '|' acceptance-cond
{
if (!res.ignore_more_acc)
error(@2, "this implementation does not support "
"disjunction in acceptance conditions");
$3->append_or(std::move(*$1));
$$ = $3;
delete $1;
}
| 't'
{
$$ = new spot::acc_cond::acc_code;
}
| 'f'
{
if (!res.ignore_more_acc)
error(@$, "this implementation does not support "
"false acceptance");
{
$$ = new spot::acc_cond::acc_code(res.h->aut->acc().fin({}));
}
}
......@@ -1213,7 +1247,10 @@ nc-transition:
lbtt: lbtt-header lbtt-body ENDAUT
{
res.pos_acc_sets = res.h->aut->acc().all_sets();
auto& acc = res.h->aut->acc();
unsigned num = acc.num_sets();
res.h->aut->set_acceptance_conditions(num);
res.pos_acc_sets = acc.all_sets();
assert(!res.states_map.empty());
auto n = res.states_map.size();
if (n != (unsigned) res.states)
......@@ -1375,33 +1412,113 @@ static void fill_guards(result_& r)
void
hoayy::parser::error(const location_type& location,
const std::string& message)
const std::string& message)
{
error_list.emplace_back(location, message);
}
static spot::acc_cond::acc_code
fix_acceptance_aux(spot::acc_cond& acc,
spot::acc_cond::acc_code in, unsigned pos,
spot::acc_cond::mark_t onlyneg,
spot::acc_cond::mark_t both,
unsigned base)
{
auto& w = in[pos];
switch (w.op)
{
case spot::acc_cond::acc_op::And:
{
unsigned sub = pos - w.size;
--pos;
auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
pos -= in[pos].size;
while (sub < pos)
{
--pos;
c.append_and(fix_acceptance_aux(acc, in, pos, onlyneg, both, base));
pos -= in[pos].size;
}
return c;
}
case spot::acc_cond::acc_op::Or:
{
unsigned sub = pos - w.size;
--pos;
auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
pos -= in[pos].size;
while (sub < pos)
{
--pos;
c.append_or(fix_acceptance_aux(acc, in, pos, onlyneg, both, base));
pos -= in[pos].size;
}
return c;
}
case spot::acc_cond::acc_op::Inf:
return acc.inf(in[pos - 1].mark);
case spot::acc_cond::acc_op::Fin:
return acc.fin(in[pos - 1].mark);
case spot::acc_cond::acc_op::FinNeg:
{
auto m = in[pos - 1].mark;
auto c = acc.fin(onlyneg & m);
spot::acc_cond::mark_t tmp = 0U;
for (auto i: both.sets())
{
if (m.has(i))
tmp.set(base);
++base;
}
if (tmp)
c.append_or(acc.fin(tmp));
return c;
}
case spot::acc_cond::acc_op::InfNeg:
{
auto m = in[pos - 1].mark;
auto c = acc.inf(onlyneg & m);
spot::acc_cond::mark_t tmp = 0U;
for (auto i: both.sets())
{
if (m.has(i))
tmp.set(base);
++base;
}
if (tmp)
c.append_and(acc.inf(tmp));
return c;
}
}
SPOT_UNREACHABLE();
return {};
}
static void fix_acceptance(result_& r)
{
auto& acc = r.h->aut->acc();
// Compute the unused sets before possibly adding some below.
auto unused = acc.comp(r.neg_acc_sets | r.pos_acc_sets);
// If a set x appears only as Inf(!x), we can complement it so that
// we work with Inf(x) instead.
if (auto onlyneg = r.neg_acc_sets - r.pos_acc_sets)
for (auto& t: r.h->aut->transition_vector())
t.acc ^= onlyneg;
auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
if (onlyneg)
{
for (auto& t: r.h->aut->transition_vector())
t.acc ^= onlyneg;
}
// However if set x is used elsewhere, for instance in
// Inf(!x) & Inf(x)
// complementing x would be wrong. We need to create a
// new set, y, that is the complement of x, and rewrite
// this as Inf(y) & Inf(x).
if (auto both = r.neg_acc_sets & r.pos_acc_sets)
auto both = r.neg_acc_sets & r.pos_acc_sets;
unsigned base = 0;
if (both)
{
auto v = acc.sets(both);
auto vs = v.size();
unsigned base = acc.add_sets(vs);
base = acc.add_sets(vs);
for (auto& t: r.h->aut->transition_vector())
if ((t.acc & both) != both)
for (unsigned i = 0; i < vs; ++i)
......@@ -1409,15 +1526,13 @@ static void fix_acceptance(result_& r)
t.acc |= acc.mark(base + i);
}
// Remove all acceptance sets that are not used in the acceptance
// condition. Because the rest of the code still assume that all
// acceptance sets have to be seen. See
// https://github.com/adl/hoaf/issues/36
if (unused)
if (onlyneg || both)
{
for (auto& t: r.h->aut->transition_vector())
t.acc = acc.strip(t.acc, unused);
r.h->aut->set_acceptance_conditions(acc.num_sets() - unused.count());
auto& acc = r.h->aut->acc();
auto code = acc.get_acceptance();
r.h->aut->set_acceptance(acc.num_sets(),
fix_acceptance_aux(acc, code, code.size() - 1,
onlyneg, both, base));
}
}
......
......@@ -359,6 +359,7 @@ namespace spot
{
get_dict()->register_all_variables_of(&tgba_, this);
acc().add_sets(n_acc);
acc().set_generalized_buchi();
if (artificial_initial_state != 0)
{
state_ta_explicit* is = add_state(artificial_initial_state);
......
......@@ -41,6 +41,7 @@ tgba_HEADERS = \
noinst_LTLIBRARIES = libtgba.la
libtgba_la_SOURCES = \
acc.cc \
bdddict.cc \
bddprint.cc \
formula2bdd.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement de
// l'Epita.
//
// 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 <iostream>
#include "acc.hh"
namespace spot
{
std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m)
{
auto a = m.id;
os << '{';
unsigned level = 0;
const char* comma = "";
while (a)
{
if (a & 1)
{
os << comma << level;
comma = ",";
}
a >>= 1;
++level;
}
os << '}';
return os;
}
namespace
{
static void
print_code(std::ostream& os,
const acc_cond::acc_code& code, unsigned pos)
{
const char* op = " | ";
auto& w = code[pos];
const char* negated = "";
bool top = pos == code.size() - 1;
switch (w.op)
{
case acc_cond::acc_op::And:
op = " & ";
case acc_cond::acc_op::Or:
{
unsigned sub = pos - w.size;
if (!top)
os << '(';
bool first = true;
while (sub < pos)
{
--pos;
if (first)
first = false;
else
os << op;
print_code(os, code, pos);
pos -= code[pos].size;
}
if (!top)
os << ')';
}
break;
case acc_cond::acc_op::InfNeg:
negated = "!";
case acc_cond::acc_op::Inf:
{
auto a = code[pos - 1].mark.id;
if (a == 0U)
{
os << 't';
}
else
{
unsigned level = 0;
const char* and_ = "";
if (!top)
os << '(';
while (a)
{
if (a & 1)
{
os << and_ << "Inf(" << negated << level << ')';
and_ = "&";
}
a >>= 1;
++level;
}
if (!top)
os << ')';
}
}
break;
case acc_cond::acc_op::FinNeg:
negated = "!";
case acc_cond::acc_op::Fin:
{
auto a = code[pos - 1].mark.id;
if (a == 0U)
{
os << 'f';
}
else
{
unsigned level = 0;
const char* or_ = "";
if (!top)
os << '(';
while (a)
{
if (a & 1)
{
os << or_ << "Fin(" << negated << level << ')';
or_ = "|";
}
a >>= 1;
++level;
}
if (!top)
os << ')';
}
}
break;
}
}
static bool
eval(acc_cond::mark_t inf, acc_cond::mark_t fin,
const acc_cond::acc_code& code, unsigned pos)
{
auto& w = code[pos];
switch (w.op)
{
case acc_cond::acc_op::And:
{
unsigned sub = pos - w.size;
while (sub < pos)
{
--pos;
if (!eval(inf, fin, code, pos))
return false;
pos -= code[pos].size;
}
return true;
}
case acc_cond::acc_op::Or:
{
unsigned sub = pos - w.size;
while (sub < pos)
{
--pos;
if (eval(inf, fin, code, pos))
return true;
pos -= code[pos].size;
}
return false;
}
case acc_cond::acc_op::Inf:
return (code[pos - 1].mark & inf) == code[pos - 1].mark;
case acc_cond::acc_op::Fin:
return (code[pos - 1].mark & fin) != 0U;
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
return false;
}
}
bool acc_cond::accepting(mark_t inf, mark_t fin) const
{
if (code_.empty())
return true;
return eval(inf, fin, code_, code_.size() - 1);
}
bool acc_cond::accepting(mark_t inf) const
{
if (uses_fin_acceptance())
throw std::runtime_error
("Fin acceptance is not supported by this code path.");
return accepting(inf, 0U);
}
bool acc_cond::check_fin_acceptance() const
{
if (code_.empty())
return false;
unsigned pos = code_.size();
do
{
switch (code_[pos - 1].op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
--pos;
break;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
pos -= 2;
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg:
return true;
}
}
while (pos > 0);
return false;
}
std::ostream& operator<<(std::ostream& os,
const spot::acc_cond::acc_code& code)
{
if (code.empty())
os << 't';
else
print_code(os, code, code.size() - 1);
return os;
}
}
......@@ -25,10 +25,11 @@
# include <sstream>
# include <vector>
# include "ltlenv/defaultenv.hh"
# include <iostream>
namespace spot
{
class acc_cond
class SPOT_API acc_cond
{
public:
struct mark_t
......@@ -90,7 +91,6 @@ namespace spot
return id != 0;
}
bool has(unsigned u) const
{
return id & (1U << u);
......@@ -170,25 +170,142 @@ namespace spot
return *this;
}
friend std::ostream& operator<<(std::ostream& os, mark_t m)
template<class iterator>
void fill(iterator here) const
{
auto a = m.id;
os << '{';
auto a = id;
unsigned level = 0;
const char* comma = "";
while (a)
{
if (a & 1)
*here++ = level;
++level;
a >>= 1;
}
}
// FIXME: Return some iterable object without building a vector.
std::vector<unsigned> sets() const
{
std::vector<unsigned> res;
fill(std::back_inserter(res));
return res;
}
SPOT_API
friend std::ostream& operator<<(std::ostream& os, mark_t m);
};
// This encodes either an operator or set of acceptance sets.
enum class acc_op : unsigned char
{ Inf, Fin, InfNeg, FinNeg, And, Or };
union acc_word
{
mark_t mark;
struct {
acc_op op; // Operator
unsigned char size; // Size of the subtree (number of acc_word),
// not counting this node.
};
};
struct acc_code: public std::vector<acc_word>
{
bool is_true() const
{
unsigned s = size();
return s == 0
|| ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U);
}
bool is_false() const
{
unsigned s = size();
return s > 1
&& (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U;
}
void append_and(acc_code&& r)
{
if (is_true() || r.is_false())
{
*this = std::move(r);
return;
}
if (is_false() || r.is_true())
return;
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
// Inf(a) & Inf(b) = Inf(a & b)
if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf)
|| ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg))
{
(*this)[s - 1].mark |= r[rs - 1].mark;