Commit 33c496a4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

acc: Add operators == and != for acc_code

and make sure are_isomorphic does not look only at the number of
acceptance sets

* src/tgba/acc.hh: Here.
* src/tgbaalgos/are_isomorphic.cc: Use it to ensure two automata
have the same acceptance condition.
* src/tgbatest/explpro4.test: Test product between Büchi and co-Büchi,
and make sure the isomorphic check look at the acceptance condition.
parent 039274b2
......@@ -211,6 +211,42 @@ namespace spot
struct acc_code: public std::vector<acc_word>
{
bool operator==(const acc_code& other)
{
unsigned pos = size();
if (other.size() != pos)
return false;
while (pos > 0)
{
auto op = (*this)[pos - 1].op;
auto sz = (*this)[pos - 1].size;
if (other[pos - 1].op != op ||
other[pos - 1].size != sz)
return false;
switch (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:
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg:
pos -= 2;
if (other[pos].mark != (*this)[pos].mark)
return false;
break;
}
}
return true;
};
bool operator!=(const acc_code& other)
{
return !(*this == other);
}
bool is_true() const
{
unsigned s = size();
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -102,7 +102,9 @@ namespace
{
return aut1->num_states() != aut2->num_states() ||
aut1->num_transitions() != aut2->num_transitions() ||
aut1->acc().num_sets() != aut2->acc().num_sets();
// FIXME: At some point, it would be nice to support reordering
// of acceptance sets (issue #58).
aut1->acc().get_acceptance() != aut2->acc().get_acceptance();
}
}
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2009, 2014, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
......@@ -47,7 +47,7 @@ States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
......@@ -61,8 +61,21 @@ HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
Acceptance: 2 Inf(0) & Fin(1)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
[!0] 0 {1}
[0] 0 {0}
--END--
EOF
cat >unexpected <<'EOF'
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
......@@ -72,6 +85,7 @@ State: 0
EOF
run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout
run 0 ../../bin/autfilt -F stdout --isomorph expected
run 0 ../../bin/autfilt -q stdout --isomorph expected
run 1 ../../bin/autfilt -q stdout --isomorph unexpected
rm input1 input2 stdout expected
true
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment