do not use non-standard anonymous structs
For #214, as observed by Thibaud Michaud. * spot/twa/acc.hh: Name the anonymous struct. * spot/twa/acc.hh, spot/twa/acc.cc, spot/parseaut/parseaut.yy, spot/twaalgos/dtwasat.cc, spot/twaalgos/remfin.cc, spot/twaalgos/sepsets.cc, spot/twaalgos/totgba.cc: Adjust all usages. * NEWS: Mention the renaming.
This commit is contained in:
Alexandre Duret-Lutz
parent
954b9d2074
commit
70c70a63a3
8 changed files with 169 additions and 157 deletions
6
NEWS
6
NEWS
|
|
@ -14,6 +14,12 @@ New in spot 2.3.0.dev (not yet released)
|
||||||
- spot::ltsmin_model::kripke() forgot to register the "dead"
|
- spot::ltsmin_model::kripke() forgot to register the "dead"
|
||||||
proposition.
|
proposition.
|
||||||
|
|
||||||
|
- The spot::acc_word type (used to construct acceptance condition)
|
||||||
|
was using some non-standard anonymous struct. It is unlikely that
|
||||||
|
this type was actually used outside Spot, but if you do use it,
|
||||||
|
spot::acc_word::op and spot::acc_word::type had to be renamed as
|
||||||
|
spot::acc_word::sub.op and spot::acc_word::sub.type.
|
||||||
|
|
||||||
New in spot 2.3 (2017-01-19)
|
New in spot 2.3 (2017-01-19)
|
||||||
|
|
||||||
Build:
|
Build:
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
/* -*- coding: utf-8 -*-
|
/* -*- coding: utf-8 -*-
|
||||||
** Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
|
** Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
|
||||||
** Développement de l'Epita (LRDE).
|
** Développement de l'Epita (LRDE).
|
||||||
**
|
**
|
||||||
** This file is part of Spot, a model checking library.
|
** This file is part of Spot, a model checking library.
|
||||||
|
|
@ -2048,33 +2048,33 @@ fix_acceptance_aux(spot::acc_cond& acc,
|
||||||
unsigned base)
|
unsigned base)
|
||||||
{
|
{
|
||||||
auto& w = in[pos];
|
auto& w = in[pos];
|
||||||
switch (w.op)
|
switch (w.sub.op)
|
||||||
{
|
{
|
||||||
case spot::acc_cond::acc_op::And:
|
case spot::acc_cond::acc_op::And:
|
||||||
{
|
{
|
||||||
unsigned sub = pos - w.size;
|
unsigned sub = pos - w.sub.size;
|
||||||
--pos;
|
--pos;
|
||||||
auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
||||||
pos -= in[pos].size;
|
pos -= in[pos].sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
c &= fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
c &= fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
||||||
pos -= in[pos].size;
|
pos -= in[pos].sub.size;
|
||||||
}
|
}
|
||||||
return c;
|
return c;
|
||||||
}
|
}
|
||||||
case spot::acc_cond::acc_op::Or:
|
case spot::acc_cond::acc_op::Or:
|
||||||
{
|
{
|
||||||
unsigned sub = pos - w.size;
|
unsigned sub = pos - w.sub.size;
|
||||||
--pos;
|
--pos;
|
||||||
auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
||||||
pos -= in[pos].size;
|
pos -= in[pos].sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
c |= fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
c |= fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
|
||||||
pos -= in[pos].size;
|
pos -= in[pos].sub.size;
|
||||||
}
|
}
|
||||||
return c;
|
return c;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
104
spot/twa/acc.cc
104
spot/twa/acc.cc
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
|
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
|
||||||
// de l'Epita.
|
// Développement de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -73,14 +73,14 @@ namespace spot
|
||||||
auto& w = code[pos];
|
auto& w = code[pos];
|
||||||
const char* negated = "";
|
const char* negated = "";
|
||||||
bool top = pos == code.size() - 1;
|
bool top = pos == code.size() - 1;
|
||||||
switch (w.op)
|
switch (w.sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
op = html ? " & " : " & ";
|
op = html ? " & " : " & ";
|
||||||
SPOT_FALLTHROUGH;
|
SPOT_FALLTHROUGH;
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
{
|
{
|
||||||
unsigned sub = pos - w.size;
|
unsigned sub = pos - w.sub.size;
|
||||||
if (!top)
|
if (!top)
|
||||||
os << '(';
|
os << '(';
|
||||||
bool first = true;
|
bool first = true;
|
||||||
|
|
@ -92,7 +92,7 @@ namespace spot
|
||||||
else
|
else
|
||||||
os << op;
|
os << op;
|
||||||
print_code<html>(os, code, pos, set_printer);
|
print_code<html>(os, code, pos, set_printer);
|
||||||
pos -= code[pos].size;
|
pos -= code[pos].sub.size;
|
||||||
}
|
}
|
||||||
if (!top)
|
if (!top)
|
||||||
os << ')';
|
os << ')';
|
||||||
|
|
@ -177,29 +177,29 @@ namespace spot
|
||||||
static bool
|
static bool
|
||||||
eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
|
eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
{
|
{
|
||||||
auto sub = pos - pos->size;
|
auto sub = pos - pos->sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
if (!eval(inf, pos))
|
if (!eval(inf, pos))
|
||||||
return false;
|
return false;
|
||||||
pos -= pos->size;
|
pos -= pos->sub.size;
|
||||||
}
|
}
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
{
|
{
|
||||||
auto sub = pos - pos->size;
|
auto sub = pos - pos->sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
if (eval(inf, pos))
|
if (eval(inf, pos))
|
||||||
return true;
|
return true;
|
||||||
pos -= pos->size;
|
pos -= pos->sub.size;
|
||||||
}
|
}
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
@ -218,29 +218,29 @@ namespace spot
|
||||||
static bool
|
static bool
|
||||||
inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
|
inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
{
|
{
|
||||||
auto sub = pos - pos->size;
|
auto sub = pos - pos->sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
if (!inf_eval(inf, pos))
|
if (!inf_eval(inf, pos))
|
||||||
return false;
|
return false;
|
||||||
pos -= pos->size;
|
pos -= pos->sub.size;
|
||||||
}
|
}
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
{
|
{
|
||||||
auto sub = pos - pos->size;
|
auto sub = pos - pos->sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
if (inf_eval(inf, pos))
|
if (inf_eval(inf, pos))
|
||||||
return true;
|
return true;
|
||||||
pos -= pos->size;
|
pos -= pos->sub.size;
|
||||||
}
|
}
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
@ -259,11 +259,11 @@ namespace spot
|
||||||
static acc_cond::mark_t
|
static acc_cond::mark_t
|
||||||
eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
|
eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
{
|
{
|
||||||
auto sub = pos - pos->size;
|
auto sub = pos - pos->sub.size;
|
||||||
acc_cond::mark_t m = 0U;
|
acc_cond::mark_t m = 0U;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
|
|
@ -272,19 +272,19 @@ namespace spot
|
||||||
m |= s;
|
m |= s;
|
||||||
else
|
else
|
||||||
return 0U;
|
return 0U;
|
||||||
pos -= pos->size;
|
pos -= pos->sub.size;
|
||||||
}
|
}
|
||||||
return m;
|
return m;
|
||||||
}
|
}
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
{
|
{
|
||||||
auto sub = pos - pos->size;
|
auto sub = pos - pos->sub.size;
|
||||||
while (sub < pos)
|
while (sub < pos)
|
||||||
{
|
{
|
||||||
--pos;
|
--pos;
|
||||||
if (auto s = eval_sets(inf, pos))
|
if (auto s = eval_sets(inf, pos))
|
||||||
return s;
|
return s;
|
||||||
pos -= pos->size;
|
pos -= pos->sub.size;
|
||||||
}
|
}
|
||||||
return 0U;
|
return 0U;
|
||||||
}
|
}
|
||||||
|
|
@ -334,7 +334,7 @@ namespace spot
|
||||||
unsigned pos = code_.size();
|
unsigned pos = code_.size();
|
||||||
do
|
do
|
||||||
{
|
{
|
||||||
switch (code_[pos - 1].op)
|
switch (code_[pos - 1].sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
|
|
@ -369,8 +369,8 @@ namespace spot
|
||||||
acc_cond::acc_op lowop,
|
acc_cond::acc_op lowop,
|
||||||
acc_cond::mark_t all_sets)
|
acc_cond::mark_t all_sets)
|
||||||
{
|
{
|
||||||
unsigned s = code.back().size;
|
unsigned s = code.back().sub.size;
|
||||||
auto mainop = code.back().op;
|
auto mainop = code.back().sub.op;
|
||||||
if (mainop == highop)
|
if (mainop == highop)
|
||||||
{
|
{
|
||||||
// The size must be a multiple of 5.
|
// The size must be a multiple of 5.
|
||||||
|
|
@ -388,11 +388,11 @@ namespace spot
|
||||||
acc_cond::mark_t seen_inf = 0U;
|
acc_cond::mark_t seen_inf = 0U;
|
||||||
while (s)
|
while (s)
|
||||||
{
|
{
|
||||||
if (code[--s].op != lowop)
|
if (code[--s].sub.op != lowop)
|
||||||
return false;
|
return false;
|
||||||
auto o1 = code[--s].op;
|
auto o1 = code[--s].sub.op;
|
||||||
auto m1 = code[--s].mark;
|
auto m1 = code[--s].mark;
|
||||||
auto o2 = code[--s].op;
|
auto o2 = code[--s].sub.op;
|
||||||
auto m2 = code[--s].mark;
|
auto m2 = code[--s].mark;
|
||||||
|
|
||||||
// We assume
|
// We assume
|
||||||
|
|
@ -454,10 +454,10 @@ namespace spot
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
if (code_.is_t()
|
if (code_.is_t()
|
||||||
|| code_.back().op != acc_op::Or)
|
|| code_.back().sub.op != acc_op::Or)
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
auto s = code_.back().size;
|
auto s = code_.back().sub.size;
|
||||||
acc_cond::mark_t seen_fin = 0U;
|
acc_cond::mark_t seen_fin = 0U;
|
||||||
acc_cond::mark_t seen_inf = 0U;
|
acc_cond::mark_t seen_inf = 0U;
|
||||||
// Each pairs is the position of a Fin followed
|
// Each pairs is the position of a Fin followed
|
||||||
|
|
@ -466,11 +466,11 @@ namespace spot
|
||||||
while (s)
|
while (s)
|
||||||
{
|
{
|
||||||
--s;
|
--s;
|
||||||
if (code_[s].op == acc_op::And)
|
if (code_[s].sub.op == acc_op::And)
|
||||||
{
|
{
|
||||||
auto o1 = code_[--s].op;
|
auto o1 = code_[--s].sub.op;
|
||||||
auto m1 = code_[--s].mark;
|
auto m1 = code_[--s].mark;
|
||||||
auto o2 = code_[--s].op;
|
auto o2 = code_[--s].sub.op;
|
||||||
auto m2 = code_[--s].mark;
|
auto m2 = code_[--s].mark;
|
||||||
|
|
||||||
// We assume
|
// We assume
|
||||||
|
|
@ -503,7 +503,7 @@ namespace spot
|
||||||
seen_fin |= m1;
|
seen_fin |= m1;
|
||||||
seen_inf |= m2;
|
seen_inf |= m2;
|
||||||
}
|
}
|
||||||
else if (code_[s].op == acc_op::Fin)
|
else if (code_[s].sub.op == acc_op::Fin)
|
||||||
{
|
{
|
||||||
auto m1 = code_[--s].mark;
|
auto m1 = code_[--s].mark;
|
||||||
for (auto s: m1.sets())
|
for (auto s: m1.sets())
|
||||||
|
|
@ -597,9 +597,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map)
|
bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map)
|
||||||
{
|
{
|
||||||
auto sz = c->size;
|
auto sz = c->sub.size;
|
||||||
auto start = c - sz - 1;
|
auto start = c - sz - 1;
|
||||||
auto op = c->op;
|
auto op = c->sub.op;
|
||||||
switch (op)
|
switch (op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
|
|
@ -609,7 +609,7 @@ namespace spot
|
||||||
do
|
do
|
||||||
{
|
{
|
||||||
res |= to_bdd_rec(c, map);
|
res |= to_bdd_rec(c, map);
|
||||||
c -= c->size + 1;
|
c -= c->sub.size + 1;
|
||||||
}
|
}
|
||||||
while (c > start);
|
while (c > start);
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -621,7 +621,7 @@ namespace spot
|
||||||
do
|
do
|
||||||
{
|
{
|
||||||
res &= to_bdd_rec(c, map);
|
res &= to_bdd_rec(c, map);
|
||||||
c -= c->size + 1;
|
c -= c->sub.size + 1;
|
||||||
}
|
}
|
||||||
while (c > start);
|
while (c > start);
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -1005,16 +1005,16 @@ namespace spot
|
||||||
auto pos = &back();
|
auto pos = &back();
|
||||||
auto start = &front();
|
auto start = &front();
|
||||||
auto and_scope = pos + 1;
|
auto and_scope = pos + 1;
|
||||||
if (pos->op == acc_cond::acc_op::Or)
|
if (pos->sub.op == acc_cond::acc_op::Or)
|
||||||
--pos;
|
--pos;
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
return false;
|
return false;
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
and_scope = std::min(and_scope, pos - pos->size);
|
and_scope = std::min(and_scope, pos - pos->sub.size);
|
||||||
--pos;
|
--pos;
|
||||||
break;
|
break;
|
||||||
case acc_cond::acc_op::Fin:
|
case acc_cond::acc_op::Fin:
|
||||||
|
|
@ -1038,16 +1038,16 @@ namespace spot
|
||||||
auto pos = &back();
|
auto pos = &back();
|
||||||
auto start = &front();
|
auto start = &front();
|
||||||
auto or_scope = pos + 1;
|
auto or_scope = pos + 1;
|
||||||
if (pos->op == acc_cond::acc_op::And)
|
if (pos->sub.op == acc_cond::acc_op::And)
|
||||||
--pos;
|
--pos;
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
return false;
|
return false;
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
or_scope = std::min(or_scope, pos - pos->size);
|
or_scope = std::min(or_scope, pos - pos->sub.size);
|
||||||
--pos;
|
--pos;
|
||||||
break;
|
break;
|
||||||
case acc_cond::acc_op::Inf:
|
case acc_cond::acc_op::Inf:
|
||||||
|
|
@ -1068,8 +1068,8 @@ namespace spot
|
||||||
{
|
{
|
||||||
acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos)
|
acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos)
|
||||||
{
|
{
|
||||||
auto start = pos - pos->size;
|
auto start = pos - pos->sub.size;
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
{
|
{
|
||||||
|
|
@ -1079,7 +1079,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
auto tmp = complement_rec(pos) | std::move(res);
|
auto tmp = complement_rec(pos) | std::move(res);
|
||||||
std::swap(tmp, res);
|
std::swap(tmp, res);
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
while (pos > start);
|
while (pos > start);
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -1092,7 +1092,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
auto tmp = complement_rec(pos) & std::move(res);
|
auto tmp = complement_rec(pos) & std::move(res);
|
||||||
std::swap(tmp, res);
|
std::swap(tmp, res);
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
while (pos > start);
|
while (pos > start);
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -1125,8 +1125,8 @@ namespace spot
|
||||||
static acc_cond::acc_code
|
static acc_cond::acc_code
|
||||||
strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing)
|
strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing)
|
||||||
{
|
{
|
||||||
auto start = pos - pos->size;
|
auto start = pos - pos->sub.size;
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
{
|
{
|
||||||
|
|
@ -1136,7 +1136,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
auto tmp = strip_rec(pos, rem, missing) & std::move(res);
|
auto tmp = strip_rec(pos, rem, missing) & std::move(res);
|
||||||
std::swap(tmp, res);
|
std::swap(tmp, res);
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
while (pos > start);
|
while (pos > start);
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -1149,7 +1149,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
auto tmp = strip_rec(pos, rem, missing) | std::move(res);
|
auto tmp = strip_rec(pos, rem, missing) | std::move(res);
|
||||||
std::swap(tmp, res);
|
std::swap(tmp, res);
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
while (pos > start);
|
while (pos > start);
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -1190,7 +1190,7 @@ namespace spot
|
||||||
auto end = &front();
|
auto end = &front();
|
||||||
while (pos > end)
|
while (pos > end)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
|
|
@ -1220,7 +1220,7 @@ namespace spot
|
||||||
auto end = &front();
|
auto end = &front();
|
||||||
while (pos > end)
|
while (pos > end)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
|
|
|
||||||
126
spot/twa/acc.hh
126
spot/twa/acc.hh
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
|
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita.
|
// Développement de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -294,7 +294,7 @@ namespace spot
|
||||||
acc_op op; // Operator
|
acc_op op; // Operator
|
||||||
unsigned short size; // Size of the subtree (number of acc_word),
|
unsigned short size; // Size of the subtree (number of acc_word),
|
||||||
// not counting this node.
|
// not counting this node.
|
||||||
};
|
} sub;
|
||||||
};
|
};
|
||||||
|
|
||||||
struct SPOT_API acc_code: public std::vector<acc_word>
|
struct SPOT_API acc_code: public std::vector<acc_word>
|
||||||
|
|
@ -306,10 +306,10 @@ namespace spot
|
||||||
return false;
|
return false;
|
||||||
while (pos > 0)
|
while (pos > 0)
|
||||||
{
|
{
|
||||||
auto op = (*this)[pos - 1].op;
|
auto op = (*this)[pos - 1].sub.op;
|
||||||
auto sz = (*this)[pos - 1].size;
|
auto sz = (*this)[pos - 1].sub.size;
|
||||||
if (other[pos - 1].op != op ||
|
if (other[pos - 1].sub.op != op ||
|
||||||
other[pos - 1].size != sz)
|
other[pos - 1].sub.size != sz)
|
||||||
return false;
|
return false;
|
||||||
switch (op)
|
switch (op)
|
||||||
{
|
{
|
||||||
|
|
@ -340,14 +340,14 @@ namespace spot
|
||||||
return false;
|
return false;
|
||||||
while (pos > 0)
|
while (pos > 0)
|
||||||
{
|
{
|
||||||
auto op = (*this)[pos - 1].op;
|
auto op = (*this)[pos - 1].sub.op;
|
||||||
auto oop = other[pos - 1].op;
|
auto oop = other[pos - 1].sub.op;
|
||||||
if (op < oop)
|
if (op < oop)
|
||||||
return true;
|
return true;
|
||||||
if (op > oop)
|
if (op > oop)
|
||||||
return false;
|
return false;
|
||||||
auto sz = (*this)[pos - 1].size;
|
auto sz = (*this)[pos - 1].sub.size;
|
||||||
auto osz = other[pos - 1].size;
|
auto osz = other[pos - 1].sub.size;
|
||||||
if (sz < osz)
|
if (sz < osz)
|
||||||
return true;
|
return true;
|
||||||
if (sz > osz)
|
if (sz > osz)
|
||||||
|
|
@ -398,15 +398,15 @@ namespace spot
|
||||||
bool is_t() const
|
bool is_t() const
|
||||||
{
|
{
|
||||||
unsigned s = size();
|
unsigned s = size();
|
||||||
return s == 0
|
return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
|
||||||
|| ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U);
|
&& (*this)[s - 2].mark == 0U);
|
||||||
}
|
}
|
||||||
|
|
||||||
bool is_f() const
|
bool is_f() const
|
||||||
{
|
{
|
||||||
unsigned s = size();
|
unsigned s = size();
|
||||||
return s > 1
|
return s > 1
|
||||||
&& (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U;
|
&& (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0U;
|
||||||
}
|
}
|
||||||
|
|
||||||
static acc_code f()
|
static acc_code f()
|
||||||
|
|
@ -414,8 +414,8 @@ namespace spot
|
||||||
acc_code res;
|
acc_code res;
|
||||||
res.resize(2);
|
res.resize(2);
|
||||||
res[0].mark = 0U;
|
res[0].mark = 0U;
|
||||||
res[1].op = acc_op::Fin;
|
res[1].sub.op = acc_op::Fin;
|
||||||
res[1].size = 1;
|
res[1].sub.size = 1;
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -429,8 +429,8 @@ namespace spot
|
||||||
acc_code res;
|
acc_code res;
|
||||||
res.resize(2);
|
res.resize(2);
|
||||||
res[0].mark = m;
|
res[0].mark = m;
|
||||||
res[1].op = acc_op::Fin;
|
res[1].sub.op = acc_op::Fin;
|
||||||
res[1].size = 1;
|
res[1].sub.size = 1;
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -444,8 +444,8 @@ namespace spot
|
||||||
acc_code res;
|
acc_code res;
|
||||||
res.resize(2);
|
res.resize(2);
|
||||||
res[0].mark = m;
|
res[0].mark = m;
|
||||||
res[1].op = acc_op::FinNeg;
|
res[1].sub.op = acc_op::FinNeg;
|
||||||
res[1].size = 1;
|
res[1].sub.size = 1;
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -459,8 +459,8 @@ namespace spot
|
||||||
acc_code res;
|
acc_code res;
|
||||||
res.resize(2);
|
res.resize(2);
|
||||||
res[0].mark = m;
|
res[0].mark = m;
|
||||||
res[1].op = acc_op::Inf;
|
res[1].sub.op = acc_op::Inf;
|
||||||
res[1].size = 1;
|
res[1].sub.size = 1;
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -474,8 +474,8 @@ namespace spot
|
||||||
acc_code res;
|
acc_code res;
|
||||||
res.resize(2);
|
res.resize(2);
|
||||||
res[0].mark = m;
|
res[0].mark = m;
|
||||||
res[1].op = acc_op::InfNeg;
|
res[1].sub.op = acc_op::InfNeg;
|
||||||
res[1].size = 1;
|
res[1].sub.size = 1;
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -572,8 +572,10 @@ namespace spot
|
||||||
unsigned rs = r.size() - 1;
|
unsigned rs = r.size() - 1;
|
||||||
// We want to group all Inf(x) operators:
|
// We want to group all Inf(x) operators:
|
||||||
// Inf(a) & Inf(b) = Inf(a & b)
|
// Inf(a) & Inf(b) = Inf(a & b)
|
||||||
if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf)
|
if (((*this)[s].sub.op == acc_op::Inf
|
||||||
|| ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg))
|
&& r[rs].sub.op == acc_op::Inf)
|
||||||
|
|| ((*this)[s].sub.op == acc_op::InfNeg
|
||||||
|
&& r[rs].sub.op == acc_op::InfNeg))
|
||||||
{
|
{
|
||||||
(*this)[s - 1].mark |= r[rs - 1].mark;
|
(*this)[s - 1].mark |= r[rs - 1].mark;
|
||||||
return *this;
|
return *this;
|
||||||
|
|
@ -585,43 +587,43 @@ namespace spot
|
||||||
// left_inf points to the left Inf mark if any.
|
// left_inf points to the left Inf mark if any.
|
||||||
// right_inf points to the right Inf mark if any.
|
// right_inf points to the right Inf mark if any.
|
||||||
acc_word* left_inf = nullptr;
|
acc_word* left_inf = nullptr;
|
||||||
if ((*this)[s].op == acc_op::And)
|
if ((*this)[s].sub.op == acc_op::And)
|
||||||
{
|
{
|
||||||
auto start = &(*this)[s] - (*this)[s].size;
|
auto start = &(*this)[s] - (*this)[s].sub.size;
|
||||||
auto pos = &(*this)[s] - 1;
|
auto pos = &(*this)[s] - 1;
|
||||||
pop_back();
|
pop_back();
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_op::Inf)
|
if (pos->sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
left_inf = pos - 1;
|
left_inf = pos - 1;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if ((*this)[s].op == acc_op::Inf)
|
else if ((*this)[s].sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
left_inf = &(*this)[s - 1];
|
left_inf = &(*this)[s - 1];
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_word* right_inf = nullptr;
|
acc_word* right_inf = nullptr;
|
||||||
auto right_end = &r.back();
|
auto right_end = &r.back();
|
||||||
if (right_end->op == acc_op::And)
|
if (right_end->sub.op == acc_op::And)
|
||||||
{
|
{
|
||||||
auto start = &r[0];
|
auto start = &r[0];
|
||||||
auto pos = --right_end;
|
auto pos = --right_end;
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_op::Inf)
|
if (pos->sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
right_inf = pos - 1;
|
right_inf = pos - 1;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (right_end->op == acc_op::Inf)
|
else if (right_end->sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
right_inf = right_end - 1;
|
right_inf = right_end - 1;
|
||||||
}
|
}
|
||||||
|
|
@ -645,8 +647,8 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_word w;
|
acc_word w;
|
||||||
w.op = acc_op::And;
|
w.sub.op = acc_op::And;
|
||||||
w.size = size();
|
w.sub.size = size();
|
||||||
emplace_back(w);
|
emplace_back(w);
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
@ -663,8 +665,10 @@ namespace spot
|
||||||
unsigned s = size() - 1;
|
unsigned s = size() - 1;
|
||||||
unsigned rs = r.size() - 1;
|
unsigned rs = r.size() - 1;
|
||||||
// Inf(a) & Inf(b) = Inf(a & b)
|
// Inf(a) & Inf(b) = Inf(a & b)
|
||||||
if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf)
|
if (((*this)[s].sub.op == acc_op::Inf
|
||||||
|| ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg))
|
&& r[rs].sub.op == acc_op::Inf)
|
||||||
|
|| ((*this)[s].sub.op == acc_op::InfNeg
|
||||||
|
&& r[rs].sub.op == acc_op::InfNeg))
|
||||||
{
|
{
|
||||||
(*this)[s - 1].mark |= r[rs - 1].mark;
|
(*this)[s - 1].mark |= r[rs - 1].mark;
|
||||||
return *this;
|
return *this;
|
||||||
|
|
@ -676,43 +680,43 @@ namespace spot
|
||||||
// left_inf points to the left Inf mark if any.
|
// left_inf points to the left Inf mark if any.
|
||||||
// right_inf points to the right Inf mark if any.
|
// right_inf points to the right Inf mark if any.
|
||||||
acc_word* left_inf = nullptr;
|
acc_word* left_inf = nullptr;
|
||||||
if ((*this)[s].op == acc_op::And)
|
if ((*this)[s].sub.op == acc_op::And)
|
||||||
{
|
{
|
||||||
auto start = &(*this)[s] - (*this)[s].size;
|
auto start = &(*this)[s] - (*this)[s].sub.size;
|
||||||
auto pos = &(*this)[s] - 1;
|
auto pos = &(*this)[s] - 1;
|
||||||
pop_back();
|
pop_back();
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_op::Inf)
|
if (pos->sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
left_inf = pos - 1;
|
left_inf = pos - 1;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if ((*this)[s].op == acc_op::Inf)
|
else if ((*this)[s].sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
left_inf = &(*this)[s - 1];
|
left_inf = &(*this)[s - 1];
|
||||||
}
|
}
|
||||||
|
|
||||||
const acc_word* right_inf = nullptr;
|
const acc_word* right_inf = nullptr;
|
||||||
auto right_end = &r.back();
|
auto right_end = &r.back();
|
||||||
if (right_end->op == acc_op::And)
|
if (right_end->sub.op == acc_op::And)
|
||||||
{
|
{
|
||||||
auto start = &r[0];
|
auto start = &r[0];
|
||||||
auto pos = --right_end;
|
auto pos = --right_end;
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_op::Inf)
|
if (pos->sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
right_inf = pos - 1;
|
right_inf = pos - 1;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (right_end->op == acc_op::Inf)
|
else if (right_end->sub.op == acc_op::Inf)
|
||||||
{
|
{
|
||||||
right_inf = right_end - 1;
|
right_inf = right_end - 1;
|
||||||
}
|
}
|
||||||
|
|
@ -736,8 +740,8 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_word w;
|
acc_word w;
|
||||||
w.op = acc_op::And;
|
w.sub.op = acc_op::And;
|
||||||
w.size = size();
|
w.sub.size = size();
|
||||||
emplace_back(w);
|
emplace_back(w);
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
@ -768,20 +772,22 @@ namespace spot
|
||||||
unsigned s = size() - 1;
|
unsigned s = size() - 1;
|
||||||
unsigned rs = r.size() - 1;
|
unsigned rs = r.size() - 1;
|
||||||
// Fin(a) | Fin(b) = Fin(a | b)
|
// Fin(a) | Fin(b) = Fin(a | b)
|
||||||
if (((*this)[s].op == acc_op::Fin && r[rs].op == acc_op::Fin)
|
if (((*this)[s].sub.op == acc_op::Fin
|
||||||
|| ((*this)[s].op == acc_op::FinNeg && r[rs].op == acc_op::FinNeg))
|
&& r[rs].sub.op == acc_op::Fin)
|
||||||
|
|| ((*this)[s].sub.op == acc_op::FinNeg
|
||||||
|
&& r[rs].sub.op == acc_op::FinNeg))
|
||||||
{
|
{
|
||||||
(*this)[s - 1].mark |= r[rs - 1].mark;
|
(*this)[s - 1].mark |= r[rs - 1].mark;
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
if ((*this)[s].op == acc_op::Or)
|
if ((*this)[s].sub.op == acc_op::Or)
|
||||||
pop_back();
|
pop_back();
|
||||||
if (r.back().op == acc_op::Or)
|
if (r.back().sub.op == acc_op::Or)
|
||||||
r.pop_back();
|
r.pop_back();
|
||||||
insert(this->end(), r.begin(), r.end());
|
insert(this->end(), r.begin(), r.end());
|
||||||
acc_word w;
|
acc_word w;
|
||||||
w.op = acc_op::Or;
|
w.sub.op = acc_op::Or;
|
||||||
w.size = size();
|
w.sub.size = size();
|
||||||
emplace_back(w);
|
emplace_back(w);
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
@ -812,7 +818,7 @@ namespace spot
|
||||||
unsigned pos = size();
|
unsigned pos = size();
|
||||||
do
|
do
|
||||||
{
|
{
|
||||||
switch ((*this)[pos - 1].op)
|
switch ((*this)[pos - 1].sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
|
|
@ -1008,7 +1014,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
unsigned s = code_.size();
|
unsigned s = code_.size();
|
||||||
return num_ == 1 &&
|
return num_ == 1 &&
|
||||||
s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets();
|
s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool is_co_buchi() const
|
bool is_co_buchi() const
|
||||||
|
|
@ -1024,15 +1030,15 @@ namespace spot
|
||||||
bool is_generalized_buchi() const
|
bool is_generalized_buchi() const
|
||||||
{
|
{
|
||||||
unsigned s = code_.size();
|
unsigned s = code_.size();
|
||||||
return (s == 0 && num_ == 0) ||
|
return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
|
||||||
(s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets());
|
&& code_[0].mark == all_sets());
|
||||||
}
|
}
|
||||||
|
|
||||||
bool is_generalized_co_buchi() const
|
bool is_generalized_co_buchi() const
|
||||||
{
|
{
|
||||||
unsigned s = code_.size();
|
unsigned s = code_.size();
|
||||||
return (s == 2 &&
|
return (s == 2 &&
|
||||||
code_[1].op == acc_op::Fin && code_[0].mark == all_sets());
|
code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
|
||||||
}
|
}
|
||||||
|
|
||||||
// Returns a number of pairs (>=0) if Rabin, or -1 else.
|
// Returns a number of pairs (>=0) if Rabin, or -1 else.
|
||||||
|
|
|
||||||
|
|
@ -128,27 +128,27 @@ namespace spot
|
||||||
trimming_map res;
|
trimming_map res;
|
||||||
auto acc = input_acc.to_dnf();
|
auto acc = input_acc.to_dnf();
|
||||||
auto pos = &acc.back();
|
auto pos = &acc.back();
|
||||||
if (pos->op == acc_cond::acc_op::Or)
|
if (pos->sub.op == acc_cond::acc_op::Or)
|
||||||
--pos;
|
--pos;
|
||||||
acc_cond::mark_t all_fin = 0U;
|
acc_cond::mark_t all_fin = 0U;
|
||||||
auto start = &acc.front();
|
auto start = &acc.front();
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_cond::acc_op::Fin)
|
if (pos->sub.op == acc_cond::acc_op::Fin)
|
||||||
{
|
{
|
||||||
// We have only a Fin term, without Inf.
|
// We have only a Fin term, without Inf.
|
||||||
// There is nothing to do about it.
|
// There is nothing to do about it.
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
// We have a conjunction of Fin and Inf sets.
|
// We have a conjunction of Fin and Inf sets.
|
||||||
auto end = pos - pos->size - 1;
|
auto end = pos - pos->sub.size - 1;
|
||||||
acc_cond::mark_t fin = 0U;
|
acc_cond::mark_t fin = 0U;
|
||||||
acc_cond::mark_t inf = 0U;
|
acc_cond::mark_t inf = 0U;
|
||||||
while (pos > end)
|
while (pos > end)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
--pos;
|
--pos;
|
||||||
|
|
|
||||||
|
|
@ -318,12 +318,12 @@ namespace spot
|
||||||
{
|
{
|
||||||
std::map<acc_cond::mark_t, acc_cond::acc_code> res;
|
std::map<acc_cond::mark_t, acc_cond::acc_code> res;
|
||||||
auto pos = &acc.back();
|
auto pos = &acc.back();
|
||||||
if (pos->op == acc_cond::acc_op::Or)
|
if (pos->sub.op == acc_cond::acc_op::Or)
|
||||||
--pos;
|
--pos;
|
||||||
auto start = &acc.front();
|
auto start = &acc.front();
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_cond::acc_op::Fin)
|
if (pos->sub.op == acc_cond::acc_op::Fin)
|
||||||
{
|
{
|
||||||
// We have only a Fin term, without Inf. In this case
|
// We have only a Fin term, without Inf. In this case
|
||||||
// only, the Fin() may encode a disjunction of sets.
|
// only, the Fin() may encode a disjunction of sets.
|
||||||
|
|
@ -333,17 +333,17 @@ namespace spot
|
||||||
fin.set(s);
|
fin.set(s);
|
||||||
res[fin] = acc_cond::acc_code{};
|
res[fin] = acc_cond::acc_code{};
|
||||||
}
|
}
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
// We have a conjunction of Fin and Inf sets.
|
// We have a conjunction of Fin and Inf sets.
|
||||||
auto end = pos - pos->size - 1;
|
auto end = pos - pos->sub.size - 1;
|
||||||
acc_cond::mark_t fin = 0U;
|
acc_cond::mark_t fin = 0U;
|
||||||
acc_cond::mark_t inf = 0U;
|
acc_cond::mark_t inf = 0U;
|
||||||
while (pos > end)
|
while (pos > end)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
--pos;
|
--pos;
|
||||||
|
|
@ -367,8 +367,8 @@ namespace spot
|
||||||
assert(pos == end);
|
assert(pos == end);
|
||||||
acc_cond::acc_word w[2];
|
acc_cond::acc_word w[2];
|
||||||
w[0].mark = inf;
|
w[0].mark = inf;
|
||||||
w[1].op = acc_cond::acc_op::Inf;
|
w[1].sub.op = acc_cond::acc_op::Inf;
|
||||||
w[1].size = 1;
|
w[1].sub.size = 1;
|
||||||
acc_cond::acc_code c;
|
acc_cond::acc_code c;
|
||||||
c.insert(c.end(), w, w + 2);
|
c.insert(c.end(), w, w + 2);
|
||||||
auto p = res.emplace(fin, c);
|
auto p = res.emplace(fin, c);
|
||||||
|
|
@ -428,27 +428,27 @@ namespace spot
|
||||||
acc_cond::mark_t inf_alone = 0U;
|
acc_cond::mark_t inf_alone = 0U;
|
||||||
acc_cond::mark_t fin_alone = 0U;
|
acc_cond::mark_t fin_alone = 0U;
|
||||||
|
|
||||||
auto s = code.back().size;
|
auto s = code.back().sub.size;
|
||||||
|
|
||||||
// Rabin 1
|
// Rabin 1
|
||||||
if (code.back().op == acc_cond::acc_op::And && s == 4)
|
if (code.back().sub.op == acc_cond::acc_op::And && s == 4)
|
||||||
goto start_and;
|
goto start_and;
|
||||||
// Co-Büchi
|
// Co-Büchi
|
||||||
else if (code.back().op == acc_cond::acc_op::Fin && s == 1)
|
else if (code.back().sub.op == acc_cond::acc_op::Fin && s == 1)
|
||||||
goto start_fin;
|
goto start_fin;
|
||||||
// Rabin >1
|
// Rabin >1
|
||||||
else if (code.back().op != acc_cond::acc_op::Or)
|
else if (code.back().sub.op != acc_cond::acc_op::Or)
|
||||||
return nullptr;
|
return nullptr;
|
||||||
|
|
||||||
while (s)
|
while (s)
|
||||||
{
|
{
|
||||||
--s;
|
--s;
|
||||||
if (code[s].op == acc_cond::acc_op::And)
|
if (code[s].sub.op == acc_cond::acc_op::And)
|
||||||
{
|
{
|
||||||
start_and:
|
start_and:
|
||||||
auto o1 = code[--s].op;
|
auto o1 = code[--s].sub.op;
|
||||||
auto m1 = code[--s].mark;
|
auto m1 = code[--s].mark;
|
||||||
auto o2 = code[--s].op;
|
auto o2 = code[--s].sub.op;
|
||||||
auto m2 = code[--s].mark;
|
auto m2 = code[--s].mark;
|
||||||
// We expect
|
// We expect
|
||||||
// Fin({n}) & Inf({n+1})
|
// Fin({n}) & Inf({n+1})
|
||||||
|
|
@ -460,12 +460,12 @@ namespace spot
|
||||||
return nullptr;
|
return nullptr;
|
||||||
inf_pairs |= m2;
|
inf_pairs |= m2;
|
||||||
}
|
}
|
||||||
else if (code[s].op == acc_cond::acc_op::Fin)
|
else if (code[s].sub.op == acc_cond::acc_op::Fin)
|
||||||
{
|
{
|
||||||
start_fin:
|
start_fin:
|
||||||
fin_alone |= code[--s].mark;
|
fin_alone |= code[--s].mark;
|
||||||
}
|
}
|
||||||
else if (code[s].op == acc_cond::acc_op::Inf)
|
else if (code[s].sub.op == acc_cond::acc_op::Inf)
|
||||||
{
|
{
|
||||||
auto m1 = code[--s].mark;
|
auto m1 = code[--s].mark;
|
||||||
if (m1.count() != 1)
|
if (m1.count() != 1)
|
||||||
|
|
@ -551,7 +551,7 @@ namespace spot
|
||||||
auto end = &p.second.front();
|
auto end = &p.second.front();
|
||||||
while (pos > end)
|
while (pos > end)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
|
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
|
||||||
// de l'Epita.
|
// Développement de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -60,7 +60,7 @@ namespace spot
|
||||||
acc_cond::acc_word* start = &code.front();
|
acc_cond::acc_word* start = &code.front();
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::Or:
|
case acc_cond::acc_op::Or:
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
|
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
|
||||||
// de l'Epita.
|
// Développement de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -70,17 +70,17 @@ namespace spot
|
||||||
terms_t res;
|
terms_t res;
|
||||||
auto pos = &code.back();
|
auto pos = &code.back();
|
||||||
auto end = &code.front();
|
auto end = &code.front();
|
||||||
if (pos->op == acc_cond::acc_op::And)
|
if (pos->sub.op == acc_cond::acc_op::And)
|
||||||
--pos;
|
--pos;
|
||||||
while (pos >= end)
|
while (pos >= end)
|
||||||
{
|
{
|
||||||
auto term_end = pos - 1 - pos->size;
|
auto term_end = pos - 1 - pos->sub.size;
|
||||||
if (pos->op == acc_cond::acc_op::Or)
|
if (pos->sub.op == acc_cond::acc_op::Or)
|
||||||
--pos;
|
--pos;
|
||||||
acc_cond::mark_t m = 0U;
|
acc_cond::mark_t m = 0U;
|
||||||
while (pos > term_end)
|
while (pos > term_end)
|
||||||
{
|
{
|
||||||
assert(pos->op == acc_cond::acc_op::Inf);
|
assert(pos->sub.op == acc_cond::acc_op::Inf);
|
||||||
m |= pos[-1].mark;
|
m |= pos[-1].mark;
|
||||||
pos -= 2;
|
pos -= 2;
|
||||||
}
|
}
|
||||||
|
|
@ -319,7 +319,7 @@ namespace spot
|
||||||
auto cnf = res->get_acceptance().to_cnf();
|
auto cnf = res->get_acceptance().to_cnf();
|
||||||
// If we are very lucky, building a CNF actually gave us a GBA...
|
// If we are very lucky, building a CNF actually gave us a GBA...
|
||||||
if (cnf.empty() ||
|
if (cnf.empty() ||
|
||||||
(cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Inf))
|
(cnf.size() == 2 && cnf.back().sub.op == acc_cond::acc_op::Inf))
|
||||||
{
|
{
|
||||||
res->set_acceptance(res->num_sets(), cnf);
|
res->set_acceptance(res->num_sets(), cnf);
|
||||||
cleanup_acceptance_here(res);
|
cleanup_acceptance_here(res);
|
||||||
|
|
@ -379,28 +379,28 @@ namespace spot
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
auto pos = &acc.back();
|
auto pos = &acc.back();
|
||||||
if (pos->op == acc_cond::acc_op::Or)
|
if (pos->sub.op == acc_cond::acc_op::Or)
|
||||||
--pos;
|
--pos;
|
||||||
auto start = &acc.front();
|
auto start = &acc.front();
|
||||||
while (pos > start)
|
while (pos > start)
|
||||||
{
|
{
|
||||||
if (pos->op == acc_cond::acc_op::Fin)
|
if (pos->sub.op == acc_cond::acc_op::Fin)
|
||||||
{
|
{
|
||||||
// We have only a Fin term, without Inf. In this case
|
// We have only a Fin term, without Inf. In this case
|
||||||
// only, the Fin() may encode a disjunction of sets.
|
// only, the Fin() may encode a disjunction of sets.
|
||||||
for (auto s: pos[-1].mark.sets())
|
for (auto s: pos[-1].mark.sets())
|
||||||
res.emplace_back(acc_cond::mark_t({s}), 0U);
|
res.emplace_back(acc_cond::mark_t({s}), 0U);
|
||||||
pos -= pos->size + 1;
|
pos -= pos->sub.size + 1;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
// We have a conjunction of Fin and Inf sets.
|
// We have a conjunction of Fin and Inf sets.
|
||||||
auto end = pos - pos->size - 1;
|
auto end = pos - pos->sub.size - 1;
|
||||||
acc_cond::mark_t fin = 0U;
|
acc_cond::mark_t fin = 0U;
|
||||||
acc_cond::mark_t inf = 0U;
|
acc_cond::mark_t inf = 0U;
|
||||||
while (pos > end)
|
while (pos > end)
|
||||||
{
|
{
|
||||||
switch (pos->op)
|
switch (pos->sub.op)
|
||||||
{
|
{
|
||||||
case acc_cond::acc_op::And:
|
case acc_cond::acc_op::And:
|
||||||
--pos;
|
--pos;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue