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

acc: make &= and |= symmetrical

Operator &= used to always move Fin to the front, it does not anymore.
The only thing it does now is to merge Inf(x)&Inf(y) as Inf({x,y}).
Operator |= is now symmetrical and merges Fin()s.

Fixes #253.

* spot/twa/acc.cc, spot/twa/acc.hh: Simplify &= and make |= symmetrical.
* spot/twaalgos/cleanacc.cc: Fix conjunction order.
* tests/core/acc.test, tests/core/acc2.test, tests/core/parseaut.test,
tests/core/readsave.test, tests/core/satmin2.test,
tests/core/sccdot.test, tests/python/acc_cond.ipynb,
tests/python/accparse.ipynb, tests/python/automata.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
parent 8e685e00
......@@ -156,6 +156,12 @@ New in spot 2.3.5.dev (not yet released)
- If the SPOT_BDD_TRACE envorinment variable is set, statistics
about BDD garbage collection and table resizing are shown.
- The & and | operators for acceptannce conditions have been changed
slightly to be more symmetrical. In older version, operator &
would move Fin() terms to the front, but that is not the case
anymore. Also operator & was already grouping all Inf() terms
(for efficiency reasons), in this version operator | is
symmetrically grouping all Fin() terms.
Python:
......
......@@ -914,7 +914,7 @@ namespace spot
while ((cube = isop.next()) != bddfalse)
{
mark_t i = 0U;
acc_code c;
acc_code f;
while (cube != bddtrue)
{
// The acceptance set associated to this BDD variable
......@@ -928,8 +928,7 @@ namespace spot
// The strange order here make sure we can smaller set
// numbers at the end of the acceptance code, i.e., at
// the front of the output.
auto a = fin(s) & std::move(c);
std::swap(a, c);
f = fin(s) & f;
}
else // Positive variable? -> Inf
{
......@@ -937,10 +936,8 @@ namespace spot
cube = h;
}
}
c &= inf(i);
// See comment above for the order.
c |= std::move(rescode);
std::swap(c, rescode);
rescode = (inf(i) & f) | rescode;
}
return rescode;
......@@ -986,7 +983,7 @@ namespace spot
while ((cube = isop.next()) != bddfalse)
{
mark_t m = 0U;
acc_code c = f();
acc_code i = f();
while (cube != bddtrue)
{
// The acceptance set associated to this BDD variable
......@@ -1000,8 +997,7 @@ namespace spot
// The strange order here make sure we can smaller set
// numbers at the end of the acceptance code, i.e., at
// the front of the output.
auto a = inf(s) | std::move(c);
std::swap(a, c);
i = inf(s) | i;
}
else // Positive variable? -> Fin
{
......@@ -1009,10 +1005,8 @@ namespace spot
cube = h;
}
}
c |= fin(m);
// See comment above for the order.
c &= std::move(rescode);
std::swap(c, rescode);
rescode = (fin(m) | i) & rescode;
}
return rescode;
}
......
......@@ -578,11 +578,11 @@ namespace spot
unsigned n = 0;
for (Iterator i = begin; i != end; ++i)
{
acc_cond::acc_code pair = fin({n++});
unsigned f = n++;
acc_cond::mark_t m = 0U;
for (unsigned ni = *i; ni > 0; --ni)
m.set(n++);
pair &= inf(m);
auto pair = inf(m) & fin({f});
std::swap(pair, res);
res |= std::move(pair);
}
......@@ -596,11 +596,11 @@ namespace spot
// acceptance formula.
static acc_code random(unsigned n, double reuse = 0.0);
acc_code& operator&=(acc_code&& r)
acc_code& operator&=(const acc_code& r)
{
if (is_t() || r.is_f())
{
*this = std::move(r);
*this = r;
return *this;
}
if (is_f() || r.is_t())
......@@ -644,7 +644,7 @@ namespace spot
left_inf = &(*this)[s - 1];
}
acc_word* right_inf = nullptr;
const acc_word* right_inf = nullptr;
auto right_end = &r.back();
if (right_end->sub.op == acc_op::And)
{
......@@ -665,23 +665,17 @@ namespace spot
right_inf = right_end - 1;
}
acc_cond::mark_t carry = 0U;
if (left_inf && right_inf)
{
left_inf->mark |= right_inf->mark;
insert(this->end(), &r[0], right_inf);
insert(this->end(), right_inf + 2, right_end + 1);
}
else if (right_inf)
{
// Always insert Inf() at the very first entry.
insert(this->begin(), right_inf, right_inf + 2);
insert(this->end(), &r[0], right_inf);
insert(this->end(), right_inf + 2, right_end + 1);
}
else
{
insert(this->end(), &r[0], right_end + 1);
carry = left_inf->mark;
auto pos = left_inf - &(*this)[0];
erase(begin() + pos, begin() + pos + 2);
}
auto sz = size();
insert(end(), &r[0], right_end + 1);
if (carry)
(*this)[sz + (right_inf - &r[0])].mark |= carry;
acc_word w;
w.sub.op = acc_op::And;
......@@ -690,138 +684,97 @@ namespace spot
return *this;
}
acc_code& operator&=(const acc_code& r)
acc_code operator&(const acc_code& r)
{
return *this &= r;
}
acc_code operator&(acc_code&& r)
{
acc_code res = *this;
res &= r;
return res;
}
acc_code& operator|=(const acc_code& r)
{
if (is_t() || r.is_f())
return *this;
if (is_f() || r.is_t())
{
*this = r;
return *this;
}
if (is_f() || r.is_t())
return *this;
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
// Inf(a) & Inf(b) = Inf(a & b)
if (((*this)[s].sub.op == acc_op::Inf
&& r[rs].sub.op == acc_op::Inf)
|| ((*this)[s].sub.op == acc_op::InfNeg
&& r[rs].sub.op == acc_op::InfNeg))
// Fin(a) | Fin(b) = Fin(a | b)
if (((*this)[s].sub.op == acc_op::Fin
&& 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;
return *this;
}
// In the more complex scenarios, left and right may both
// be conjunctions, and Inf(x) might be a member of each
// be disjunctions, and Fin(x) might be a member of each
// side. Find it if it exists.
// left_inf points to the left Inf mark if any.
// right_inf points to the right Inf mark if any.
acc_word* left_inf = nullptr;
if ((*this)[s].sub.op == acc_op::And)
acc_word* left_fin = nullptr;
if ((*this)[s].sub.op == acc_op::Or)
{
auto start = &(*this)[s] - (*this)[s].sub.size;
auto pos = &(*this)[s] - 1;
pop_back();
while (pos > start)
{
if (pos->sub.op == acc_op::Inf)
if (pos->sub.op == acc_op::Fin)
{
left_inf = pos - 1;
left_fin = pos - 1;
break;
}
pos -= pos->sub.size + 1;
}
}
else if ((*this)[s].sub.op == acc_op::Inf)
else if ((*this)[s].sub.op == acc_op::Fin)
{
left_inf = &(*this)[s - 1];
left_fin = &(*this)[s - 1];
}
const acc_word* right_inf = nullptr;
const acc_word* right_fin = nullptr;
auto right_end = &r.back();
if (right_end->sub.op == acc_op::And)
if (right_end->sub.op == acc_op::Or)
{
auto start = &r[0];
auto pos = --right_end;
while (pos > start)
{
if (pos->sub.op == acc_op::Inf)
if (pos->sub.op == acc_op::Fin)
{
right_inf = pos - 1;
right_fin = pos - 1;
break;
}
pos -= pos->sub.size + 1;
}
}
else if (right_end->sub.op == acc_op::Inf)
{
right_inf = right_end - 1;
}
if (left_inf && right_inf)
{
left_inf->mark |= right_inf->mark;
insert(this->end(), &r[0], right_inf);
insert(this->end(), right_inf + 2, right_end + 1);
}
else if (right_inf)
else if (right_end->sub.op == acc_op::Fin)
{
// Always insert Inf() at the very first entry.
insert(this->begin(), right_inf, right_inf + 2);
insert(this->end(), &r[0], right_inf);
insert(this->end(), right_inf + 2, right_end + 1);
right_fin = right_end - 1;
}
else
{
insert(this->end(), &r[0], right_end + 1);
}
acc_word w;
w.sub.op = acc_op::And;
w.sub.size = size();
emplace_back(w);
return *this;
}
acc_code operator&(acc_code&& r)
{
acc_code res = *this;
res &= r;
return res;
}
acc_code operator&(const acc_code& r)
{
acc_code res = *this;
res &= r;
return res;
}
acc_code& operator|=(acc_code&& r)
{
if (is_t() || r.is_f())
return *this;
if (is_f() || r.is_t())
acc_cond::mark_t carry = 0U;
if (left_fin && right_fin)
{
*this = std::move(r);
return *this;
carry = left_fin->mark;
auto pos = (left_fin - &(*this)[0]);
this->erase(begin() + pos, begin() + pos + 2);
}
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
// Fin(a) | Fin(b) = Fin(a | b)
if (((*this)[s].sub.op == acc_op::Fin
&& 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;
return *this;
}
if ((*this)[s].sub.op == acc_op::Or)
pop_back();
if (r.back().sub.op == acc_op::Or)
r.pop_back();
insert(this->end(), r.begin(), r.end());
auto sz = size();
insert(end(), &r[0], right_end + 1);
if (carry)
(*this)[sz + (right_fin - &r[0])].mark |= carry;
acc_word w;
w.sub.op = acc_op::Or;
w.sub.size = size();
......@@ -829,11 +782,6 @@ namespace spot
return *this;
}
acc_code& operator|=(const acc_code& r)
{
return *this |= acc_code(r);
}
acc_code operator|(acc_code&& r)
{
acc_code res = *this;
......@@ -841,11 +789,9 @@ namespace spot
return res;
}
acc_code operator|(const acc_code& r)
acc_code& operator|(const acc_code& r)
{
acc_code res = *this;
res |= r;
return res;
return *this |= r;
}
acc_code& operator<<=(unsigned sets)
......
......@@ -193,8 +193,7 @@ namespace spot
for (auto m: seen_fin.sets())
inf.front().mark -= complement[m];
res &= inf;
return res;
return inf & res;
}
case acc_cond::acc_op::Or:
{
......@@ -225,8 +224,7 @@ namespace spot
for (auto m: seen_inf.sets())
fin.front().mark -= complement[m];
res |= fin;
return res;
return res | fin;
}
case acc_cond::acc_op::Fin:
return acc_cond::acc_code::fin(pos[-1].mark);
......
......@@ -64,12 +64,12 @@ stripping
#1: {2}
2 Inf(0)&Inf(1)&Inf(3) 1
5 Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
10 (Fin(0)|Fin(1)) & (Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))) 0
5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
8 (Fin(0)|Fin(1)) & ((Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3))) 0
2 f 1
9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
5 (Fin(0)|Fin(1)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
(Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) {0} true
{1}
......@@ -82,9 +82,9 @@ f
Fin(2)
Inf(2)
Fin(2) | Inf(2)
Fin(2) & Inf(2)
Fin(0) | (Fin(2) & Inf(1)) | Fin(3)
Fin(0) | (Fin(2) & Inf(1)) | Fin(3)
Inf(2) & Fin(2)
(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))
(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))
EOF
run 0 ../acc | tee stdout
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -71,13 +71,13 @@ diff acceptances output
#------------- CNF -------------
res="(Fin(2) | Inf(1)) & (Fin(1) | Inf(3)) & Inf(0)"
res="Inf(0) & (Inf(1) | Fin(2)) & (Inf(3) | Fin(1))"
cat >acceptances<<EOF
2 Inf(0)&Inf(1), 2 Inf(0)&Inf(1)
2 Fin(0) & Inf(1), 2 Fin(0) & Inf(1)
2 t, 2 t
2 f, 2 f
3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(2) | Inf(1)) & Inf(0)
3 (Inf(1) | Fin(2)) & Inf(0), 3 Inf(0) & (Inf(1) | Fin(2))
4 (Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3)), 4 $res
4 $res, 4 $res
3 (Fin(0) & Fin(2)) | (Fin(1) & Fin(2)), 3 (Fin(0)|Fin(1)) & Fin(2)
......@@ -94,7 +94,7 @@ diff acceptances output
#------------- COMP -------------
a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)"
b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)"
b="(Fin(1) & Inf(2)) | (Inf(1) & Fin(3)) | Fin(0)"
cat >acceptances<<EOF
2 Inf(0)&Inf(1), 2 Fin(0)|Fin(1)
2 Fin(0) & Inf(1), 2 Inf(0) | Fin(1)
......@@ -102,7 +102,7 @@ cat >acceptances<<EOF
2 f, 2 t
3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(1) & Inf(2)) | Fin(0)
4 $a, 4 $b
4 $b, 4 (Inf(1) | Fin(2)) & (Inf(3) | Fin(1)) & Inf(0)
4 $b, 4 (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)
3 (Fin(0)|Fin(1)) & Fin(2), 3 (Inf(0)&Inf(1)) | Inf(2)
EOF
......
......@@ -2508,7 +2508,7 @@ HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 4 (Fin(1) & Inf(0)) | (Fin(3) & Inf(2))
Acceptance: 4 (Inf(0) & Fin(1)) | (Inf(2) & Fin(3))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
......@@ -2522,7 +2522,7 @@ HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 4 (Fin(3) & Inf(2)) | (Fin(1) & Inf(0))
Acceptance: 4 (Fin(3) & Inf(2)) | (Inf(0) & Fin(1))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
......@@ -2536,7 +2536,7 @@ HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 6 (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5)) & Inf(0)
Acceptance: 6 Inf(0) & (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
......@@ -2550,7 +2550,7 @@ HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 6 (Inf(4) | Fin(5)) & (Inf(1) | (Fin(2)|Fin(3))) & Inf(0)
Acceptance: 6 (Fin(5) | Inf(4)) & Inf(0) & ((Fin(2)|Fin(3)) | Inf(1))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
......@@ -2624,7 +2624,7 @@ HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Fin(0) & ((Fin(2) & Inf(3)) | Inf(1))
Acceptance: 4 Fin(0) & ((Inf(3) & Fin(2)) | Inf(1))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
......
......@@ -470,7 +470,7 @@ EOF
cat >expected <<EOF
digraph G {
rankdir=LR
label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))"
labelloc="t"
I [label="", style=invis, width=0]
I -> 0
......@@ -524,7 +524,7 @@ diff out expected
cat >expected2 <<EOF
digraph G {
rankdir=LR
label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))"
labelloc="t"
node [shape="circle"]
I [label="", style=invis, width=0]
......
......@@ -335,7 +335,7 @@ HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 2 (Fin(1) & Inf(0)) | (Fin(0) & Inf(1))
Acceptance: 2 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
......
......@@ -74,7 +74,7 @@ run 0 autfilt --dot=as in.hoa > out.dot
cat <<EOF >expected
digraph G {
rankdir=LR
label="Fin(2) & (Inf(0)&Inf(1))"
label="(Inf(0)&Inf(1)) & Fin(2)"
labelloc="t"
node [shape="circle"]
I [label="", style=invis, width=0]
......@@ -156,7 +156,7 @@ HOA: v1
States: 8
Start: 0
AP: 2 "a" "b"
Acceptance: 3 Fin(2) & (Inf(0)&Inf(1))
Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
......
......@@ -15,7 +15,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.5.3"
"version": "3.5.3+"
},
"name": ""
},
......@@ -489,7 +489,7 @@
"output_type": "pyout",
"prompt_number": 17,
"text": [
"(Fin(1) & Inf(0)) | Inf(2)"
"(Inf(0) & Fin(1)) | Inf(2)"
]
}
],
......@@ -571,7 +571,7 @@
"output_type": "pyout",
"prompt_number": 20,
"text": [
"(Fin(3) | Inf(1)) & (Fin(0)|Fin(2)) & Inf(4)"
"(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))"
]
}
],
......@@ -619,7 +619,7 @@
"output_type": "pyout",
"prompt_number": 22,
"text": [
"Fin(0) & (Fin(2) | Inf(1)) & (Fin(4) | Inf(1) | Inf(3))"
"Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))"
]
}
],
......@@ -720,8 +720,8 @@
"output_type": "stream",
"stream": "stdout",
"text": [
"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
"(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))\n"
"((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n",
"((Inf(4) | Fin(5)) & (Inf(6) | Fin(7))) | ((Inf(0) | Fin(1)) & (Inf(2) | Fin(3)))\n"
]
}
],
......
......@@ -15,10 +15,9 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.4.3+"
"version": "3.5.3+"
},
"name": "",
"signature": "sha256:1ee7951bed30652ae110a14b210541829221552eb944ff01f25236179673dd5b"
"name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
......@@ -51,7 +50,7 @@
"output_type": "pyout",
"prompt_number": 2,
"text": [
"(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
"(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))"
]
}
],
......@@ -91,7 +90,7 @@
"output_type": "pyout",
"prompt_number": 4,
"text": [
"(Inf(0) | Inf(2)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (Fin(1)|Fin(3))"